This PR fixes an issue introduced bug #6125 where an `inductive` or
`structure` with an autoimplicit parameter with a type that has a
metavariable would lead to a panic. Closes#7788.
This was due to switching from `Term.addAutoBoundImplicits'` to
`Term.addAutoBoundImplicits` and not properly handling metavariables in
the parameters list. To fix this, now the inductive type headers record
the abstracted type and the number of parameters, rather than record the
parameters, the type, the local context, and the local instances. A
benefit to this over `Term.addAutoBoundImplicits'` is that the type's
parameters do not appear twice in the local context.
This PR fixes two bugs in `grind`.
1. Model-based theory combination was creating type incorrect terms.
2. `Nat.cast` vs `NatCast.natCast` issue during normalization.
This PR fixes an issue where `let n : Nat := sorry` in the Infoview
pretty prints as ``n : ℕ := sorry `«Foo:17:17»``. This was caused by
top-level expressions being pretty printed with the same rules as
Infoview hovers. Closes#6715. Refactors `Lean.Widget.ppExprTagged`; now
it takes a delaborator, and downstream users should configure their own
pretty printer option overrides if necessary if they used the `explicit`
argument (see `Lean.Widget.makePopup.ppExprForPopup` for an example).
Breaking change: `ppExprTagged` does not set `pp.proofs` on the root
expression.
This PR cleans up the `Option` development, upstreaming some results
from mathlib in the process.
Notable changes:
- the name `<op>_eq_some_iff` is preferred over `<op>_eq_some`
- the `simp` normal form for `<$>` is `Option.map`, for `>>=` is
`Option.bind` and for `<|>` is `Option.orElse` (for the former two, this
was already true before this PR). All further lemmas about these
operations are now stated only in terms of
`Option.map`/`Option.bind`/`Option.orElse`. Previously, in some cases
both versions were available, with a prime used to disambiguate (the
primed version was usually the "non-ascii-art" version). Now, there are
no lemmas about the ascii-art versions besides the ones turning them
into the non-ascii-art operations, and there is only one version of
every lemma, about the non-ascii-art operation, and named without a
prime.
This PR fixes a regression where elaboration of a previous document
version is not cancelled on changes to the document.
Done by removing the default from `SnapshotTask.cancelTk?` and
consistently passing the current thread's token for synchronous
elaboration steps.
This PR adds a mixin typeclass for `Lean.Grind.CommRing` recording the
characteristic of the ring, and constructs instances for `Int`, `IntX`,
`UIntX`, and `BitVec`.
This PR fixes a number of bugs related to the handling of the source
search path in the language server, where deleting files could cause
several features to stop functioning and both untitled files and files
that don't exist on disc could have conflicting module names.
In detail, it makes the following adjustments:
- The URI <-> module name conversion was adjusted to produce no name
collisions.
- File URIs in the search path yield a module name relative to the
search path, as before.
- File URIs not in the search path, non-file URIs and non-`.lean` files
yield a `«external:<full uri>»` module name.
- To avoid the issue of the URI -> module name conversion failing when a
file is deleted from disc, we now cache the result of this conversion in
the watchdog and the file worker when the file is first opened.
- All of the URI <-> module name conversions now consistently go through
`Server.documentUriFromModule?` and `moduleFromDocumentUri` to ensure
that we don't have minor deviations for this conversion all over the
place.
- The threading of the source search path through the file worker (from
`lake setup-file`) is removed. It turns out that `lake serve` already
sets the correct source search path in the environment, so we can just
always use the search path from the environment.
- Since we can now answer more requests that need the .ileans in
untitled files, a lot of the tests that test 'Go to definition' needed
to be adjusted so that they use the information from the watchdog, not
the file worker. As we load references asynchronously, this PR adds an
internal `$/lean/waitForILeans` request that tests can use to wait for
all .ilean files to be loaded and for the ilean references from the file
worker for the current document version to be finalized.
- As part of this PR, we noticed that the .ileans aren't available in
the NixOS setup, so @Kha adjusted the Nix CI to fix this.
### Breaking changes
- `Server.documentUriFromModule` has been renamed to
`Server.documentUriFromModule?` and doesn't take a `SearchPath` argument
anymore, as the `SearchPath` is now computed from the `LEAN_SRC_PATH`
environment variable. It has also been moved from `Lean.Server.GoTo` to
`Lean.Server.Utils`.
- `Server.moduleFromDocumentUri` does not take a `SearchPath` argument
anymore and won't return an `Option` anymore. It has also been moved
from `Lean.Server.GoTo` to `Lean.Server.Utils`.
- The `System.SearchPath.searchModuleNameOfUri` function has been
removed. It is recommended to use `Server.moduleFromDocumentUri`
instead.
- The `initSrcSearchPath` function has been renamed to
`getSrcSearchPath` and has been moved from `Lean.Util.Paths` to
`Lean.Util.Path`. It also doesn't need to take a `pkgSearchPath`
argument anymore.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR eliminates another source of facts of the form `-1 *
NatCast.natCast x <= 0` for each `x : Nat` in the local context. These
facts are now stored internally in the cutsat state.
cc @kim-em
This PR improves the normalization of `Bool` terms in `grind`. Recall
that `grind` currently does not case split on Boolean terms to reduce
the size of the search space.
This PR updates `rw?`, `show_term`, and other tactic-suggesting tactics
to suggest `expose_names` when necessary and validate tactics prior to
suggesting them, as `exact?` already did, and it also ensures all such
tactics produce hover info in the messages showing tactic suggestions.
This introduces a breaking change in the `TryThis` API: the `type?`
parameter of `addRewriteSuggestion` is now an `LOption`, not an
`Option`, to obviate the need for a hack we previously used to indicate
that a rewrite closed the goal.
Closes#7350
This PR fixes an issue where uses of 'noncomputable' definitions can get
incorrectly compiled, while also removing the use of 'noncomputable'
definitions altogether. Some uses of 'noncomputable' definitions (e.g.
Classical.propDecidable) do not get compiled correctly by type erasure.
Running the optimizer on the result can lead to them being optimized
away, eluding the later IR-level check for uses of noncomputable
definitions.
To fix this, we add a 'noncomputable' check earlier in the
erase_irrelevant pass.
This PR adds extensibility to the `evalAndSuggest` procedure used to
implement `try?`. Users can now implement their own handlers for any
tactic. The new test demonstrates how this feature works.
This PR fixes an issue in the cutsat counterexamples. It removes the
optimization (`Cutsat.State.terms`) that was used to avoid the new
theorem `eq_def`. In the two new tests, prior to this PR, `cutsat`
produced a bogus counterexample with `b := 2`.
This PR prevents redundant invocations to `markAsCutsatTerm` which would
trigger equalities of the form `x = x` being propagated. This redundancy
only affected performance and "polluted" trace messages with redundant
information.
This PR changes Lake to use normalized absolute paths for its various
files and directories.
This is done by storing absolute paths for the workspace directory,
package directories, and configuration files. These are then joined to
relative paths (e.g., for source directories) using a custom join
function that eliminates `.` paths.
Closes#7498. Closes#4042.
This PR improves support for `Nat` in the `cutsat` procedure used in
`grind`:
- `cutsat` no longer *pollutes* the local context with facts of the form
`-1 * NatCast.natCast x <= 0` for each `x : Nat`. These facts are now
stored internally in the `cutsat` state.
- A single context is now used for all `Nat` terms.
The PR also introduces a mapping mechanism for all "foreign" types that
can be converted to `Int`. Currently, only `Nat` is supported, but
additional types will be added in the future.
This PR fixes an issue where `x.f.g` wouldn't work but `(x.f).g` would
when `x.f` is generalized field notation. The problem was that `x.f.g`
would assume `x : T` should be the first explicit argument to `T.f`. Now
it uses consistent argument insertion rules. Closes#6400.
This also improves the algorithm for finding a relevant argument. Before
it would try looking at the type and the whnf of the type, but now it
iteratively unfolds types, checking each intermediate expansion.
This PR modifies the pretty printing of pi types. Now `∀` will be
preferred over `→` for propositions if the domain is not a proposition.
For example, `∀ (n : Nat), True` pretty prints as `∀ (n : Nat), True`
rather than as `Nat → True`. There is also now an option `pp.foralls`
(default true) that when false disables using `∀` at all, for
pedagogical purposes. This PR also adjusts instance implicit binder
pretty printing — nondependent pi types won't show the instance binder
name. Closes#1834.
The linked RFC also suggests using `_` for binder names in case of
non-dependance. We're tabling that idea. Potentially it is useful for
hygienic names; this could improve how `Nat → True` pretty prints as `∀
(a : Nat), True`, with this `a` that's chosen by implication notation
elaboration. Relatedly, this PR exposes even further the issue where
binder names are reused in a confusing way. Consider: `Nat → Nat → (a :
Nat) → a = a` pretty prints as `∀ (a a a : Nat), a = a`.
This PR modifies the pretty printing of raw natural number literals; now
both `pp.explicit` and `pp.natLit` enable the `nat_lit` prefix. An
effect of this is that the hover on such a literal in the Infoview has
the `nat_lit` prefix.
Amendment to RFC #3021: In the reference-level explanation, now it
should read
> When `pp.natLit` and `pp.explicit` are false, then the `nat_lit n`
expression delaborates as `n`, and otherwise it delaborates as `nat_lit
n`.
This PR adds SMT-LIB operators to detect overflow
`BitVec.(umul_overflow, smul_overflow)`, according to the definitions
[here](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2),
and the theorems proving equivalence of such definitions with the
`BitVec` library functions (`umulOverflow_eq`, `smulOverflow_eq`).
Support theorems for these proofs are `BitVec.toInt_one_of_lt,
BitVec.toInt_mul_toInt_lt, BitVec.le_toInt_mul_toInt,
BitVec.toNat_mul_toNat_lt, BitVec.two_pow_le_toInt_mul_toInt_iff,
BitVec.toInt_mul_toInt_lt_neg_two_pow_iff` and `Int.neg_mul_le_mul,
Int.bmod_eq_self_of_le_mul_two, Int.mul_le_mul_of_natAbs_le,
Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonpos, Int.pow_lt_pow`. The PR
also includes a set of tests.
Co-authored by @tobiasgrosser.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR adds a shared mutex (or read-write lock) as `Std.SharedMutex`.
In order to easily migrate a `Std.Mutex` to `Std.SharedMutex` if
necessary, the functions for obtaining exclusive access are named the
same, allowing a correct drop in to be done by just swapping types.
Links to the language reference include a version slug, either `latest`
or `v4.X.0`. These are included in hovers, which then get tested. To
avoid test breakages, in the testing framework we normalize all such URL
prefixes back to `REFERENCE`.
This PR adds a new propagation rule for `Bool` disequalities to `grind`.
It now propagates `x = true` (`x = false`) from the disequality `x =
false` (`x = true`). It ensures we don't have to perform case analysis
on `x` to learn this fact. See tests.
This PR adds missing propagation rules for `LawfulBEq A` to `grind`.
They are needed in a context where the instance `DecidableEq A` is not
available. See new test.
