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.
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).
`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.
Makes the LLVM triple of the current platform available to Lean code
towards a solution for #2754.
Defaults to the empty string if the compiler is not clang, which can
introduce some divergence between CI and local builds but should not be
noticeable in most cases and is not really possible to avoid.
