You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This issue is a tracker issue for bumping Physlib 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.
Remove the .lake file, e.g. on unix run rm -rf .lake.
Run lake update.
Check lean-toolchain updates correctly.
Update the Lean version badge in the README.md file.
Build
Run lake build and fix any errors.
Scripts
Ensure lake exe lint_all runs without errors.
Ensure lake exe TODO_to_yml mkFile runs without errors.
Ensure lake exe stats mkHTML runs without errors.
Ensure lake exe informal mkFile mkDot mkHTML runs without errors.
Ensure lake exe make_tag runs 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.
Version bump
This issue is a tracker issue for bumping Physlib to new versions of Lean.
The checklist below should be used to ensure that the bump is done correctly.
Basics
.lakefile, e.g. on unix runrm -rf .lake.lake update.lean-toolchainupdates correctly.README.mdfile.Build
lake buildand fix any errors.Scripts
lake exe lint_allruns without errors.lake exe TODO_to_yml mkFileruns without errors.lake exe stats mkHTMLruns without errors.lake exe informal mkFile mkDot mkHTMLruns without errors.lake exe make_tagruns without errors.rm ./docs/Informal.md; rm ./docs/InformalDot.dot; rm ./docs/InformalGraph.html; rm ./docs/Stats.html; rm ./docs/_data/TODO.yml.Afterwards
Example past bumps
v4.20.0,
v4.20.0-rc5
v4.27.0