diff options
author | Hendrik Tews <hendrik@askra.de> | 2012-10-30 21:05:53 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2012-10-30 21:05:53 +0000 |
commit | bb232c2828132ddde9285bf368c8f16e54b1da36 (patch) | |
tree | b571b88a12551f615ddde6598124a5a863f4efcb /coq/coq-compile-common.el | |
parent | ad142b89511bc01fff26bae8073f6c362d913d71 (diff) |
move general part of compilation into coq-compile-common.el
Diffstat (limited to 'coq/coq-compile-common.el')
-rw-r--r-- | coq/coq-compile-common.el | 384 |
1 files changed, 384 insertions, 0 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el new file mode 100644 index 00000000..bc7cf03f --- /dev/null +++ b/coq/coq-compile-common.el @@ -0,0 +1,384 @@ +;; coq-compile-common.el --- common part of compilation feature +;; Copyright (C) 1994-2012 LFCS Edinburgh. +;; Authors: Hendrik Tews +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Hendrik Tews <hendrik@askra.de> +;; +;; $Id$ +;; +;;; Commentary: +;; +;; This file holds constants, options and some general functions for +;; the compilation feature. +;; + + +(require 'proof-shell) + +(eval-when (compile) + (defvar coq-confirm-external-compilation nil); defpacustom + (proof-ready-for-assistant 'coq)) ; compile for coq + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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-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-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)))) + + +(provide 'coq-compile-common) + + + +;; Local Variables: *** +;; coding: utf-8 *** +;; End: *** + +;;; coq-compile-common.el ends here |