Add helper function for computing the number of allocated
sub-expressions in a given expression. Note: Use this function primarily
for diagnosing performance issues.
This adds support for mutual structural recursive functions.
For now this is opt-in: The functions must have a `termination_by
structural …` annotation (new since #4542) for this to work:
```lean
mutual
inductive A
| self : A → A
| other : B → A
| empty
inductive B
| self : B → B
| other : A → B
| empty
end
mutual
def A.size : A → Nat
| .self a => a.size + 1
| .other b => b.size + 1
| .empty => 0
termination_by structural x => x
def B.size : B → Nat
| .self b => b.size + 1
| .other a => a.size + 1
| .empty => 0
termination_by structural x => x
end
```
The recursive functions don’t have to be in a one-to-one relation to a
set of mutually recursive inductive data types. It is possible to ignore
some of the types:
```lean
def A.self_size : A → Nat
| .self a => a.self_size + 1
| .other _ => 0
| .empty => 0
termination_by structural x => x
```
or have more than one function per argument type:
```lean
def isEven : Nat → Prop
| 0 => True
| n+1 => ¬ isOdd n
termination_by structural x => x
def isOdd : Nat → Prop
| 0 => False
| n+1 => ¬ isEven n
termination_by structural x => x
```
This does not include
* Support for nested inductive data types or nested recursion
* Inferring mutual structural recursion in the absence of
`termination_by`.
* Functional induction principles for these.
* Mutually recursive functions that live in different universes. This
may be possible,
maybe after beefing up the `.below` and `.brecOn` functions; we can look
into this some
other time, maybe when there are concrete use cases.
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Summary:
- Adds configuration option `exponentiation.threshold`
- An expression `b^n` where `b` and `n` are literals is not reduced by
`whnf`, `simp`, and `isDefEq` if `n > exponentiation.threshold`.
Motivation: prevents system from becoming irresponsive and/or crashing
without memory.
TODO: improve support in the kernel. It is using a hard-coded limit for
now.
Before, `pp.instantiateMVars` generally had no effect because most call
sites for the pretty printer instantiated metavariables first, but now
this functionality is entrusted upon the `pp.instantiateMVars` option.
This also has an effect in hovers, where metavariables can be unfolded
one assignment at a time. However, the goal state still sees all
metavariables instantiated due to the fact that the algorithm relies on
expression equality post-instantiation (see
`Lean.Widget.goalToInteractive`).
Closes#4406
The linters in Batteries can be used to spot mistakes in Lean. See the
message on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Go-to-def.20on.20typeclass.20fields.20and.20type-dependent.20notation/near/442613564).
These are the different linters with errors:
- unusedArguments:
There are many unused instance arguments, especially a redundant `[Monad
m]` is very common
- checkUnivs:
There was a problem with universes in a definition in
`Init.Control.StateCps`. I fixed it by adding a `variable` statement for
the implicit arguments in the file.
- defLemma:
many proofs are written as `def` instead of `theorem`, most notably
`rfl`. Because `rfl` is used as a match pattern, it must be a def. Is
this desirable?
The keyword `abbrev` is sometimes used for an alias of a theorem, which
also results in a def. I would want to replace it with the `alias`
keyword to fix this, but it isn't available.
- dupNamespace:
I fixed some of these, but left `Tactic.Tactic` and `Parser.Parser` as
they are as these seem intended.
- unusedHaveSuffices:
I cleaned up a few proofs with unused `have` or `suffices`
- explicitVarsOfIff:
I didn't fix any of these, because that would be a breaking change.
- simpNF:
I didn't fix any of these, because I think that requires knowing the
intended simplification order.
The modules `CollectMVars` and `FindMVars` only search for expression
metavariables and not level metavariables, so we should use
`Expr.hasExprMVar` instead of `Expr.hasMVar`.
luckily the necessary functionality already exists in the form of
`addPPExplicitToExposeDiff`. But it is not cheap, and we should not run
this code
when the error message isn’t shown, so we should do this lazily.
We already had `MessageData.ofPPFormat` to assemble the error message
lazily, but it
was restricted to returning `FormatWithInfo`, a data type that doesn’t
admit a nice
API to compose more complex messages (like `Format` or `MessageData`
has; an attempt to
fix that is in #3926).
Therefore we split the functionality of `.ofPPFormat` into
`.ofFormatWithInfo` and `.ofLazy`,
and use `.ofLazy` to compute the more complex error message of `apply`.
Fixes#3232.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
This reverts commit 706a4cfd73 introduced
in #3970
As explained in #4124, `findM?` can become a footgun if used in monads
which induce side-effects such as caching. This PR removes that
function, and fixes the code introduced by #3398 for which the function
was first added.
cc @semorrison.
Adds `ppLevel` to the `PPFns` extension so that the coercion can pass
the pretty printing context (including the `pp.mvars` option setting) to
the `Level` formatter.
Adds the ability to show a diff when `guard_msgs` fails, using the
histogram diff algorithm pioneered in jgit. This algorithm tends to
produce more user-friendly diffs, but it can be quadratic in the worst
case. Empirically, the quadratic case of this implementation doesn't
seem to be slow enough to matter for messages smaller than hundreds of
megabytes, but if it's ever a problem, we can mitigate it the same way
jgit does by falling back to Myers diff.
See lean/run/guard_msgs.lean in the tests directory for some examples of
its output.
Reusing the best profiling UI out there
Usage:
```
lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json foo.lean ...
```
then open `profile.json` in https://profiler.firefox.com/.
See also `script/collideProfiles.lean` for minimizing and merging
profiles.
This is still a draft PR, but includes the core exact? and apply?
tactics.
Still need to convert to builtin syntax and test on Std.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
Before this commit, `Simproc`s were defined as `Expr -> SimpM (Option Step)`, where `Step` is inductively defined as follows:
```
inductive Step where
| visit : Result → Step
| done : Result → Step
```
Here, `Result` is a structure containing the resulting expression and a proof demonstrating its equality to the input. Notably, the proof is optional; in its absence, `simp` assumes reflexivity.
A simproc can:
- Fail by returning `none`, indicating its inapplicability. In this case, the next suitable simproc is attempted, along with other simp extensions.
- Succeed and invoke further simplifications using the `.visit`
constructor. This action returns control to the beginning of the
simplification loop.
- Succeed and indicate that the result should not undergo further
simplifications. However, I find the current approach unsatisfactory, as it does not align with the methodology employed in `Transform.lean`, where we have the type:
```
inductive TransformStep where
/-- Return expression without visiting any subexpressions. -/
| done (e : Expr)
/--
Visit expression (which should be different from current expression) instead.
The new expression `e` is passed to `pre` again.
-/
| visit (e : Expr)
/--
Continue transformation with the given expression (defaults to current expression).
For `pre`, this means visiting the children of the expression.
For `post`, this is equivalent to returning `done`. -/
| continue (e? : Option Expr := none)
```
This type makes it clearer what is going on. The new `Simp.Step` type is similar but use `Result` instead of `Expr` because we need a proof.
This introduces `FilePath.addExtension` to take a path that we know has
no prior extension, and append a new extension to it.
As this function is simpler than `FilePath.withExtension`, this change
eagerly replaces uses of the latter with the former, except in a few
cases where stripping the extension really is the right thing to do.
This should fix the bug described at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Import.20file.20with.20multiple.20dots.20in.20file.20name/near/404508048,
where `import «A.B».«C.D.lean»` is needed to import `A.B/C.D.lean`.
Closes#2999
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This adds a `test_extern` command.
Usage:
```
import Lean.Util.TestExtern
test_extern Nat.add 17 37
```
This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.
Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.
This PR adds per-package server options to resolve#2455. It is based on
the previous work in #2456, but takes a different approach: options are
loaded for the specific file in the file worker when `print-paths` is
called, instead of loading them in the watchdog with a separate Lake
command. This change addresses review comments made in #2456.
In doing so, it introduces two new Lake config fields:
- `leanOptions`: `-D` flag options that are passed to both the language
server and `lean` when building.
- `moreServerOptions`: `-D` flag options that are passed to the language
server.
Since `print-paths` must also accept a file path to compute the options
for that file, this PR is changing the API for `print-paths`. As there
have been numerous complaints about the name `print-paths`, I also
decided to change it to `setup-file` in this PR, since it would break
compatibility with the old Lake API anyways.
This PR deprecates the Lakefile field `moreServerArgs` in favor of
`moreGlobalServerArgs`, as suggested in the review for #2456.
Fixes#2455
---------
Co-authored-by: digama0 <mcarneir@andrew.cmu.edu>
This PR adds basic auto-completion support for imports. Since it still
lacks Lake support for accurate completion suggestions (cc @tydeu - we
already know what needs to be done), it falls back to traversing the
`LEAN_SRC_PATH` for available imports.
Three kinds of import completion requests are supported:
- Completion of the full `import` command. Triggered when requesting
completions in an empty space within the header.
- Known issue: It is possible to trigger this completion within a
comment in the header. Fixing this would require architecture for
parsing some kind of sub-syntax between individual commands.
- Completion of the full module name after an incomplete `import`
command.
- Completion of a partial module name with a trailing dot.
Since the set of imports is potentially expensive to compute, they are
cached for 10 seconds after the last import auto-completion request.
Closes#2655.
### Changes
This PR also makes the following changes:
- To support completions on the trailing dot, the `import` syntax was
adjusted to provide partial syntax when a trailing dot is used.
- `FileWorker.lean` was refactored lightly with some larger definitions
being broken apart.
- The `WorkerState` gained two new fields:
- `currHeaderStx` tracks the current header syntax, as opposed to
tracking only the initial header syntax in `initHeaderStx`. When the
header syntax changes, a task is launched that restarts the file worker
after a certain delay to avoid constant restarts while editing the
header. During this time period, we may still want to serve import
auto-completion requests, so we need to know the up-to-date header
syntax.
- `importCachingTask?` contains a task that computes the set of
available imports.
- `determineLakePath` has moved to a new file `Lean/Util/LakePath.lean`
as it is now needed both in `ImportCompletion.lean` and
`FileWorker.lean`.
- `forEachModuleIn` from `Lake/Config/Blob.lean` has moved to
`Lean/Util/Path.lean` as it is a generally useful utility function that
was useful for traversing the `LEAN_SRC_PATH` as well.
### Tests
Unfortunately, this PR lacks tests since the set of imports available in
`tests/lean/interactive` will not be stable. In the future, I will add
support for testing LSP requests in full project setups, which is when
tests for import auto-completion will be added as well.
