| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
| |
|
|
|
|
|
|
|
|
| |
We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.
To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.
|
| |
|
|
| |
4.02.3 has been the minimal OCaml version for a while now.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
| | |
|
| |
|
|
|
| |
This is a small, but convenient refactoring, as it will allow common
argument parsing.
|
| | |
|
| | |
|
| |
|
|
|
| |
This is mainly shuffling code around and removing internal
refs that are not needed anymore.
|
| | |
|
|
|
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
Théo Zimmermann
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Pierre-Marie Pédrot
Maxime Dénès
Enrico Tassi