Hi, 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 Background - 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 coq/coq-par-compile.el. 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. FUTURE PLANS: 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
