Add voting, truth predictions, and difficulty ratings to the website#3589
Open
zond wants to merge 24 commits intogoogle-deepmind:mainfrom
Open
Add voting, truth predictions, and difficulty ratings to the website#3589zond wants to merge 24 commits intogoogle-deepmind:mainfrom
zond wants to merge 24 commits intogoogle-deepmind:mainfrom
Conversation
Switch the voting/rating system from Cloudflare KV to GitHub Discussions. Likes are HEART reactions, truth predictions are THUMBS_UP/DOWN reactions, and difficulty ratings are discussion comments. Replace the Cloudflare Worker with an App Engine proxy that loads secrets from Google Cloud Secret Manager. Add a consent modal explaining that all activity is public on GitHub. Enable voting, truth prediction, difficulty rating, and discussion links on both the browse and theorem detail pages. Allow build.js to accept pre-processed JSON from the live site.
The /discussions endpoint now accepts ?owner=X&repo=Y instead of reading the repo from server config. This lets one shared App Engine proxy serve discussions for any repo.
Document the default shared proxy setup (zero config for forkers), local development, and how to run your own proxy. Update API docs to reflect the owner/repo query parameters on /discussions.
Branches ending in -webtest skip the Lean build, docgen, and extract_names. Instead they download the processed conjectures JSON from the live site and inject repo-specific voting config (owner, name, repo ID) automatically. The site is deployed to GitHub Pages. On main, the full build runs unchanged.
Replace GH_READ_TOKEN (a fine-grained PAT scoped to specific repos) with GH_APP_PRIVATE_KEY (the GitHub App's private key). The proxy now obtains short-lived installation tokens automatically for any repo where the app is installed. Forkers no longer need PAT updates — just install the app.
Allow any *.github.io origin automatically so forks don't need CORS config. Fix the App Engine URL to .uc.r (us-central). Bump runtime from Node 20 to Node 22 (current LTS).
…andling - Add repo validation to /discussions endpoint: only serves google-deepmind/formal-conjectures and its forks - Fix docs: replace "read-only PAT" with "installation token", clarify config table shows injected values not source defaults, document failure modes and discussion creation triggers - Add error handling for node_id fetch in CI workflow - Fix Node.js version reference in appengine README
…Storage GitHub Apps require redirect_uri to exactly match a registered callback URL. Use the site root (which is registered) and store the user's current page in localStorage. After token exchange, redirect back to the original page.
Register a single callback URL on the App Engine worker (/oauth/callback) that bounces the OAuth code back to whichever fork the user came from. This eliminates the need for per-fork callback URL registration in the GitHub App. The redirect target is validated to be *.github.io or localhost.
- Use Node 22 in CI workflow (matches App Engine runtime and package.json) - Check for missing access_token in OAuth callback before proceeding - Deduplicate voting.md and appengine/README.md: voting.md has the overview and forker quickstart, README.md has proxy-specific details
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
zond
force-pushed
the
discussions-voting-webtest
branch
from
f972104 to
64a1850
Compare
…plicate extract_names step
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds a GitHub Discussions-backed voting system to the Formal Conjectures website:
All data is stored as native GitHub Discussions features — no separate database.
Architecture
formal-conjectures-web-worker) fetches discussions using GitHub App installation tokensgoogle-deepmind/formal-conjecturesor forks of it*.github.ioorigin automaticallyWhat changed
site/src/js/voting.js— complete rewrite: GitHub Discussions backend, consent modal, truth predictionssite/src/js/theorem.js,browse.js— enable voting integration, new sort optionssite/src/css/style.css— truth widget, consent modal, discussion link stylessite/src/templates/— uncomment voting.js, add sort optionssite/appengine/— new App Engine proxy (replacessite/worker/Cloudflare Worker)site/build.js— accept pre-processed JSON from the live site.github/workflows/build-and-docs.yml—-webtestbranch support, voting config injectionHow to try it
The branch is deployed at https://zond.github.io/formal-conjectures/. Click any theorem, then try voting, predicting, or rating difficulty.
Zero-config for forkers
Branches ending in
-webtestskip the expensive Lean build, download the conjectures JSON from the live site, and deploy to GitHub Pages. To try on your own fork:-webtestNo GCP project, secrets, or tokens needed. See
site/docs/voting.mdfor full details.Test plan
🤖 Generated with Claude Code