diff options
Diffstat (limited to 'coq/coq-system.el')
| -rw-r--r-- | coq/coq-system.el | 140 |
1 files changed, 78 insertions, 62 deletions
diff --git a/coq/coq-system.el b/coq/coq-system.el index aad7d386..63ee57ac 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -1,30 +1,49 @@ -;; coq-system.el --- common part of compilation feature -;; Copyright (C) 2015 LFCS Edinburgh. +;;; coq-system.el --- common part of compilation feature + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Hendrik Tews, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre.Courtieu<Pierre.Courtieu@cnam.fr> -;; + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: ;; ;; This file holds constants, options and some general functions for -;; setting coq command arguments. Some code is dedicated as a light +;; setting coq command arguments. Some code is dedicated as a light ;; support for older versions of coq. ;; +;;; Code: + (require 'proof) (eval-when-compile (require 'cl) - (require 'proof-compat) - (proof-ready-for-assistant 'coq)) + (require 'proof-compat)) + +(eval-when-compile + (defvar coq-prog-args) + (defvar coq-debug)) + +;; Arbitrary arguments can already be passed through _CoqProject. +;; However this is not true for all assistants, so we don't modify the +;; (defpgcustom prog-args) declaration. +(defun coq--string-list-p (obj) + "Determine if OBJ is a list of strings." + (or (null obj) (and (consp obj) (stringp (car obj)) (coq--string-list-p (cdr obj))))) -(eval-when (compile) - (defvar coq-prog-args nil) - (defvar coq-debug nil)) +(put 'coq-prog-args 'safe-local-variable #'coq--string-list-p) (defcustom coq-prog-env nil - "List of environment settings d to pass to Coq process. + "List of environment settings to pass to Coq process. On Windows you might need something like: (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))" :group 'coq) @@ -32,12 +51,12 @@ On Windows you might need something like: (defcustom coq-prog-name (if (executable-find "coqtop") "coqtop" (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))) - "*Name of program to run as Coq. See `proof-prog-name', set from this. + "*Name of program to run as Coq. See `proof-prog-name', set from this. On Windows with latest Coq package you might need something like: C:/Program Files/Coq/bin/coqtop.opt.exe instead of just \"coqtop\". -This must be a single program name with no arguments; see `coq-prog-args' -to manually adjust the arguments to the Coq process. +This must be a single program name with no arguments. See option +`coq-prog-args' to manually adjust the arguments to the Coq process. See also `coq-prog-env' to adjust the environment." :type 'string :group 'coq) @@ -75,8 +94,8 @@ See also `coq-prog-env' to adjust the environment." (defcustom coq-pinned-version nil "Which version of Coq you are using. There should be no need to set this value unless you use the trunk from -the Coq github repository. For Coq versions with decent version numbers -Proof General detects the version automatically and adjusts itself. This +the Coq github repository. For Coq versions with decent version numbers +Proof General detects the version automatically and adjusts itself. This variable should contain nil or a version string." :type 'string :group 'coq) @@ -226,12 +245,12 @@ Set to t if you want this feature, but note that it is deprecated." (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 +coqtop. Usually, the elements of this list are strings (for \"-I\") or lists of two strings (for \"-R\" dir path and \"-Q\" dir path). The possible forms of elements of this list correspond to the 4 -forms of include options (`-I' `-Q' and `-R'). An element can be +forms of include options (`-I' `-Q' and `-R'). An element can be - A list of the form `(\\='ocamlimport dir)', specifying (in 8.5) a directory to be added to ocaml path (`-I'). @@ -284,10 +303,10 @@ not the same (-I is for coq path)." (make-variable-buffer-local 'coq-load-path) (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 -Q dir \"\" to coqdep when -processing files in directory \"dir\" in addition to any entries -in `coq-load-path'. + "If t, let coqdep search the current directory too. +Should be t for normal users. If t, pass -Q dir \"\" to coqdep when +processing files in directory \"dir\" in addition to any entries in +`coq-load-path'. This setting is only relevant with Coq < 8.5." :type 'boolean @@ -323,9 +342,9 @@ request compatibility handling of flags." ((or `(rec ,dir ,alias) `(,dir ,alias)) (list "-R" (expand-file-name dir) alias))))) -(defun coq-include-options (load-path &optional current-directory pre-v85) +(defun coq-include-options (loadpath &optional current-directory pre-v85) "Build the base list of include options for coqc, coqdep and coqtop. -The options list includes all entries from argument LOAD-PATH +The options list includes all entries from argument LOADPATH \(which should be `coq-load-path' of the buffer that invoked the compilation) prefixed with suitable options and (for coq<8.5), if `coq-load-path-include-current' is enabled, the directory base of @@ -336,12 +355,12 @@ CURRENT-DIRECTORY should be an absolute directory name. It can be nil if `coq-load-path-include-current' is nil. A non-nil PRE-V85 flag requests compatibility handling of flags." - (unless (coq-load-path-safep load-path) + (unless (coq-load-path-safep loadpath) (error "Invalid value in coq-load-path")) (when (and pre-v85 coq-load-path-include-current) (cl-assert current-directory) - (push current-directory load-path)) - (cl-loop for entry in load-path + (push current-directory loadpath)) + (cl-loop for entry in loadpath append (coq-option-of-load-path-entry entry pre-v85))) (defun coq--options-test-roundtrip-1 (coq-project parsed pre-v85) @@ -375,31 +394,31 @@ options of a few coq-project files does the right thing." (coq--options-test-roundtrip "-R /test Test") (coq--options-test-roundtrip "-I /test"))) -(defun coq-coqdep-prog-args (load-path &optional current-directory pre-v85) +(defun coq-coqdep-prog-args (loadpath &optional current-directory pre-v85) "Build a list of options for coqdep. -LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." - (coq-include-options load-path current-directory pre-v85)) +LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." + (coq-include-options loadpath current-directory pre-v85)) -(defun coq-coqc-prog-args (load-path &optional current-directory pre-v85) +(defun coq-coqc-prog-args (loadpath &optional current-directory pre-v85) "Build a list of options for coqc. -LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." +LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." ;; coqtop always adds the current directory to the LoadPath, so don't ;; include it in the -Q options. - (append (remove "-emacs" (remove "-emacs-U" coq-prog-args)) + (append (remove "-emacs" coq-prog-args) (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3 - (coq-coqdep-prog-args coq-load-path current-directory pre-v85)))) + (coq-coqdep-prog-args loadpath current-directory pre-v85)))) ;;XXXXXXXXXXXXXX ;; coq-coqtop-prog-args is the user-set list of arguments to pass to ;; Coq process, see 'defpacustom prog-args' in pg-custom.el for ;; documentation. -(defun coq-coqtop-prog-args (load-path &optional current-directory pre-v85) +(defun coq-coqtop-prog-args (loadpath &optional current-directory pre-v85) ;; coqtop always adds the current directory to the LoadPath, so don't ;; include it in the -Q options. This is not true for coqdep. "Build a list of options for coqc. -LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." - (cons "-emacs" (coq-coqc-prog-args load-path current-directory pre-v85))) +LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." + (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85))) (defun coq-prog-args () "Recompute `coq-load-path' before calling `coq-coqtop-prog-args'." @@ -408,8 +427,8 @@ LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." (coq-coqtop-prog-args coq-load-path)) (defcustom coq-use-project-file t - "If t, when opening a coq file read the dominating _CoqProject. -If t, when a coq file is opened, Proof General will look for a + "If t, when opening a Coq file read the dominating _CoqProject. +If t, when a Coq file is opened, Proof General will look for a project file (see `coq-project-filename') somewhere in the current directory or its parent directories. If there is one, its contents are read and used to determine the arguments that @@ -421,17 +440,16 @@ path (including the -R lib options) (see `coq-load-path')." (defcustom coq-project-filename "_CoqProject" "The name of coq project file. -The coq project file of a coq developpement (Cf Coq documentation -on \"makefile generation\") should contain the arguments given to +The coq project file of a coq developpement (cf. Coq documentation on +\"makefile generation\") should contain the arguments given to coq_makefile. In particular it contains the -I and -R -options (preferably one per line). If `coq-use-coqproject' is -t (default) the content of this file will be used by proofgeneral -to infer the `coq-load-path' and the `coq-prog-args' variables -that set the coqtop invocation by proofgeneral. This is now the -recommended way of configuring the coqtop invocation. Local file -variables may still be used to override the coq project file's -configuration. .dir-locals.el files also work and override -project file settings." +options (preferably one per line). If `coq-use-coqproject' is +t (default) the content of this file will be used by proofgeneral to +infer the `coq-load-path' and the `coq-prog-args' variables that set +the coqtop invocation by proofgeneral. This is now the recommended +way of configuring the coqtop invocation. Local file variables may +still be used to override the coq project file's configuration. +.dir-locals.el files also work and override project file settings." :type 'string :safe 'stringp :group 'coq) @@ -481,7 +499,7 @@ Returns a mixed list of option-value pairs and strings." (arity (cdr (assoc switch coq--makefile-switch-arities)))) (push (coq--read-one-option-from-project-file switch arity raw-args) options) (setq raw-args (nthcdr (or arity 0) raw-args)))) - options)) + (nreverse options))) ; Order of options is important sometimes (Cf. #7980) (defun coq--extract-prog-args (options) "Extract coqtop arguments from _CoqProject options OPTIONS. @@ -550,12 +568,10 @@ variable." (defun coq-load-project-file () "Set `coq-prog-args' and `coq-load-path' according to _CoqProject file. -Obeys `coq-use-project-file'. Note that if a variable is already -set by dir/file local variables, this function will not override -its value. -See `coq-project-filename' to change the name of the -project file, and `coq-use-project-file' to disable this -feature." +Obeys `coq-use-project-file'. Note that if a variable is already set +by dir/file local variables, this function will not override its value. +See `coq-project-filename' to change the name of the project file, and +`coq-use-project-file' to disable this feature." (when coq-use-project-file ;; Let us reread dir/file local vars, in case the user mmodified them (let* ((oldargs (assoc 'coq-prog-args file-local-variables-alist)) @@ -622,11 +638,11 @@ Does nothing if `coq-use-project-file' is nil." ;; OBSOLETE, should take _CoqProject into account. (defun coq-guess-command-line (filename) "Guess the right command line options to compile FILENAME using `make -n'. -This function is obsolete, the recommended way of setting the -coqtop options is to use a _Coqproject file as described in coq -documentation. ProofGeneral reads this file and sets compilation -options according to its contents. See `coq-project-filename'. Per file configuration may -then be set using local file variables." +This function is obsolete, the recommended way of setting the coqtop +options is to use a _Coqproject file as described in coq +documentation. ProofGeneral reads this file and sets compilation +options according to its contents. See `coq-project-filename'. Per +file configuration may then be set using local file variables." (if (local-variable-p 'coq-prog-name (current-buffer)) coq-prog-name (let* ((dir (or (file-name-directory filename) ".")) @@ -655,7 +671,7 @@ then be set using local file variables." (setq coq-prog-args nil) (concat (substring command 0 (string-match " [^ ]*$" command)) - "-emacs-U")) + "-emacs")) coq-prog-name)))) ;;; coq-system.el ends here |