This PR develops custom simprocs for dealing with `ite`/`dite`
expressions in `cbv` tactics, based on equivalent simprocs from
`Sym.simp`, with the difference that if the condition is not reduced to
`True`/`False`, we make use of the decidable instance and calculate to
what the condition reduces to.
Stacked on top of #12391.
This PR adds `IO.FS.Metadata.numLinks`, which contains the number of
hard links to a file.
This changes the implementation of `System.FilePath.metadata` and
`System.FilePath.symlinkMetadata` to use libuv. Otherwise, `st_nlink`
was not properly set on Windows. This also has the side benefit of
provided sub-second precision for file times on Windows (fulfilling an
old TODO). Also, while libuv supports `lstat` for Windows, enabling that
is left to a future PR.
This PR fixes a platform inconsistency in `IO.FS.removeFile` where it
could not delete read-only files on Windows.
The implementation now uses `uv_fs_unlink` instead of `std::remove`, as
libuv can delete read-only files. The PR also fixes a inconsistency in
`IO_test.lean` where it would generate files in the wrong directory when
run interactively.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR fixes an issue in LCNF simp where it would attempt to act on
type incorrect `cases`
statements and look for a branch, otherwise panic. This issue did not
yet manifest in production as
various other invariants upheld by LCNF simp help mask it but will start
to become an issue with the
upcoming changes.
This is the proper fix for #6957.
This PR provides a `LawfulForwardPatternModel` instance for string
patterns, i.e., it proves correctness of the `dropPrefix?` and
`startsWith` functions for string patterns.
Note that this is "just" the correctness proof; there isn't a way to
actually use it yet. API lemmas will follow.
This PR adds identifying information about a module available to `lean`
(e.g., its name and package identifier) to the module's dependency
trace. This ensures modules with different identification have different
input hashes even if their source files and imports are identical.
This PR adds a few unification hints that we will need after
`backward.isDefEq.respectTransparency` is `true` by default.
See #12338
It was part of #12179.
This PR makes disabling the artifact cache (e.g., via
`LAKE_ARTIFACT_CACHE=false` or `enableArtifactCache = false`) now stop
Lake from fetching from the cache (whereas it previously only stopped
writing to it).
There are now 3 possible configuration of the local artifact cache for a
package:
* `true`: Artifacts will be fetched from the cache before building (if
available) and built artifacts will be cached.
* `false:`: Lake will neither fetch artifacts from the cache or store
them into it.
* **default** (no configuration set): Lake will fetch artifacts from the
cache but not store them into it. A key motivation for this is to, by
default, reuse artifacts downloaded into the cache from a remote
service.
This PR tags `List.reduceOption` with `@[expose]`. #12348 accidentally
moved the definition out of an `@[expose] section` which caused problems
in mathlib because `List.reduceOption` was expected to be exposed.
This PR extends shake with tracking of attribute names passed to
`simp`/`grind`.
On the way there, it also fixes `register_simp/grind_attr` uses outside
`public meta section` as well as go-to-definition on declaration-level
uses of the created attributes (tactic-level goto would be a separate
todo).
This PR moves the elaboration of structure/class Verso docstrings until
after the fact that it's a class is registered, so code samples in the
docstring can use it as a class. Redundant addition of structure and
constructor docstrings are also removed, because they're already handled
in MutualInductive.lean.
Closes#11651
This PR uses an `Array` instead of a `List` to store the clauses in
`Std.CNF`. This reduces the memory footprint and pressure on the
allocator, leading to noticeable performance changes with gigantic CNFs.
This PR treats the first character of the first line of a docstring as
being in the leftmost column, even if it physically is not. This allows
left-column items like headers to be used even after spaces. It also
detects the indentation of the entire docstring, using it as the
zero-point for indentation sensitive syntax such as headers.
Closes#12067.
This PR fixes poor error reporting from Verso docstrings. Before, if the
Verso parser didn't consume the whole docstring, then Lean would try to
parse the closing -/ and fail; this would lead to backtracking and an
assumption that the docstring must be non-Verso, with only the non-Verso
commands like #guard_msgs as possibilities. Now, the input is always
consumed.
Closes#12118.
This PR implements better support for unfolding class fields marked as
`reducible`. For example, we want to mark fields that are types such as
```lean
MonadControlT.stM : Type u -> Type u
```
The motivation is similar to our heuristic that type definitions should
be abbreviations.
Now, suppose we want to unfold `stM m (ExceptT ε m) α` using the
`.reducible` transparency setting, we want the result to be `stM m m
(MonadControl.stM m (ExceptT ε m) α)` instead of
`(instMonadControlTOfMonadControl m m (ExceptT ε m)).1 α`. The latter
would defeat the intent of marking the field as reducible, since the
instance `instMonadControlTOfMonadControl` is `[instance_reducible]` and
the resulting term would be stuck when using `.reducible` transparency
mode.
**Remark**: This feature introduces a few breakages in core and Mathlib.
So, it is disabled for now in this PR. To enable, we must use
`set_option backward.whnf.reducibleClassField true`
This PR adds two benchmarks (sieve of Eratosthenes, removing duplicates
from the list) and one test (a function with sublinear complexity
defined via well-founded recursion evaluated on large naturals with up
to `60` digits).
The tests have been suggested by @b-mehta.
This PR changes the semantics of `inline` annotations in the compiler.
The behavior of the original `@[inline]` attribute remains the same but
the function `inline` now comes with a restriction that it can only use
declarations that are local to the current module. This comes as a
preparation to pulling the compiler out into a separate process.
Closes: #12334
This PR changes the handling of over-applied cases expressions in
`ToLCNF` to avoid generating function declarations that are called
immediately. For example, `ToLCNF` previously produced this:
```lean-4
set_option trace.Compiler.init true
/--
trace: [Compiler.init] size: 4
def test x y : Bool :=
fun _y.1 _y.2 : Bool :=
cases x : Bool
| PUnit.unit =>
fun _f.3 a : Bool :=
return a;
let _x.4 := _f.3 _y.2;
return _x.4;
let _x.5 := _y.1 y;
return _x.5
-/
#guard_msgs in
def test (x : Unit) (y : Bool) : Bool :=
x.casesOn (fun a => a) y
```
which is now simplified to
```lean-4
set_option trace.Compiler.init true
/--
trace: [Compiler.init] size: 3
def test x y : Bool :=
cases x : Bool
| PUnit.unit =>
let a := y;
return a
-/
#guard_msgs in
def test (x : Unit) (y : Bool) : Bool :=
x.casesOn (fun a => a) y
```
This is especially relevant for #8309 because there `dite` is defined as
an over-applied `Bool.casesOn`.
