- use low-level compilation interface for external coq

  compilation with our own customization variables

2 files changed, 99 insertions, 48 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 49106827..5c426d48 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1108,8 +1108,6 @@ Currently this doesn't take the loadpath into account."
 ;; - clean old multiple file stuff
 ;; - fix places marked with XXX
 ;; - enable next-error in recompile-response buffers
-;; - call compile more cleverly, with a coq-specific option for compile
-;;   command confirmation
 
 ;; user options and variables
 
@@ -1133,25 +1131,40 @@ If unset (the empty string) ProofGeneral computes the dependencies of
 required modules with coqdep and compiles as necessary. This internal
 dependency checking does currently not handle ML modules.
 
-If a non-empty string, the denoted command is called to do the dependency
-checking and compilation. Before calling this command via `compile'
-the following keys are substituted as follows:
+If a non-empty string, the denoted command is called to do the
+dependency checking and compilation. Before executing this
+command the following keys are substituted as follows:
   %p  the (physical) directory containing the source of
       the required module
   %o  the coq object file in the physical directory that will
       be loaded
+  %s  the coq source file in the physical directory whose
+      object will be loaded
   %q  the qualified id of the \"Require\" command
   %r  the source file containing the \"Require\"
 
 For instance, \"make -C %p %o\" expands to \"make -C bar foo.vo\"
-when module \"foo\" from directory \"bar\" is required."
+when module \"foo\" from directory \"bar\" is required.
+
+After the substitution the command can be changed in the
+minibuffer if `coq-confirm-external-compilation-command' is t."
   :type 'string
-  :safe 'stringp
+  :safe '(lambda (v)
+           (and (stringp v)
+                (or (not (boundp 'coq-confirm-external-compilation-command))
+                    coq-confirm-external-compilation-command)))
+  :group 'coq-auto-compile)
+
+(defcustom coq-confirm-external-compilation-command t
+  "*If set let user change and confirm the compilation command.
+Otherwise start the external compilation without confirmation."
+  :type 'boolean
   :group 'coq-auto-compile)
 
 (defconst coq-compile-substitution-list
   '(("%p" physical-dir)
     ("%o" module-object)
+    ("%s" module-source)
     ("%q" qualified-id)
     ("%r" requiring-file))
   "Substitutions for `coq-compile-command'.
@@ -1160,12 +1173,13 @@ a 2-element list. The first element of a substitution is the
 regexp to substitute, the second the replacement. The replacement
 is evaluated before passing it to `replace-regexp-in-string', so
 it might be a string, or one of the symbols 'physical-dir,
-'module-object, 'qualified-id and 'requiring-file, which are
-bound, respectively, to the the physical directory containing the
-source file, the Coq object file in 'physical-dir that will be
-loaded, the qualified module identifier that occurs in the
-\"Require\" command, and the file that contains the
-\"Require\".")
+'module-object, 'module-source, 'qualified-id and
+'requiring-file, which are bound to, respectively, the physical
+directory containing the source file, the Coq object file in
+'physical-dir that will be loaded, the Coq source file in
+'physical-dir whose object will be loaded, the qualified module
+identifier that occurs in the \"Require\" command, and the file
+that contains the \"Require\".")
 
 (defcustom coq-compile-auto-save 'ask-coq
   "*Buffers to save before checking dependencies for compilation.
@@ -1265,6 +1279,9 @@ white space. The module identifier must be matched with group number 1.
 Note that the trailing dot in \"Require A.\" is not part of the module
 identifier and should therefore not be matched by this regexp.")
 
+(defvar coq-compile-history nil
+  "History of external Coq compilation commands.")
+
 ;; basic utilities
 
 (defun time-less-or-equal (time-1 time-2)
@@ -1543,31 +1560,43 @@ function."
 
 (defun coq-auto-compile-externally (span qualified-id absolute-module-obj-file)
   "Make MODULE up-to-date according to `coq-compile-command'.
-Call `compile' to make MODULE up-to-date. The compile command is derived
-from `coq-compile-command' by substituting certain keys, see
-`coq-compile-command' for details. Customizing `compile-command' has
-therefore no effect, customize `coq-compile-command' instead. All other
-customizations of `compile' apply, so set the variable
-`compilation-read-command' to nil if you don't want to confirm the
-compilation command. Further, set `compilation-ask-about-save' to nil
-to save all buffers without confirmation before compilation.
+Start a compilation to make ABSOLUTE-MODULE-OBJ-FILE up-to-date.
+The compilation command is derived from `coq-compile-command' by
+substituting certain keys, see `coq-compile-command' for details.
+If `coq-confirm-external-compilation-command' is t then the user
+must confirm the external command in the minibuffer, otherwise
+the command is executed without confirmation.
 
 Argument SPAN is the span of the \"Require\" command. The
 ancestor ABSOLUTE-MODULE-OBJ-FILE is locked and registered in the
-span for for proper unlocking on retract."
+span for for proper unlocking on retract.
+
+This function uses the low-level interface `compilation-start',
+therefore the customizations for `compile' do not apply."
   (unless (coq-compile-ignore-file absolute-module-obj-file)
-    (let ((compile-command coq-compile-command)
-          (physical-dir (file-name-directory absolute-module-obj-file))
-          (module-object (file-name-nondirectory absolute-module-obj-file))
-          (requiring-file buffer-file-name))
+    (let* ((local-compile-command coq-compile-command)
+           (physical-dir (file-name-directory absolute-module-obj-file))
+           (module-object (file-name-nondirectory absolute-module-obj-file))
+           (module-source (coq-library-src-of-obj-file module-object))
+           (requiring-file buffer-file-name))
       (mapc
        (lambda (substitution)
-         (setq compile-command
+         (setq local-compile-command
                (replace-regexp-in-string
                 (car substitution) (eval (car (cdr substitution)))
-                compile-command)))
+                local-compile-command)))
        coq-compile-substitution-list)
-      (call-interactively 'compile)
+      (if coq-confirm-external-compilation-command
+          (setq local-compile-command
+                (read-shell-command
+                 "Coq compile command: " local-compile-command
+                 (if (equal (car coq-compile-history) local-compile-command)
+                     '(coq-compile-history . 1)
+                   'coq-compile-history))))
+      ;; buffers have already been saved before we entered this function
+      ;; the next line is probably necessary to make recompile work
+      (setq-default compilation-directory default-directory)
+      (compilation-start local-compile-command)
       (coq-lock-ancestor
        span
        (coq-library-src-of-obj-file absolute-module-obj-file)))))
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 6cf876b1..6715c48b 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4102,16 +4102,23 @@ itself. Otherwise the command in @code{coq-compile-command} is
 started as an external process after substituting certain keys,
 @ref{Customizing Coq Multiple File Support}. 
 
-If Proof General uses an external command for compilation, this
-command is started via @code{compile}, @ref{Compilation,,,emacs}.
-Because Proof General cannot know if some library files have been
-updated outside of Proof General, it must perform the dependency
-checking for each @code{Require} command. The continuous
-confirmation of the external compilation commands can soon become
-tedious. Set @code{compilation-read-command} to nil to disable
-command confirmation for all invocations of @code{compile}, see
-the documentation of @code{compile} (which is displayed after
-typing C-h f compile). 
+For an external compilation command Proof General uses the
+general compilation facilities of Emacs
+(@inforef{Compilation,,emacs}) with its own customization variables.
+The compilation command must be customized in
+@code{coq-compile-command} and the flag
+@code{coq-confirm-external-compilation-command} determines
+whether the user must confirm the compilation command. The output
+of the compilation appears in the @code{*compilation*} buffer and
+one can use @code{C-x `} (bound to @code{next-error},
+@inforef{Compilation Mode,,emacs}) to jump to error locations.
+
+Proof General cannot know if some library files have been updated
+outside of Proof General, therefore, it must perform the
+dependency checking for each @code{Require} command. If the
+continuous confirmation of the external compilation commands
+becomes tedious, set
+@code{coq-confirm-external-compilation-command} to nil.
 
 When a @code{Require} command causes a compilation of some files
 one may wish to save some buffers to disk beforehand. The option
@@ -4183,24 +4190,38 @@ If unset (the empty string) ProofGeneral computes the dependencies of
 required modules with coqdep and compiles as necessary. This internal
 dependency checking does currently not handle ML modules.
 
-If a non-empty string, the denoted command is called to do the dependency
-checking and compilation. Before calling this command via @samp{compile}
-the following keys are substituted as follows:
+If a non-empty string, the denoted command is called to do the
+dependency checking and compilation. Before executing this
+command the following keys are substituted as follows:
 @lisp
   %p  the (physical) directory containing the source of
       the required module
   %o  the coq object file in the physical directory that will
       be loaded
+  %s  the coq source file in the physical directory whose
+      object will be loaded
   %q  the qualified id of the "Require" command
   %r  the source file containing the "Require"
 @end lisp
 For instance, "make -C %p %o" expands to "make -C bar foo.vo"
 when module "foo" from directory "bar" is required.
 
+After the substitution the command can be changed in the
+minibuffer if @samp{@code{coq-confirm-external-compilation-command}} is t.
+
 The default value is @code{""}.
 @end defopt
 
 
+@c TEXI DOCSTRING MAGIC: coq-confirm-external-compilation-command
+@defopt coq-confirm-external-compilation-command 
+If set let user change and confirm the compilation command.@*
+Otherwise start the external compilation without confirmation.
+
+The default value is @code{t}.
+@end defopt
+
+
 @c TEXI DOCSTRING MAGIC: coq-compile-auto-save
 @defopt coq-compile-auto-save 
 Buffers to save before checking dependencies for compilation.@*
@@ -4315,12 +4336,13 @@ a 2-element list. The first element of a substitution is the
 regexp to substitute, the second the replacement. The replacement
 is evaluated before passing it to @samp{@code{replace-regexp-in-string}}, so
 it might be a string, or one of the symbols @code{'physical-dir},
-@code{'module-object}, @code{'qualified-id} and @code{'requiring-file}, which are
-bound, respectively, to the the physical directory containing the
-source file, the Coq object file in @code{'physical-dir} that will be
-loaded, the qualified module identifier that occurs in the
-"Require" command, and the file that contains the
-"Require".
+@code{'module-object}, @code{'module-source}, @code{'qualified-id} and
+@code{'requiring-file}, which are bound to, respectively, the physical
+directory containing the source file, the Coq object file in
+@code{'physical-dir} that will be loaded, the Coq source file in
+@code{'physical-dir} whose object will be loaded, the qualified module
+identifier that occurs in the "Require" command, and the file
+that contains the "Require".
 @end defvar