Skip to content

Commit aaa6453

Browse files
Garmelongithub-actions[bot]david-christiansendatokratsgraf812
authored
chore: bump toolchain to v4.34.0-rc1 (#917)
Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Sebastian Graf <sgraf1337@gmail.com> Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Phil Nguyen <pcn@cs.umd.edu> Co-authored-by: Violetta Sim <38787503+eyihluyc@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com> Co-authored-by: u <u@h> Co-authored-by: Pablo Graubner <2234137+pgraubner@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Marc Huisinga <mhuisi@protonmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> Co-authored-by: Leonardo de Moura <leomoura@amazon.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: jcreedcmu <jcreed@gmail.com> Co-authored-by: Violetta Sim <38787503+viol37@users.noreply.github.com> Co-authored-by: Rob Simmons <rob@lean-fro.org> Co-authored-by: leanprover-bot <leanprover-bot@lean-fro.org> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Wojciech Różowski <wojciech@lean-fro.org> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Richard Davison <richard.neil.davison@gmail.com> Co-authored-by: Chris Su <102528557+chrissuu@users.noreply.github.com> Co-authored-by: ericrbg-harmonic <eric@harmonic.fun> Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Orfeas Stefanos Thyfronitis Litos <18602747+OrfeasLitos@users.noreply.github.com> Co-authored-by: Juan José Madrigal <juanjomadrigal326@gmail.com> Co-authored-by: Julien Cretin <github@ia0.eu>
1 parent 02d0d61 commit aaa6453

12 files changed

Lines changed: 661 additions & 107 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,16 @@ jobs:
139139
- name: Verify tutorial project zip files build
140140
if: github.event_name != 'release'
141141
run: |
142-
scripts/check-tutorial-zips.sh
142+
# On Linux, some nightly toolchains currently report a version string that
143+
# the zips turn into a toolchain name that elan rejects, so build the
144+
# projects with this repository's toolchain instead. Releases and release
145+
# candidates are unaffected and build with the toolchain from the zip.
146+
# See https://github.com/leanprover/lean4/issues/14702
147+
if grep -q nightly lean-toolchain; then
148+
scripts/check-tutorial-zips.sh "$(cat lean-toolchain)"
149+
else
150+
scripts/check-tutorial-zips.sh
151+
fi
143152
144153
- name: Generate proofreading HTML
145154
if: github.event_name == 'pull_request'

‎Manual/BuildTools/Lake/CLI.lean‎

Lines changed: 125 additions & 93 deletions
Large diffs are not rendered by default.

‎Manual/Grind/EMatching.lean‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -305,6 +305,8 @@ grindExt
305305
grindFunCC
306306
grindFwd
307307
grindGen
308+
grindHom
309+
grindHomPred
308310
grindInj
309311
grindIntro
310312
grindLR
@@ -643,6 +645,26 @@ norm
643645
{includeDocstring Lean.Parser.Attr.grindNorm}
644646
:::
645647

648+
The {tactic}`grind` tactic can work with a source algebra that doesn't have a great deal of solving infrastructure (e.g. bitvectors) by “̲injecting”̲ it into another algebra that has more solving infrastructure (like natural numbers or integers).
649+
Homomorphism rules describe the injection from source to target, and how the injection commutes with other operations (like addition or multiplication in the case of bitvectors).
650+
Homomorphism predicates present additional facts that {tactic}`grind` can use about the injection (like that a bitvector of length $`n` corresponds to a natural number less than $`2^n`).
651+
652+
:::syntax Lean.Parser.Attr.grindMod (title := "Homomorphism Rules")
653+
```grammar
654+
hom
655+
```
656+
{includeDocstring Lean.Parser.Attr.grindHom}
657+
:::
658+
659+
:::syntax Lean.Parser.Attr.grindMod (title := "Homomorphism Predicates")
660+
```grammar
661+
hom_pred
662+
```
663+
{includeDocstring Lean.Parser.Attr.grindHomPred}
664+
:::
665+
666+
{TODO}[Grind's hom infrastructure could use an example]
667+
646668
{TODO}[Document `gen` modifier for `grind` patterns]
647669

648670
# Inspecting Patterns

‎Manual/Releases.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Author: Joachim Breitner
66

77
import VersoManual
88

9+
import Manual.Releases.«v4_34_0»
910
import Manual.Releases.«v4_33_0»
1011
import Manual.Releases.«v4_32_2»
1112
import Manual.Releases.«v4_32_1»
@@ -66,6 +67,8 @@ This section provides release notes about recent versions of Lean. When updating
6667
read the corresponding release notes. They may contain advice that will help you understand
6768
the differences with the previous version and upgrade your projects.
6869

70+
{include 0 Manual.Releases.«v4_34_0»}
71+
6972
{include 0 Manual.Releases.«v4_33_0»}
7073

7174
{include 0 Manual.Releases.«v4_32_2»}

‎Manual/Releases/v4_34_0.lean‎

Lines changed: 477 additions & 0 deletions
Large diffs are not rendered by default.

‎Manual/Runtime.lean‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -472,23 +472,18 @@ For modules in the Lean core (e.g., {module}`Init.Prelude`), the initializer is
472472
Module initializers will automatically initialize any imported modules.
473473
They are also idempotent (when run with the same `builtin` flag), but not thread-safe.
474474

475-
*Important for process-related functionality*: applications that use process-related functions from `libuv`, such as {name}`Std.IO.Process.getProcessTitle` and {name}`Std.IO.Process.setProcessTitle`, must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) *before* calling `lean_initialize()` or `lean_initialize_runtime_module()`.
475+
*Important for process-related functionality*: applications that use process-related functions from `libuv`, such as {name}`Std.IO.Process.getProcessTitle` and {name}`Std.IO.Process.setProcessTitle`, must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) *before* calling any module initializer.
476476
This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
477477

478-
Together with initialization of the Lean runtime, code like the following should be run exactly once before accessing any Lean declarations:
478+
Putting everything together, code like the following should be run exactly once before accessing any Lean declarations:
479479
```C
480-
void lean_initialize_runtime_module();
481-
void lean_initialize();
482480
char ** lean_setup_args(int argc, char ** argv);
483481

484482
lean_object * initialize_A_B(uint8_t builtin);
485483
lean_object * initialize_C(uint8_t builtin);
486484
...
487485

488486
argv = lean_setup_args(argc, argv); // if using process-related functionality
489-
lean_initialize_runtime_module();
490-
// necessary (and replaces `lean_initialize_runtime_module`) for code that (indirectly) accesses the `Lean` package:
491-
//lean_initialize();
492487

493488
lean_object * res;
494489
// use same default as for Lean executables

‎Manual/Tactics/Reference.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -570,7 +570,7 @@ tag := "tactic-ref-sat"
570570
:::tactic "bv_check"
571571
:::
572572

573-
:::tactic Lean.Parser.Tactic.bvTraceMacro
573+
:::tactic Lean.Parser.Tactic.bvTrace
574574
:::
575575

576576
# Call-by-Value Evaluation

‎extended-examples/IndexMap.lean.hash‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
becacf8dd6806dd3

‎extended-examples/IndexMapGrind.lean.hash‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
6ee88e1d3c83f7a4

‎lake-manifest.json‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "f60239aad00fe8476449bbe863d23d5e97a915fd",
8+
"rev": "3c1e322f38aeeb2cb60c3cfdd7533dbf7b932714",
99
"name": "verso",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "nightly-testing",
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "6bc815869cba1f19515715dc6b47795acd521f1c",
18+
"rev": "76f052847294d189dc9924a33466b4b677f47e67",
1919
"name": "illuminate",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "c6e665d0f83a1e9f31535c0834e3f0a7bd0cc7d0",
28+
"rev": "c271f30a1bf40c7292e1a82c9d5e6f3e389c23b3",
2929
"name": "versowebcomponents",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "",
38-
"rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
38+
"rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669",
3939
"name": "plausible",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",

0 commit comments

Comments
 (0)