sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: add a few lines to the v4.16.0 release notes (#6916)

Browse Source
This commit is contained in:
Johan Commelin
2025-02-03 09:22:33 +01:00
committed by GitHub
parent 809ae9aac3
commit a1d522ab14
1 changed files with 14 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
RELEASES.md
View File

@@ -470,6 +470,14 @@ incorrect results for objects that had already been processed by
* [#6429](https://github.com/leanprover/lean4/pull/6429) adds support for extern LCNF decls, which is required for parity
with the existing code generator.
* [#6535](https://github.com/leanprover/lean4/pull/6535) avoids a linker warning on Windows.
* [#6547](https://github.com/leanprover/lean4/pull/6547) should prevent Lake from accidentally picking up other linkers
installed on the machine.
* [#6574](https://github.com/leanprover/lean4/pull/6574) actually prevents Lake from accidentally picking up other
toolchains installed on the machine.
## Pretty Printing
* [#5689](https://github.com/leanprover/lean4/pull/5689) adjusts the way the pretty printer unresolves names. It used to
@@ -545,6 +553,12 @@ with `--packages` or applied persistently by placing it at
functions would produce different traces depending on whether the cache
was fetched.
* [#6627](https://github.com/leanprover/lean4/pull/6627) aims to fix the trace issues reported by Mathlib that are
breaking `lake exe cache` in downstream projects.
* [#6631](https://github.com/leanprover/lean4/pull/6631) sets `MACOSX_DEPLOYMENT_TARGET` for shared libraries (it was
previously only set for executables).
## Other
* [#6285](https://github.com/leanprover/lean4/pull/6285) upstreams the `ToLevel` typeclass from mathlib and uses it to