This implements a naive version of `getline` because Windows does not
have `getline`. Given the fact that `FILE` has buffered IO, calling
`fgetc` in a loop is not as big of a performance hazard as it might seem
at first glance.
The proper solution to this would of course be to have our own buffered
IO so we are fully in charge of the buffer. In this situation we could
check the entire buffer for a newline at once instead of char by char.
However that is not going to happen for the near future so I propose we
stay with this implementation. If reading individual lines of a file
does truly end up being the performance bottle neck we have already
won^^.
previously, `#eval` would happily evaluate expressions that contain
`sorry`, either explicitly or because of failing tactics. In conjunction
with operations like array access this can lead to the lean process
crashing, which isn't particularly great.
So how `#eval` will refuse to run code that (transitively) depends on
the `sorry` axiom (using the same code as `#print axioms`).
If the user really wants to run it, they can use `#eval!`.
Closes#1697
Add efficient `usize` functions for `Array`, `ByteArray`, `FloatArray`.
This is part 1 of 2 since there is a need to update stage0 between the
two parts. (See discussion below.)
Closes#4654
the internal constructions for structural and well-founded recursion
use plenty of `PProd` and `MProd`, and reading these, deeply
nested and in prefix notation, is unnecessarily troublesome.
Therefore this introduces notations
```
a ×ₚ b -- PProd a b
a ×ₘ b -- MProd a b
()ₚ -- PUnit.unit
(x,y,z)ₚ -- PProd.mk x (PProd.mk y z)
(x,y,z)ₘ -- MProd.mk x (MProd.mk y z)
```
(This is part 1, the rest will follow in #4730 after a stage0 update.)
Fixes the Windows build. As libLean is by far the biggest component,
there is no need for a separate libStd_shared for now.
```
$ find build/release/stage1/lib/lean -name '*.a' -exec bash -c 'echo -n "{} " ; nm {} | grep " T " | wc -l' \;
build/release/stage1/lib/lean/libleanrt.a 497
build/release/stage1/lib/lean/libleancpp.a 1320
build/release/stage1/lib/lean/libInit.a 7476
build/release/stage1/lib/lean/libStd.a 1696
build/release/stage1/lib/lean/libLean.a 64339
build/release/stage1/lib/lean/libLake.a 5722
```
This implements the `termination_by structural` syntax proposed in
#3909.
I went with `termination_by structural` over, say,
`termination_by (config := {method := .structural})` mainly because it
was
easier to get going (otherwise I’d have to look into how to define
recursive
parsers, as `Parser.config` depends on `term` and `termination_by` is
part of
term. But also because I find it more ergonomic and aesthetic as a user.
But syntax can still change.
The `termination_by?` syntax will no longer force well-founded
recursion,
and instead the inferred `termination_by structurally` annotation will
be shown
if structural termination is possible.
While I was it, this fixes#4546 the easy way (log errors about but
otherwise
ignore incomplete `termination_by` sets for mutual recursion). Maybe we
get
multiple replacements (#4551), but even then this this good behavior.
Involves a bit of shuffling around `TerimationHints` (now validated for
a
clique already by `PreDefinition.main`) and `TerminationArguments` (now
lifted
out of the `WF` namespace, and a bit simplified).
Fixes#3909
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
we keep running into examples where working with well-founded recursion
is slow because defeq checks (which are all over the place, including
failing ones that are back-tracked) unfold well-founded definitions.
The definition of a function defined by well-founded recursion should be
an implementation detail that should only be peeked inside by the
equation generator and the functional induction generator.
We now mark the mutual recursive function as irreducible (if the user
did not
set a flag explicitly), and use `withAtLeastTransparency .all` when
producing
the equations.
Proofs can be fixed by using rewriting, or – a bit blunt, but nice for
adjusting
existing proofs – using `unseal` (a.k.a. `attribute [local
semireducible]`).
Mathlib performance does not change a whole lot:
http://speed.lean-fro.org/mathlib4/compare/08b82265-75db-4a28-b12b-08751b9ad04a/to/16f46d5e-28b1-41c4-a107-a6f6594841f8
Build instructions -0.126 %, four modules with significant instructions
decrease.
To reduce impact, these definitions were changed:
* `Nat.mod`, to make `1 % n` reduce definitionally, so that `1` as a
`Fin 2` literal
works nicely. Theorems with larger `Fin` literals tend to need a `unseal
Nat.modCore`
https://github.com/leanprover/lean4/pull/4098
* `List.ofFn` rewritten to be structurally recursive and not go via
`Array.ofFn`:
https://github.com/leanprover-community/batteries/pull/784
Alternative designs explored were
* Making `WellFounded.fix` irreducible.
One benefit is that recursive functions with equal definitions (possibly
after
instantiating fixed parameters) are defeq; this is used in mathlib to
relate
[`OrdinalApprox.gfpApprox`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/FixedPointApproximants.html#OrdinalApprox.gfpApprox)
with `.lfpApprox`.
But the downside is that one cannot use `unseal` in a
targeted way, being explicit in which recursive function needs to be
reducible here.
And in cases where Lean does unwanted unfolding, we’d still unfold the
recursive
definition once to expose `WellFounded.fix`, leading to large terms for
often no good
reason.
* Defining `WellFounded.fix` to unroll defintionally once before hitting
a irreducible
`WellFounded.fixF`. This was explored in #4002. It shares most of the
ups and downs
with the previous variant, with the additional neat benefit that
function calls that
do not lead to recursive cases (e.g. a `[]` base case) reduce nicely.
This means that
the majority of existing `rfl` proofs continue to work.
Issue #4051, which demonstrates how badly things can go if wf recursive
functions can be
unrolled, showed that making the recursive function irreducible there
leads to noticeably
faster elaboration than making `WellFounded.fix` irreducible; this is
good evidence that
the present PR is the way to go.
This fixes https://github.com/leanprover/lean4/issues/3988
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
`Nat.repr` was implemented by generating a list of `Chars`, each created
by a 10-way if-then-else. This can cause significant slow down in some
particular use cases.
Now `Nat.repr` is `implemented_by` a faster implementation that uses
C++’s `std::to_string` on small numbers (< USize.size) and maintains an
array of pre-allocated strings for the first 128 numbers.
The handling of big numbers (≥ USize.size) remains as before.
Adds options to control whitespace normalization and message ordering in
`#guard_msgs`.
Examples:
1. `#guard_msgs (whitespace := lax)` ignores differences in whitespace
completely.
2. `#guard_msgs (whitespace := exact)` requires an exact match for
whitespace (after trimming).
3. `#guard_msgs (ordering := sorted)` sorts the list of messages, to
make it insensitive to message order.
