| Age | Commit message (Collapse) | Author |
|---|
|
The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).
This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Add headers to a few files which were missing them.
|
|
We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
|
|
|
|
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
|
|
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
|
As a bonus we remove some trailing whitespace, and implement a couple
of hints suggested in the discussion.
|
|
4.02.3 has been the minimal OCaml version for a while now.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Generalize the old model by letting one park a worker and
by letting the (parked) worker be picky about the tasks it
picks up.
The use of that is the following: a proof worker, while performing
its "main" task (building a proof term) computes all the intermediate
states but returns only its main result. One can ask the worker
to hang around, and react to special tasks, like printing the
goals of an intermediate state.
|
|
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).
|
|
|
