I just committed the first version of parallel background
compilation for Coq. It is disabled by default in favor of the
old synchronous compilation method.
Parallel compilation required one fundamental and one minor
change in the general proof shell treatment, see below.
If you want to try parallel compilation:
- Check menu entry Coq -> Settings -> Compile Parallel In
- Configure coq-max-background-compilation-jobs to something
greater than 1 to actually experience parallel compilation
- C-c C-c kills all compilation jobs
- you may try M-: (coq-par-emergency-cleanup) in emergencies
Information about the implementation is in
THE FUNDAMENTAL PROOF SHELL CHANGE:
The Require command and the items that follow it must not be
added to proof-action-list before the compilation finishes.
Therefore, from now on, proof-action-list does not necessarily
contain all items from the queue region.
Require commands and items that follow them are stored in some
property list of some uninterned symbols that I manage in the
background compilation process. If compilation finishes these
items are put back into proof-action-list. Typically,
proof-action-list gets empty before this happens.
Nevertheless, the proof shell lock must not be released and the
queue span must stay active in such cases.
I therefore added the variable proof-second-action-list-active,
which gets set to t if some queue items are stored elsewhere.
This variable then modifies the behavior of the proof shell
functions at appropriate places.
THE MINOR PROOF SHELL CHANGE:
I added a new hook proof-shell-signal-interrupt-hook, that is
called in proof-interrupt-process and proof-shell-kill-function.
With this hook I can kill all background compilation jobs as
early as possible.
There are a number of TODO's in coq/coq-par-compile.el.
Synchronous and asynchronous compilation are in separate files
with the common functionality in coq/coq-compile-common.el. My
plan is to leave both coexist for a while.
ProofGeneral-devel mailing list