draft: range migration test run #8841
Draft
Conversation
This file contains hidden or 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
This PR makes `unsafeBaseIO` `noinline`. The new compiler is better at optimizing `Result`-like types, which can cause the final operation in an `unsafeBaseIO` block to be dropped, since `unsafeBaseIO` is discarding the state.
This PR implements support for inequalities in the `grind` linear
arithmetic procedure and simplifies its design. Some examples that can
already be solved:
```lean
open Lean.Grind
example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c d : α)
: a + d < c → b = a + (2:Int)*d → b - d > c → False := by
grind
example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
: a = 0 → b = 1 → a + b ≤ 2 := by
grind
example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c d e : α) :
2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0
→ a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0
→ a + b + 3*c + d + 2*e < 0 → False := by
grind
```
The original annotations produced patterns that matched too often.
This PR turns off the default warning when using `grind`, in preparation for v4.22. I'll removing all the `set_option grind.warning false` in our codebase in a second PR, after an update-stage0.
This PR cleans up some notes about `grind` failures in the LRAT checker, now that some `grind` bugs have been fixed.
This PR enhances the PR release workflow to create both short format and
SHA-suffixed release tags. Creates both pr-release-{PR_NUMBER} and
pr-release-{PR_NUMBER}-{SHORT_SHA} tags, generates separate releases for
both formats, adds separate GitHub status checks, and updates
Batteries/Mathlib testing branches to use SHA-suffixed tags for exact
commit traceability.
This removes the need for downstream repositories to deal with the
toolchain changing without the toolchain name changing.
This PR enables auto-implicits in the Lake math template. This resolves an issue where new users sometimes set up a new project for math formalization and then quickly realize that none of the code samples in our official books and docs that use auto-implicits work in their projects. With the introduction of [inlay hints for auto-implicits](#6768), we consider the auto-implicit UX to be sufficiently usable that they can be enabled by default in the math template. Notably, this change does not affect Mathlib itself, which will proceed to disable auto-implicits. This change was previously discussed with and agreed to by the Mathlib maintainer team.
The details of `identWithPartialTrailingDot` prevent a robust approach using quotations.
This PR bumps the version number of the Lean project to 4.22.0, since v4.21.0 is now in the release candidate stage.
This PR adds an equivalence relation to tree maps akin to the existing one for hash maps. In order to get many congruence lemmas to eventually use for defining functions on extensional tree maps, almost all of the remaining tree map functions have also been given lemmas to relate them to list functions, although these aren't currently used to prove lemmas other than congruence lemmas.
…#8708) This PR fixes an internalization bug in the interface between linarith and ring modules in `grind`. The `CommRing` module may create new terms during normalization.
This PR handles constants with erased types in `toMonoType`. It is much harder to write a test case for this than you would think, because most references to such types get replaced with `lcErased` earlier.
It would accidentally fall back to stage 1 otherwise
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
This PR improves the release checklist and scripts: * Check that the release's commit hash is not all-numeric starting with 0 (this can break SemVer, which [required us to release v4.21.0-rc2](https://github.com/leanprover/lean4/releases/tag/v4.21.0-rc2)). * Check that projects being bumped to a release tag do not reference `nightly-testing` anymore. * Clarify how to create subsequent release candidates if an `-rc1` already exists. * Fix typos in the release checklist documentation.
This PR pins the precise hash of softprops/action-gh-release to
softprops/action-gh-release@da05d55
because the latest version is broken.
See softprops/action-gh-release#628 for more
details.
This PR optimizes let decls of an erased type to an erased value. Specialization can create local functions that produce a Prop, and there's no point in keeping them around.
…8715) This PR implements the basic infrastructure for processing disequalities in the `grind linarith` module. We still have to implement backtracking.
This PR removes the now unnecessary `set_option grind.warning false` statements, now that the warning is disabled by default.
This PR uses the fvar substitution mechanism to replace erased code. This isn't entirely satisfactory, since LCNF's `.return` doesn't support a general `Arg` (which has a `.erased` constructor), it only supports an `FVarId`. This is in contrast to the IR `.ret`, which does support a general `Arg`.
This PR makes the LHS of `isSome_finIdxOf?` and `isNone_finIdxOf?` more general.
…ccidentally more general (#8703) This PR corrects the `IteratorLoop` instance in `DropWhile`, which previously triggered for arbitrary iterator types.
This PR adds server-side support for a new module hierarchy component in VS Code that can be used to navigate both the import tree of a module and the imported-by tree of a module. Specifically, it implements new requests `$/lean/prepareModuleHierarchy`, `$/lean/moduleHierarchy/imports` and `$/lean/moduleHierarchy/importedBy`. These requests are not supported by standard LSP. Companion PR at [leanprover/vscode-lean4#620](leanprover/vscode-lean4#620).   ### Breaking changes This PR augments the .ilean format with the direct imports of a file in order to implement the `$/lean/moduleHierarchy/importedBy` request and bumps the .ilean format version.
065901b to
70e4029
Compare
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.
The branch on which I try migrating the old ranges to the new ones.