From 48ab233ea7e317a5fa0875a462a6a711d91c6392 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 5 Jun 2022 22:43:28 +0200 Subject: [PATCH 1/2] coq: make Proof General/coq opam-switch-mode aware See `coq-kill-coq-on-opam-switch`: Proof General can now reset the proof shell when the opam switch is changed via opam-switch-mode. --- CHANGES | 7 +++++ coq/coq-compile-common.el | 18 ------------- coq/coq.el | 54 ++++++++++++++++++++++++++++++++++----- 3 files changed, 54 insertions(+), 25 deletions(-) diff --git a/CHANGES b/CHANGES index 0c45024b8..e20941ce1 100644 --- a/CHANGES +++ b/CHANGES @@ -108,6 +108,13 @@ standard support. documentation of this variable for an explanation of the different possible values and some more information. +*** Make Proof General/Coq `opam-switch-mode` aware + + When opam-switch-mode is loaded, the Coq background process can be + killed when changing the opam switch through opam-switch-mode, see + `coq-kill-coq-on-opam-switch` and + https://github.com/ProofGeneral/opam-switch-mode. + *** Limited extensibility for indentation Coq indentation mechanism is based on a fixed set of tokens and diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 1055c7443..8074d7faf 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -798,24 +798,6 @@ current buffer (which contains the Require command) to (save-some-buffers unconditionally buffer-filter))) -;;; kill coqtop on script buffer change - -(defun coq-switch-buffer-kill-proof-shell () - "Kill the proof shell without asking the user. -This function is for `proof-deactivate-scripting-hook'. It kills -the proof shell without asking the user for -confirmation (assuming she agreed already on switching the active -scripting buffer). This is needed to ensure the load path is -correct in the new scripting buffer." - (unless proof-shell-exit-in-progress - (proof-shell-exit t))) - -;; This is now always done (in coq.el) -;(add-hook 'proof-deactivate-scripting-hook -; 'coq-switch-buffer-kill-proof-shell -; t) - - (provide 'coq-compile-common) ;; Local Variables: *** diff --git a/coq/coq.el b/coq/coq.el index c8d92ca7e..5a85bf7b9 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -3422,15 +3422,55 @@ priority to the former." (put 'coq-terminator-insert 'delete-selection t) -;;;;;;;;;;;;;; -;; This was done in coq-compile-common, but it is actually a good idea even -;; when "compile when require" is off. When switching scripting buffer, let us -;; restart the coq shell process, so that it applies local coqtop options. -(add-hook 'proof-deactivate-scripting-hook - #'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common - t) +;;;;;;;;;;;;;; kill coq background process on different occasions ;;;;;;;;;;;;;; + +;; This originates from background compilation, but it is actually a good idea +;; even when "compile when require" is off. When switching scripting buffer, +;; let us restart the coq shell process, so that it applies local coqtop +;; options. + +(defun coq-kill-proof-shell () + "Kill the proof shell without asking the user. +This function is for `proof-deactivate-scripting-hook'. It kills +the proof shell without asking the user for +confirmation (assuming she agreed already on switching the active +scripting buffer). This is needed to ensure the load path is +correct in the new scripting buffer." + (unless proof-shell-exit-in-progress + (proof-shell-exit t))) + +(add-hook 'proof-deactivate-scripting-hook #'coq-kill-proof-shell t) + +(defcustom coq-kill-coq-on-opam-switch t + "If t kill coq when the opam switch changes (requires `opam-switch-mode'). +When `opam-switch-mode' is loaded and the user changes the opam switch +through `opam-switch-mode' then this option controls whether the coq +background process (the proof shell) is killed such that the next +assert command starts a new proof shell, probably using a +different coq version from a different opam switch. + +See https://github.com/ProofGeneral/opam-switch-mode for `opam-switch-mode'" + :type 'boolean + :group 'coq) + + +(defun coq-kill-proof-shell-on-opam-switch () + "Kill proof shell when the opam switch changes (requires `opam-switch-mode'). +This function is for the `opam-switch-mode' hook +`opam-switch-change-opam-switch-hook', which runs when the user +changes the opam switch through `opam-switch-mode'. If +`coq-kill-coq-on-opam-switch' is t, then the proof shell is +killed such that the next assert starts a new proof shell, using +coq from the new opam switch." + (when (and coq-kill-coq-on-opam-switch proof-script-buffer) + (coq-kill-proof-shell))) + + +(add-hook 'opam-switch-change-opam-switch-hook + #'coq-kill-proof-shell-on-opam-switch t) +;;;;;;;;;;;;;;; ;; overwriting the default behavior, this is an experiment, *frames* will be ;; deleted only if only displaying associated buffers. If this is OK the From a3d0fc9875e5d24de52be6685c885a60aca4c05b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 13 Jul 2022 17:19:56 +0200 Subject: [PATCH 2/2] docs: Document OPSW in ProofGeneral.texi & Run (make -C doc magic) --- CHANGES | 6 +++--- doc/ProofGeneral.texi | 36 ++++++++++++++++++++++++++++++++++++ 2 files changed, 39 insertions(+), 3 deletions(-) diff --git a/CHANGES b/CHANGES index e20941ce1..bfce6dcd8 100644 --- a/CHANGES +++ b/CHANGES @@ -108,12 +108,12 @@ standard support. documentation of this variable for an explanation of the different possible values and some more information. -*** Make Proof General/Coq `opam-switch-mode` aware +*** Make ProofGeneral/Coq `opam-switch-mode' aware When opam-switch-mode is loaded, the Coq background process can be killed when changing the opam switch through opam-switch-mode, see - `coq-kill-coq-on-opam-switch` and - https://github.com/ProofGeneral/opam-switch-mode. + `coq-kill-coq-on-opam-switch' and + https://github.com/ProofGeneral/opam-switch-mode *** Limited extensibility for indentation diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index f7748846f..bb51dbb55 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4187,6 +4187,7 @@ assistant. It supports most of the generic features of Proof General. * Holes feature:: * Proof-Tree Visualization:: * Showing Proof Diffs:: +* Opam-switch-mode support:: @end menu @@ -5320,6 +5321,41 @@ have added or removed tokens are shown with the entire line highlighted with a @code{Coq Diffs ... Bg} face. The added or removed tokens themselves are highlighted with non-@code{Bg} faces. +@node Opam-switch-mode support +@section Opam-switch-mode support + +Coq can be installed using @code{opam} (the OCaml package manager), +which makes it easy to manage several different switches, having each +a different version of Coq. + +Instead of running a command like @code{opam switch ...} in a terminal +and restarting emacs to benefit from a different switch, one can: + +@itemize @bullet +@item +@b{Install} the +@uref{https://github.com/ProofGeneral/opam-switch-mode, +opam-switch-mode} and use the dedicated mode bar menu @code{OPSW} it +provides. +@item +@b{Configure} Proof General using the customization option +@code{coq-kill-coq-on-opam-switch}, so that the Coq background process +is killed when changing the opam switch through +@code{opam-switch-mode}. +@end itemize + +@c TEXI DOCSTRING MAGIC: coq-kill-coq-on-opam-switch +@defvar coq-kill-coq-on-opam-switch +If t kill coq when the opam switch changes (requires @samp{opam-switch-mode}).@* +When @samp{opam-switch-mode} is loaded and the user changes the opam switch +through @samp{opam-switch-mode} then this option controls whether the coq +background process (the proof shell) is killed such that the next +assert command starts a new proof shell, probably using a +different coq version from a different opam switch. + +See https://github.com/ProofGeneral/opam-switch-mode for @samp{opam-switch-mode} +@end defvar + @c ================================================================= @c @c CHAPTER: EasyCrypt Proof General