TODO:
- Support for `zeta := true` at `apply_beta`.
- Investigate test failure.
- Break PR in pieces because of bootstrapping issues. The current PR
updates a stage0 file to workaround the issue.
Motivation: significant performance improvement at
https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean
With M1 Pro:
- Before: 4.56 secs
- After: 3.16 secs
Successfully built stage2 using this PR
Those represent ~13% of the time spent in `save_result`,
even though `r` is a temporary in all cases but one.
See #4698 for details.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
…rators
Right now those constructors result in a copy instead of the desired
move. We've measured that expr copying and assignment by itself uses
around 10% of total runtime on our workloads.
See #4698 for details.
Changes:
- We avoid the thread local storage.
- We use a hash map to ensure that cached values are not lost.
- We remove `check_system`. If this becomes an issue in the future we
should precompute the remaining amount of stack space, and use a cheaper
check.
- We add a `Expr.replaceImpl`, and will use it to implement
`Expr.replace` after update-stage0
right now, in order to find out how many auxilary datatype are in a
mutual group of inductive with nested data type, one has to jump
through hoops like this:
```
private def numNestedInducts (indName : Name) : MetaM Nat := do
let .inductInfo indVal ← getConstInfo indName | panic! "{indName} is an inductive"
let .recInfo recVal ← getConstInfo (mkRecName indName) | panic! "{indName} has a recursor"
return recVal.numMotives - indVal.all.lengt
```
The `InductiveVal` data structure already has `.isNested : Bool`, so it
seems to be a natural extension to beef that up to `.numNested: Nat`.
This touched kernel code.
This file has comments that recall the data type definitions in Lean.
Most of them were still using lean3 syntax, and at least one of them was
out of date (one field missing), so I updated them.
I took the liberty to shorten the comments from the original file, or
omit them if they don’t add much over the field names.
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.
Remark: I had to comment
```
if debug.skipKernelTC.get opts then
addDeclWithoutChecking env decl
else
```
because the build was crashing when trying to compile Lake.
Going to perform `update-stage0` and try again.
