Skip to content

Bump to version: v4.27.0 #928

@zhikaip

Description

@zhikaip

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-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.

Afterwards

  • Create a tag for the new version.

Previous bump

v4.26.0

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions