Quality: Unauthenticated GitHub API request is susceptible to rate limiting

[tomaioo]

Summary

Quality: Unauthenticated GitHub API request is susceptible to rate limiting

Problem

Severity: Medium | File: scripts/update_formalization_status.py:L21

The fetch_formalized_problem_numbers function makes an unauthenticated request to the GitHub API. GitHub severely rate-limits unauthenticated API requests (60 requests per hour per IP). In shared or CI environments, this can easily cause the script to fail unexpectedly.

Solution

Use the GITHUB_TOKEN environment variable if available to authenticate the request by adding an 'Authorization': f'Bearer {os.environ.get("GITHUB_TOKEN")}' header to the requests.get() call.

Changes

• scripts/update_formalization_status.py (modified)

[teorth]

Merged, thanks — the underlying concern is real. scripts/update_formalization_status.py held the only unauthenticated GitHub API call in the repo, and since raise_for_status() is followed by sys.exit(1), a rate-limit refusal takes down the whole formalization-status update rather than degrading gracefully.

One thing to flag for future reference: as submitted, this change had no effect in CI, which is the only place it matters. GitHub Actions does not export GITHUB_TOKEN into the environment of run: steps — it is reachable only through ${{ secrets.GITHUB_TOKEN }} / ${{ github.token }} expressions and has to be passed explicitly. There was no env: block anywhere in this repo's workflows, so os.environ.get("GITHUB_TOKEN") returned None and the request went out unauthenticated exactly as before.

I've completed it in ba206c5, which adds to .github/workflows/update-formal-conjectures.yml:

      - name: Run update script
        run: python3 scripts/update_formalization_status.py
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

The Python side is unchanged and was already correct — backward compatible when no token is set, if github_token: handles an empty value, and nothing is written to the logs since only API_URL is printed.

If you send further changes of this kind, please check that the mechanism is actually wired up end to end, and note that CONTRIBUTING.md asks contributions produced with AI assistance to disclose it.