diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e1f8f424823d..56f5dfbd829f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -238,7 +238,7 @@ jobs: "name": "Linux 32bit", "os": "ubuntu-latest", // Use 32bit on stage0 and stage1 to keep oleans compatible - "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/", + "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config", "cmultilib": true, "release": true, "check-level": 2, @@ -327,7 +327,7 @@ jobs: run: | sudo dpkg --add-architecture i386 sudo apt-get update - sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 + sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386 if: matrix.cmultilib - name: Cache uses: actions/cache@v4 diff --git a/CMakeLists.txt b/CMakeLists.txt index 0626f53fc94c..5e0c2977bce3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -18,6 +18,9 @@ foreach(var ${vars}) if("${var}" MATCHES "LLVM*") list(APPEND STAGE0_ARGS "-D${var}=${${var}}") endif() + if("${var}" MATCHES "PKG_CONFIG*") + list(APPEND STAGE0_ARGS "-D${var}=${${var}}") + endif() elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY")) list(APPEND PLATFORM_ARGS "-D${var}=${${var}}") endif() diff --git a/RELEASES.md b/RELEASES.md index 7360725db20b..d1958e403f8f 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -11,12 +11,1197 @@ of each version. v4.16.0 ---------- -Development in progress. +## Language + +* [#3696](https://github.com/leanprover/lean4/pull/3696) makes all message constructors handle pretty printer errors. + +* [#4460](https://github.com/leanprover/lean4/pull/4460) runs all linters for a single command (together) on a separate +thread from further elaboration, making a first step towards +parallelizing the elaborator. + +* [#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that +are stubbed-out with `sorry` by ensuring that each `sorry` is not +definitionally equal to any other. For example, this now fails: +```lean +example : (sorry : Nat) = sorry := rfl -- fails +``` +However, this still succeeds, since the `sorry` is a single +indeterminate `Nat`: +```lean +def f (n : Nat) : Nat := sorry +example : f 0 = f 1 := rfl -- succeeds +``` +One can be more careful by putting parameters to the right of the colon: +```lean +def f : (n : Nat) → Nat := sorry +example : f 0 = f 1 := rfl -- fails +``` +Most sources of synthetic sorries (recall: a sorry that originates from +the elaborator) are now unique, except for elaboration errors, since +making these unique tends to cause a confusing cascade of errors. In +general, however, such sorries are labeled. This enables "go to +definition" on `sorry` in the Infoview, which brings you to its origin. +The option `set_option pp.sorrySource true` causes the pretty printer to +show source position information on sorries. + +* [#6123](https://github.com/leanprover/lean4/pull/6123) ensures that the configuration in `Simp.Config` is used when +reducing terms and checking definitional equality in `simp`. + +* [#6204](https://github.com/leanprover/lean4/pull/6204) lets `_` be used in numeric literals as a separator. For +example, `1_000_000`, `0xff_ff` or `0b_10_11_01_00`. New lexical syntax: +```text +numeral10 : [0-9]+ ("_"+ [0-9]+)* +numeral2 : "0" [bB] ("_"* [0-1]+)+ +numeral8 : "0" [oO] ("_"* [0-7]+)+ +numeral16 : "0" [xX] ("_"* hex_char+)+ +float : numeral10 "." numeral10? [eE[+-]numeral10] +``` + +* [#6270](https://github.com/leanprover/lean4/pull/6270) fixes a bug that could cause the `injectivity` tactic to fail in +reducible mode, which could cause unfolding lemma generation to fail +(used by tactics such as `unfold`). In particular, +`Lean.Meta.isConstructorApp'?` was not aware that `n + 1` is equivalent +to `Nat.succ n`. + +* [#6273](https://github.com/leanprover/lean4/pull/6273) modifies the "foo has been deprecated: use betterFoo instead" +warning so that foo and betterFoo are hoverable. + +* [#6278](https://github.com/leanprover/lean4/pull/6278) enables simp configuration options to be passed to `norm_cast`. + +* [#6286](https://github.com/leanprover/lean4/pull/6286) ensure `bv_decide` uses definitional equality in its reflection +procedure as much as possible. Previously it would build up explicit +congruence proofs for the kernel to check. This reduces the size of +proof terms passed to kernel speeds up checking of large reflection +proofs. + +* [#6288](https://github.com/leanprover/lean4/pull/6288) uses Lean.RArray in bv_decide's reflection proofs. Giving +speedups on problems with lots of variables. + +* [#6295](https://github.com/leanprover/lean4/pull/6295) sets up simprocs for all the remaining operations defined in +`Init.Data.Fin.Basic` + +* [#6300](https://github.com/leanprover/lean4/pull/6300) adds the `debug.proofAsSorry` option. When enabled, the proofs +of theorems are ignored and replaced with `sorry`. + +* [#6330](https://github.com/leanprover/lean4/pull/6330) removes unnecessary parameters from the funcion induction +principles. This is a breaking change; broken code can typically be adjusted +simply by passing fewer parameters. + +* [#6330](https://github.com/leanprover/lean4/pull/6330) removes unnecessary parameters from the funcion induction +principles. This is a breaking change; broken code can typically be adjusted +simply by passing fewer parameters. + +* [#6362](https://github.com/leanprover/lean4/pull/6362) adds the `--error=kind` option (shorthand: `-Ekind`) to the +`lean` CLI. When set, messages of `kind` (e.g., +`linter.unusedVariables`) will be reported as errors. This setting does +nothing in interactive contexts (e.g., the server). + +* [#6366](https://github.com/leanprover/lean4/pull/6366) adds support for `Float32` and fixes a bug in the runtime. + +* [#6375](https://github.com/leanprover/lean4/pull/6375) fixes a bug in the simplifier. It was producing terms with loose +bound variables when eliminating unused `let_fun` expressions. + +* [#6378](https://github.com/leanprover/lean4/pull/6378) adds an explanation to the error message when `cases` and +`induction` are applied to a term whose type is not an inductive type. +For `Prop`, these tactics now suggest the `by_cases` tactic. Example: +``` +tactic 'cases' failed, major premise type is not an inductive type + Prop +``` + +* [#6381](https://github.com/leanprover/lean4/pull/6381) fixes a bug in `withTrackingZetaDelta` and +`withTrackingZetaDeltaSet`. The `MetaM` caches need to be reset. See new +test. + +* [#6385](https://github.com/leanprover/lean4/pull/6385) fixes a bug in `simp_all?` that caused some local declarations +to be omitted from the `Try this:` suggestions. + +* [#6386](https://github.com/leanprover/lean4/pull/6386) ensures that `revertAll` clears auxiliary declarations when +invoked directly by users. + +* [#6387](https://github.com/leanprover/lean4/pull/6387) fixes a type error in the proof generated by the `contradiction` +tactic. + +* [#6397](https://github.com/leanprover/lean4/pull/6397) ensures that `simp` and `dsimp` do not unfold definitions that +are not intended to be unfolded by the user. See issue #5755 for an +example affected by this issue. + +* [#6398](https://github.com/leanprover/lean4/pull/6398) ensures `Meta.check` check projections. + +* [#6412](https://github.com/leanprover/lean4/pull/6412) adds reserved names for congruence theorems used in the +simplifier and `grind` tactics. The idea is prevent the same congruence +theorems to be generated over and over again. + +* [#6413](https://github.com/leanprover/lean4/pull/6413) introduces the following features to the WIP `grind` tactic: +- `Expr` internalization. +- Congruence theorem cache. +- Procedure for adding new facts +- New tracing options +- New preprocessing steps: fold projections and eliminate dangling +`Expr.mdata` + +* [#6414](https://github.com/leanprover/lean4/pull/6414) fixes a bug in `Lean.Meta.Closure` that would introduce +under-applied delayed assignment metavariables, which would keep them +from ever getting instantiated. This bug affected `match` elaboration +when the expected type contained postponed elaboration problems, for +example tactic blocks. + +* [#6419](https://github.com/leanprover/lean4/pull/6419) fixes multiple bugs in the WIP `grind` tactic. It also adds +support for printing the `grind` internal state. + +* [#6428](https://github.com/leanprover/lean4/pull/6428) adds a new preprocessing step to the `grind` tactic: +universe-level normalization. The goal is to avoid missing equalities in +the congruence closure module. + +* [#6430](https://github.com/leanprover/lean4/pull/6430) adds the predicate `Expr.fvarsSet a b`, which returns `true` if +and only if the free variables in `a` are a subset of the free variables +in `b`. + +* [#6433](https://github.com/leanprover/lean4/pull/6433) adds a custom type and instance canonicalizer for the (WIP) +`grind` tactic. The `grind` tactic uses congruence closure but +disregards types, type formers, instances, and proofs. Proofs are +ignored due to proof irrelevance. Types, type formers, and instances are +considered supporting elements and are not factored into congruence +detection. Instead, `grind` only checks whether elements are +structurally equal, which, in the context of the `grind` tactic, is +equivalent to pointer equality. See new tests for examples where the +canonicalizer is important. + +* [#6435](https://github.com/leanprover/lean4/pull/6435) implements the congruence table for the (WIP) `grind` tactic. It +also fixes several bugs, and adds a new preprocessing step. + +* [#6437](https://github.com/leanprover/lean4/pull/6437) adds support for detecting congruent terms in the (WIP) `grind` +tactic. It also introduces the `grind.debug` option, which, when set to +`true`, checks many invariants after each equivalence class is merged. +This option is intended solely for debugging purposes. + +* [#6438](https://github.com/leanprover/lean4/pull/6438) ensures `norm_cast` doesn't fail to act in the presence of +`no_index` annotations + +* [#6441](https://github.com/leanprover/lean4/pull/6441) adds basic truth value propagation rules to the (WIP) `grind` +tactic. + +* [#6442](https://github.com/leanprover/lean4/pull/6442) fixes the `checkParents` sanity check in `grind`. + +* [#6443](https://github.com/leanprover/lean4/pull/6443) adds support for propagating the truth value of equalities in +the (WIP) `grind` tactic. + +* [#6447](https://github.com/leanprover/lean4/pull/6447) refactors `grind` and adds support for invoking the simplifier +using the `GrindM` monad. + +* [#6448](https://github.com/leanprover/lean4/pull/6448) declares the command `builtin_grind_propagator` for registering +equation propagator for `grind`. It also declares the auxiliary the +attribute. + +* [#6449](https://github.com/leanprover/lean4/pull/6449) completes the implementation of the command +`builtin_grind_propagator`. + +* [#6452](https://github.com/leanprover/lean4/pull/6452) adds support for generating (small) proofs for any two +expressions that belong to the same equivalence class in the `grind` +tactic state. + +* [#6453](https://github.com/leanprover/lean4/pull/6453) improves bv_decide's performance in the presence of large +literals. + +* [#6455](https://github.com/leanprover/lean4/pull/6455) fixes a bug in the equality proof generator in the (WIP) `grind` +tactic. + +* [#6456](https://github.com/leanprover/lean4/pull/6456) fixes another bug in the equality proof generator in the (WIP) +`grind` tactic. + +* [#6457](https://github.com/leanprover/lean4/pull/6457) adds support for generating congruence proofs for congruences +detected by the `grind` tactic. + +* [#6458](https://github.com/leanprover/lean4/pull/6458) adds support for compact congruence proofs in the (WIP) `grind` +tactic. The `mkCongrProof` function now verifies whether the congruence +proof can be constructed using only `congr`, `congrFun`, and `congrArg`, +avoiding the need to generate the more complex `hcongr` auxiliary +theorems. + +* [#6459](https://github.com/leanprover/lean4/pull/6459) adds the (WIP) `grind` tactic. It currently generates a warning +message to make it clear that the tactic is not ready for production. + +* [#6461](https://github.com/leanprover/lean4/pull/6461) adds a new propagation rule for negation to the (WIP) `grind` +tactic. + +* [#6463](https://github.com/leanprover/lean4/pull/6463) adds support for constructors to the (WIP) `grind` tactic. When +merging equivalence classes, `grind` checks for equalities between +constructors. If they are distinct, it closes the goal; if they are the +same, it applies injectivity. + +* [#6464](https://github.com/leanprover/lean4/pull/6464) completes support for literal values in the (WIP) `grind` +tactic. `grind` now closes the goal whenever it merges two equivalence +classes with distinct literal values. + +* [#6465](https://github.com/leanprover/lean4/pull/6465) adds support for projection functions to the (WIP) `grind` +tactic. + +* [#6466](https://github.com/leanprover/lean4/pull/6466) completes the implementation of `addCongrTable` in the (WIP) +`grind` tactic. It also adds a new test to demonstrate why the extra +check is needed. It also updates the field `cgRoot` (congruence root). + +* [#6468](https://github.com/leanprover/lean4/pull/6468) fixes issue #6467 + +* [#6469](https://github.com/leanprover/lean4/pull/6469) adds support code for implementing e-match in the (WIP) `grind` +tactic. + +* [#6470](https://github.com/leanprover/lean4/pull/6470) introduces a command for specifying patterns used in the +heuristic instantiation of global theorems in the `grind` tactic. Note +that this PR only adds the parser. + +* [#6472](https://github.com/leanprover/lean4/pull/6472) implements the command `grind_pattern`. The new command allows +users to associate patterns with theorems. These patterns are used for +performing heuristic instantiation with e-matching. In the future, we +will add the attributes `@[grind_eq]`, `@[grind_fwd]`, and +`@[grind_bwd]` to compute the patterns automatically for theorems. + +* [#6473](https://github.com/leanprover/lean4/pull/6473) adds a deriving handler for the `ToExpr` class. It can handle +mutual and nested inductive types, however it falls back to creating +`partial` instances in such cases. This is upstreamed from the Mathlib +deriving handler written by @kmill, but has fixes to handle autoimplicit +universe level variables. + +* [#6474](https://github.com/leanprover/lean4/pull/6474) adds pattern validation to the `grind_pattern` command. The new +`checkCoverage` function will also be used to implement the attributes +`@[grind_eq]`, `@[grind_fwd]`, and `@[grind_bwd]`. + +* [#6475](https://github.com/leanprover/lean4/pull/6475) adds support for activating relevant theorems for the (WIP) +`grind` tactic. We say a theorem is relevant to a `grind` goal if the +symbols occurring in its patterns also occur in the goal. + +* [#6478](https://github.com/leanprover/lean4/pull/6478) internalize nested ground patterns when activating ematch +theorems in the (WIP) `grind` tactic. + +* [#6481](https://github.com/leanprover/lean4/pull/6481) implements E-matching for the (WIP) `grind` tactic. We still +need to finalize and internalize the new instances. + +* [#6484](https://github.com/leanprover/lean4/pull/6484) addresses a few error messages where diffs weren't being +exposed. + +* [#6485](https://github.com/leanprover/lean4/pull/6485) implements `Grind.EMatch.instantiateTheorem` in the (WIP) +`grind` tactic. + +* [#6487](https://github.com/leanprover/lean4/pull/6487) adds source position information for `structure` parent +projections, supporting "go to definition". Closes #3063. + +* [#6488](https://github.com/leanprover/lean4/pull/6488) fixes and refactors the E-matching module for the (WIP) `grind` +tactic. + +* [#6490](https://github.com/leanprover/lean4/pull/6490) adds basic configuration options for the `grind` tactic. + +* [#6492](https://github.com/leanprover/lean4/pull/6492) fixes a bug in the theorem instantiation procedure in the (WIP) +`grind` tactic. For example, it was missing the following instance in +one of the tests: + +* [#6497](https://github.com/leanprover/lean4/pull/6497) fixes another theorem instantiation bug in the `grind` tactic. +It also moves new instances to be processed to `Goal`. + +* [#6498](https://github.com/leanprover/lean4/pull/6498) adds support in the `grind` tactic for propagating dependent +forall terms `forall (h : p), q[h]` where `p` is a proposition. + +* [#6499](https://github.com/leanprover/lean4/pull/6499) fixes the proof canonicalizer for `grind`. + +* [#6500](https://github.com/leanprover/lean4/pull/6500) fixes a bug in the `markNestedProofs` used in `grind`. See new +test. + +* [#6502](https://github.com/leanprover/lean4/pull/6502) fixes a bug in the proof assembly procedure utilized by the +`grind` tactic. + +* [#6503](https://github.com/leanprover/lean4/pull/6503) adds a simple strategy to the (WIP) `grind` tactic. It just +keeps internalizing new theorem instances found by E-matching. The +simple strategy can solve examples such as: + +* [#6506](https://github.com/leanprover/lean4/pull/6506) adds the `monotonicity` tactic, intended to be used inside the +`partial_fixpoint` feature. + +* [#6508](https://github.com/leanprover/lean4/pull/6508) fixes a bug in the sanity checkers for the `grind` tactic. See +the new test for an example of a case where it was panicking. + +* [#6509](https://github.com/leanprover/lean4/pull/6509) fixes a bug in the congruence closure data structure used in the +`grind` tactic. The new test includes an example that previously caused +a panic. A similar panic was also occurring in the test +`grind_nested_proofs.lean`. + +* [#6510](https://github.com/leanprover/lean4/pull/6510) adds a custom congruence rule for equality in `grind`. The new +rule takes into account that `Eq` is a symmetric relation. In the +future, we will add support for arbitrary symmetric relations. The +current rule is important for propagating disequalities effectively in +`grind`. + +* [#6512](https://github.com/leanprover/lean4/pull/6512) introduces support for user-defined fallback code in the `grind` +tactic. The fallback code can be utilized to inspect the state of +failing `grind` subgoals and/or invoke user-defined automation. Users +can now write `grind on_failure `, where `` should have the +type `GoalM Unit`. See the modified tests in this PR for examples. + +* [#6513](https://github.com/leanprover/lean4/pull/6513) adds support for (dependent) if-then-else terms (i.e., `ite` and +`dite` applications) in the `grind` tactic. + +* [#6514](https://github.com/leanprover/lean4/pull/6514) enhances the assertion of new facts in `grind` by avoiding the +creation of unnecessary metavariables. + +## Library + +* [#6182](https://github.com/leanprover/lean4/pull/6182) adds `BitVec.[toInt|toFin]_concat` and moves a couple of +theorems into the concat section, as `BitVec.msb_concat` is needed for +the `toInt_concat` proof. + +* [#6188](https://github.com/leanprover/lean4/pull/6188) completes the `toNat` theorems for the bitwise operations +(`and`, `or`, `xor`, `shiftLeft`, `shiftRight`) of the UInt types and +adds `toBitVec` theorems as well. It also renames `and_toNat` to +`toNat_and` to fit with the current naming convention. + +* [#6238](https://github.com/leanprover/lean4/pull/6238) adds theorems characterizing the value of the unsigned shift +right of a bitvector in terms of its 2s complement interpretation as an +integer. +Unsigned shift right by at least one bit makes the value of the +bitvector less than or equal to `2^(w-1)`, +makes the interpretation of the bitvector `Int` and `Nat` agree. +In the case when `n = 0`, then the shift right value equals the integer +interpretation. + +* [#6244](https://github.com/leanprover/lean4/pull/6244) changes the implementation of `HashMap.toList`, so the ordering +agrees with `HashMap.toArray`. + +* [#6272](https://github.com/leanprover/lean4/pull/6272) introduces the basic theory of permutations of `Array`s and +proves `Array.swap_perm`. + +* [#6282](https://github.com/leanprover/lean4/pull/6282) moves `IO.Channel` and `IO.Mutex` from `Init` to `Std.Sync` and +renames them to `Std.Channel` and `Std.Mutex`. + +* [#6294](https://github.com/leanprover/lean4/pull/6294) upstreams `List.length_flatMap`, `countP_flatMap` and +`count_flatMap` from Mathlib. These were not possible to state before we +upstreamed `List.sum`. + +* [#6315](https://github.com/leanprover/lean4/pull/6315) adds `protected` to `Fin.cast` and `BitVec.cast`, to avoid +confusion with `_root_.cast`. These should mostly be used via +dot-notation in any case. + +* [#6316](https://github.com/leanprover/lean4/pull/6316) adds lemmas simplifying `for` loops over `Option` into +`Option.pelim`, giving parity with lemmas simplifying `for` loops of +`List` into `List.fold`. + +* [#6317](https://github.com/leanprover/lean4/pull/6317) completes the basic API for BitVec.ofBool. + +* [#6318](https://github.com/leanprover/lean4/pull/6318) generalizes the universe level for `Array.find?`, by giving it a +separate implementation from `Array.findM?`. + +* [#6324](https://github.com/leanprover/lean4/pull/6324) adds `GetElem` lemmas for the basic `Vector` operations. + +* [#6333](https://github.com/leanprover/lean4/pull/6333) generalizes the panic functions to a type of `Sort u` rather +than `Type u`. This better supports universe polymorphic types and +avoids confusing errors. + +* [#6334](https://github.com/leanprover/lean4/pull/6334) adds `Nat` theorems for distributing `>>>` over bitwise +operations, paralleling those of `BitVec`. + +* [#6338](https://github.com/leanprover/lean4/pull/6338) adds `BitVec.[toFin|getMsbD]_setWidth` and +`[getMsb|msb]_signExtend` as well as `ofInt_toInt`. + +* [#6341](https://github.com/leanprover/lean4/pull/6341) generalizes `DecidableRel` to allow a heterogeneous relation. + +* [#6353](https://github.com/leanprover/lean4/pull/6353) reproduces the API around `List.any/all` for `Array.any/all`. + +* [#6364](https://github.com/leanprover/lean4/pull/6364) makes fixes suggested by the Batteries environment linters, +particularly `simpNF`, and `unusedHavesSuffices`. + +* [#6365](https://github.com/leanprover/lean4/pull/6365) expands the `Array.set` and `Array.setIfInBounds` lemmas to +match existing lemmas for `List.set`. + +* [#6367](https://github.com/leanprover/lean4/pull/6367) brings Vector lemmas about membership and indexing to parity +with List and Array. + +* [#6369](https://github.com/leanprover/lean4/pull/6369) adds lemmas about `Vector.set`, `anyM`, `any`, `allM`, and +`all`. + +* [#6376](https://github.com/leanprover/lean4/pull/6376) adds theorems about `==` on `Vector`, reproducing those already +on `List` and `Array`. + +* [#6379](https://github.com/leanprover/lean4/pull/6379) replaces the inductive predicate `List.lt` with an upstreamed version of `List.Lex` from Mathlib. +(Previously `Lex.lt` was defined in terms of `<`; now it is generalized to take an arbitrary relation.) +This subtly changes the notion of ordering on `List α`. + + `List.lt` was a weaker relation: in particular if `l₁ < l₂`, then `a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b` are merely incomparable (either neither `a < b` nor `b < a`), whereas according to `List.Lex` this would require `a = b`. + + When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then the two relations coincide. + + Mathlib was already overriding the order instances for `List α`, so this change should not be noticed by anyone already using Mathlib. + + We simultaneously add the boolean valued `List.lex` function, parameterised by a `BEq` typeclass and an arbitrary `lt` function. This will support the flexibility previously provided for `List.lt`, via a `==` function which is weaker than strict equality. + +* [#6390](https://github.com/leanprover/lean4/pull/6390) redefines `Range.forIn'` and `Range.forM`, in preparation for +writing lemmas about them. + +* [#6391](https://github.com/leanprover/lean4/pull/6391) requires that the step size in `Std.Range` is positive, to avoid +ill-specified behaviour. + +* [#6396](https://github.com/leanprover/lean4/pull/6396) adds lemmas reducing for loops over `Std.Range` to for loops +over `List.range'`. + +* [#6399](https://github.com/leanprover/lean4/pull/6399) adds basic lemmas about lexicographic order on Array and Vector, +achieving parity with List. + +* [#6423](https://github.com/leanprover/lean4/pull/6423) adds missing lemmas about lexicographic order on +List/Array/Vector. + +* [#6477](https://github.com/leanprover/lean4/pull/6477) adds the necessary domain theory that backs the +`partial_fixpoint` feature. + +## Compiler + +* [#6311](https://github.com/leanprover/lean4/pull/6311) adds support for `HEq` to the new code generator. + +* [#6348](https://github.com/leanprover/lean4/pull/6348) adds support for `Float32` to the Lean runtime. + +* [#6350](https://github.com/leanprover/lean4/pull/6350) adds missing features and fixes bugs in the `Float32` support + +* [#6383](https://github.com/leanprover/lean4/pull/6383) ensures the new code generator produces code for `opaque` +definitions that are not tagged as `@[extern]`. +Remark: This is the behavior of the old code generator. + +* [#6405](https://github.com/leanprover/lean4/pull/6405) adds support for erasure of `Decidable.decide` to the new code +generator. It also adds a new `Probe.runOnDeclsNamed` function, which is +helpful for writing targeted single-file tests of compiler internals. + +* [#6415](https://github.com/leanprover/lean4/pull/6415) fixes a bug in the `sharecommon` module, which was returning +incorrect results for objects that had already been processed by +`sharecommon`. See the new test for an example that triggered the bug. + +* [#6429](https://github.com/leanprover/lean4/pull/6429) adds support for extern LCNF decls, which is required for parity +with the existing code generator. + +## Pretty Printing + +* [#5689](https://github.com/leanprover/lean4/pull/5689) adjusts the way the pretty printer unresolves names. It used to +make use of all `export`s when pretty printing, but now it only uses +`export`s that put names into parent namespaces (heuristic: these are +"API exports" that are intended by the library author), rather than +"horizontal exports" that put the names into an unrelated namespace, +which the dot notation feature in #6189 now incentivizes. + +* [#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that +are stubbed-out with `sorry` by ensuring that each `sorry` is not +definitionally equal to any other. For example, this now fails: +```lean +example : (sorry : Nat) = sorry := rfl -- fails +``` +However, this still succeeds, since the `sorry` is a single +indeterminate `Nat`: +```lean +def f (n : Nat) : Nat := sorry +example : f 0 = f 1 := rfl -- succeeds +``` +One can be more careful by putting parameters to the right of the colon: +```lean +def f : (n : Nat) → Nat := sorry +example : f 0 = f 1 := rfl -- fails +``` +Most sources of synthetic sorries (recall: a sorry that originates from +the elaborator) are now unique, except for elaboration errors, since +making these unique tends to cause a confusing cascade of errors. In +general, however, such sorries are labeled. This enables "go to +definition" on `sorry` in the Infoview, which brings you to its origin. +The option `set_option pp.sorrySource true` causes the pretty printer to +show source position information on sorries. + +## Documentation + +* [#6450](https://github.com/leanprover/lean4/pull/6450) adds a docstring to the `@[app_delab]` attribute. + +## Server + +* [#6279](https://github.com/leanprover/lean4/pull/6279) fixes a bug in structure instance field completion that caused +it to not function correctly for bracketed structure instances written +in Mathlib style. + +* [#6408](https://github.com/leanprover/lean4/pull/6408) fixes a regression where goals that don't exist were being +displayed. The regression was triggered by #5835 and originally caused +by #4926. + +## Lake + +* [#6176](https://github.com/leanprover/lean4/pull/6176) changes Lake's build process to no longer use `leanc` for +compiling C files or linking shared libraries and executables. Instead, +it directly invokes the bundled compiler (or the native compiler if +none) using the necessary flags. + +* [#6289](https://github.com/leanprover/lean4/pull/6289) adapts Lake modules to use `prelude` and includes them in the +`check-prelude` CI. + +* [#6291](https://github.com/leanprover/lean4/pull/6291) ensures the the log error position is properly preserved when +prepending stray log entries to the job log. It also adds comparison +support for `Log.Pos`. + +* [#6388](https://github.com/leanprover/lean4/pull/6388) merges `BuildJob` and `Job`, deprecating the former. `Job` now +contains a trace as part of its state which can be interacted with +monadically. also simplifies the implementation of `OpaqueJob`. + +* [#6411](https://github.com/leanprover/lean4/pull/6411) adds the ability to override package entries in a Lake manifest +via a separate JSON file. This file can be specified on the command line +with `--packages` or applied persistently by placing it at +`.lake/package-overrides.json`. + +* [#6422](https://github.com/leanprover/lean4/pull/6422) fixes a bug in #6388 where the `Package.afterBuildCahe*` +functions would produce different traces depending on whether the cache +was fetched. + +## Other + +* [#6285](https://github.com/leanprover/lean4/pull/6285) upstreams the `ToLevel` typeclass from mathlib and uses it to +fix the existing `ToExpr` instances so that they are truly universe +polymorphic (previously it generated malformed expressions when the +universe level was nonzero). We improve on the mathlib definition of +`ToLevel` to ensure the class always lives in `Type`, irrespective of +the universe parameter. + +* [#6363](https://github.com/leanprover/lean4/pull/6363) fixes errors at load time in the comparison mode of the Firefox +profiler. v4.15.0 ---------- -Release candidate, release notes will be copied from the branch `releases/v4.15.0` once completed. +## Language + +- [#4595](https://github.com/leanprover/lean4/pull/4595) implements `Simp.Config.implicitDefEqsProofs`. When `true` +(default: `true`), `simp` will **not** create a proof term for a +rewriting rule associated with an `rfl`-theorem. Rewriting rules are +provided by users by annotating theorems with the attribute `@[simp]`. +If the proof of the theorem is just `rfl` (reflexivity), and +`implicitDefEqProofs := true`, `simp` will **not** create a proof term +which is an application of the annotated theorem. + +- [#5429](https://github.com/leanprover/lean4/pull/5429) avoid negative environment lookup + +- [#5501](https://github.com/leanprover/lean4/pull/5501) ensure `instantiateMVarsProfiling` adds a trace node + +- [#5856](https://github.com/leanprover/lean4/pull/5856) adds a feature to the the mutual def elaborator where the +`instance` command yields theorems instead of definitions when the class +is a `Prop`. + +- [#5907](https://github.com/leanprover/lean4/pull/5907) unset trailing for `simpa?` "try this" suggestion + +- [#5920](https://github.com/leanprover/lean4/pull/5920) changes the rule for which projections become instances. Before, +all parents along with all indirect ancestors that were represented as +subobject fields would have their projections become instances. Now only +projections for direct parents become instances. + +- [#5934](https://github.com/leanprover/lean4/pull/5934) make `all_goals` admit goals on failure + +- [#5942](https://github.com/leanprover/lean4/pull/5942) introduce synthetic atoms in bv_decide + +- [#5945](https://github.com/leanprover/lean4/pull/5945) adds a new definition `Message.kind` which returns the top-level +tag of a message. This is serialized as the new field `kind` in +`SerialMessaege` so that i can be used by external consumers (e.g., +Lake) to identify messages via `lean --json`. + +- [#5968](https://github.com/leanprover/lean4/pull/5968) `arg` conv tactic misreported number of arguments on error + +- [#5979](https://github.com/leanprover/lean4/pull/5979) BitVec.twoPow in bv_decide + +- [#5991](https://github.com/leanprover/lean4/pull/5991) simplifies the implementation of `omega`. + +- [#5992](https://github.com/leanprover/lean4/pull/5992) fix style in bv_decide normalizer + +- [#5999](https://github.com/leanprover/lean4/pull/5999) adds configuration options for +`decide`/`decide!`/`native_decide` and refactors the tactics to be +frontends to the same backend. Adds a `+revert` option that cleans up +the local context and reverts all local variables the goal depends on, +along with indirect propositional hypotheses. Makes `native_decide` fail +at elaboration time on failure without sacrificing performance (the +decision procedure is still evaluated just once). Now `native_decide` +supports universe polymorphism. + +- [#6010](https://github.com/leanprover/lean4/pull/6010) changes `bv_decide`'s configuration from lots of `set_option` to +an elaborated config like `simp` or `omega`. The notable exception is +`sat.solver` which is still a `set_option` such that users can configure +a custom SAT solver globally for an entire project or file. Additionally +it introduces the ability to set `maxSteps` for the simp preprocessing +run through the new config. + +- [#6012](https://github.com/leanprover/lean4/pull/6012) improves the validation of new syntactic tokens. Previously, the +validation code had inconsistencies: some atoms would be accepted only +if they had a leading space as a pretty printer hint. Additionally, +atoms with internal whitespace are no longer allowed. + +- [#6016](https://github.com/leanprover/lean4/pull/6016) removes the `decide!` tactic in favor of `decide +kernel` +(breaking change). + +- [#6019](https://github.com/leanprover/lean4/pull/6019) removes @[specilize] from `MkBinding.mkBinding`, which is a +function that cannot be specialized (as none of its arguments are +functions). As a result, the specializable function `Nat.foldRevM.loop` +doesn't get specialized, which leads to worse performing code. + +- [#6022](https://github.com/leanprover/lean4/pull/6022) makes the `change` tactic and conv tactic use the same +elaboration strategy. It works uniformly for both the target and local +hypotheses. Now `change` can assign metavariables, for example: +```lean +example (x y z : Nat) : x + y = z := by + change ?a = _ + let w := ?a + -- now `w : Nat := x + y` +``` + +- [#6024](https://github.com/leanprover/lean4/pull/6024) fixes a bug where the monad lift coercion elaborator would +partially unify expressions even if they were not monads. This could be +taken advantage of to propagate information that could help elaboration +make progress, for example the first `change` worked because the monad +lift coercion elaborator was unifying `@Eq _ _` with `@Eq (Nat × Nat) +p`: +```lean +example (p : Nat × Nat) : p = p := by + change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't + change ⟨_, _⟩ = _ -- never worked +``` +As such, this is a breaking change; you may need to adjust expressions +to include additional implicit arguments. + +- [#6029](https://github.com/leanprover/lean4/pull/6029) adds a normalization rule to `bv_normalize` (which is used by +`bv_decide`) that converts `x / 2^k` into `x >>> k` under suitable +conditions. This allows us to simplify the expensive division circuits +that are used for bitblasting into much cheaper shifting circuits. +Concretely, it allows for the following canonicalization: + +- [#6030](https://github.com/leanprover/lean4/pull/6030) fixes `simp only [· ∈ ·]` after #5020. + +- [#6035](https://github.com/leanprover/lean4/pull/6035) introduces the and flattening pre processing pass from Bitwuzla +to `bv_decide`. It splits hypotheses of the form `(a && b) = true` into +`a = true` and `b = true` which has synergy potential with the already +existing embedded constraint substitution pass. + +- [#6037](https://github.com/leanprover/lean4/pull/6037) fixes `bv_decide`'s embedded constraint substitution to generate +correct counter examples in the corner case where duplicate theorems are +in the local context. + +- [#6045](https://github.com/leanprover/lean4/pull/6045) add `LEAN_ALWAYS_INLINE` to some functions + +- [#6048](https://github.com/leanprover/lean4/pull/6048) fixes `simp?` suggesting output with invalid indentation + +- [#6051](https://github.com/leanprover/lean4/pull/6051) mark `Meta.Context.config` as private + +- [#6053](https://github.com/leanprover/lean4/pull/6053) fixes the caching infrastructure for `whnf` and `isDefEq`, +ensuring the cache accounts for all relevant configuration flags. It +also cleans up the `WHNF.lean` module and improves the configuration of +`whnf`. + +- [#6061](https://github.com/leanprover/lean4/pull/6061) adds a simp_arith benchmark. + +- [#6062](https://github.com/leanprover/lean4/pull/6062) optimize Nat.Linear.Expr.toPoly + +- [#6064](https://github.com/leanprover/lean4/pull/6064) optimize Nat.Linear.Poly.norm + +- [#6068](https://github.com/leanprover/lean4/pull/6068) improves the asymptotic performance of `simp_arith` when there are many variables to consider. + +- [#6077](https://github.com/leanprover/lean4/pull/6077) adds options to `bv_decide`'s configuration structure such that +all non mandatory preprocessing passes can be disabled. + +- [#6082](https://github.com/leanprover/lean4/pull/6082) changes how the canonicalizer handles `forall` and `lambda`, +replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth +on +[zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Quantifiers.20in.20CanonM/near/482483448). + +- [#6093](https://github.com/leanprover/lean4/pull/6093) use mkFreshUserName in ArgsPacker + +- [#6096](https://github.com/leanprover/lean4/pull/6096) improves the `#print` command for structures to show all fields +and which parents the fields were inherited from, hiding internal +details such as which parents are represented as subobjects. This +information is still present in the constructor if needed. The pretty +printer for private constants is also improved, and it now handles +private names from the current module like any other name; private names +from other modules are made hygienic. + +- [#6098](https://github.com/leanprover/lean4/pull/6098) modifies `Lean.MVarId.replaceTargetDefEq` and +`Lean.MVarId.replaceLocalDeclDefEq` to use `Expr.equal` instead of +`Expr.eqv` when determining whether the expression has changed. This is +justified on the grounds that binder names and binder infos are +user-visible and affect elaboration. + +- [#6105](https://github.com/leanprover/lean4/pull/6105) fixes a stack overflow caused by a cyclic assignment in the +metavariable context. The cycle is unintentionally introduced by the +structure instance elaborator. + +- [#6108](https://github.com/leanprover/lean4/pull/6108) turn off pp.mvars in apply? results + +- [#6109](https://github.com/leanprover/lean4/pull/6109) fixes an issue in the `injection` tactic. This tactic may +execute multiple sub-tactics. If any of them fail, we must backtrack the +partial assignment. This issue was causing the error: "`mvarId` is +already assigned" in issue #6066. The issue is not yet resolved, as the +equation generator for the match expressions is failing in the example +provided in this issue. + +- [#6112](https://github.com/leanprover/lean4/pull/6112) makes stricter requirements for the `@[deprecated]` attribute, +requiring either a replacement identifier as `@[deprecated bar]` or +suggestion text `@[deprecated "Past its use by date"]`, and also +requires a `since := "..."` field. + +- [#6114](https://github.com/leanprover/lean4/pull/6114) liberalizes atom rules by allowing `''` to be a prefix of an +atom, after #6012 only added an exception for `''` alone, and also adds +some unit tests for atom validation. + +- [#6116](https://github.com/leanprover/lean4/pull/6116) fixes a bug where structural recursion did not work when indices +of the recursive argument appeared as function parameters in a different +order than in the argument's type's definition. + +- [#6125](https://github.com/leanprover/lean4/pull/6125) adds support for `structure` in `mutual` blocks, allowing +inductive types defined by `inductive` and `structure` to be mutually +recursive. The limitations are (1) that the parents in the `extends` +clause must be defined before the `mutual` block and (2) mutually +recursive classes are not allowed (a limitation shared by `class +inductive`). There are also improvements to universe level inference for +inductive types and structures. Breaking change: structure parents now +elaborate with the structure in scope (fix: use qualified names or +rename the structure to avoid shadowing), and structure parents no +longer elaborate with autoimplicits enabled. + +- [#6128](https://github.com/leanprover/lean4/pull/6128) does the same fix as #6104, but such that it doesn't break the +test/the file in `Plausible`. This is done by not creating unused let +binders in metavariable types that are made by `elimMVar`. (This is also +a positive thing for users looking at metavariable types, for example in +error messages) + +- [#6129](https://github.com/leanprover/lean4/pull/6129) fixes a bug at `isDefEq` when `zetaDelta := false`. See new test +for a small example that exposes the issue. + +- [#6131](https://github.com/leanprover/lean4/pull/6131) fixes a bug at the definitional equality test (`isDefEq`). At +unification constraints of the form `c.{u} =?= c.{v}`, it was not trying +to unfold `c`. This bug did not affect the kernel. + +- [#6141](https://github.com/leanprover/lean4/pull/6141) make use of recursive structures in snapshot types + +- [#6145](https://github.com/leanprover/lean4/pull/6145) fixes the `revert` tactic so that it creates a `syntheticOpaque` +metavariable as the new goal, instead of a `natural` metavariable + +- [#6146](https://github.com/leanprover/lean4/pull/6146) fixes a non-termination bug that occurred when generating the +match-expression splitter theorem. The bug was triggered when the proof +automation for the splitter theorem repeatedly applied `injection` to +the same local declaration, as it could not be removed due to forward +dependencies. See issue #6065 for an example that reproduces this issue. + +- [#6165](https://github.com/leanprover/lean4/pull/6165) modifies structure instance notation and `where` notation to use +the same notation for fields. Structure instance notation now admits +binders, type ascriptions, and equations, and `where` notation admits +full structure lvals. Examples of these for structure instance notation: +```lean +structure PosFun where + f : Nat → Nat + pos : ∀ n, 0 < f n +``` + +- [#6168](https://github.com/leanprover/lean4/pull/6168) extends the "motive is not type correct" error message for the +rewrite tactic to explain what it means. It also pretty prints the +type-incorrect motive and reports the type error. + +- [#6170](https://github.com/leanprover/lean4/pull/6170) adds core metaprogramming functions for forking off background +tasks from elaboration such that their results are visible to reporting +and the language server + +- [#6175](https://github.com/leanprover/lean4/pull/6175) fixes a bug with the `structure`/`class` command where if there +are parents that are not represented as subobjects but which used other +parents as instances, then there would be a kernel error. Closes #2611. + +- [#6180](https://github.com/leanprover/lean4/pull/6180) fixes a non-termination bug that occurred when generating the +match-expression equation theorems. The bug was triggered when the proof +automation for the equation theorem repeatedly applied `injection(` to +the same local declaration, as it could not be removed due to forward +dependencies. See issue #6067 for an example that reproduces this issue. + +- [#6189](https://github.com/leanprover/lean4/pull/6189) changes how generalized field notation ("dot notation") resolves +the function. The new resolution rule is that if `x : S`, then `x.f` +resolves the name `S.f` relative to the root namespace (hence it now +affected by `export` and `open`). Breaking change: aliases now resolve +differently. Before, if `x : S`, and if `S.f` is an alias for `S'.f`, +then `x.f` would use `S'.f` and look for an argument of type `S'`. Now, +it looks for an argument of type `S`, which is more generally useful +behavior. Code making use of the old behavior should consider defining +`S` or `S'` in terms of the other, since dot notation can unfold +definitions during resolution. + +- [#6206](https://github.com/leanprover/lean4/pull/6206) makes it possible to write `rw (occs := [1,2]) ...` instead of +`rw (occs := .pos [1,2]) ...` by adding a coercion from `List.Nat` to +`Lean.Meta.Occurrences`. + +- [#6220](https://github.com/leanprover/lean4/pull/6220) adds proper support for `let_fun` in `simp`. + +- [#6236](https://github.com/leanprover/lean4/pull/6236) fixes an issue where edits to a command containing a nested +docstring fail to reparse the entire command. + +## Library + +- [#4904](https://github.com/leanprover/lean4/pull/4904) introduces date and time functionality to the Lean 4 Std. + +- [#5616](https://github.com/leanprover/lean4/pull/5616) is a follow-up to https://github.com/leanprover/lean4/pull/5609, +where we add lemmas characterizing `smtUDiv` and `smtSDiv`'s behavior +when the denominator is zero. + +- [#5866](https://github.com/leanprover/lean4/pull/5866) verifies the `keys` function on `Std.HashMap`. + +- [#5885](https://github.com/leanprover/lean4/pull/5885) add Int16/Int32/Int64 + +- [#5926](https://github.com/leanprover/lean4/pull/5926) add `Option.or_some'` + +- [#5927](https://github.com/leanprover/lean4/pull/5927) `List.pmap_eq_self` + +- [#5937](https://github.com/leanprover/lean4/pull/5937) upstream lemmas about Fin.foldX + +- [#5938](https://github.com/leanprover/lean4/pull/5938) upstream List.ofFn and relate to Array.ofFn + +- [#5941](https://github.com/leanprover/lean4/pull/5941) List.mapFinIdx, lemmas, relate to Array version + +- [#5949](https://github.com/leanprover/lean4/pull/5949) consolidate `decide_True` and `decide_true_eq_true` + +- [#5950](https://github.com/leanprover/lean4/pull/5950) relate Array.takeWhile with List.takeWhile + +- [#5951](https://github.com/leanprover/lean4/pull/5951) remove @[simp] from BitVec.ofFin_sub and sub_ofFin + +- [#5952](https://github.com/leanprover/lean4/pull/5952) relate Array.eraseIdx with List.eraseIdx + +- [#5961](https://github.com/leanprover/lean4/pull/5961) define ISize and basic operations on it + +- [#5969](https://github.com/leanprover/lean4/pull/5969) upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas + +- [#5970](https://github.com/leanprover/lean4/pull/5970) deprecate Array.split in favour of identical Array.partition + +- [#5971](https://github.com/leanprover/lean4/pull/5971) relate Array.isPrefixOf with List.isPrefixOf + +- [#5972](https://github.com/leanprover/lean4/pull/5972) relate Array.zipWith/zip/unzip with List versions + +- [#5974](https://github.com/leanprover/lean4/pull/5974) add another List.find?_eq_some lemma + +- [#5981](https://github.com/leanprover/lean4/pull/5981) names the default SizeOf instance `instSizeOfDefault` + +- [#5982](https://github.com/leanprover/lean4/pull/5982) minor lemmas about List.ofFn + +- [#5984](https://github.com/leanprover/lean4/pull/5984) adds lemmas for `List` for the interactions between {`foldl`, +`foldr`, `foldlM`, `foldlrM`} and {`filter`, `filterMap`}. + +- [#5985](https://github.com/leanprover/lean4/pull/5985) relates the operations `findSomeM?`, `findM?`, `findSome?`, and +`find?` on `Array` with the corresponding operations on `List`, and also +provides simp lemmas for the `Array` operations `findSomeRevM?`, +`findRevM?`, `findSomeRev?`, `findRev?` (in terms of `reverse` and the +usual forward find operations). + +- [#5987](https://github.com/leanprover/lean4/pull/5987) BitVec.getMsbD in bv_decide + +- [#5988](https://github.com/leanprover/lean4/pull/5988) changes the signature of `Array.set` to take a `Nat`, and a +tactic-provided bound, rather than a `Fin`. + +- [#5995](https://github.com/leanprover/lean4/pull/5995) BitVec.sshiftRight' in bv_decide + +- [#6007](https://github.com/leanprover/lean4/pull/6007) List.modifyTailIdx naming fix + +- [#6008](https://github.com/leanprover/lean4/pull/6008) missing @[ext] attribute on monad transformer ext lemmas + +- [#6023](https://github.com/leanprover/lean4/pull/6023) variants of List.forIn_eq_foldlM + +- [#6025](https://github.com/leanprover/lean4/pull/6025) deprecate duplicated Fin.size_pos + +- [#6032](https://github.com/leanprover/lean4/pull/6032) changes the signature of `Array.get` to take a Nat and a proof, +rather than a `Fin`, for consistency with the rest of the (planned) +Array API. Note that because of bootstrapping issues we can't provide +`get_elem_tactic` as an autoparameter for the proof. As users will +mostly use the `xs[i]` notation provided by `GetElem`, this hopefully +isn't a problem. + +- [#6041](https://github.com/leanprover/lean4/pull/6041) modifies the order of arguments for higher-order `Array` +functions, preferring to put the `Array` last (besides positional +arguments with defaults). This is more consistent with the `List` API, +and is more flexible, as dot notation allows two different partially +applied versions. + +- [#6049](https://github.com/leanprover/lean4/pull/6049) adds a primitive for accessing the current thread ID + +- [#6052](https://github.com/leanprover/lean4/pull/6052) adds `Array.pmap`, as well as a `@[csimp]` lemma in terms of the +no-copy `Array.attachWith`. + +- [#6055](https://github.com/leanprover/lean4/pull/6055) adds lemmas about for loops over `Array`, following the existing +lemmas for `List`. + +- [#6056](https://github.com/leanprover/lean4/pull/6056) upstream some NameMap functions + +- [#6060](https://github.com/leanprover/lean4/pull/6060) implements conversion functions from `Bool` to all `UIntX` and +`IntX` types. + +- [#6070](https://github.com/leanprover/lean4/pull/6070) adds the Lean.RArray data structure. + +- [#6074](https://github.com/leanprover/lean4/pull/6074) allow `Sort u` in `Squash` + +- [#6094](https://github.com/leanprover/lean4/pull/6094) adds raw transmutation of floating-point numbers to and from +`UInt64`. Floats and UInts share the same endianness across all +supported platforms. The IEEE 754 standard precisely specifies the bit +layout of floats. Note that `Float.toBits` is distinct from +`Float.toUInt64`, which attempts to preserve the numeric value rather +than the bitwise value. + +- [#6095](https://github.com/leanprover/lean4/pull/6095) generalize `List.get_mem` + +- [#6097](https://github.com/leanprover/lean4/pull/6097) naming convention and `NaN` normalization + +- [#6102](https://github.com/leanprover/lean4/pull/6102) moves `IO.rand` and `IO.setRandSeed` to be in the `BaseIO` +monad. + +- [#6106](https://github.com/leanprover/lean4/pull/6106) fix naming of left/right injectivity lemmas + +- [#6111](https://github.com/leanprover/lean4/pull/6111) fills in the API for `Array.findSome?` and `Array.find?`, +transferring proofs from the corresponding List statements. + +- [#6120](https://github.com/leanprover/lean4/pull/6120) adds theorems `BitVec.(getMsbD, msb)_(rotateLeft, rotateRight)`. + +- [#6126](https://github.com/leanprover/lean4/pull/6126) adds lemmas for extracting a given bit of a `BitVec` obtained +via `sub`/`neg`/`sshiftRight'`/`abs`. + +- [#6130](https://github.com/leanprover/lean4/pull/6130) adds `Lean.loadPlugin` which exposes functionality similar to +the `lean` executable's `--plugin` option to Lean code. + +- [#6132](https://github.com/leanprover/lean4/pull/6132) duplicates the verification API for +`List.attach`/`attachWith`/`pmap` over to `Array`. + +- [#6133](https://github.com/leanprover/lean4/pull/6133) replaces `Array.feraseIdx` and `Array.insertAt` with +`Array.eraseIdx` and `Array.insertIdx`, both of which take a `Nat` +argument and a tactic-provided proof that it is in bounds. We also have +`eraseIdxIfInBounds` and `insertIdxIfInBounds` which are noops if the +index is out of bounds. We also provide a `Fin` valued version of +`Array.findIdx?`. Together, these quite ergonomically improve the array +indexing safety at a number of places in the compiler/elaborator. + +- [#6136](https://github.com/leanprover/lean4/pull/6136) fixes the run-time evaluation of `(default : Float)`. + +- [#6139](https://github.com/leanprover/lean4/pull/6139) modifies the signature of the functions `Nat.fold`, +`Nat.foldRev`, `Nat.any`, `Nat.all`, so that the function is passed the +upper bound. This allows us to change runtime array bounds checks to +compile time checks in many places. + +- [#6148](https://github.com/leanprover/lean4/pull/6148) adds a primitive for creating temporary directories, akin to the +existing functionality for creating temporary files. + +- [#6149](https://github.com/leanprover/lean4/pull/6149) completes the elementwise accessors for `ofNatLt`, `allOnes`, +and `not` by adding their implementations of `getMsbD`. + +- [#6151](https://github.com/leanprover/lean4/pull/6151) completes the `toInt` interface for `BitVec` bitwise operations. + +- [#6154](https://github.com/leanprover/lean4/pull/6154) implements `BitVec.toInt_abs`. + +- [#6155](https://github.com/leanprover/lean4/pull/6155) adds `toNat` theorems for `BitVec.signExtend.` + +- [#6157](https://github.com/leanprover/lean4/pull/6157) adds toInt theorems for BitVec.signExtend. + +- [#6160](https://github.com/leanprover/lean4/pull/6160) adds theorem `mod_eq_sub`, makes theorem +`sub_mul_eq_mod_of_lt_of_le` not private anymore and moves its location +within the `rotate*` section to use it in other proofs. + +- [#6184](https://github.com/leanprover/lean4/pull/6184) uses `Array.findFinIdx?` in preference to `Array.findIdx?` where +it allows converting a runtime bounds check to a compile time bounds +check. + +- [#6188](https://github.com/leanprover/lean4/pull/6188) completes the `toNat` theorems for the bitwise operations +(`and`, `or`, `xor`, `shiftLeft`, `shiftRight`) of the UInt types and +adds `toBitVec` theorems as well. It also renames `and_toNat` to +`toNat_and` to fit with the current naming convention. + +- [#6190](https://github.com/leanprover/lean4/pull/6190) adds the builtin simproc `USize.reduceToNat` which reduces the +`USize.toNat` operation on literals less than `UInt32.size` (i.e., +`4294967296`). + +- [#6191](https://github.com/leanprover/lean4/pull/6191) adds `Array.zipWithAll`, and the basic lemmas relating it to +`List.zipWithAll`. + +- [#6192](https://github.com/leanprover/lean4/pull/6192) adds deprecations for `Lean.HashMap` functions which did not +receive deprecation attributes initially. + +- [#6193](https://github.com/leanprover/lean4/pull/6193) completes the TODO in `Init.Data.Array.BinSearch`, removing the +`partial` keyword and converting runtime bounds checks to compile time +bounds checks. + +- [#6194](https://github.com/leanprover/lean4/pull/6194) changes the signature of `Array.swap`, so it takes `Nat` +arguments with tactic provided bounds checking. It also renames +`Array.swap!` to `Array.swapIfInBounds`. + +- [#6195](https://github.com/leanprover/lean4/pull/6195) renames `Array.setD` to `Array.setIfInBounds`. + +- [#6197](https://github.com/leanprover/lean4/pull/6197) upstreams the definition of `Vector` from Batteries, along with +the basic functions. + +- [#6200](https://github.com/leanprover/lean4/pull/6200) upstreams `Nat.lt_pow_self` and `Nat.lt_two_pow` from Mathlib +and uses them to prove the simp theorem `Nat.mod_two_pow`. + +- [#6202](https://github.com/leanprover/lean4/pull/6202) makes `USize.toUInt64` a regular non-opaque definition. + +- [#6203](https://github.com/leanprover/lean4/pull/6203) adds the theorems `le_usize_size` and `usize_size_le`, which +make proving inequalities about `USize.size` easier. + +- [#6205](https://github.com/leanprover/lean4/pull/6205) upstreams some UInt theorems from Batteries and adds more +`toNat`-related theorems. It also adds the missing `UInt8` and `UInt16` +to/from `USize` conversions so that the the interface is uniform across +the UInt types. + +- [#6207](https://github.com/leanprover/lean4/pull/6207) ensures the `Fin.foldl` and `Fin.foldr` are semireducible. +Without this the defeq `example (f : Fin 3 → ℕ) : List.ofFn f = [f 0, f +1, f 2] := rfl` was failing. + +- [#6208](https://github.com/leanprover/lean4/pull/6208) fix Vector.indexOf? + +- [#6217](https://github.com/leanprover/lean4/pull/6217) adds `simp` lemmas about `List`'s `==` operation. + +- [#6221](https://github.com/leanprover/lean4/pull/6221) fixes: +- Problems in other linux distributions that the default `tzdata` +directory is not the same as previously defined by ensuring it with a +fallback behavior when directory is missing. +- Trim unnecessary characters from local time identifier. + +- [#6222](https://github.com/leanprover/lean4/pull/6222) changes the definition of `HashSet.insertMany` and +`HashSet.Raw.insertMany` so that it is equivalent to repeatedly calling +`HashSet.insert`/`HashSet.Raw.insert`. It also clarifies the docstrings +of all the `insert` and `insertMany` functions. + +- [#6230](https://github.com/leanprover/lean4/pull/6230) copies some lemmas about `List.foldX` to `Array`. + +- [#6233](https://github.com/leanprover/lean4/pull/6233) upstreams lemmas about `Vector` from Batteries. + +- [#6234](https://github.com/leanprover/lean4/pull/6234) upstreams the definition and basic lemmas about `List.finRange` +from Batteries. + +- [#6235](https://github.com/leanprover/lean4/pull/6235) relates that operations `Nat.fold`/`foldRev`/`any`/`all` to the +corresponding List operations over `List.finRange`. + +- [#6241](https://github.com/leanprover/lean4/pull/6241) refactors `Array.qsort` to remove runtime array bounds checks, +and avoids the use of `partial`. We use the `Vector` API, along with +auto_params, to avoid having to write any proofs. The new code +benchmarks indistinguishably from the old. + +- [#6242](https://github.com/leanprover/lean4/pull/6242) deprecates `Fin.ofNat` in favour of `Fin.ofNat'` (which takes an +`[NeZero]` instance, rather than returning an element of `Fin (n+1)`). + +- [#6247](https://github.com/leanprover/lean4/pull/6247) adds the theorems `numBits_pos`, `le_numBits`, `numBits_le` , +which make proving inequalities about `System.Platform.numBits` easier. + +## Compiler + +- [#5840](https://github.com/leanprover/lean4/pull/5840) changes `lean_sharecommon_{eq,hash}` to only consider the +salient bytes of an object, and not any bytes of any +unspecified/uninitialized unused capacity. + +- [#6087](https://github.com/leanprover/lean4/pull/6087) fixes a bug in the constant folding for the `Nat.ble` and +`Nat.blt` function in the old code generator, leading to a +miscompilation. + +- [#6143](https://github.com/leanprover/lean4/pull/6143) should make lean better-behaved around sanitizers, per +https://github.com/google/sanitizers/issues/1688. +As far as I can tell, +https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterReturn#algorithm +replaces local variables with heap allocations, and so taking the +address of a local is not effective at producing a monotonic measure of +stack usage. + +- [#6209](https://github.com/leanprover/lean4/pull/6209) documents under which conditions `Runtime.markPersistent` is +unsafe and adjusts the elaborator accordingly + +- [#6257](https://github.com/leanprover/lean4/pull/6257) harden `markPersistent` uses + +## Pretty Printing + +- [#2934](https://github.com/leanprover/lean4/pull/2934) adds the option `pp.parens` (default: false) that causes the +pretty printer to eagerly insert parentheses, which can be useful for +teaching and for understanding the structure of expressions. For +example, it causes `p → q → r` to pretty print as `p → (q → r)`. + +- [#6014](https://github.com/leanprover/lean4/pull/6014) prevents `Nat.succ ?_` from pretty printing as `?_.succ`, which +should make `apply?` be more usable. + +- [#6085](https://github.com/leanprover/lean4/pull/6085) improves the term info for coercions marked with +`CoeFnType.coeFun` (such as `DFunLike.coe` in Mathlib), making "go to +definition" on the function name work. Hovering over such a coerced +function will show the coercee rather than the coercion expression. The +coercion expression can still be seen by hovering over the whitespace in +the function application. + +- [#6096](https://github.com/leanprover/lean4/pull/6096) improves the `#print` command for structures to show all fields +and which parents the fields were inherited from, hiding internal +details such as which parents are represented as subobjects. This +information is still present in the constructor if needed. The pretty +printer for private constants is also improved, and it now handles +private names from the current module like any other name; private names +from other modules are made hygienic. + +- [#6119](https://github.com/leanprover/lean4/pull/6119) adds a new delab option `pp.coercions.types` which, when +enabled, will display all coercions with an explicit type ascription. + +- [#6161](https://github.com/leanprover/lean4/pull/6161) ensures whitespace is printed before `+opt` and `-opt` +configuration options when pretty printing, improving the experience of +tactics such as `simp?`. + +- [#6181](https://github.com/leanprover/lean4/pull/6181) fixes a bug where the signature pretty printer would ignore the +current setting of `pp.raw`. This fixes an issue where `#check ident` +would not heed `pp.raw`. Closes #6090. + +- [#6213](https://github.com/leanprover/lean4/pull/6213) exposes the difference in "synthesized type class instance is +not definitionally equal" errors. + +## Documentation + +- [#6009](https://github.com/leanprover/lean4/pull/6009) fixes a typo in the docstring for prec and makes the text +slightly more precise. + +- [#6040](https://github.com/leanprover/lean4/pull/6040) join → flatten in docstring + +- [#6110](https://github.com/leanprover/lean4/pull/6110) does some mild refactoring of the `Lean.Elab.StructInst` module +while adding documentation. + +- [#6144](https://github.com/leanprover/lean4/pull/6144) converts 3 doc-string to module docs since it seems that this is +what they were intended to be! + +- [#6150](https://github.com/leanprover/lean4/pull/6150) refine kernel code comments + +- [#6158](https://github.com/leanprover/lean4/pull/6158) adjust file reference in Data.Sum + +- [#6239](https://github.com/leanprover/lean4/pull/6239) explains the order in which `Expr.abstract` introduces de Bruijn +indices. + +## Server + +- [#5835](https://github.com/leanprover/lean4/pull/5835) adds auto-completion for the fields of structure instance notation. Specifically, querying the completions via `Ctrl+Space` in the whitespace of a structure instance notation will now bring up the full list of fields. Whitespace structure completion can be enabled for custom syntax by wrapping the parser for the list of fields in a `structInstFields` parser. + +- [#5837](https://github.com/leanprover/lean4/pull/5837) fixes an old auto-completion bug where `x.` would issue +nonsensical completions when `x.` could not be elaborated as a dot +completion. + +- [#5996](https://github.com/leanprover/lean4/pull/5996) avoid max heartbeat error in completion + +- [#6031](https://github.com/leanprover/lean4/pull/6031) fixes a regression with go-to-definition and document highlight +misbehaving on tactic blocks. + +- [#6246](https://github.com/leanprover/lean4/pull/6246) fixes a performance issue where the Lean language server would +walk the full project file tree every time a file was saved, blocking +the processing of all other requests and notifications and significantly +increasing overall language server latency after saving. + +## Lake + +- [#5684](https://github.com/leanprover/lean4/pull/5684) update toolchain on `lake update` + +- [#6026](https://github.com/leanprover/lean4/pull/6026) adds a newline at end of each Lean file generated by `lake new` +templates. + +- [#6218](https://github.com/leanprover/lean4/pull/6218) makes Lake no longer automatically fetch GitHub cloud releases +if the package build directory is already present (mirroring the +behavior of the Reservoir cache). This prevents the cache from +clobbering existing prebuilt artifacts. Users can still manually fetch +the cache and clobber the build directory by running `lake build +:release`. + +- [#6225](https://github.com/leanprover/lean4/pull/6225) makes `lake build` also eagerly print package materialization +log lines. Previously, only a `lake update` performed eager logging. + +- [#6231](https://github.com/leanprover/lean4/pull/6231) improves the errors Lake produces when it fails to fetch a +dependency from Reservoir. If the package is not indexed, it will +produce a suggestion about how to require it from GitHub. + +## Other + +- [#6137](https://github.com/leanprover/lean4/pull/6137) adds support for displaying multiple threads in the trace +profiler output. + +- [#6138](https://github.com/leanprover/lean4/pull/6138) fixes `trace.profiler.pp` not using the term pretty printer. + +- [#6259](https://github.com/leanprover/lean4/pull/6259) ensures that nesting trace nodes are annotated with timing +information iff `trace.profiler` is active. v4.14.0 ---------- diff --git a/doc/dev/commit_convention.md b/doc/dev/commit_convention.md index 80362c175bec..9793350521a7 100644 --- a/doc/dev/commit_convention.md +++ b/doc/dev/commit_convention.md @@ -33,6 +33,9 @@ Format of the commit message - chore (maintain, ex: travis-ci) - perf (performance improvement, optimization, ...) +Every `feat` or `fix` commit must have a `changelog-*` label, and a commit message +beginning with "This PR " that will be included in the changelog. + ```` has the following constraints: - use imperative, present tense: "change" not "changed" nor "changes" @@ -44,6 +47,7 @@ Format of the commit message - just as in ````, use imperative, present tense - includes motivation for the change and contrasts with previous behavior + - If a `changelog-*` label is present, the body must begin with "This PR ". ``