diff options
| -rw-r--r-- | coq/coq.el | 133 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 6 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 128 |
3 files changed, 178 insertions, 89 deletions
@@ -1234,15 +1234,6 @@ minibuffer if `coq-confirm-external-compilation' is t." coq-confirm-external-compilation))) :group 'coq-auto-compile) -(defpacustom confirm-external-compilation t - "If set let user change and confirm the compilation command. -Otherwise start the external compilation without confirmation. - -This option can be set/reset via menu -`Coq -> Settings -> Confirm External Compilation'." - :type 'boolean - :group 'coq-auto-compile) - (defconst coq-compile-substitution-list '(("%p" physical-dir) ("%o" module-object) @@ -1263,6 +1254,53 @@ directory containing the source file, the Coq object file in identifier that occurs in the \"Require\" command, and the file that contains the \"Require\".") +(defcustom coq-load-path nil + "Non-standard coq library load path. +This list specifies the LoadPath extension for coqdep, coqc and +coqtop. Usually, the elements of this list are strings (for +\"-I\") or lists of two strings (for \"-R\" dir \"-as\" path). + +The possible forms of elements of this list correspond to the 4 +possible forms of the Add LoadPath command and the 4 forms of the +include options ('-I' and '-R'). An element can be + + - A string, specifying a directory to be mapped to the empty + logical path ('-I'). + - A list of the form '(rec dir path)' (where dir and path are + strings) specifying a directory to be recursively mapped to the + logical path 'path' ('-R dir -as path'). + - A list of the form '(rec dir)', specifying a directory to be + recursively mapped to the empty logical path ('-R dir'). + - A list of the form '(norec dir path)', specifying a directory + to be mapped to the logical path 'path' ('-I dir -as path'). + +For convenience the symbol 'rec' can be omitted and entries of +the form '(dir)' and '(dir path)' are interpreted as '(rec dir) +and '(rec dir path)', respectively. + +Under normal circumstances this list does not need to +contain the coq standard library or \".\" for the current +directory (see `coq-load-path-include-current')." + :type '(repeat (choice (string :tag "simple directory without path (-I)") + (list :tag "recursive directory without path (-R)" + (const rec) (string)) + (list :tag + "recursive directory with path (-R ... -as ...)" + (const rec) (string) (string)) + (list :tag + "simple directory with path (-R ... -as ...)" + (const nonrec) (string) (string)))) + :safe '(lambda (v) (every + '(lambda (entry) + (or (stringp entry) + (and (eq (car entry) 'rec) + (every 'stringp (cdr entry))) + (and (eq (car entry) 'nonrec) + (every 'stringp (cdr entry))) + (every 'stringp entry))) + v)) + :group 'coq-auto-compile) + (defcustom coq-compile-auto-save 'ask-coq "Buffers to save before checking dependencies for compilation. There are two orthogonal choices: Firstly one can save all or only the coq @@ -1297,14 +1335,20 @@ locked when the \"Require\" command is processed." :safe 'booleanp :group 'coq-auto-compile) -(defcustom coq-compile-ignore-library-directory t - "If non-nil, ProofGeneral does not compile modules from the coq library. -Should be `t' for normal coq users. If `nil' library modules are -compiled if their sources are newer. +(defpacustom confirm-external-compilation t + "If set let user change and confirm the compilation command. +Otherwise start the external compilation without confirmation. -This option has currently no effect, because Proof General uses -coqdep to translate qualified identifiers into library file names -and coqdep does not output dependencies in the standard library." +This option can be set/reset via menu +`Coq -> Settings -> Confirm External Compilation'." + :type 'boolean + :group 'coq-auto-compile) + +(defcustom coq-load-path-include-current t + "If `t' let coqdep search the current directory too. +Should be `t' for normal users. If `t' pass \"-I dir\" to coqdep when +processing files in directory \"dir\" in addition to any entries +in `coq-load-path'." :type 'boolean :safe 'booleanp :group 'coq-auto-compile) @@ -1322,24 +1366,14 @@ that dependency checking takes noticeable time." :safe '(lambda (v) (every 'stringp v)) :group 'coq-auto-compile) -(defcustom coq-load-path nil - "Non-standard coq library load path. -List of directories to be added to the LoadPath of coqdep, coqc -and coqtop. Under normal circumstances this list does not need to -contain the coq standard library or \".\" for the current -directory (see `coq-load-path-include-current'). - -Elements of this list should be strings, which are passed as -\"-I\" options over the command line to coqdep, coqc and coqtop." - :type '(repeat string) - :safe '(lambda (v) (every 'stringp v)) - :group 'coq-auto-compile) +(defcustom coq-compile-ignore-library-directory t + "If non-nil, ProofGeneral does not compile modules from the coq library. +Should be `t' for normal coq users. If `nil' library modules are +compiled if their sources are newer. -(defcustom coq-load-path-include-current t - "If `t' let coqdep search the current directory too. -Should be `t' for normal users. If `t' pass \"-I dir\" to coqdep when -processing files in directory \"dir\" in addition to any entries -in `coq-load-path'." +This option has currently no effect, because Proof General uses +coqdep to translate qualified identifiers into library file names +and coqdep does not output dependencies in the standard library." :type 'boolean :safe 'booleanp :group 'coq-auto-compile) @@ -1471,20 +1505,37 @@ is up-to-date." Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"." (substring lib-obj-file 0 (- (length lib-obj-file) 1))) +(defun coq-option-of-load-path-entry (entry) + "Translate a single element from `coq-load-path' into options. +See `coq-load-path' for the possible forms of entry and to which +options they are translated." + (cond + ((stringp entry) + (list "-I" (expand-file-name entry))) + ((eq (car entry) 'nonrec) + (list "-I" (expand-file-name (nth 1 entry)) "-as" (nth 2 entry))) + (t + (if (eq (car entry) 'rec) + (setq entry (cdr entry))) + (if (nth 1 entry) + (list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry)) + (list "-R" (expand-file-name (car entry))))))) + (defun coq-include-options (file) - "Build a -I options list for coqc and coqdep. -The options list includes all directories from `coq-load-path' and, -if `coq-load-path-include-current' is enabled, the directory base of FILE. -The resulting list is fresh for every call, callers can append more -arguments with `nconc'. + "Build the list of include options for coqc, coqdep and coqtop. +The options list includes all entries from `coq-load-path' +prefixed with suitable options and, if +`coq-load-path-include-current' is enabled, the directory base of +FILE. The resulting list is fresh for every call, callers can +append more arguments with `nconc'. FILE should be an absolute file name. It can be nil if `coq-load-path-include-current' is nil." (let ((result nil)) (when coq-load-path - (setq result (list "-I" (expand-file-name (car coq-load-path)))) - (dolist (dir (cdr coq-load-path)) - (nconc result (list "-I" (expand-file-name dir))))) + (setq result (coq-option-of-load-path-entry (car coq-load-path))) + (dolist (entry (cdr coq-load-path)) + (nconc result (coq-option-of-load-path-entry entry)))) (if coq-load-path-include-current (setq result (cons "-I" (cons (file-name-directory file) result)))) diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index fe516973..0f8a1047 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3409,7 +3409,7 @@ restarting the process. Function run when a proof-shell buffer is killed.@* Try to shut down the proof process nicely and clear locked regions and state variables. Value for @samp{@code{kill-buffer-hook}} in -shell buffer, alled by @samp{@code{proof-shell-bail-out}} if process exits. +shell buffer, called by @samp{@code{proof-shell-bail-out}} if process exits. @end defun @c TEXI DOCSTRING MAGIC: proof-shell-exit @@ -3424,6 +3424,10 @@ without confirmation. The kill function uses @samp{<PA>-quit-timeout} as a timeout to wait after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process. + +This function should not be called if +@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of +@samp{@code{proof-shell-kill-function}} will give strange errors. @end deffn @c TEXI DOCSTRING MAGIC: proof-shell-bail-out diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index bade2ed4..ef6e0fb3 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1636,6 +1636,10 @@ without confirmation. The kill function uses @samp{<PA>-quit-timeout} as a timeout to wait after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process. + +This function should not be called if +@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of +@samp{@code{proof-shell-kill-function}} will give strange errors. @end deffn @c TEXI DOCSTRING MAGIC: proof-shell-restart @@ -4053,6 +4057,12 @@ Nonstandard load path elements @emph{must} be configured in the option @code{coq-load-path}. @code{-I} options in @code{coq-prog-name} or @code{coq-prog-args} must be deleted. @item +In @code{coq-load-path} use strings @code{"dir"} for @code{-I} +options and lists of two strings @code{("dir" "path")} for +@code{-R "dir" -as "path"} (for more details see the +documentation of `coq-load-path' or @ref{Customizing Coq Multiple +File Support}). +@item For a nonstandard compilation procedure and limited ML module support, @code{coq-compile-command} can be set to an external compilation command. For standard dependency analysis with @@ -4202,6 +4212,76 @@ This option can be set/reset via menu @end defvar +@c TEXI DOCSTRING MAGIC: coq-compile-auto-save +@defvar coq-compile-auto-save +Buffers to save before checking dependencies for compilation.@* +There are two orthogonal choices: Firstly one can save all or only the coq +buffers, where coq buffers means all buffers in coq mode except the current +buffer. Secondly, Emacs can ask about each such buffer or save all of them +unconditionally. + +This makes four permitted values: @code{'ask-coq} to confirm saving all +modified Coq buffers, @code{'ask-all} to confirm saving all modified +buffers, @code{'save-coq} to save all modified Coq buffers without +confirmation and @code{'save-all} to save all modified buffers without +confirmation. +@end defvar + + +The following two options deal with the load path. Proof General +divides the load path into the standard load path (which is +hardwired in the tools and need not be set explicitly), the +nonstandard load path (which must always be set explicitly), and +the current directory (which must be set explicitly for +@code{coqdep}). The option @code{coq-load-path} determines the +nonstandard load path and @code{coq-load-path-include-current} +determines whether the current directory is put into the load +path of @code{coqdep}. + +@c TEXI DOCSTRING MAGIC: coq-load-path +@defvar coq-load-path +Non-standard coq library load path.@* +This list specifies the LoadPath extension for coqdep, coqc and +coqtop. Usually, the elements of this list are strings (for +"-I") or lists of two strings (for "-R" dir "-as" path). + +The possible forms of elements of this list correspond to the 4 +possible forms of the Add LoadPath command and the 4 forms of the +include options ('-I' and @code{'-R'}). An element can be +@lisp + - A string, specifying a directory to be mapped to the empty + logical path ('-I'). + - A list of the form '(rec dir path)' (where dir and path are + strings) specifying a directory to be recursively mapped to the + logical path @code{'path'} ('-R dir -as path'). + - A list of the form '(rec dir)', specifying a directory to be + recursively mapped to the empty logical path ('-R dir'). + - A list of the form '(norec dir path)', specifying a directory + to be mapped to the logical path @code{'path'} ('-I dir -as path'). +@end lisp +For convenience the symbol @code{'rec'} can be omitted and entries of +the form '(dir)' and '(dir path)' are interpreted as '(rec dir) +and '(rec dir path)', respectively. + +Under normal circumstances this list does not need to +contain the coq standard library or "." for the current +directory (see @samp{@code{coq-load-path-include-current}}). +@end defvar + + +@c TEXI DOCSTRING MAGIC: coq-load-path-include-current +@defvar coq-load-path-include-current +If @samp{t} let coqdep search the current directory too.@* +Should be @samp{t} for normal users. If @samp{t} pass "-I dir" to coqdep when +processing files in directory "dir" in addition to any entries +in @samp{@code{coq-load-path}}. +@end defvar + + +The following two options configure an external compilation +process. + + @c TEXI DOCSTRING MAGIC: coq-compile-command @defvar coq-compile-command External compilation command. If empty ProofGeneral compiles itself.@* @@ -4240,21 +4320,7 @@ This option can be set/reset via menu @end defvar -@c TEXI DOCSTRING MAGIC: coq-compile-auto-save -@defvar coq-compile-auto-save -Buffers to save before checking dependencies for compilation.@* -There are two orthogonal choices: Firstly one can save all or only the coq -buffers, where coq buffers means all buffers in coq mode except the current -buffer. Secondly, Emacs can ask about each such buffer or save all of them -unconditionally. - -This makes four permitted values: @code{'ask-coq} to confirm saving all -modified Coq buffers, @code{'ask-all} to confirm saving all modified -buffers, @code{'save-coq} to save all modified Coq buffers without -confirmation and @code{'save-all} to save all modified buffers without -confirmation. -@end defvar - +Locking ancestors can be disabled with the following option. @c TEXI DOCSTRING MAGIC: coq-lock-ancestors @defvar coq-lock-ancestors @@ -4265,38 +4331,6 @@ locked when the "Require" command is processed. @end defvar -The following two options deal with the load path. Proof General -divides the load path into the standard load path (which is -hardwired in the tools and need not be set explicitly), the -nonstandard load path (which must always be set explicitly), and -the current directory (which must be set explicitly for -@code{coqdep}). The option @code{coq-load-path} determines the -nonstandard load path and @code{coq-load-path-include-current} -determines whether the current directory is put into the load -path of @code{coqdep}. - -@c TEXI DOCSTRING MAGIC: coq-load-path -@defvar coq-load-path -Non-standard coq library load path.@* -List of directories to be added to the LoadPath of coqdep, coqc -and coqtop. Under normal circumstances this list does not need to -contain the coq standard library or "." for the current -directory (see @samp{@code{coq-load-path-include-current}}). - -Elements of this list should be strings, which are passed as -"-I" options over the command line to coqdep, coqc and coqtop. -@end defvar - - -@c TEXI DOCSTRING MAGIC: coq-load-path-include-current -@defvar coq-load-path-include-current -If @samp{t} let coqdep search the current directory too.@* -Should be @samp{t} for normal users. If @samp{t} pass "-I dir" to coqdep when -processing files in directory "dir" in addition to any entries -in @samp{@code{coq-load-path}}. -@end defvar - - The following two options do only influence the behaviour if Proof General does dependency checking and compilation itself. These options determine whether Proof General should descend into |