-
Notifications
You must be signed in to change notification settings - Fork 71
Closed
Description
Version bump
This issue is a tracker issue for bumping PhysLean to new versions of Lean.
The checklist below should be used to ensure that the bump is done correctly.
Basics
- Update mathlib rev in lakefile.toml.
- Update doc-gen4 rev in lakefile.toml.
- Run
rm -rf .lake; lake update. - Check
lean-toolchainupdates correctly. - Update the Lean version badge in the
README.mdfile.
Build
- Run
lake buildand fix any errors.
Scripts
- Ensure
lake exe lint_allruns without errors. - Ensure
lake exe TODO_to_yml mkFileruns without errors. - Ensure
lake exe stats mkHTMLruns without errors. - Ensure
lake exe informal mkFile mkDot mkHTMLruns without errors. - Ensure
lake exe make_tagruns without errors. - Remove the created files
rm ./docs/Informal.md; rm ./docs/InformalDot.dot; rm ./docs/InformalGraph.html; rm ./docs/Stats.html; rm ./docs/_data/TODO.yml.
Afterwards
- Create a tag for the new version.
Previous bump
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels