Repository navigation
ci: publish student and terse as the latest release, drop publish-book.sh - #33
Merged
Merged
Conversation
…k.sh
Build the terse variant too, publish it to this repo's Pages, and
publish both variants as the `latest` release, one
`<variant>-{lean,html}.tar.gz` each plus `commit.txt`. The book
repository syncs itself from that release, so the local
publish-book.sh and its Makefile target go.
Refs #18
--
AI-usage disclosure: the workflow was drafted with the assistance of
Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author
reviewed the changes and takes full responsibility for the final content.
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Resolve artifact completeness, tag-target consistency, and non-atomic latest release publication concerns.
Review effort: Lite
Findings: 1
Open (1)
What changed in this PR
Moves book publication into CI, serving terse on Pages and publishing student/terse artifacts in the latest release.
Changes:
- Builds and packages both variants.
- Publishes Lean/HTML archives and commit metadata.
- Removes the obsolete local publishing script and Make target.
| File | Description |
|---|---|
scripts/publish-book.sh |
Removes local repository synchronization. |
Makefile |
Removes the obsolete publishing target. |
.github/workflows/pages.yml |
Builds, deploys, and publishes book variants. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Copy the terse Lake project to a local working directory outside the repository, `../aula` by default, and build it. The directory is its own git repository and is never published, so what is written in class can be committed there; the target refuses to overwrite uncommitted changes. Refs #18 -- AI-usage disclosure: the target was drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content.
actions/upload-artifact@v4 leaves hidden files out by default, so the `.gitignore` that keeps `.lake/` out of the students' commits never reached the release. -- AI-usage disclosure: the fix was drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content.
Drop the references to a particular course's repositories from the Pages workflow comments and from CLAUDE.md, which now states the rule, and point the doc-gen4 note at this repository's issue. -- AI-usage disclosure: the change was drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content.
Mathlib's cache has no compiled C objects, so linking the executables compiled every Mathlib module from scratch whenever the pull request had no cache of its own. Restore the cache of `main` instead, which has them, and do not save one per pull request: at a few gigabytes each against the 10 GB limit, they evicted the one on `main`. -- AI-usage disclosure: the workflow was drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content.
-- AI-usage disclosure: the change was made with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed it and takes full responsibility for the final content.
-- AI-usage disclosure: the text was drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed it and takes full responsibility for the final content.
GitHub is deprecating Node.js 20 on its runners. -- AI-usage disclosure: the change was made with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed it and takes full responsibility for the final content.
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
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.
Part of #18.
pages.ymlbuilds thetersevariant besidesstudent, and this repository's Pages now servesterse, the lecture cut used in class.latest(the oldstudent-latestis deleted by the workflow). It carriesstudent-{lean,html}.tar.gz,terse-{lean,html}.tar.gzandcommit.txt, the CSwL commit they were built from.solutionsandgradingare not published.scripts/publish-book.shandmake publish-bookgo.make lecturecopies theterseLake project to../lecture(orLECTURE=<dir>), a local git repository outside CSwL that is never published, and builds it, for the instructor to open in VS Code in class. It refuses to overwrite uncommitted changes.lean_action_ci.yml) restores the Lake cache thatpages.ymlsaves onmain, which holds the compiled C objects of Mathlib that linking the executables needs, and no longer saves a cache per pull request, which evicted the one onmainunder the 10 GB limit.AI-usage disclosure: the workflow and the target were drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content.