Repository navigation
Common compile - #911
Merged
Merged
Common compile#911
Conversation
Three extension points, buffer local in the script buffer: release of the queue items of a require job (coq-par-release-items-function, given the job too), failure (coq-par-failure-function) and abort (coq-par-abort-function). Their defaults keep the behavior of Proof General. New entry point coq-par-start-compilation, outside proof-action-list. Taken from the Eglot branch (00528ce, 4915e1f), unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
coq-system.el no longer requires proof. It reads proof-prog-name only if it is bound. The detection of the programs just before starting the proof shell moves to coq.el, as coq-pg-detect-programs in proof-shell-before-process-hook (the code is unchanged). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
pg-pamacs.el, required by proof-utils.el, does not need the proof shell: Coq options can then define their toggle commands without loading Proof General. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
coq-compile-common.el and coq-par-compile.el no longer require proof-shell, another backend can load them without Proof General: - The functions putting the compilation into the hooks of the proof shell (coq-par-enable, coq-seq-enable, coq-switch-compilation-method) move to coq.el, with the toggle of coq-show-proof-stepwise, an option of coq.el. - The variables and functions of Proof General are only declared. They are used on the paths of the proof shell (default functions of the interface of coq-par-compile.el, ancestor locking), or read only when they are bound. The compilation errors are displayed with display-buffer without Proof General. - coq-seq-compile.el, for the proof shell only, requires it. - The tests that relied on coq-system or coq-compile-common to load the proof shell require it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
With coq-par-start-compilation and local interface functions: a library is compiled, a failure is reported, and the proof shell is not loaded. The test found that coq-prog-args was void without Proof General when there is no project file: coq-project.el, which sets it from the project file, now defines it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The Auto Compilation menu moves from coq-abbrev.el to coq-compile-common.el, as coq-compile-menu, so that other backends can use it. The menu of Proof General is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Coq: compilation of the Requires without the proof shell
Another backend can now load coq-par-compile.el without Proof General.
Test: the compilation of a Require without the proof shell, both success and failure. Also a CHANGES entry.