From bb232c2828132ddde9285bf368c8f16e54b1da36 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 30 Oct 2012 21:05:53 +0000 Subject: move general part of compilation into coq-compile-common.el --- coq/coq-seq-compile.el | 353 +------------------------------------------------ 1 file changed, 2 insertions(+), 351 deletions(-) (limited to 'coq/coq-seq-compile.el') diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 5a8a157d..d7b50f8c 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -19,330 +19,17 @@ (require 'proof-compat)) (eval-when (compile) - (require 'proof-shell) (defvar queueitems nil) ; dynamic scope in p-s-extend-queue-hook (defvar coq-compile-before-require nil) ; defpacustom - (defvar coq-confirm-external-compilation nil); defpacustom - (proof-ready-for-assistant 'coq)) ; compile for coq + (defvar coq-confirm-external-compilation nil)); defpacustom +(require 'coq-compile-common) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Multiple file handling -- sequential compilation of required modules ;; -;; constants - -(defun get-coq-library-directory () - (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 ))) - (if (string-match c "not found") - "/usr/local/lib/coq" - c))) - -(defconst coq-library-directory (get-coq-library-directory) - "The coq library directory, as reported by \"coqtop -where\".") - -(defcustom coq-dependency-analyzer - (proof-locate-executable "coqdep" t nil) - "Command to invoke coqdep." - :type 'string - :group 'coq) - -(defcustom coq-compiler - (proof-locate-executable "coqc" t nil) - "Command to invoke the coq compiler." - :type 'string - :group 'coq) - - -;; user options and variables - -(defgroup coq-auto-compile () - "Customization for automatic compilation of required files" - :group 'coq - :package-version '(ProofGeneral . "4.1")) - -(defpacustom compile-before-require nil - "If non-nil, check dependencies of required modules and compile if necessary. -If non-nil ProofGeneral intercepts \"Require\" commands and checks if the -required library module and its dependencies are up-to-date. If not, they -are compiled from the sources before the \"Require\" command is processed. - -This option can be set/reset via menu -`Coq -> Settings -> Compile Before Require'." - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - -(defcustom coq-compile-command "" - "External compilation command. If empty ProofGeneral compiles itself. -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 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. - -After the substitution the command can be changed in the -minibuffer if `coq-confirm-external-compilation' is t." - :type 'string - :safe (lambda (v) - (and (stringp v) - (or (not (boundp 'coq-confirm-external-compilation)) - coq-confirm-external-compilation))) - :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'. -Value must be a list of substitutions, where each substitution is -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, '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-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 3 -forms of 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 '(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 path)' are interpreted as '(rec dir path)'. - -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 with path (-R ... -as ...)" - (const rec) - (string :tag "directory") - (string :tag "log path")) - (list :tag - "simple directory with path (-I ... -as ...)" - (const nonrec) - (string :tag "directory") - (string :tag "log path")))) - :safe 'coq-load-path-safep - :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 -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: 'ask-coq to confirm saving all -modified Coq buffers, 'ask-all to confirm saving all modified -buffers, 'save-coq to save all modified Coq buffers without -confirmation and 'save-all to save all modified buffers without -confirmation." - :type - '(radio - (const :tag "ask for each coq-mode buffer, except the current buffer" - ask-coq) - (const :tag "ask for all buffers" ask-all) - (const - :tag - "save all coq-mode buffers except the current buffer without confirmation" - save-coq) - (const :tag "save all buffers without confirmation" save-all)) - :safe (lambda (v) (member v '(ask-coq ask-all save-coq save-all))) - :group 'coq-auto-compile) - -(defcustom coq-lock-ancestors t - "If non-nil, lock ancestor module files. -If external compilation is used (via `coq-compile-command') then -only the direct ancestors are locked. Otherwise all ancestors are -locked when the \"Require\" command is processed." - :type 'boolean - :safe 'booleanp - :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) - -(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) - -(defcustom coq-compile-ignored-directories nil - "Directories in which ProofGeneral should not compile modules. -List of regular expressions for directories in which ProofGeneral -should not compile modules. If a library file name matches one -of the regular expressions in this list then ProofGeneral does -neither compile this file nor check its dependencies for -compilation. It makes sense to include non-standard coq library -directories here if they are not changed and if they are so big -that dependency checking takes noticeable time." - :type '(repeat regexp) - :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. - -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) - -(defcustom coq-coqdep-error-regexp - (concat "^\\*\\*\\* Warning: in file .*, library .* is required " - "and has not been found") - "Regexp to match errors in the output of coqdep. -coqdep indicates errors not always via a non-zero exit status, -but sometimes only via printing warnings. This regular expression -is used for recognizing error conditions in the output of -coqdep (when coqdep terminates with exit status 0). Its default -value matches the warning that some required library cannot be -found on the load path and ignores the warning for finding a -library at multiple places in the load path. If you want to turn -the latter condition into an error, then set this variable to -\"^\\*\\*\\* Warning\"." - :type 'string - :safe 'stringp - :group 'coq-auto-compile) - -(defconst coq-require-command-regexp - "^Require[ \t\n]+\\(Import\\|Export\\)?[ \t\n]*" - "Regular expression matching Require commands in Coq. -Should match \"Require\" with its import and export variants up to (but not -including) the first character of the first required module. The required -modules are matched separately with `coq-require-id-regexp'") - -(defconst coq-require-id-regexp - "[ \t\n]*\\([A-Za-z0-9_']+\\(\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*" - "Regular expression matching one Coq module identifier. -Should match precisely one complete module identifier and surrounding -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.") - -(defvar coq-compile-response-buffer "*coq-compile-response*" - "Name of the buffer to display error messages from coqc and coqdep.") - - -(defvar coq-debug-auto-compilation nil - "*Display more messages during compilation") - - -;; basic utilities - -(defun time-less-or-equal (time-1 time-2) - "Return `t' if time value time-1 is earlier or equal to time-2. -A time value is a list of two integers as returned by `file-attributes'. -The first integer contains the upper 16 bits and the second the lower -16 bits of the time." - (or (time-less-p time-1 time-2) - (equal time-1 time-2))) - -(defun coq-max-dep-mod-time (dep-mod-times) - "Return the maximum in DEP-MOD-TIMES. -Argument DEP-MOD-TIMES is a list where each element is either a -time value (see `time-less-or-equal') or 'just-compiled. The -function returns the maximum of the elements in DEP-MOD-TIMES, -where 'just-compiled is considered the greatest time value. If -DEP-MOD-TIMES is empty it returns nil." - (let ((max nil)) - (while dep-mod-times - (cond - ((eq (car dep-mod-times) 'just-compiled) - (setq max 'just-compiled - dep-mod-times nil)) - ((eq max nil) - (setq max (car dep-mod-times))) - ((time-less-p max (car dep-mod-times)) - (setq max (car dep-mod-times)))) - (setq dep-mod-times (cdr-safe dep-mod-times))) - max)) - - -;; safety predicate for coq-load-path - -(defun coq-load-path-safep (path) - "Check if PATH is a safe value for `coq-load-path'." - (and - (listp path) - (every - (lambda (entry) - (or (stringp entry) - (and (listp entry) - (eq (car entry) 'rec) - (every 'stringp (cdr entry)) - (equal (length entry) 3)) - (and (listp entry) - (eq (car entry) 'nonrec) - (every 'stringp (cdr entry)) - (equal (length entry) 3)) - (and (listp entry) - (every 'stringp entry) - (equal (length entry) 2)))) - path))) - -;; Compute command line for starting coqtop - -(defun coq-prog-args () - ;; coqtop always adds the current directory to the LoadPath, so don't - ;; include it in the -I options. - (let ((coq-load-path-include-current nil)) - (append coq-prog-args (coq-include-options nil)))) - - ;; ancestor (un-)locking (defun coq-lock-ancestor (span ancestor-src) @@ -404,42 +91,6 @@ 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))) - (list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry))))) - -(defun coq-include-options (file) - "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)) - (unless (coq-load-path-safep coq-load-path) - (error "Invalid value in coq-load-path")) - (when coq-load-path - (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)))) - result)) - (defun coq-init-compile-response-buffer (command) "Initialize the buffer for the compilation output. If `coq-compile-response-buffer' exists, empty it. Otherwise -- cgit v1.2.3