chore: remove save tactic
#7047
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 16, 2025
This PR removes the `save` and `checkpoint` tactics that have been superseded by incremental elaboration
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 24, 2025
This PR removes the `save` and `checkpoint` tactics that have been superseded by incremental elaboration
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 25, 2025
This PR removes the `save` and `checkpoint` tactics that have been superseded by incremental elaboration
luisacicolini
added a commit
to opencompl/lean4
that referenced
this pull request
Mar 17, 2025
commit dcfd4a5f3f099bbed73dbc2a208d8474f1d7ea85 Author: Luisa Cicolini <[email protected]> Date: Tue Feb 18 14:50:39 2025 +0000 chore: remove redundant Co-authored-by: Siddharth <[email protected]> commit 9c1b8f6808ce667705de5ce57ea9f1b72b2b2b5a Author: luisacicolini <[email protected]> Date: Mon Feb 17 23:31:09 2025 +0000 chore: updated examples commit c292ee8cd820bc92f87cba9929c237f8eec0b56d Author: luisacicolini <[email protected]> Date: Mon Feb 17 23:13:52 2025 +0000 chore: check simp onlys commit d7d3abf838e0fa46a3082b372471bf28434b909f Author: luisacicolini <[email protected]> Date: Mon Feb 17 23:11:37 2025 +0000 chore: check simp onlys commit b9b60410785709c42c8241738522e3916336d0f6 Author: luisacicolini <[email protected]> Date: Mon Feb 17 23:10:53 2025 +0000 chore: check simp onlys commit 4d509bf33bbc2ee315b9f4a022d571ffc2003c88 Author: luisacicolini <[email protected]> Date: Mon Feb 17 23:08:49 2025 +0000 chore: fix umoo title format commit c803b56fa6714bd23503a280f7e8d7ef74dc11d9 Author: luisacicolini <[email protected]> Date: Mon Feb 17 17:47:23 2025 +0000 chore: fix build commit 2d5b3519c4345c61b00dcfe0027bfefcd3438c59 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:43:11 2025 +0000 chore: remove useless parentheses Co-authored-by: Tobias Grosser <[email protected]> commit 8c6e69f8e88a7acf84e9cda565361ff7aad255c2 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:40:09 2025 +0000 chore: remove useless parentheses Co-authored-by: Tobias Grosser <[email protected]> commit bae2439078692dd5ba53be41e8db73a2ac275e29 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:39:55 2025 +0000 chore: spacing format Co-authored-by: Tobias Grosser <[email protected]> commit ed7af08600a3ebb9ac259f8733e151cb7bcca7e5 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:39:39 2025 +0000 chore: remove useless parentheses Co-authored-by: Tobias Grosser <[email protected]> commit 831cd70cfee4e656ff2d6c14c6d617025a395c03 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:34:15 2025 +0000 chore: remove useless parentheses Co-authored-by: Tobias Grosser <[email protected]> commit 1316186868f7508f815b858a625a11ee79b90fc7 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:34:01 2025 +0000 chore: remove useless parentheses Co-authored-by: Tobias Grosser <[email protected]> commit c5169062f6431d170e9ae5ce8f439994e6653177 Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:33:04 2025 +0000 chore: remove useless parentheses Co-authored-by: Tobias Grosser <[email protected]> commit 7ec9ece80146e3d0c405f8adaf3e0c37cb02e66d Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 17:32:12 2025 +0000 chore: golf toInt_intMax Co-authored-by: Siddharth <[email protected]> commit a47b51f73a269c6bb30e4860071826db4c7d5af3 Author: luisacicolini <[email protected]> Date: Mon Feb 17 17:19:49 2025 +0000 chore: golf toInt_intMax commit 6ee013954e7269a1d509381e55a5314350dc13c5 Author: luisacicolini <[email protected]> Date: Mon Feb 17 17:14:55 2025 +0000 chore: remove redundant coercion commit 758bfad8aaaab377c89c6c7642f02ac745485119 Author: luisacicolini <[email protected]> Date: Mon Feb 17 16:05:41 2025 +0000 chore: reuse previous proof commit b7934d7c0f92defdcd4bf40bcb1f70990ad7f07d Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 15:49:54 2025 +0000 chore: formatting Co-authored-by: Siddharth <[email protected]> commit 66c3d7345db66eb726cc4e5b92c8f5f7b764523c Author: Luisa Cicolini <[email protected]> Date: Mon Feb 17 15:49:43 2025 +0000 chore: format Co-authored-by: Siddharth <[email protected]> commit 0a8a754009c761e3f0dd1f3b5b7cc0a938f1f0f8 Author: luisacicolini <[email protected]> Date: Mon Feb 17 15:48:22 2025 +0000 chore: less ugly proof commit c1a32372d0ac4e78d46a26d5b868b0c664574951 Author: luisacicolini <[email protected]> Date: Mon Feb 17 15:43:04 2025 +0000 chore: ugly proof commit 42e0b5103d19318de9b8502038204b0e5b10f0c1 Author: luisacicolini <[email protected]> Date: Mon Feb 17 15:01:18 2025 +0000 chore: fix toInt_intMax commit e294f27d23646a656e7ae6b77cedf2c06424087c Author: luisacicolini <[email protected]> Date: Mon Feb 17 10:36:00 2025 +0000 chore: smul example commit e00ebf97202321946b3839fd7aafc39dde0880e5 Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:59:44 2025 +0000 chore: replace theorem commit 5379dad35e07d190f5ff739aaa6e1b2899a8946d Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:38:03 2025 +0000 chore: format commit a11b10b8d6abf66df36335fbb3f7b1868e8ac739 Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:33:59 2025 +0000 chore: fix example and format commit 2de60122537568be3af0c376cc4aaccb08ecb264 Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:29:09 2025 +0000 chore: cleaning 3 commit 555157e7af39fafc1fdcbf30139c8f91d3a456b4 Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:24:17 2025 +0000 feat: add bv_decide test commit 3aa2cdb17203dc837215667c3ebbc924763adaaa Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:14:44 2025 +0000 chore: cleaning 2 commit be1e3ff03ccc82f12d0641a08ea92d356ca40cf8 Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:11:31 2025 +0000 chore: cleaning 1 commit 9bd164566de55d2399e4cc89f24b85136489270d Author: luisacicolini <[email protected]> Date: Mon Feb 17 09:02:19 2025 +0000 chore: fix sorrys commit 38308335be8d8c29d04a3904b795caf6c71c0430 Author: Tobias Grosser <[email protected]> Date: Sun Feb 16 13:25:22 2025 +0000 push sorry commit 07cc6f48fc55c075cc86158aaad1611bcc411351 Merge: 07e89ce0bf f50b863868 Author: Tobias Grosser <[email protected]> Date: Sun Feb 16 13:17:40 2025 +0000 Merge remote-tracking branch 'origin/master' into overflow-mul-defs commit 07e89ce0bf58d74ea034365b1b0cb87701c04f3b Author: Tobias Grosser <[email protected]> Date: Sun Feb 16 13:14:03 2025 +0000 Fix the broken proofs commit 6233f87e2f4230bea59e66c7404f34a79b204830 Author: Leonardo de Moura <[email protected]> Date: Sat Feb 15 21:32:46 2025 -0800 feat: cutsat helper functions (#7098) This PR adds some helper functions for cutsat in the `grind` tactic. commit b94b704a6f169766277cbb9199157be45bab775a Author: Leonardo de Moura <[email protected]> Date: Sat Feb 15 18:52:14 2025 -0800 feat: cutsat preparations (#7097) This PR implements several modifications for the cutsat procedure in `grind`. - The maximal variable is now at the beginning of linear polynomials. - The old `LinearArith.Solver` was deleted, and the normalizer was moved to `Simp`. - cutsat first files were created, and basic infrastructure for representing divisibility constraints was added. commit fe6263754afc3d9872e078284d8b158d119d3366 Author: Tobias Grosser <[email protected]> Date: Sun Feb 16 00:04:56 2025 +0000 feat: make `BitVec.getElem` the simp normal form and use it in `ext` (#5498) This PR makes `BitVec.getElem` the simp normal form in case a proof is available and changes `ext` to return `x[i]` + a hypothesis that proves that we are in-bounds. This aligns `BitVec` further with the API conventions of the Lean standard datatypes. We move our proofs to this new normal form, which results in slightly smaller proofs. With the exception of `getElem_ofFin`, no new API surface is added as the `getElem` API has already been completed over the previous months. We also move `getElem_shiftConcat_*` a bit higher as they are needed in earlier proofs. To keep the changeset small, we do not update the API of `BVDecide` but insert `← BitVec.getLsbD_eq_getElem` at the few locations where it is needed. Finally, we add a simproc for getElem, mirroring the existing ones for getLsbD/getMsdD. --------- Co-authored-by: Alex Keizer <[email protected]> commit 29da643c15c5024161d73d6ddf2a0456a11585a1 Author: Leonardo de Moura <[email protected]> Date: Sat Feb 15 15:45:35 2025 -0800 chore: cleanup and missing `grind` normalization rules (#7095) This PR adds missing `grind` normalization rules, and removes dead theorems. commit a9a1c8330a15f5039de2c1b4b1ba5e6ff32a92cd Author: Leonardo de Moura <[email protected]> Date: Sat Feb 15 14:10:23 2025 -0800 refactor: add `denote'` functions to `Int/Linear.lean` (#7094) This PR adds the functions `Poly.denote'`, `RelCnstr.denote'`, and `DvdCnstr.denote'`. These functions are useful for representing the denotation of normalized results in `simp +arith` and the `grind` preprocessor. This PR also adjusts all auxiliary normalization theorems to use them to represent the normalized constraints. Previously, we were converting `RelCnstr` and `DvdCnstr` back into raw constraints. While this overhead was reasonable for `simp +arith`, it is not for the cutsat procedure, which has no need for raw constraints. All constraints have already been normalized by the time they reach cutsat. commit b1c6a58b6ed5bc3df1eca38e040c49e512ea5e50 Author: Leonardo de Moura <[email protected]> Date: Sat Feb 15 11:20:18 2025 -0800 refactor: `Int.Linear` module (#7093) This PR cleans up the `Int.Linear` module by normalizing function and type names and adding documentation strings. We will use it to implement cutsat in the `grind` tactic. commit f57029d0f39fe9023df2900a34b36d474d03bb76 Author: Leonardo de Moura <[email protected]> Date: Fri Feb 14 20:20:40 2025 -0800 feat: divisibility constraint normalizer (#7092) This PR implements divisibility constraint normalization in `simp +arith`. commit 12813e925986b020d0f2ac2e55be040917272d79 Author: jrr6 <[email protected]> Date: Fri Feb 14 22:00:36 2025 -0500 fix: ensure `get_elem_tactic` works in absence of goals (#7088) This PR fixes the behavior of the indexed-access notation `xs[i]` in cases where the proof of `i`'s validity is filled in during unification. Closes #6999. commit 81cf202725ad6a83adc6a1609fc8036c5cc7cf55 Author: Leonardo de Moura <[email protected]> Date: Fri Feb 14 18:44:49 2025 -0800 feat: add helper theorems for normalizing divisibility constraints (#7091) This PR adds helper theorems for normalizing divisibility constraints. They are going to be used to implement the cutsat procedure in the `grind` tactic. commit c5f13132a24bf2bd736b29a47a0f84e03e67599c Author: Kyle Miller <[email protected]> Date: Fri Feb 14 09:28:54 2025 -0800 feat: make binders in `#check` be hoverable (#7074) This PR modifies the signature pretty printer to add hover information for parameters in binders. This makes the binders be consistent with the hovers in pi types. Suggested by @david-christiansen commit c31d3e2cba169ae9ba419829fdfde35db275b712 Author: Markus Himmel <[email protected]> Date: Fri Feb 14 12:59:44 2025 +0100 feat: `Fin.toNat` (#7079) This PR introduces `Fin.toNat` as an alias for `Fin.val`. We add this function for discoverability and consistency reasons. The normal form for proofs remains `Fin.val`, and there is a `simp` lemma rewriting `Fin.toNat` to `Fin.val`. commit e98e635ff7c73005ca500efe830c40cac46b3336 Author: Markus Himmel <[email protected]> Date: Fri Feb 14 12:59:41 2025 +0100 feat: `UIntX.ofNatTruncate` (#7080) This PR adds the functions `UIntX.ofNatTruncate` (the version for `UInt32` already exists). commit dea6bf4c19a949addc2178464d470364cb4499bb Author: Markus Himmel <[email protected]> Date: Fri Feb 14 12:59:37 2025 +0100 feat: `IntX.minValue`, `IntX.maxValue`, `IntX.ofIntLE`, `IntX.ofIntTruncate` (#7081) This PR adds functions `IntX.ofIntLE`, `IntX.ofIntTruncate`, which are analogous to the unsigned counterparts `UIntX.ofNatLT` and `UInt.ofNatTruncate`. commit 40b74248100d02392591fdb22acc55d859def24f Author: Marc Huisinga <[email protected]> Date: Fri Feb 14 12:55:43 2025 +0100 feat: request cancellation (#7054) This PR adds language server support for request cancellation to the following expensive requests: Code actions, auto-completion, document symbols, folding ranges and semantic highlighting. This means that when the client informs the language server that a request is stale (e.g. because it belongs to a previous state of the document), the language server will now prematurely cancel the computation of the response in order to reduce the CPU load for requests that will be discarded by the client anyways. commit ade075bd22e854dc91f5fdb22cf1a1ea786dca29 Author: Marc Huisinga <[email protected]> Date: Fri Feb 14 12:53:24 2025 +0100 fix: incremental goal state requests select incomplete snapshot (#6887) This PR fixes a bug where the goal state selection would sometimes select incomplete incremental snapshots on whitespace, leading to an incorrect "no goals" response. Fixes #6594, a regression that was originally introduced in 4.11.0 by #4727. The fundamental cause of #6594 was that the snapshot selection would always select the first snapshot with a range that contains the cursor position. For tactics, whitespace had to be included in this range. However, in the test case of #6594, this meant that the snapshot selection would also sometimes pick a snapshot before the cursor that still contains the cursor in its whitespace, but which also does not necessarily contain all the information needed to produce a correct goal state. Specifically, at the `InfoTree`-level, when the cursor is in whitespace, we distinguish competing goal states by their level of indentation. The snapshot selection did not have access to this information, so it necessarily had to do the wrong thing in some cases. This PR fixes the issue by adjusting the snapshot selection for goals to explicitly account for whitespace and indentation, and refactoring the language processor architecture to thread enough information through to the snapshot selection so that it can decide which snapshots to use without having to force too many tasks, which would destroy incrementality in goal state requests. Specifically, this PR makes the following adjustments: - Refactor `SnapshotTask` to contain both a `Syntax` and a `Range`. Before, `SnapshotTask`s had a single range that was used both for displaying file progress information and for selecting snapshots in server requests. For most snapshots, this range did not include whitespace, though for tactics it did. Now, the `reportingRange` field of `SnapshotTask` is intended exclusively for reporting file progress information, and the `Syntax` is used for selecting snapshots in server requests. Importantly, the `Syntax` contains the full range information of the snapshot, i.e. its regular range and its range including whitespace. - Adjust all call-sites of `SnapshotTask` to produce a reasonable `Syntax`. - Adjust the goal snapshot selection to account for whitespace and indentation, as the `InfoTree` goal selection does. - Fix a bug in the snapshot tree tracing that would cause it to render the `Info` of a snapshot at the wrong location when `trace.Elab.info` was also set. This PR is based on #6329. commit 38a93e962052f7ee226a7e19b245600a5286f4f6 Author: Paul Reichert <[email protected]> Date: Fri Feb 14 09:24:33 2025 +0100 feat: insertMany, ofList, ofArray, foldr, foldM functions for the tree map (#7051) This PR implements the methods `insertMany`, `ofList`, `ofArray`, `foldr` and `foldrM` on the tree map. --------- Co-authored-by: Paul Reichert <[email protected]> commit 1c522cc2e2b5150a1cab09c82a114957a21d5b6b Author: Markus Himmel <[email protected]> Date: Fri Feb 14 07:58:15 2025 +0100 chore: rename `UIntX.ofNatCore`, `UIntX.ofNat'` -> `UIntX.ofNatLT` (#7071) This PR unifies the existing functions `UIntX.ofNatCore` and `UIntX.ofNat'` under a new name, `UIntX.ofNatLT`. commit 523df207303806451d4037ed240050b72550bc0a Author: Leonardo de Moura <[email protected]> Date: Thu Feb 13 21:43:38 2025 -0800 feat: simprocs for `Int` and `Nat` divides predicates (#7078) This PR implements simprocs for `Int` and `Nat` divides predicates. commit 7da2c917aada5957f7e05d8f3b9c2d97c6cb73b9 Author: Mac Malone <[email protected]> Date: Thu Feb 13 23:57:31 2025 -0500 feat: lake: support plugins (#7001) This PR adds support for plugins to Lake. Precompiled modules are now loaded as plugins rather than via `--load-dynlib`. Additional plugins can be added through an experimental `plugins` configuration option. The syntax for specifying this is not yet convenient, and will be improved in future changes. A parallel `dynlibs` configuration option has been added for specifying additional dynamic libraries to build and pass to `--load-dynlib`. This PR also changes the default directory for `.olean`, `.ilean`, and module dynamic libraries (i.e., `leanLibDir`) to `lib/lean` instead of the previous default of `lib`. This avoids potential name clashes between single module shared libraries and the shared libraries of a full `lean_lib`. On non-Windows systems, module dynamic libraries are no longer linked to their imports or external symbols. Symbols from those libraries are left unresolved until load time. This avoids nesting these dependencies within the shared library and means Lake no longer needs to augment the shared library path to allow Lean to resolve such nested dependencies on load. commit da4f887cbdb6caf6262a72ad9064d25f6446f803 Author: Leonardo de Moura <[email protected]> Date: Thu Feb 13 20:55:58 2025 -0800 feat: support theorems for cutsat `Div-Solve` rule (#7077) This PR proves the helper theorems for justifying the "Div-Solve" rule in the cutsat procedure. commit d01d43316154b0944da03eda828850f82bb5ee76 Author: Kim Morrison <[email protected]> Date: Fri Feb 14 15:08:18 2025 +1100 feat: premise selection API (#7061) This PR provides a basic API for a premise selection tool, which can be provided in downstream libraries. It does not implement premise selection itself! commit 383ffc121f0d2e914679cd9f45aea62a8bacc154 Author: Lean stage0 autoupdater <> Date: Thu Feb 13 16:00:29 2025 +0000 chore: update stage0 commit cb856bcd8414a348c56da09bf8d41dafcdbb0dc4 Author: Markus Himmel <[email protected]> Date: Thu Feb 13 15:51:42 2025 +0100 chore: dsimproc for UIntX.ofNatLT (#7068) This PR is a follow-up to #7057 and adds a builtin dsimproc for `UIntX.ofNatLT` which it turns out we need in stage0 before we can get the deprecation of `UIntX.ofNatCore` in favor of `UIntX.ofNatLT` off the ground. commit 37574d65b7e6efbe138c75f9579b5b46fd4f9843 Author: Bulhwi Cha <[email protected]> Date: Thu Feb 13 22:21:18 2025 +0900 doc: fix typo (#7067) commit e4d96ab4d38fc758b4b7bbb3b009d261ca5ecb51 Author: Markus Himmel <[email protected]> Date: Thu Feb 13 13:52:31 2025 +0100 chore: rename `BitVec.ofNatLt` -> `BitVec.ofNatLT` (#7064) This PR renames `BitVec.ofNatLt` to `BitVec.ofNatLT` and sets up deprecations for the old name. commit a8053d1eb70b1adaa1907237609ae4f63cc0a2da Author: Markus Himmel <[email protected]> Date: Thu Feb 13 13:14:28 2025 +0100 chore: rename `IntX.toNat` -> `IntX.toNatClampNeg` (#7066) This PR renames `IntX.toNat` to `IntX.toNatClampNeg` (to reduce surprises) and sets up a deprecation. commit 7a887d60ae3f8a35eaaf488acccf1e6858d233be Author: Markus Himmel <[email protected]> Date: Thu Feb 13 12:29:31 2025 +0100 chore: make `IntX` constructor private, provide `UIntX.toIntX` (#7062) This PR introduces the functions `UIntX.toIntX` as the public API to obtain the `IntX` that is 2's complement equivalent to a given `UIntX`. commit 6b46cf583c0ed4f489305264a22a4d55e10f9f3a Author: Paul Reichert <[email protected]> Date: Thu Feb 13 12:12:22 2025 +0100 feat: deprecated find, fold, foldM, mergeBy functions for the tree map (#7036) This PR adds some deprecated function aliases to the tree map in order to ease the transition from the `RBMap` to the tree map. --------- Co-authored-by: Paul Reichert <[email protected]> commit 37827565d23ce62c3898dcd532c6a3021e262cef Author: Markus Himmel <[email protected]> Date: Thu Feb 13 12:02:00 2025 +0100 feat: missing conversion functions for `ISize` (#7063) This PR adds `ISize.toInt8`, `ISize.toInt16`, `Int8.toISize`, `Int16.toISize`. commit 2ebedea21a49e0f060ffcc045caaf1781636726e Author: Joachim Breitner <[email protected]> Date: Thu Feb 13 10:38:42 2025 +0100 feat: binderNameHint in congr (#7053) This PR makes `simp` heed the `binderNameHint` also in the assumptions of congruence rules. Fixes #7052. commit ab65a54dec15f293b21f3e62e4e0ad822ae99a8f Author: Markus Himmel <[email protected]> Date: Thu Feb 13 09:45:01 2025 +0100 feat: `UIntX.ofFin` (#7056) This PR adds the `UIntX.ofFin` conversion functions. commit 0c219197ff2596d9525546ab752893870dc7e78b Author: Markus Himmel <[email protected]> Date: Thu Feb 13 08:50:47 2025 +0100 chore: rename `UIntX.val` -> `UIntX.toFin` (#7050) This PR renames the functions `UIntX.val` to `UIntX.toFin`. commit a5fdbb12896f82bbfb0500372d0943efa1209a31 Author: Kim Morrison <[email protected]> Date: Thu Feb 13 14:19:02 2025 +1100 chore: upstream an Int lemma (#7060) commit 6a586e67d9b8448d8c43b81d1e61756a8969a759 Author: Leonardo de Moura <[email protected]> Date: Wed Feb 12 15:16:07 2025 -0800 refactor: move `grind` offset constraint module to `Grind/Arith/Offset` (#7058) This PR moves the `grind` offset constraint module to the `Grind/Arith/Offset` subdirectory in preparation to the full linear integer arithmetic module. commit ec514da34fc2a93b90f4515c2c213c04fdfe2b33 Author: Lean stage0 autoupdater <> Date: Wed Feb 12 17:09:23 2025 +0000 chore: update stage0 commit 76f5c3746024a2b7bb9be32a34d10341d6f7101a Author: Markus Himmel <[email protected]> Date: Wed Feb 12 17:08:03 2025 +0100 chore: rename `UIntX.mk` -> `UIntX.ofBitVec` (#7046) This PR renames `UIntX.mk` to `UIntX.ofBitVec` and adds deprecations. commit 40630e6ea9b0dec005e46d0cf08a3656fef0d0c1 Author: Markus Himmel <[email protected]> Date: Wed Feb 12 16:12:29 2025 +0100 chore: add `UIntX.ofNatLT` (#7057) This PR adds the function `UIntX.ofNatLT`. This is supposed to be a replacement for `UIntX.ofNatCore` and `UIntX.ofNat'`, but for bootstrapping reasons we need this function to exist in stage0 before we can proceed with the renaming and deprecations, so this PR just adds the function. commit 3fd31da818c2b86fe523aaac313b26897e0f1938 Author: Markus Himmel <[email protected]> Date: Wed Feb 12 15:49:31 2025 +0100 feat: `IntX.ofBitVec` (#7048) This PR adds the functions `IntX.ofBitVec`. commit daddcb81147fbf423e64ae9de6f4cba6dffa02c5 Author: Joachim Breitner <[email protected]> Date: Wed Feb 12 14:22:08 2025 +0100 feat: propagate wfParam through let (#7039) This PR improves the well-founded definition preprocessing to propagate `wfParam` through let expressions. Fixes #7038. commit 995751bdd506422ab66e5297d2f08c4ab8976b85 Author: Sebastian Ullrich <[email protected]> Date: Wed Feb 12 10:29:51 2025 +0100 chore: compile against glibc 2.26 (#7037) This PR relaxes the minimum required glibc version for Lean and Lean executables to 2.26 on x86-64 Linux commit ea02231b46e122b9b099684e2ffee637884f200f Author: Sebastian Ullrich <[email protected]> Date: Wed Feb 12 10:19:30 2025 +0100 chore: remove `save` tactic (#7047) This PR removes the `save` and `checkpoint` tactics that have been superseded by incremental elaboration commit 3a91e7a0499d0a316c78ba620c75276e4f0cf8c9 Author: Cameron Zwarich <[email protected]> Date: Wed Feb 12 01:13:49 2025 -0800 fix: make several LCNF environment extensions have asyncMode of .sync (#7041) This PR marks several LCNF-specific environment extensions as having an asyncMode of .sync rather than the default of .mainOnly, so they work correctly even in async contexts. commit 5b5fbcd86ed2b42fd5093b357ca6a2333e20c02d Author: Joachim Breitner <[email protected]> Date: Wed Feb 12 10:06:12 2025 +0100 feat: wf_preprocess for {List,Array}.Monadic functions (#7034) This PR adds `wf_preprocess` theorems for `{List,Array}.{foldlM,foldrM,mapM,filterMapM,flatMapM}` commit d4ccc335279e53683f80b1b1ceffa93593452698 Author: Sebastian Ullrich <[email protected]> Date: Wed Feb 12 11:22:32 2025 +0100 test: fix `simp_arith1` benchmark (#7049) commit ca764bd88abd9ffef64c6729f509d23eeb3fc8dd Author: Lean stage0 autoupdater <> Date: Wed Feb 12 09:15:43 2025 +0000 chore: update stage0 commit 9dbbc4823dcd3a3dd356445b6167b70f59adf91d Author: Kim Morrison <[email protected]> Date: Wed Feb 12 16:17:39 2025 +1100 chore: fix `linter.listVariables` naming (#7044) commit 64fb473fa735f98385c3c1d3604a4237190fb139 Author: Leonardo de Moura <[email protected]> Date: Tue Feb 11 19:55:45 2025 -0800 chore: `simp_arith` has been deprecated (#7043) This PR deprecates the tactics `simp_arith`, `simp_arith!`, `simp_all_arith` and `simp_all_arith!`. Users can just use the `+arith` option. commit e4b50ac5ae692d1e3641b748f2058cf5bbe4bf39 Author: Leonardo de Moura <[email protected]> Date: Tue Feb 11 18:14:00 2025 -0800 chore: remove dead code from `Nat/Linear.lean` (#7042) commit a37d386aca0b634f8b6ac4e376157afb50895e65 Author: Leonardo de Moura <[email protected]> Date: Tue Feb 11 15:37:30 2025 -0800 feat: `simp +arith` sorts linear atoms (#7040) This PR ensures that terms such as `f (2*x + y)` and `f (y + x + x)` have the same normal form when using `simp +arith` commit 73e20798bd147b5d15685797a33c22d510d3a475 Author: Paul Reichert <[email protected]> Date: Tue Feb 11 15:47:47 2025 +0100 feat: tree map data structures and operations (#6914) This PR introduces ordered map data structures, namely `DTreeMap`, `TreeMap`, `TreeSet` and their `.Raw` variants, into the standard library. There are still some operations missing that the hash map has. As of now, the operations are unverified, but the corresponding lemmas will follow in subsequent PRs. While the tree map has already been optimized, more micro-optimization will follow as soon as the new code generator is ready. --------- Co-authored-by: Paul Reichert <[email protected]> commit bbd41d5374ba1603c41ecc94ff85002f62691167 Author: Henrik Böving <[email protected]> Date: Tue Feb 11 12:01:40 2025 +0100 feat: present bv_decide counter examples for UIntX and enums better (#7033) This PR improves presentation of counter examples for UIntX and enum inductives in bv_decide. commit f07e640ddb08499a3256fe55d51712243f9656da Author: Leonardo de Moura <[email protected]> Date: Mon Feb 10 19:45:25 2025 -0800 feat: linear integer inequality normalization using `gcd` of coefficients (#7030) This PR adds completes the linear integer inequality normalizer for `grind`. The missing normalization step replaces a linear inequality of the form `a_1*x_1 + ... + a_n*x_n + b <= 0` with `a_1/k * x_1 + ... + a_n/k * x_n + ceil(b/k) <= 0` where `k = gcd(a_1, ..., a_n)`. `ceil(b/k)` is implemented using the helper `cdiv b k`. commit 8abeb42c4f744919578f60be94edf5d230d88986 Author: Mac Malone <[email protected]> Date: Mon Feb 10 19:43:38 2025 -0500 feat: lake: provide help on Elan's `+` option (#7024) This PR documents how to use Elan's `+` option with `lake new|init`. It also provides an more informative error message if a `+` option leaks into Lake (e.g., if a user provides the option to a Lake run without Elan). commit 0e328f06781d9881a8838b13bf03a03805804cc2 Author: Sebastian Ullrich <[email protected]> Date: Mon Feb 10 19:16:20 2025 +0100 chore: build Lean with `Elab.async` (#6989) commit 519f70cc1c7b72e51089a5d52d5164826510b91d Author: Henrik Böving <[email protected]> Date: Mon Feb 10 18:42:59 2025 +0100 feat: bv_decide rewrite multiplication with power of two to shift (#7029) This PR adds simprocs to bv_decide's preprocessor that rewrite multiplication with powers of two to constant shifts. commit 45e5deb1acfb717caf720cc5359297ffc6c62a97 Author: Sebastian Ullrich <[email protected]> Date: Mon Feb 10 17:44:05 2025 +0100 chore: trivial changes from async-proofs branch (#7028) commit 98e0e308c72ce0168de01bf5838fc44b0f4d6bcb Author: Joachim Breitner <[email protected]> Date: Mon Feb 10 17:43:41 2025 +0100 feat: nested well-founded recursion via automatic preprocessing (#6744) This PR extend the preprocessing of well-founded recursive definitions to bring assumptions like `h✝ : x ∈ xs` into scope automatically. This fixes #5471, and follows (roughly) the design written there. See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean` for details on the implementation. This only works for higher-order functions that have a suitable setup. See for example section “Well-founded recursion preprocessing setup” in `src/Init/Data/List/Attach.lean`. This does not change the `decreasing_tactic`, so in some cases there is still the need for a manual termination proof some cases. We expect a better termination tactic in the near future. commit bb5a71d6d32d970a6323b9ff30e486fc5015429e Author: Lean stage0 autoupdater <> Date: Mon Feb 10 16:30:51 2025 +0000 chore: update stage0 commit dfc1eeb8c2ae15ab8453ad8a6315a0a4048cab7c Author: Markus Himmel <[email protected]> Date: Mon Feb 10 16:27:30 2025 +0100 doc: misc. style guide and naming scheme additions (#7026) This PR clarifies the styling of `do` blocks, and enhanes the naming conventions with information about the `ext` and `mono` name components as well as advice about primed names and naming of simp sets. commit ca73817b5c83ac3e7877c77f6acbef3b926c30b5 Author: Sebastian Ullrich <[email protected]> Date: Mon Feb 10 16:08:02 2025 +0100 fix: codegen was allowed improper env ext accesses (#7023) commit f5d861f4294b6b17713a152572377fdc9049185b Author: Kim Morrison <[email protected]> Date: Tue Feb 11 01:20:18 2025 +1100 chore: rename simp sets (#7017) This PR renames the simp set `boolToPropSimps` to `bool_to_prop` and `bv_toNat` to `bitvec_to_nat`. I'll be adding more similarly named simp sets. commit 6584cb93b237d98fd46ac0fe35ca5fe0a5c37ee4 Author: Kim Morrison <[email protected]> Date: Tue Feb 11 00:49:17 2025 +1100 chore: deprecated compile_time_search_path% (#7022) This PR deprecates `compile_time_search_path%`; it didn't prove useful, and we've shot ourselves in the foot with it more than once. commit b70fb04ba69b1ea14b330bd476ae7a39343b88eb Author: Henrik Böving <[email protected]> Date: Mon Feb 10 14:48:20 2025 +0100 feat: add basic extract theorems for bv_decide (#7021) This PR adds theorems for interactions of extractLsb with `&&&`, `^^^`, `~~~` and `bif` to bv_decide's preprocessor. commit 17ef9f8c6e01491ff92dc9042d54f27177bbc134 Author: Kim Morrison <[email protected]> Date: Mon Feb 10 23:17:44 2025 +1100 feat: improvements to simp confluence (#7013) This PR makes improvements to the simp set for List/Array/Vector/Option to improve confluence, in preparation for `simp_lc`. commit 497946851699b3c128e9ae4fdbbe835f8e5caf33 Author: Henrik Böving <[email protected]> Date: Mon Feb 10 12:24:52 2025 +0100 fix: correct trace nodes in bv_decide (#7019) This PR properly spells out the trace nodes in bv_decide so they are visible with just `trace.Meta.Tactic.bv` and `trace.Meta.Tactic.sat` instead of always having to enable the profiler. commit f2762ac06d3dbbc7d8e3ed62f92f6874c13e62be Author: Lean stage0 autoupdater <> Date: Mon Feb 10 11:58:06 2025 +0000 chore: update stage0 commit ec8eb9a6e9ee5df67521bd181b189f7ebf06088d Author: Sebastian Ullrich <[email protected]> Date: Mon Feb 10 11:56:49 2025 +0100 chore: `Task.get` block profiling (#7016) * `--profile` now reports `blocking` time spent in `Task.get` inside other profiling categories * environment variable `LEAN_TRACE_TASK_GET_BLOCKED` when set makes `lean` dump stack traces of `Task.get` blocks commit 057c72f545c325564734b50ebd3c03f881fe4bc5 Author: Kim Morrison <[email protected]> Date: Mon Feb 10 21:56:20 2025 +1100 chore: rename simp sets (#7018) This is preliminary to #7017; we'll need an update-stage0 before the actual rename can take place. commit 93b622f05869605a47a2a9cefd170f558631a95f Author: Kim Morrison <[email protected]> Date: Mon Feb 10 21:37:21 2025 +1100 chore: replace HashMap.get_ lemmas with getElem_ versions (#7004) This PR replaces various `HashMap.get_X` with `getElem_X` versions. Now the left hand sides are in simp normal form (and this fixes some confluence problems). commit 8b65ab0be4c66508fb93cc0ef32f619d4d097a80 Author: Kim Morrison <[email protected]> Date: Mon Feb 10 21:30:41 2025 +1100 chore: add @[simp] to List.flatten_toArray (#7014) commit db2b9e4663b4a74791e2b724bc6a6a72776ee3db Author: Henrik Böving <[email protected]> Date: Mon Feb 10 11:00:20 2025 +0100 feat: basic support for handling enum inductives in bv_decide (#6946) This PR implements basic support for handling of enum inductives in `bv_decide`. It now supports equality on enum inductive variables (or other uninterpreted atoms) and constants. commit c51d82c8408c056f5e4e9a752906529bd36b71df Author: Leonardo de Moura <[email protected]> Date: Sun Feb 9 22:13:28 2025 -0800 feat: `simp +arith` normalizes coefficient in linear integer polynomials (#7015) This PR makes sure `simp +arith` normalizes coefficients in linear integer polynomials. There is still one todo: tightening the bound of inequalities. commit 59c602fd808c1b00eaf8bfb6d2739de254f3c5dd Author: Kim Morrison <[email protected]> Date: Mon Feb 10 09:54:51 2025 +1100 chore: unprotect List.foldlM (#7003) commit 290e5311f971f2410d734b9694b8ad3fcc8e8c00 Author: Leonardo de Moura <[email protected]> Date: Sun Feb 9 14:46:09 2025 -0800 chore: improve `withAbstractAtoms` (#7012) We should not abstract free variables commit 9769781a083bbb760155863e77ccd9ddd803a143 Author: Leonardo de Moura <[email protected]> Date: Sun Feb 9 13:41:58 2025 -0800 feat: `simp +arith` for integers (#7011) This PR adds `simp +arith` for integers. It uses the new `grind` normalizer for linear integer arithmetic. We still need to implement support for dividing the coefficients by their GCD. It also fixes several bugs in the normalizer. commit dc8073e54f8deee3223fc388490f9ca50c869be9 Author: Leonardo de Moura <[email protected]> Date: Sun Feb 9 09:24:07 2025 -0800 chore: improve `expose_names` doc string (#7010) commit 5b5b52ab88918ad1766787c60319554978e4557c Author: Leonardo de Moura <[email protected]> Date: Sun Feb 9 09:11:28 2025 -0800 feat: `bv_decide` hint (#7009) This PR ensures users get an error message saying which module to import when they try to use `bv_decide`. commit 12b2f731180ccf80c3ed290491dae489ce29bc59 Author: Kim Morrison <[email protected]> Date: Mon Feb 10 03:20:38 2025 +1100 chore: remove unused Int simp lemmas (#7005) commit 940afe624efaf6ffb428fdacee8a4c5f77c01696 Author: Leonardo de Moura <[email protected]> Date: Sat Feb 8 20:32:54 2025 -0800 feat: linear integer arith normalizer (#7002) This PR implements the normalizer for linear integer arithmetic expressions. It is not connect to `simp +arith` yet because of some spurious `[simp]` attributes. commit 00d884c49802fcd338c252c7b70b31c2bd491b68 Author: Leonardo de Moura <[email protected]> Date: Sat Feb 8 15:01:01 2025 -0800 feat: add `Int.Linear` normalization support (#7000) This PR adds helper theorems for justifying the linear integer normalizer. commit 859015f335d2b13acbe50a29deda909c1ea8575b Author: Kyle Miller <[email protected]> Date: Sat Feb 8 10:11:26 2025 -0800 doc: mention `Prop`s are equal to `True` or `False` (#6998) This PR modifies the `Prop` docstring to point out that every proposition is propositionally equal to either `True` or `False`. This will help point users toward seeing that `Prop` is like `Bool`. I considered mentioning `Classical.propComplete`, but it's probably better not making it seem like that's how you should work with propositions. commit 869a2b9cbda726f0b2289d8821d4f18ce2fadbfe Author: Bolton Bailey <[email protected]> Date: Sat Feb 8 07:04:39 2025 -0800 chore: change Lake configuration error message (#6829) This PR changes the error message for Lake configuration failure to reflect that issues do not always arise from an invalid lakefile, but sometimes arise from other issues like network errors. The new error message encompasses all of these possibilities. Closes #6827 commit 2392d4abe443cfd495da2026bbfa044395ddd19e Author: Joachim Breitner <[email protected]> Date: Sat Feb 8 11:32:34 2025 +0100 refactor: elaborate forIn notation without extra let (#6977) This PR avoids a `let` in the elaboration of `forIn`. It was introduced in https://github.com/leanprover/lean4/commit/f51328ff112 but nothing seems to break when I simplify the code. This removes an unexpected `let col✝ :=…` from the “Expected type” view in the Info View and from the termination proofs. commit dea9fcec136c60cba0a58cf4e157ce77e2f6d359 Author: Leonardo de Moura <[email protected]> Date: Fri Feb 7 14:43:30 2025 -0800 feat: `exact?` in `try?` (#6995) This PR implements support for `exact?` in the `try?` tactic. commit a6f14f52e5d4ee7063ee6f318da8df9d506f2ada Author: Leonardo de Moura <[email protected]> Date: Fri Feb 7 11:17:25 2025 -0800 feat: compress `try?` suggestions (#6994) This PR adds the `Try.Config.merge` flag (`true` by default) to the `try?` tactic. When set to `true`, `try?` compresses suggestions such as: ```lean · induction xs, ys using bla.induct · grind only [List.length_reverse] · grind only [bla] ``` into: ```lean induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla] ``` This PR also ensures `try?` does not generate suggestions that mixes `grind` and `grind only`, or `simp` and `simp only` tactics. This PR also adds the `try? +harder` option (previously called `lib`), but it has not been fully implemented yet. commit 20f5666ce2b2d041ebed7d3f805c4ab849619a01 Author: Leonardo de Moura <[email protected]> Date: Fri Feb 7 11:13:50 2025 -0800 chore: disable broken test It is timing out on OSX, and `master` is failing to build. This is a temporary "fix." commit 8ab3a81901b79fcd65c84ccc7923d5ab6cb0d3b4 Author: Sebastian Ullrich <[email protected]> Date: Fri Feb 7 17:50:31 2025 +0100 feat: parallel progress notifications (#6329) This PR enables the language server to present multiple disjoint line ranges as being worked on. Even before parallelism lands, we make use of this feature to show post-elaboration tasks such as kernel checking on the first line of a declaration to distinguish them from the final tactic step.  commit f3d8c6be9d64c13874740a27b334afba18ce6dab Author: Leonardo de Moura <[email protected]> Date: Fri Feb 7 08:33:25 2025 -0800 feat: improve `try?` suggestion (#6991) This PR improves how suggestions for the `<;>` combinator are generated. commit 8c297201e0f806d49fdac48554e911b8a2732c69 Author: Sebastian Ullrich <[email protected]> Date: Fri Feb 7 17:12:31 2025 +0100 chore: re-enable `Elab.async` in the server (#6990) commit 14c4620cd2f83be2f50ec41f597c0d7532b27b73 Author: Sebastian Ullrich <[email protected]> Date: Fri Feb 7 16:55:32 2025 +0100 fix: convert kernel interrupt into elab interrupt (#6988) This PR ensures interrupting the kernel does not lead to wrong, sticky error messages in the editor commit 64794357be33dc4695ffad7896383711e65e0e7a Author: Sebastian Ullrich <[email protected]> Date: Fri Feb 7 16:33:10 2025 +0100 feat: API to avoid deadlocks from dropped promises (#6958) This PR improves the `Promise` API by considering how dropped promises can lead to never-finished tasks. commit 73d7a3f6ae93c667e184f6888348e5828d8e0880 Author: Sebastian Ullrich <[email protected]> Date: Fri Feb 7 11:14:35 2025 +0100 perf: avoid taking mutex on already-resolved promises (#6984) commit 3824513a51e5205849a867da39eb71ee6e9e45cb Author: Sebastian Ullrich <[email protected]> Date: Fri Feb 7 10:06:57 2025 +0100 feat: respect `Task.map/bind (sync := true)` after waiting (#6976) This PR extends the behavior of the `sync` flag for `Task.map/bind` etc. to encompass synchronous execution even when they first have to wait on completion of the first task, drastically lowering the overhead of such tasks. Thus the flag is now equivalent to e.g. .NET's `TaskContinuationOptions.ExecuteSynchronously`. commit 17a5c420b1723f1ba0156480d6b966feb589a9d4 Author: Kim Morrison <[email protected]> Date: Fri Feb 7 15:02:02 2025 +1100 feat: improve monadic Array lemmas (#6982) This PR improves some lemmas about monads and monadic operations on Array/Vector, using @Rob23oa's work in https://github.com/leanprover-community/batteries/pull/1109, and adding/generalizing some additional lemmas. commit dccbb94b0b98cc3df1513498308e0fabd56231f4 Author: Kim Morrison <[email protected]> Date: Fri Feb 7 12:44:51 2025 +1100 chore: linting List (#6970) commit a246933999b5ecc988a1d0035df2a7b78b191039 Author: Leonardo de Moura <[email protected]> Date: Thu Feb 6 17:35:41 2025 -0800 feat: `try?` tactic improvements (#6981) This PR adds new configuration options to `try?`. - `try? -only` omits `simp only` and `grind only` suggestions - `try? +missing` enables partial solutions where some subgoals are "solved" using `sorry`, and must be manually proved by the user. - `try? (max:=<num>)` sets the maximum number of suggestions produced (default is 8). commit 5355badf854ec3dbddd793d97a3c25f43bb1b0c7 Author: Leonardo de Moura <[email protected]> Date: Thu Feb 6 15:59:38 2025 -0800 feat: `try?` validation and cleanup (#6980) This PR improves the `try?` tactic runtime validation and error messages. It also simplifies the implementation, and removes unnecessary code. commit 89f643b8e7a2403d42d2e751f00788c94bf49d7c Author: Sofia Rodrigues <[email protected]> Date: Thu Feb 6 20:24:42 2025 -0300 feat: improve some files separation and standardize error messages in UV modules (#6830) This PR improves some files separation and standardize error messages in UV modules commit 4ac6d0807a437476b45b47ff0e8311a466284283 Author: Leonardo de Moura <[email protected]> Date: Thu Feb 6 13:56:14 2025 -0800 feat: `try?` composite suggestions (#6979) This PR adds support for more complex suggestions in `try?`. Example: ```lean example (as : List α) (a : α) : concat as a = as ++ [a] := by try? ``` suggestion ``` Try this: · induction as, a using concat.induct · rfl · simp_all ``` commit 1d42ab8be66135a7a7511ead28ed64bc5b9bc9e8 Author: Marc Huisinga <[email protected]> Date: Thu Feb 6 20:26:11 2025 +0100 fix: inlay hints in untitled files (#6978) This PR fixes a bug where both the inlay hint change invalidation logic and the inlay hint edit delay logic were broken in untitled files. Thanks to @Julian for spotting this! commit da5d7760ae5cd62541b5721efee67ffa15f887c6 Author: Lean stage0 autoupdater <> Date: Thu Feb 6 17:39:42 2025 +0000 chore: update stage0 commit 65c0674ba2c2d7b0b2296466946f185479cedcf5 Author: Marc Huisinga <[email protected]> Date: Thu Feb 6 17:43:56 2025 +0100 feat: inlay hint refinements (#6959) This PR implements a number of refinements for the auto-implicit inlay hints implemented in #6768. Specifically: - In #6768, there was a bug where the inlay hint edit delay could accumulate on successive edits, which meant that it could sometimes take much longer for inlay hints to show up. This PR implements the basic infrastructure for request cancellation and implements request cancellation for semantic tokens and inlay hints to resolve the issue. With this edit delay bug fixed, it made more sense to increase the edit delay slightly from 2000ms to 3000ms. - In #6768, we applied the edit delay to every single inlay hint request in order to reduce the amount of inlay hint flickering. This meant that the edit delay also had a significant effect on how far inlay hints would lag behind the file progress bar. This PR adjusts the edit delay logic so that it only affects requests sent directly after a corresponding `didChange` notification. Once the edit delay is used up, all further semantic token requests are responded to without delay, so that the only latency that affects how far the inlay hints lag behind the progress bar is how often we emit refresh requests and how long VS Code takes to respond to them. - For inlay hints, refresh requests are now emitted 500ms after a response to an inlay hint request, not 2000ms, which means that after the edit delay, inlay hints should only lag behind the progress bar by about up to 500ms. This is justifiable for inlay hints because the response should be much smaller than e.g. is the case for semantic tokens. - In #6768, 'Restart File' did not prompt a refresh, but it does now. - VS Code does not immediately remove old inlay hints from the document when they are applied. In #6768, this meant that inlay hints would linger around for a bit once applied. To mitigate this issue, this PR adjusts the inlay hint edit delay logic to identify edits sent from the client as being inlay hint applications, and sets the edit delay to 0ms for the inlay hint requests following it. This means that inlay hints are now applied immediately. - In #6768, hovering over single-letter auto-implicit inlay hints was a bit finicky because VS Code uses the regular cursor icon on inlay hints, not the thin text cursor icon, which means that it is easy to put the cursor in the wrong spot. We now add the separation character (` ` or `{`) preceding an auto-implicit to the hover range as well, which makes hovering over inlay hints much smoother. commit acb971a81a5f0f509253dfeaced92df7de0e1ed9 Author: Lean stage0 autoupdater <> Date: Thu Feb 6 12:27:11 2025 +0000 chore: update stage0 commit db885bb7fb8196ef56d8014b44c65db5321016e0 Author: Joachim Breitner <[email protected]> Date: Thu Feb 6 12:28:23 2025 +0100 refactor: rename auto_attach attribute to wf_preprocess (#6972) As per dicussion with team colleages, the feature shouldn’t be called “auto attach” but rather “well-founded recursion preprocessing” to avoid (imprecise) jargon. commit ad7371de69868b161a1b3befa46715f694db1785 Author: Henrik Böving <[email protected]> Date: Thu Feb 6 12:16:57 2025 +0100 refactor: bv_decide's type analysis to prepare for enum support (#6971) This PR does some refactoring on bv_decide's type analysis in preparation for enum support in #6946. commit 32a22d81e9ef675f411792d560ba9419466f90dc Author: Joachim Breitner <[email protected]> Date: Thu Feb 6 12:03:27 2025 +0100 feat: binderNameHint (#6947) This PR adds the `binderNameHint` gadget. It can be used in rewrite and simp rules to preserve a user-provided name where possible. The expression `binderNameHint v binder e` defined to be `e`. If it is used on the right-hand side of an equation that is applied by a tactic like `rw` or `simp`, and `v` is a local variable, and `binder` is an expression that (after beta-reduction) is a binder (so `fun w => …` or `∀ w, …`), then it will rename `v` to the name used in the binder, and remove the `binderNameHint`. A typical use of this gadget would be as follows; the gadget ensures that after rewriting, the local variable is still `name`, and not `x`: ``` theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by rw [all_eq_not_any_not] -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true ``` This gadget is supported by `simp`, `dsimp` and `rw` in the right-hand-side of an equation, but not in hypotheses or by other tactics. commit 9e9b29f5f3f23e7514d934a68211388a2505023f Author: Kim Morrison <[email protected]> Date: Thu Feb 6 21:20:17 2025 +1100 chore: rename Nat.not_eq_zero_of_lt (#6968) Renames a lemma. Closes #6714 commit c5bc29568fd6cf14f58bf2725d2a34513fcd0bd1 Author: Markus Himmel <[email protected]> Date: Thu Feb 6 09:33:48 2025 +0100 doc: style guide and naming convention for the standard library (#6950) This PR adds a style guide and a naming convention for the standard library. commit 1f905640257a28f33b118930af0cd52d633eab15 Author: Lean stage0 autoupdater <> Date: Thu Feb 6 08:27:23 2025 +0000 chore: update stage0 commit 9bcb48157fadc661ae51677128688112fb4d1490 Author: Leonardo de Moura <[email protected]> Date: Wed Feb 5 21:44:25 2025 -0800 feat: use `expose_names` in `try?` (#6967) This PR ensures `try?` can suggest tactics that need to reference inaccessible local names. Example: ```lean /-- info: Try these: • · expose_names; induction as, bs_1 using app.induct <;> grind [= app] • · expose_names; induction as, bs_1 using app.induct <;> grind only [app] -/ #guard_msgs (info) in example : app (app as bs) cs = app as (app bs cs) := by have bs := 20 -- shadows `bs` in the target try? ``` commit f458b99779c0e5e45c31a312426d016f271ceea1 Author: Kim Morrison <[email protected]> Date: Thu Feb 6 15:49:21 2025 +1100 feat: add internal linter for List/Array/Vector variable names (#6966) This PR adds an internal-use-only strict linter for the variable names of `List`/`Array`/`Vector` variables, and begins cleaning up. commit fa5ac2ec5bfea3d2bd8bfedf6a7c3a2cb97562c9 Author: Leonardo de Moura <[email protected]> Date: Wed Feb 5 20:47:26 2025 -0800 feat: implement `try?` using `evalAndSuggest` (#6965) This PR re-implements the `try?` tactic using the new `evalAndSuggest` infrastructure. commit b62b9d4ce6e1a630ae9d365c18f2fae99e024673 Author: Kim Morrison <[email protected]> Date: Thu Feb 6 14:11:53 2025 +1100 feat: `#info_trees in` command (#6964) This PR adds a convenience command `#info_trees in`, which prints the info trees generated by the following command. It is useful for debugging or learning about `InfoTree`. commit 00dc96ef6163f26ef281b73d5463b9138b0e9e4a Author: Kim Morrison <[email protected]> Date: Thu Feb 6 13:39:06 2025 +1100 chore: further cleanup of index variable naming in List (#6963) commit 6c0d0ef74ab86167d731b828b1c5878c4ff7576c Author: Kim Morrison <[email protected]> Date: Thu Feb 6 12:56:47 2025 +1100 doc: improve List.toArray doc-string (#6962) This PR improves the doc-string for `List.toArray`. Thanks to @jt0202 for pointing this out. commit 8ade4a54e533202224023ce2ea179a44458ba348 Author: Leonardo de Moura <[email protected]> Date: Wed Feb 5 14:13:47 2025 -0800 feat: `evalAndSuggest` helper tactic (#6961) This PR adds the auxiliary tactic `evalAndSuggest`. It will be used to refactor `try?`. commit f0b956830df0732fa45036a7c03fae33854ffa6c Author: Lean stage0 autoupdater <> Date: Wed Feb 5 16:42:25 2025 +0000 chore: update stage0 commit dc9806e9d569432651f17114463ba582ea39f213 Author: jrr6 <[email protected]> Date: Wed Feb 5 10:43:54 2025 -0500 feat: allow updating binders to and from strict- and instance-implicit (#6634) This PR adds support for changing the binder annotations of existing variables to and from strict-implicit and instance-implicit using the `variable` command. This PR requires a stage0 update to fully take effect. Closes #6078 commit c7ee39543fb63fe22bf9e1a6f47f4780e650ef54 Author: Lean stage0 autoupdater <> Date: Wed Feb 5 14:42:28 2025 +0000 chore: update stage0 commit 973a745bc0209410868d88b00521343725fab4e3 Author: Joachim Breitner <[email protected]> Date: Wed Feb 5 14:33:35 2025 +0100 feat: add `auto_attach` simp set (no functionality yet) (#6956) this PR helps with bootstrapping #6744. commit f65dc78c4f6aca25f142ede951ac5f76866c8eb3 Author: Tobias Grosser <[email protected]> Date: Sun Feb 16 11:45:30 2025 +0000 Update src/Init/Data/BitVec/Lemmas.lean commit d7d39848d91720c5bf1a9ec957cb017c087e229b Author: Tobias Grosser <[email protected]> Date: Sun Feb 16 11:44:51 2025 +0000 Update src/Init/Data/BitVec/Lemmas.lean commit 94a68d45584ffd70b6154012732564df083adfaa Author: luisacicolini <[email protected]> Date: Tue Feb 11 08:41:18 2025 +0000 chore: smul correct def commit 87b1a873ae804c96995dc201debdb655749616f2 Author: luisacicolini <[email protected]> Date: Mon Feb 10 10:36:13 2025 +0000 chore: simplify mul_le_mul_self commit 24e9bc92578c91ae9cb66754d27381671139757a Author: luisacicolini <[email protected]> Date: Mon Feb 10 09:31:36 2025 +0000 chore: fix theorem name commit 67d5900e5445ef8de1e608771ed4d0860d90d652 Author: luisacicolini <[email protected]> Date: Mon Feb 10 09:30:51 2025 +0000 chore: fix theorem name commit 155971c6072ff8fd1f8cd87160446ea784cfa0c9 Author: Siddharth Bhat <[email protected]> Date: Thu Feb 6 14:36:55 2025 +0000 chore: shorter proof of toInt_one_of_lt commit 89a87da466e1890dcb88d73b9293ab197677f04c Author: luisacicolini <[email protected]> Date: Thu Feb 6 14:08:28 2025 +0000 chore: undo unwanted change commit fcce13fc5da7e39ac4cbf82d34809f72686d2f09 Author: luisacicolini <[email protected]> Date: Thu Feb 6 13:56:26 2025 +0000 chore: more cleaning commit 1ebc9b43a406f4291bc42ecf5dfa7aedbc076419 Author: luisacicolini <[email protected]> Date: Thu Feb 6 11:45:02 2025 +0000 chore: undo unwanted change commit 199f7cc993bb7c3c64b8fe7de2436c442b28ccf0 Author: luisacicolini <[email protected]> Date: Thu Feb 6 11:44:51 2025 +0000 chore: undo unwanted change commit cc7128ffeee09b84a68dd990308da79dcd482a81 Author: luisacicolini <[email protected]> Date: Thu Feb 6 11:44:36 2025 +0000 chore: undo unwanted change commit 7509cb60d4929db13ffcd0dd824291c8709b6936 Author: luisacicolini <[email protected]> Date: Thu Feb 6 11:44:04 2025 +0000 chore: undo unwanted change commit a9527249b93d6a246f789fbcd21667a239a67151 Author: luisacicolini <[email protected]> Date: Thu Feb 6 11:43:23 2025 +0000 chore: bring the theorems back home commit 6f7469b430f88b9425c05f3554030101d062cf2c Author: luisacicolini <[email protected]> Date: Wed Feb 5 18:52:05 2025 +0000 chore: clean proof commit dee6fa2f91daa36a7eda1b1290f8a9fa0665aa92 Author: Tobias Grosser <[email protected]> Date: Wed Feb 5 16:52:06 2025 +0000 drop sorries commit 741107e68ed8e325b14f806b6b88384380395dab Author: luisacicolini <[email protected]> Date: Wed Feb 5 14:36:48 2025 +0000 chore: giving up commit 43b174e0be48259b36202daf14e572a8a346955d Author: luisacicolini <[email protected]> Date: Wed Feb 5 12:42:46 2025 +0000 chore: fix build commit 5786b41d55f8a0f3ab19b8aa53fbed20a127f127 Author: luisacicolini <[email protected]> Date: Wed Feb 5 11:38:34 2025 +0000 chore: reorder theorems commit f7d800aada32f68fd97948e731afc37fb904ce63 Merge: 540349d567 53ed233f38 Author: Luisa Cicolini <[email protected]> Date: Wed Feb 5 11:37:59 2025 +0000 Merge branch 'master' into overflow-mul-defs commit 540349d567e58395b918b0aa65ca39d126d8ce42 Author: luisacicolini <[email protected]> Date: Tue Feb 4 12:25:02 2025 +0000 chore: useless newline commit a2695ab452057661bcdbc0fd6ab4f64cdd43e5ed Author: luisacicolini <[email protected]> Date: Tue Feb 4 12:08:59 2025 +0000 chore: first cleaning pass
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR removes the
saveandcheckpointtactics that have been superseded by incremental elaboration