- Lean strings (like std::string) may contain null characters. The
codebase was ignoring this issue.
- We now have a wrapper `string_ref` for wrapping Lean string objects in
C++. This wrapper also implements correctly the coercions std::string <-> string_ref.
Remark: I also found a few places where the code relies on the
following property which is not true
Forall s : std::string, std::string(s.c_str()) == s
- `name` object wrapper was assuming that all numerals were small
`nat` values. This is true in most cases, but the system would
crash when processing if it is a big number.
- The commit tries to make sure runtime/util/kernel are correct.
Modules that will be deleted contain many `TODO` comments
indicating they may crash and/or produce incorrect results
when strings contain null characters and numerals are big.
cc @kha
@kha: I thought about using `string` instead of `string_ref`.
We consistently use `std::string`. So, it should be fine, but I
was concerned about code readability.
After we bootstrap Lean4, we will be able to delete `lean::list`
template, and rename `lean::list_ref` to `lean::list`.
I am going to add `pair_ref` for wrapping Lean pair objects.
If we use `lean::string` instead of `lean::string_ref`, then
we should also use `lean::pair` instead of `lean::pair_ref`.
But, there is a problem in this case since we have
https://github.com/leanprover/lean4/blob/master/src/util/pair.h#L13
:(
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
The new lean_obj objects will be defined at util.
Reason: we will define `name`, `options`, `format`, ... on top of lean_obj.
lean_obj depends on mpz.
Remark: lean_obj will replace vm_obj.
This abstraction was added when we started Lean.
We wanted to focus on nonlinear arithmetic and support dReal.
The zpz module was going to be used to implement polynomial
factorization procedures similar to the ones in Z3 and computer algebra
systems.
This is not a goal for the Lean project anymore.
These two abstractions were added when we planned to have an efficient
Simplex module, written in C++, in Lean. We have moved this module to
Z3. So, we don't need these abstractions anymore.
Binary rationals were added when we started the Lean project.
We wanted to use them to implement an algebraic number module similar to the
one we implemented in Z3.
If one day we implement algebraic numbers in Lean, we will do it in Lean
instead of C++.
