feat: add Blueprint deployment for proof tracking#5
Conversation
- Add blueprint directory with web.tex and print.tex sources - Add GitHub Actions workflow for automated deployment - Configure plastex and leanblueprint dependencies - Add .gitignore for build artifacts
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3e70924958
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| path: blueprint/web | ||
|
|
||
| - name: Deploy to GitHub Pages | ||
| uses: actions/deploy-pages@v4 |
There was a problem hiding this comment.
This workflow deploys unconditionally, but the same job is triggered on pull_request (on.pull_request at lines 9-10), so actions/deploy-pages will run during PR checks as well. For forked PRs, the token does not get pages: write, so the deployment step fails and turns otherwise-valid PRs red; add an if guard (or split build/deploy jobs) so deployment only runs on trusted push/manual contexts.
Useful? React with 👍 / 👎.
| \DeclareOption*{} | ||
| \ProcessOptions | ||
|
|
||
| \newcommand{\graphcolor}[3]{} |
There was a problem hiding this comment.
The committed blueprint.sty is only a stub and does not define the theorem/definition macros used throughout print.tex/web.tex (for example \begindefinition), so invoke build (tasks.py runs pdflatex print.tex) cannot succeed from a fresh checkout unless a separate manual copy step has already overwritten this file. This makes the advertised local PDF build path broken by default.
Useful? React with 👍 / 👎.
1 participant
Summary
Changes
blueprint/src/web.tex- Main blueprint content with theorems and definitionsblueprint/src/print.tex- Print version sourceblueprint/src/plastex.cfg- plastex configuration.github/workflows/blueprint.yml- CI workflow for building and deployingTest plan
leanblueprint websucceedsPreview
After merging, the blueprint will be available at:
https://FrankieeW.github.io/ANT/blueprint/