A more restrictive but efficient max sharing primitive.
**Motivation:** Some software verification proofs may contain
significant redundancy that can be eliminated using hash-consing (also
known as `shareCommon`). For example, [theorem
`sha512_block_armv8_test_4_sym`](460fe5d74c/Proofs/SHA512/SHA512Sym.lean (L29))
took a few seconds at [`addPreDefinitions`
](1a12f63f74/src/Lean/Elab/PreDefinition/Main.lean (L155))
and one second at `fixLevelParams` on a MacBook Pro (with M1 Pro). The
proof term initially had over 16 million subterms, but the redundancy
was indirectly and inefficiently eliminated using `Core.transform` at
`addPreDefinitions`. I tried to use `shareCommon` method to fix the
performance issue, but it was too inefficient. This PR introduces a new
`shareCommon'` method that, although less flexible (e.g., it uses only a
local cache and hash-consing table), is much more efficient. The new
procedure minimizes the number of RC operations and optimizes the
caching strategy. It is 20 times faster than the old `shareCommon`
procedure for theorem `sha512_block_armv8_test_4_sym`.
Continuation of #3958. To ensure that lean code is able to uphold the
invariant that `String`s are valid UTF-8 (which is assumed by the lean
model), we have to make sure that no lean objects are created with
invalid UTF-8. #3958 covers the case of lean code creating strings via
`fromUTF8Unchecked`, but there are still many cases where C++ code
constructs strings from a `const char *` or `std::string` with unclear
UTF-8 status.
To address this and minimize accidental missed validation, the
`(lean_)mk_string` function is modified to validate UTF-8. The original
function is renamed to `mk_string_unchecked`, with several other
variants depending on whether we know the string is UTF-8 or ASCII and
whether we have the length and/or utf8 char count on hand. I reviewed
every function which leads to `mk_string` or its variants in the C code,
and used the appropriate validation function, defaulting to `mk_string`
if the provenance is unclear.
This PR adds no new error handling paths, meaning that incorrect UTF-8
will still produce incorrect results in e.g. IO functions, they are just
not causing unsound behavior anymore. A subsequent PR will handle adding
better error reporting for bad UTF-8.
Extends Lean's incremental reporting and reuse between commands into
various steps inside declarations:
* headers and bodies of each (mutual) definition/theorem
* `theorem ... := by` for each contained tactic step, including
recursively inside supported combinators currently consisting of
* `·` (cdot), `case`, `next`
* `induction`, `cases`
* macros such as `next` unfolding to the above
*Incremental reuse* means not recomputing any such steps if they are not
affected by a document change. *Incremental reporting* includes the
parts seen in the recording above: the progress bar and messages. Other
language server features such as hover etc. are *not yet* supported
incrementally, i.e. they are shown only when the declaration has been
fully processed as before.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Adds `IO.getTaskState` which returns the state of a `Task` in the Lean
runtime's task manager. The `TaskState` inductive has 3 constructors:
`waiting`, `running`, and `finished`. The `waiting` constructor
encompasses the waiting and queued states within the C task object
documentation, because the task object does not provide a low cost way
to distinguish these different forms of waiting. Furthermore, it seems
unlikely for consumers to wish to distinguish between these internal
states. The `running` constructor encompasses both the running and
promised states in C docs. While not ideal, the C implementation does
not provide a way to distinguish between a running `Task` and a waiting
`Promise.result` (they both have null closures).
Adds `IO.Process.getCurrentDir` and `IO.Process.setCurrentDir` for
retrieving and setting, respectively, the current working directory of a
process. The names of the functions are inspired by Rust (e.g.,
[`set_current_dir`](https://doc.rust-lang.org/std/env/fn.set_current_dir.html)).
- [x] Depends on: #3958
- [x] Depends on: #3960
This makes the UTF-8 encode and decode functions have lean definitions,
so that we can prove properties about them downstream.
Previously, there was a function `opaque fromUTF8Unchecked : ByteArray
-> String` which would convert a list of bytes into a string, but as the
name implies it does not validate that the string is UTF-8 before doing
so and as a result it produces unsound results in the compiler (because
the lean model of `String` indirectly asserts UTF-8 validity). This PR
replaces that function by
```lean
opaque validateUTF8 (a : @& ByteArray) : Bool
opaque fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String
```
so that while the function is still "unchecked", we have a proof witness
that the string is valid. To recover the original, actually unchecked
version, use `lcProof` or other unsafe methods to produce the proof
witness.
Because this was the only `ByteArray -> String` conversion function, it
was used in several places in an unsound way (e.g. reading untrusted
input from IO and treating it as UTF-8). These have been replaced by
`fromUTF8?` or `fromUTF8!` as appropriate.
Adds `IO.FS.Handle.isTty` to check whether a handle is a Windows console
or Unix terminal. Also adds an `isTty` field to `IO.FS.Stream`, so that
this can be checked on, e.g., `stdout`.
`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.
On Windows, we now compile all core `.o`s twice, once with and without
`dllexport`, for use in the shipped dynamic and static libraries,
respectively. On other platforms, we export always as before to avoid
the duplicate work.
---------
Co-authored-by: tydeu <tydeu@hatpress.net>
In the new snapshot design, we have a tree of `Task`s that represents
the asynchronously processed document structure. When transforming this
tree in response to a user edit, we want to quickly run through
reusable, already computed nodes of the tree synchronously and then
spawn new tasks for the new parts. The new flag allows us to do such
mixed sync/async tree transformations uniformly. This flag exists as
e.g.
[`ExecuteSynchronously`](https://learn.microsoft.com/en-us/dotnet/api/system.threading.tasks.taskcontinuationoptions?view=net-8.0)
in other runtimes.
else I see
```
[ 69%] Building CXX object runtime/CMakeFiles/leanrt.dir/platform.cpp.o
/home/jojo/build/lean/lean4/src/runtime/io.cpp:509:75: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64));
^
, ""
/home/jojo/build/lean/lean4/src/runtime/io.cpp:517:74: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64));
^
, ""
2 warnings generated.
```
when building
