This PR adds some new information to the release checklist,
as well as some new automated checks to help with the release process.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR adds `SetConsoleOutputCP(CP_UTF8)` during runtime initialization
to properly display Unicode on the Windows console. This effects both
the Lean executable itself and user executables (including Lake).
Closes#4291.
This PR adds a check to `release_checklist.py`, to check whether
`CMakeLists.txt` on `master` has been updated, and if not reminds that a
"begin dev cycle" PR (as documented in `release_checklist.md` is needed.
Some downstream repositories require a `bump/v4.X.0` branch to exist for
their integration CI. This PR updates `release_checklist.py` to check
for the existence of these branches, when needed.
Often PR descriptions end with a colon, followed by a new paragraph
containing a code block. Currently in the release notes these get
dropped. This PR attempts to include them. It's not particularly robust,
but I'll review during the next release.
This PR reports a sentence like:
```quote
For this release, 201 changes landed. In addition to the 74 feature additions and 44 fixes listed below there were 7 refactoring changes, 5 documentation improvements and 62 chores.
```
in the automatically generated release notes.
This PR updates the release checklist, reflecting changes noted while
@jcommelin has been releasing v4.16.0.
---------
Co-authored-by: Johan Commelin <johan@commelin.net>
The semantics of `release_notes.py` was slightly confusing. It is meant
to be run a `script/release_notes.py v4.15.0` on the `releases/v4.16.0`
branch. To help, I've changed the usage to `script/release_notes.py
--since v4.15.0`.
This PR updates the release checklist script to:
* validate the `releases/v4.X.0` branch
* check that the release has been tagged
* appears on the releases list
* and has release notes (and if not, prompts to run the script
* and when checking downstream repositories, if something is not tagged
properly, suggests the script to run to push the missing tag.
Users have requested toolchain tags on `lean4-cli`, so let's add it to
the release checklist to make sure these get added regularly.
Previously, `lean4-cli` has used more complicated tags, but going
forward we're going to just use the simple `v4.16.0` style tags, with no
repository-specific versioning.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR introduces a script that automates checking whether major
downstream repositories have been updated for a new toolchain release.
Sample output:
```
% ./release_checklist.py v4.16.0-rc1
Repository: Batteries
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: lean4checker
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: doc-gen4
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: Verso
❌ Not on target toolchain (needs ≥ v4.16.0-rc1, but main is on leanprover/lean4:v4.15.0)
Repository: ProofWidgets4
✅ On compatible toolchain (>= v4.16.0-rc1)
Repository: Aesop
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: import-graph
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: plausible
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: Mathlib
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: REPL
❌ Not on target toolchain (needs ≥ v4.16.0-rc1, but master is on leanprover/lean4:v4.14.0)
```
This PR adds a script to automatically generate release notes using the
new `changelog-*` labels and "This PR ..." conventions.
Usage:
```
script/release_notes.py v4.X.0
```
where `v4.X.0` is the **previous** release, i.e. the script will process
all commits *since* that tag.
Breaking changes:
To build Lean from source on Windows, it is now necessary to install the
[Windows
SDK](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The build instructions have been updated to reflect this. Note that the
Windows SDK is **not** needed to compile Lean programs using a Lean
toolchain obtained using `elan`. The Windows SDK is only needed to build
Lean itself from source.
Furthermore, we are dropping support for Windows versions older than
Windows 10 1903 (released in May 2019).
No Windows version that is still supported by Microsoft as part of
mainstream support is affected by this.
The following Windows versions are still supported by Microsoft as part
of commercial extended support but are no longer supported by Lean:
- Windows 10 Enterprise LTSC 2015
- Windows 10 Enterprise LTSC 2016
- Windows 10 Enterprise LTSC 2019
- Windows Server 2019
This is from a ~~pair~~triple programming session with @tydeu and
@mhuisi.
If stage 1 is built with `-DUSE_LAKE=ON`, the CMake run will generate
`lakefile.toml` files for the root, `src`, and `tests`. These Lake
configuration files can then be used to build core oleans. While they do
not yet allow Lake to be used to build the Lean binaries. they do allow
Lake to be used for working interactively with the Lean source. In our
preliminary experiments, this allowed updates to `Init.Data.Nat` to be
noticed automatically when reloading downstream files, rather than
requiring a full manual compiler rebuild. This will make it easier to
work on the system.
As part of this change, Lake is added to stage 0. This allows Lake to
function in `src`, which uses the stage 0 toolchain.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Reusing the best profiling UI out there
Usage:
```
lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json foo.lean ...
```
then open `profile.json` in https://profiler.firefox.com/.
See also `script/collideProfiles.lean` for minimizing and merging
profiles.
In particular:
* Do not use deprecated `potiuk/get-workflow-origin`.
* Use a bare checkout to push PR to `pr-releases`
* Replace `script/most-recent-nightly-tag.sh` by a one-liner inside the
workflow, so that th workflow is self-contained
`script/most-recent-nightly-tag.sh` determines the most recent nightly
release in your current git history.
Previously it was assuming that you had a `nightly` remote, to pull tags
from. Now it just pulls directly from the repository by URL.
