From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tools/README.emacs | 4 +- tools/beautify-archive | 4 +- tools/compat5.ml | 2 +- tools/compat5.mlp | 2 +- tools/compat5b.ml | 2 +- tools/compat5b.mlp | 2 +- tools/coq-db.el | 240 ----------- tools/coq-font-lock.el | 12 +- tools/coq-inferior.el | 6 +- tools/coq-syntax.el | 977 ------------------------------------------- tools/coq.el | 142 ------- tools/coq_makefile.ml | 543 ++++++++++++++---------- tools/coq_tex.ml | 20 +- tools/coqc.ml | 184 +++++++++ tools/coqdep.ml | 345 +++++++++++++++- tools/coqdep_boot.ml | 15 +- tools/coqdep_common.ml | 114 +++-- tools/coqdep_common.mli | 19 +- tools/coqdep_lexer.mli | 2 +- tools/coqdep_lexer.mll | 101 +++-- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 22 +- tools/coqdoc/coqdoc.css | 63 ++- tools/coqdoc/coqdoc.sty | 2 +- tools/coqdoc/cpretty.mli | 4 +- tools/coqdoc/cpretty.mll | 60 ++- tools/coqdoc/index.ml | 44 +- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 9 +- tools/coqdoc/output.ml | 92 +++-- tools/coqdoc/output.mli | 5 +- tools/coqdoc/tokens.ml | 9 +- tools/coqdoc/tokens.mli | 2 +- tools/coqmktop.ml | 306 ++++++++++++++ tools/coqwc.mll | 19 +- tools/coqworkmgr.ml | 222 ++++++++++ tools/escape_string.ml | 1 - tools/fake_ide.ml | 375 ++++++++++++++--- tools/gallina-db.el | 240 +++++++++++ tools/gallina-syntax.el | 982 ++++++++++++++++++++++++++++++++++++++++++++ tools/gallina.el | 142 +++++++ tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 3 +- tools/mingwpath.ml | 15 - tools/update-require | 103 +++++ tools/win32hack.mllib | 1 - tools/win32hack_filename.ml | 4 - 48 files changed, 3534 insertions(+), 1935 deletions(-) delete mode 100644 tools/coq-db.el delete mode 100644 tools/coq-syntax.el delete mode 100644 tools/coq.el create mode 100644 tools/coqc.ml create mode 100644 tools/coqmktop.ml create mode 100644 tools/coqworkmgr.ml delete mode 100644 tools/escape_string.ml create mode 100644 tools/gallina-db.el create mode 100644 tools/gallina-syntax.el create mode 100644 tools/gallina.el delete mode 100644 tools/mingwpath.ml create mode 100755 tools/update-require delete mode 100644 tools/win32hack.mllib delete mode 100644 tools/win32hack_filename.ml (limited to 'tools') diff --git a/tools/README.emacs b/tools/README.emacs index 0d27b607..4d8e3697 100755 --- a/tools/README.emacs +++ b/tools/README.emacs @@ -10,14 +10,14 @@ Jean-Christophe Filliatre (jcfillia@lri.fr), CONTENTS: - coq.el A major mode for editing Coq files in Gnu Emacs + gallina.el A major mode for editing Coq files in Gnu Emacs USAGE: Add the following lines to your .emacs file: (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) +(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) The Coq major mode is triggered by visiting a file with extension .v, or manually by M-x coq-mode. It gives you the correct syntax table for diff --git a/tools/beautify-archive b/tools/beautify-archive index ccfeb3db..6bfa974a 100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -30,7 +30,7 @@ beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX` for i in $beaufiles; do j=`dirname $i`/`basename $i .v$BEAUTIFYSUFFIX`.v echo Upgrading $j in the beautification directory - mv -u -f $i $j + if [ $i -nt $j ]; then mv -f $i $j; fi done echo ---- Recompiling beautified files in the beautification directory ----- make clean @@ -44,7 +44,7 @@ vfiles=`find . -name \*.v` cd .. for i in $vfiles; do echo Upgrading $i in current directory - mv -u -f $NEWARCHIVE/$i $i + if [ $NEWARCHIVE/$i -nt $i ]; then mv -f $NEWARCHIVE/$i $i; fi done echo -------- Beautification completed ------------------------------------- echo Old files are in directory '"'$OLDARCHIVE'"' diff --git a/tools/compat5.ml b/tools/compat5.ml index 11520c23..041ced00 100644 --- a/tools/compat5.ml +++ b/tools/compat5.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; - -;;; We store all information on keywords (tactics or command) in big -;; tables (ex: `coq-tactics-db') From there we get: menus including -;; "smart" commands, completions for command coq-insert-... -;; abbrev tables and font-lock keyword - -;;; real value defined below - -;;; Commentary: -;; - -;;; Code: - -;(require 'proof-config) ; for proof-face-specs, a macro -;(require 'holes) - -(defconst coq-syntax-db nil - "Documentation-only variable, for coq keyword databases. -Each element of a keyword database contains the definition of a \"form\", of the -form: - -(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE) - -MENUNAME is the name of form (or form variant) as it should appear in menus or -completion lists. - -ABBREV is the abbreviation for completion via \\[expand-abbrev]. - -INSERT is the complete text of the form, which may contain holes denoted by -\"#\" or \"@{xxx}\". - -If non-nil the optional STATECH specifies that the command is not state -preserving for coq. - -If non-nil the optional KWREG is the regexp to colorize correponding to the -keyword. ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\"). -*WARNING*: A regexp longer than another one should be put FIRST. For example: - - (\"Module Type\" ... ... t \"Module\\s-+Type\") - (\"Module\" ... ... t \"Module\") - -Is ok because the longer regexp is recognized first. - -If non-nil the optional INSERT-FUN is the function to be called when inserting -the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This -allows to write functions asking for more information to assist the user. - -If non-nil the optional HIDE specifies that this form should not appear in the -menu but only in interactive completions. - -Example of what could be in your emacs init file: - -(defvar coq-user-tactics-db - '( - (\"mytac\" \"mt\" \"mytac # #\" t \"mytac\") - (\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\") - )) - -Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, -will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a -new keyword to colorize." ) - -(defun coq-insert-from-db (db prompt) - "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion function is -present for the keyword, call it instead. see `coq-syntax-db' for DB -structure." - (let* ((tac (completing-read (concat prompt " (tab for completion) : ") - db nil nil)) - (infos (cddr (assoc tac db))) - (s (car infos)) ; completion to insert - (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function - (pt (point))) - (if f (funcall f) ; call f if present - (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt) - (indent-according-to-mode)))) - - - -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) - -;; Computes the max length of strings in a list -(defun max-length-db (db) - "Return the length of the longest first element (menu label) of DB. -See `coq-syntax-db' for DB structure." - (let ((l db) (res 0)) - (while l - (let ((lgth (length (car (car l))))) - (setq res (max lgth res)) - (setq l (cdr l)))) - res)) - - - -(defun coq-build-menu-from-db-internal (db lgth menuwidth) - "Take a keyword database DB and return one insertion submenu. -Argument LGTH is the max size of the submenu. Argument MENUWIDTH is the width -of the largest line in the menu (without abbrev and shortcut specifications). -Used by `coq-build-menu-from-db', which you should probably use instead. See -`coq-syntax-db' for DB structure." - (let ((l db) (res ()) (size lgth) - (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) - (while (and l (> size 0)) - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - (e6 (car-safe tl5)) ; e6 = function for smart insertion - (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu - (entry-with (max (- menuwidth (length e1)) 0)) - (spaces (make-string entry-with ? )) - ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) - ) - (when (not e7) ;; if not hidden - (let ((menu-entry - (vector - ;; menu entry label - (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) - ;;insertion function if present otherwise insert completion - (if e6 e6 `(holes-insert-and-expand ,e3)) - t))) - (setq res (nconc res (list menu-entry)))));; append *in place* - (setq l tl) - (setq size (- size 1)))) - res)) - - -(defun coq-build-title-menu (db size) - "Build a title for the first submenu of DB, of size SIZE. -Return the string made of the first and the SIZE nth first element of DB, -separated by \"...\". Used by `coq-build-menu-from-db'. See `coq-syntax-db' -for DB structure." - (concat (car-safe (car-safe db)) - " ... " - (car-safe (car-safe (nthcdr (- size 1) db))))) - -(defun coq-sort-menu-entries (menu) - (sort menu - '(lambda (x y) (string< - (downcase (elt x 0)) - (downcase (elt y 0)))))) - -(defun coq-build-menu-from-db (db &optional size) - "Take a keyword database DB and return a list of insertion menus for them. -Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB -structure." - ;; sort is destructive for the list, so copy list before sorting - (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) - (wdth (+ 2 (max-length-db db))) - (sz (or size 30)) (lgth (length l))) - (while l - (if (<= lgth sz) - (setq res ;; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l lgth) - (coq-build-menu-from-db-internal l lgth wdth))))) - (setq res ; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l sz) - (coq-build-menu-from-db-internal l sz wdth)))))) - (setq l (nthcdr sz l)) - (setq lgth (length l))) - res)) - -(defun coq-build-abbrev-table-from-db (db) - "Take a keyword database DB and return an abbrev table. -See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - ) - ;; careful: nconc destructive! - (when e2 - (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) - (setq l tl))) - res)) - - -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - '((t (:background "red"))) - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - - - - -(provide 'coq-db) - -;;; coq-db.el ends here - -;** Local Variables: *** -;** fill-column: 80 *** -;** End: *** diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el index 05618a04..068e6400 100644 --- a/tools/coq-font-lock.el +++ b/tools/coq-font-lock.el @@ -110,18 +110,18 @@ syntax colouring behaviour.") ;;A new face for tactics (defface coq-solve-tactics-face (proof-face-specs - (:foreground "forestgreen" t) ; pour les fonds clairs - (:foreground "forestgreen" t) ; pour les fond foncés - ()) ; pour le noir et blanc + (:foreground "forestgreen" t) ; for bright backgrounds + (:foreground "forestgreen" t) ; for dark backgrounds + ()) ; for black and white "Face for names of closing tactics in proof scripts." :group 'proof-faces) ;;A new face for tactics which fail when they don't kill the current goal (defface coq-solve-tactics-face (proof-face-specs - (:foreground "red" t) ; pour les fonds clairs - (:foreground "red" t) ; pour les fond foncés - ()) ; pour le noir et blanc + (:foreground "red" t) ; for bright backgrounds + (:foreground "red" t) ; for dark backgrounds + ()) ; for black and white "Face for names of closing tactics in proof scripts." :group 'proof-faces) diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el index d4f96a16..b79d97d6 100644 --- a/tools/coq-inferior.el +++ b/tools/coq-inferior.el @@ -46,13 +46,13 @@ ;;; Installation: -;; You need to have coq.el already installed (it comes with the +;; You need to have gallina.el already installed (it comes with the ;; standard Coq distribution) in order to use this code. Put this ;; file somewhere in you load-path and add the following lines in your ;; "~/.emacs": ;; ;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -;; (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) +;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) ;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) ;; (autoload 'run-coq-other-window "inferior-coq" ;; "Run an inferior Coq process in a new window." t) @@ -78,7 +78,7 @@ ;; From -0.0 to 1.0 brought into existence. -(require 'coq) +(require 'gallina) (require 'comint) (setq coq-program-name "coqtop") diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el deleted file mode 100644 index 8630fb3a..00000000 --- a/tools/coq-syntax.el +++ /dev/null @@ -1,977 +0,0 @@ -;; coq-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997-2007 LFCS Edinburgh. -;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu - -;; coq-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp - -;(require 'proof-syntax) -;(require 'proof-utils) ; proof-locate-executable -(require 'coq-db) - - - - ;;; keyword databases - - -(defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for - syntax. It is not necessary to add your own tactics here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your tactics will be colorized by font-lock - - 2 your tactics will be added to the menu and to completion when - calling \\[coq-insert-tactic] - - 3 you may define an abbreviation for your tactic." - - :type '(repeat sexp) - :group 'coq) - - -(defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defvar coq-tactics-db - (append - coq-user-tactics-db - '( - ("absurd " "abs" "absurd " t "absurd") - ("apply" "ap" "apply " t "apply") - ("assert by" "assb" "assert ( # : # ) by #" t "assert") - ("assert" "ass" "assert ( # : # )" t) - ;; ("assumption" "as" "assumption" t "assumption") - ("auto with arith" "awa" "auto with arith" t) - ("auto with" "aw" "auto with @{db}" t) - ("auto" "a" "auto" t "auto") - ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) - ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) - ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) - ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") - ("case" "c" "case " t "case") - ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") - ("change in" "chi" "change # in #" t) - ("change with in" "chwi" "change # with # in #" t) - ("change with" "chw" "change # with" t) - ("change" "ch" "change " t "change") - ("clear" "cl" "clear" t "clear") - ("clearbody" "cl" "clearbody" t "clearbody") - ("cofix" "cof" "cofix" t "cofix") - ("coinduction" "coind" "coinduction" t "coinduction") - ("compare" "cmpa" "compare # #" t "compare") - ("compute" "cmpu" "compute" t "compute") - ;; ("congruence" "cong" "congruence" t "congruence") - ("constructor" "cons" "constructor" t "constructor") - ;; ("contradiction" "contr" "contradiction" t "contradiction") - ("cut" "cut" "cut" t "cut") - ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") - ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") - ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") - ("decompose" "dec" "decompose [#] #" t "decompose") - ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") - ("dependent inversion with" "depinvw" "dependent inversion # with #" t) - ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") - ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t) - ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite") - ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t) - ("destruct as" "desa" "destruct # as #" t) - ("destruct using" "desu" "destruct # using #" t) - ("destruct" "des" "destruct " t "destruct") - ;; ("discriminate" "dis" "discriminate" t "discriminate") - ("discrR" "discrR" "discrR" t "discrR") - ("double induction" "dind" "double induction # #" t "double\\s-+induction") - ("eapply" "eap" "eapply #" t "eapply") - ("eauto with arith" "eawa" "eauto with arith" t) - ("eauto with" "eaw" "eauto with @{db}" t) - ("eauto" "ea" "eauto" t "eauto") - ("econstructor" "econs" "econstructor" t "econstructor") - ("eexists" "eex" "eexists" t "eexists") - ("eleft" "eleft" "eleft" t "eleft") - ("elim using" "elu" "elim # using #" t) - ("elim" "e" "elim #" t "elim") - ("elimtype" "elt" "elimtype" "elimtype") - ("eright" "erig" "eright" "eright") - ("esplit" "esp" "esplit" t "esplit") - ;; ("exact" "exa" "exact" t "exact") - ("exists" "ex" "exists #" t "exists") - ;; ("fail" "fa" "fail" nil) - ;; ("field" "field" "field" t "field") - ("firstorder" "fsto" "firstorder" t "firstorder") - ("firstorder with" "fsto" "firstorder with #" t) - ("firstorder with using" "fsto" "firstorder # with #" t) - ("fold" "fold" "fold #" t "fold") - ;; ("fourier" "four" "fourier" t "fourier") - ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") - ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") - ("generalize" "g" "generalize #" t "generalize") - ("hnf" "hnf" "hnf" t "hnf") - ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id - ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals - ("induction" "ind" "induction #" t "induction") - ("induction using" "indu" "induction # using #" t) - ("injection" "inj" "injection #" t "injection") - ("instantiate" "inst" "instantiate" t "instantiate") - ("intro" "i" "intro" t "intro") - ("intro after" "ia" "intro # after #" t) - ("intros" "is" "intros #" t "intros") - ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) - ("intros until" "isu" "intros until #" t) - ("intuition" "intu" "intuition #" t "intuition") - ("inversion" "inv" "inversion #" t "inversion") - ("inversion in" "invi" "inversion # in #" t) - ("inversion using" "invu" "inversion # using #" t) - ("inversion using in" "invui" "inversion # using # in #" t) - ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") - ("lapply" "lap" "lapply" t "lapply") - ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") - ("left" "left" "left" t "left") - ("linear" "lin" "linear" t "linear") - ("load" "load" "load" t "load") - ("move after" "mov" "move # after #" t "move") - ("omega" "o" "omega" t "omega") - ("pattern" "pat" "pattern" t "pattern") - ("pattern(s)" "pats" "pattern # , #" t) - ("pattern at" "pata" "pattern # at #" t) - ("pose" "po" "pose ( # := # )" t "pose") - ("prolog" "prol" "prolog" t "prolog") - ("quote" "quote" "quote" t "quote") - ("quote []" "quote2" "quote # [#]" t) - ("red" "red" "red" t "red") - ("refine" "ref" "refine" t "refine") - ;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("rename into" "ren" "rename # into #" t "rename") - ("replace with" "rep" "replace # with #" t "replace") - ("replace with in" "repi" "replace # with # in #" t) - ("rewrite <- in" "ri<" "rewrite <- # in #" t) - ("rewrite <-" "r<" "rewrite <- #" t) - ("rewrite in" "ri" "rewrite # in #" t) - ("rewrite" "r" "rewrite #" t "rewrite") - ("right" "rig" "right" t "right") - ;; ("ring" "ring" "ring #" t "ring") - ("set in * |-" "seth" "set ( # := #) in * |-" t) - ("set in *" "set*" "set ( # := #) in *" t) - ("set in |- *" "setg" "set ( # := #) in |- *" t) - ("set in" "seti" "set ( # := #) in #" t) - ("set" "set" "set ( # := #)" t "set") - ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") - ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") - ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") - ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") - ("simpl" "s" "simpl" t "simpl") - ("simpl" "sa" "simpl # at #" t) - ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") - ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") - ("simple induction" "sind" "simple induction" t "simple\\s-+induction") - ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") - ("specialize" "spec" "specialize" t "specialize") - ("split" "sp" "split" t "split") - ("split_Rabs" "spra" "splitRabs" t "split_Rabs") - ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") - ("stepl" "stl" "stepl #" t "stepl") - ("stepl by" "stlb" "stepl # by #" t) - ("stepr" "str" "stepr #" t "stepr") - ("stepr by" "strb" "stepr # by #" t) - ("subst" "su" "subst #" t "subst") - ("symmetry" "sy" "symmetry" t "symmetry") - ("symmetry in" "syi" "symmetry in #" t) - ;; ("tauto" "ta" "tauto" t "tauto") - ("transitivity" "trans" "transitivity #" t "transitivity") - ("trivial" "t" "trivial" t "trivial") - ("trivial with" "tw" "trivial with @{db}" t) - ("unfold" "u" "unfold #" t "unfold") - ("unfold(s)" "us" "unfold # , #" t) - ("unfold in" "unfi" "unfold # in #" t) - ("unfold at" "unfa" "unfold # at #" t) - )) - "Coq tactics information list. See `coq-syntax-db' for syntax. " - ) - -(defvar coq-solve-tactics-db - (append - coq-user-solve-tactics-db - '( - ("assumption" "as" "assumption" t "assumption") - ("by" "by" "by #" t "by") - ("congruence" "cong" "congruence" t "congruence") - ("contradiction" "contr" "contradiction" t "contradiction") - ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("discriminate" "dis" "discriminate" t "discriminate") - ("exact" "exa" "exact" t "exact") - ("fourier" "four" "fourier" t "fourier") - ("fail" "fa" "fail" nil) - ("field" "field" "field" t "field") - ("omega" "o" "omega" t "omega") - ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("ring" "ring" "ring #" t "ring") - ("solve" nil "solve [ # | # ]" nil "solve") - ("tauto" "ta" "tauto" t "tauto") - )) - "Coq tactic(al)s that solve a subgoal." - ) - - -(defvar coq-tacticals-db - (append - coq-user-tacticals-db - '( - ("info" nil "info #" nil "info") - ("first" nil "first [ # | # ]" nil "first") - ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") - ("do" nil "do @{num} @{tac}" nil "do") - ("idtac" nil "idtac") ; also in tactics - ; ("idtac \"" nil "idtac \"#\"") ; also in tactics - ("fail" "fa" "fail" nil "fail") - ; ("fail \"" "fa\"" "fail" nil) ; - ; ("orelse" nil "orelse #" t "orelse") - ("repeat" nil "repeat #" nil "repeat") - ("try" nil "try #" nil "try") - ("progress" nil "progress #" nil "progress") - ("|" nil "[ # | # ]" nil) - ("||" nil "# || #" nil) - )) - "Coq tacticals information list. See `coq-syntax-db' for syntax.") - - - - -(defvar coq-decl-db - '( - ("Axiom" "ax" "Axiom # : #" t "Axiom") - ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") - ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") - ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") - ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") - ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") - ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) - ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") - ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") - ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") - ("Parameter" "par" "Parameter #: #" t "Parameter") - ("Parameters" "par" "Parameter #: #" t "Parameters") - ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") - ("Variable" "v" "Variable #: #." t "Variable") - ("Variables" "vs" "Variables # , #: #." t "Variables") - ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") - ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." - ) - -(defvar coq-defn-db - '( - ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") - ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") - ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") - ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful - ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) - ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful - ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) - ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful - ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) - ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) - ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? - ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) - ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) - ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") - ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") - ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) - ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") - ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") - ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) - ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) - ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") - ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) - ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) - ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) - ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") - ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") - ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) - ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Let" "Let" "Let # : # := #." t "Let") - ("Ltac" "ltac" "Ltac # := #" t "Ltac") - ("Module :=" "mo" "Module # : # := #." t ) ; careful - ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful - ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful - ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful - ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful - ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful - ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") - ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") - ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) - ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) - ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") - ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; modules and section are indented like goal starters -(defvar coq-goal-starters-db - '( - ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") - ("Chapter" "chp" "Chapter # : #." t "Chapter") - ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") - ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) - ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful - ("Fact" "fct" "Fact # : #." t "Fact") - ("Goal" nil "Goal #." t "Goal") - ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") - ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) - ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful - ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful - ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful - ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") - ("Section" "sec" "Section #." t "Section") - ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") - ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") - ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") - ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") - ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; command that are not declarations, definition or goal starters -(defvar coq-other-commands-db - '( - ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu - ("About" nil "About #." nil "About") - ("Add" nil "Add #." nil "Add" nil t) - ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") - ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") - ("Add Field" nil "Add Field #." t "Add\\s-+Field") - ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") - ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") - ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") - ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") - ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") - ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") - ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") - ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") - ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") - ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") - ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") - ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") - ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") - ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") - ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") - ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") - ("Cd" nil "Cd #." nil "Cd") - ("Check" nil "Check" nil "Check") - ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") - ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") - ("Comments" nil "Comments #." nil "Comments") - ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) - ("Eval" nil "Eval #." nil "Eval") - ("Export" nil "Export #." t "Export") - ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") - ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") - ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") - ("Extraction" "extr" "Extraction @{id}." nil "Extraction") - ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) - ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") - ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") - ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") - ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") - ("Focus" nil "Focus #." nil "Focus") - ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") - ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") - ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") - ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") - ("Import" nil "Import #." t "Import") - ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Inspect" nil "Inspect #." nil "Inspect") - ("Locate" nil "Locate" nil "Locate") - ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") - ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") - ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) - ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) - ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) - ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) - ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) - ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) - ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") - ("Notation (simple)" "nots" "Notation # := #." t "Notation") - ("Opaque" nil "Opaque #." nil "Opaque") - ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") - ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") - ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") - ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") - ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) - ("Print" "p" "Print #." nil "Print") - ("Qed" nil "Qed." nil "Qed") - ("Pwd" nil "Pwd." nil "Pwd") - ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") - ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") - ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") - ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") - ("Require Export" nil "Require Export #." t "Require\\s-+Export") - ("Require Import" nil "Require Import #." t "Require\\s-+Import") - ("Require" nil "Require #." t "Require") - ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") - ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Save" nil "Save." t "Save") - ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") - ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") - ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") - ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") - ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") - ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") - ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") - ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") - ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") - ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") - ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") - ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") - ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Show" nil "Show #." nil "Show") - ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") - ("Transparent" nil "Transparent #." nil "Transparent") - ("Unfocus" nil "Unfocus." nil "Unfocus") - ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") - ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") - ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") - ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") - ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") - ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") - ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") - ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") - ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") - ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") - ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") - ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") - ; ("print" "pr" "print #" "print") - ) - "Command that are not declarations, definition or goal starters." - ) - -(defvar coq-commands-db - (append coq-decl-db coq-defn-db coq-goal-starters-db - coq-other-commands-db coq-user-commands-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " - ) - - -(defvar coq-terms-db - '( - ("fun (1 args)" "f" "fun #:# => #" nil "fun") - ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") - ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") - ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") - ("forall" "fo" "forall #:#,#" nil "forall") - ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") - ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") - ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") - ("if" "if" "if # then # else #" nil "if") - ("let in" "li" "let # := # in #" nil "let") - ("match! (from type)" nil "" nil "match" coq-insert-match) - ("match with" "m" "match # with\n| # => #\nend") - ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") - ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") - ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " - ) - - - - - - - - ;;; Goals (and module/sections) starters detection - - -;; ----- keywords for font-lock. - -;; FIXME da: this one function breaks the nice configuration of Proof General: -;; would like to have proof-goal-regexp instead. -;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, -;; so it appears more difficult than just a proof-goal-regexp setting. -;; Future improvement may simply to be allow a function value for -;; proof-goal-regexp. - -;; FIXME Pierre: the right way IMHO here would be to set a span -;; property 'goalcommand when coq prompt says it (if the name of -;; current proof has changed). - -;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry -;; for the french: -;;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de -;; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) -;; -;; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable -;; uniquement hors d'un MT -;; - si :=MEXPR est absent, elle demarre un nouveau module interactif -;; - si :=MEXPR est present, elle definit un module -;; (la fonction vernac_define_module dans toplevel/vernacentries) -;; -;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] -;; est valable uniquement dans un MT -;; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module -;; interactif -;; - si (:=MEXPR absent, :MTYP present) -;; ou (:=MEXPR present, :MTYP absent) -;; elle declare un module. -;; (la fonction vernac_declare_module dans toplevel/vernacentries) - -(defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring - of STRG matching REGEXP. Empty match are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) - (incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) - nbmatch)) - -;; This function is used for amalgamating a proof into a single -;; goal-save region (proof-goal-command-p used in -;; proof-done-advancing-save in generic/proof-script.el) for coq < -;; 8.0. It is the test when looking backward the start of the proof. -;; It is NOT used for coq > v8.1 -;; (coq-find-and-forget in coq.el uses state numbers, proof numbers and -;; lemma names given in the prompt) - -;; compatibility with v8.0, will delete it some day -(defun coq-goal-command-str-v80-p (str) - "See `coq-goal-command-p'." - (let* ((match (coq-count-match "\\" str)) - (with (coq-count-match "\\" str)) - (letwith (+ (coq-count-match "\\" str) (- with match))) - (affect (coq-count-match ":=" str))) - - (and (proof-string-match coq-goal-command-regexp str) - (not ; - (and - (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) - (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) - ) - ) - ) - -;; Module and or section openings are detected syntactically. Module -;; *openings* are difficult to detect because there can be Module -;; ...with X := ... . So we need to count :='s to detect real openings. - -;; TODO: have opened section/chapter in the prompt too, and get rid of -;; syntactical tests everywhere -(defun coq-module-opening-p (str) - "Decide whether STR is a module or section opening or not. -Used by `coq-goal-command-p'" - (let* ((match (coq-count-match "\\" str)) - (with (coq-count-match "\\" str)) - (letwith (+ (coq-count-match "\\" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match "\\`\\(Module\\)\\>" str) - (= letwith affect)) - )) - -(defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - - -(defun coq-goal-command-str-v81-p (str) - "Decide syntactically whether STR is a goal start or not. Use - `coq-goal-command-p-v81' on a span instead if possible." - (coq-goal-command-str-v80-p str) - ) - -;; This is the function that tests if a SPAN is a goal start. All it -;; has to do is look at the 'goalcmd attribute of the span. -;; It also looks if this is not a module start. - -;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs -;; something in the coq prompt telling the name of all opened modules -;; (like for open goals), and use it to set goalcmd --> no more need -;; to look at Modules and section (actually indentation will still -;; need it) -(defun coq-goal-command-p-v81 (span) - "see `coq-goal-command-p'" - (or (span-property span 'goalcmd) - ;; module and section starts are detected here - (let ((str (or (span-property span 'cmd) ""))) - (or (coq-section-command-p str) - (coq-module-opening-p str)) - ))) - -;; In coq > 8.1 This is used only for indentation. -(defun coq-goal-command-str-p (str) - "Decide whether argument is a goal or not. Use - `coq-goal-command-p' on a span instead if posible." - (cond - (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) - (t (coq-goal-command-str-v80-p str));; this is temporary - )) - -;; This is used for backtracking -(defun coq-goal-command-p (span) - "Decide whether argument is a goal or not." - (cond - (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) - (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary - )) - -(defvar coq-keywords-save-strict - '("Defined" - "Save" - "Qed" - "End" - "Admitted" - "Abort" - )) - -(defvar coq-keywords-save - (append coq-keywords-save-strict '("Proof")) - ) - -(defun coq-save-command-p (span str) - "Decide whether argument is a Save command or not" - (or (proof-string-match coq-save-command-regexp-strict str) - (and (proof-string-match "\\`Proof\\>" str) - (not (proof-string-match "Proof\\s-*\\(\\.\\|\\\\)" str))) - ) - ) - - -(defvar coq-keywords-kill-goal - '("Abort")) - -;; Following regexps are all state changing -(defvar coq-keywords-state-changing-misc-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) - -(defvar coq-keywords-goal - (coq-build-regexp-list-from-db coq-goal-starters-db)) - -(defvar coq-keywords-decl - (coq-build-regexp-list-from-db coq-decl-db)) - -(defvar coq-keywords-defn - (coq-build-regexp-list-from-db coq-defn-db)) - - -(defvar coq-keywords-state-changing-commands - (append - coq-keywords-state-changing-misc-commands - coq-keywords-decl ; all state changing - coq-keywords-defn ; idem - coq-keywords-goal)) ; idem - - -;; -(defvar coq-keywords-state-preserving-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) - -;; concat this is faster that redoing coq-build-regexp-list-from-db on -;; whole commands-db -(defvar coq-keywords-commands - (append coq-keywords-state-changing-commands - coq-keywords-state-preserving-commands) - "All commands keyword.") - -(defvar coq-solve-tactics - (coq-build-regexp-list-from-db coq-solve-tactics-db) - "Keywords for closing tactic(al)s.") - -(defvar coq-tacticals - (coq-build-regexp-list-from-db coq-tacticals-db) - "Keywords for tacticals in a Coq script.") - - - ;; From JF Monin: -(defvar coq-reserved - (append - coq-user-reserved-db - '( - "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" - "return" "struct" "else" "end" "if" "in" "into" "let" "then" - "using" "with" "beta" "delta" "iota" "zeta" "after" "until" - "at" "Sort" "Time")) - "Reserved keywords of Coq.") - - -(defvar coq-state-changing-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) - -(defvar coq-state-preserving-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) - - -(defvar coq-tactics - (append coq-state-changing-tactics coq-state-preserving-tactics)) - -(defvar coq-retractable-instruct - (append coq-state-changing-tactics coq-keywords-state-changing-commands)) - -(defvar coq-non-retractable-instruct - (append coq-state-preserving-tactics - coq-keywords-state-preserving-commands)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands) - "All keywords in a Coq script.") - - - -(defvar coq-symbols - '("|" - "||" - ":" - ";" - "," - "(" - ")" - "[" - "]" - "{" - "}" - ":=" - "=>" - "->" - ".") - "Punctuation Symbols used by Coq.") - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" - "A regexp indicating that the Coq process has identified an error.") - -(defvar coq-id proof-id) -(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") - -(defvar coq-ids (proof-ids coq-id " ")) - -(defun coq-first-abstr-regexp (paren end) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) - -(defcustom coq-variable-highlight-enable t - "Activates partial bound variable highlighting" - :type 'boolean - :group 'coq) - - -(defvar coq-font-lock-terms - (if coq-variable-highlight-enable - (list - ;; lambda binders - (list (coq-first-abstr-regexp "\\" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp "\\" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - ; (list "\\" - ; (list 0 font-lock-type-face) - ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil - ; (list 0 font-lock-variable-name-face))) - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - )) - "*Font-lock table for Coq terms.") - - - -;; According to Coq, "Definition" is both a declaration and a goal. -;; It is understood here as being a goal. This is important for -;; recognizing global identifiers, see coq-global-p. -(defconst coq-save-command-regexp-strict - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) -(defconst coq-save-command-regexp - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) - "\\)"))) -(defconst coq-save-with-hole-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) - -(defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) - -(defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) - "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) - -(defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) - "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) - -;; (defconst coq-decl-with-hole-regexp -;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) - -(defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)")) - -;; must match: -;; "with f x y :" (followed by = or not) -;; "with f x y (z:" (not followed by =) -;; BUT NOT: -;; "with f ... (x:=" -;; "match ... with .. => " -(defconst coq-with-with-hole-regexp - (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" - coq-id "\\s-*:[^=]\\)")) -;; marche aussi a peu pres -;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) -;;"\\\\|\\\\|\\" -(defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) - (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) - (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) - (cons "============================" 'font-lock-keyword-face) - (cons "Subtree proved!" 'font-lock-keyword-face) - (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) - (list "^\\([^ \n]+\\) \\(is defined\\)" - (list 2 'font-lock-keyword-face t) - (list 1 'font-lock-function-name-face t)) - - (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) - (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) - (list - (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) - ;; Remove spurious variable and function faces on commas. - '(proof-zap-commas)))) - -(defvar coq-font-lock-keywords coq-font-lock-keywords-1) - -(defun coq-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?\$ ".") - (modify-syntax-entry ?\/ ".") - (modify-syntax-entry ?\\ ".") - (modify-syntax-entry ?+ ".") - (modify-syntax-entry ?- ".") - (modify-syntax-entry ?= ".") - (modify-syntax-entry ?% ".") - (modify-syntax-entry ?< ".") - (modify-syntax-entry ?> ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - -;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug - (modify-syntax-entry ?\. ".") - - (condition-case nil - ;; Try to use Emacs-21's nested comments. - (modify-syntax-entry ?\* ". 23n") - ;; Revert to non-nested comments if that failed. - (error (modify-syntax-entry ?\* ". 23"))) - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - - -(defconst coq-generic-expression - (mapcar (lambda (kw) - (list (capitalize kw) - (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) - 1)) - (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) - -(provide 'coq-syntax) - ;;; coq-syntax.el ends here - -; Local Variables: *** -; indent-tabs-mode: nil *** -; End: *** diff --git a/tools/coq.el b/tools/coq.el deleted file mode 100644 index f4c4b033..00000000 --- a/tools/coq.el +++ /dev/null @@ -1,142 +0,0 @@ -;; coq.el --- Coq mode editing commands for Emacs -;; -;; Jean-Christophe Filliatre, march 1995 -;; Honteusement pompé de caml.el, Xavier Leroy, july 1993. -;; -;; modified by Marco Maggesi for coq-inferior - -; compatibility code for proofgeneral files -(require 'coq-font-lock) -; ProofGeneral files. remember to remove coq version tests in -; coq-syntax.el -(require 'coq-syntax) - -(defvar coq-mode-map nil - "Keymap used in Coq mode.") -(if coq-mode-map - () - (setq coq-mode-map (make-sparse-keymap)) - (define-key coq-mode-map "\t" 'coq-indent-command) - (define-key coq-mode-map "\M-\t" 'coq-unindent-command) - (define-key coq-mode-map "\C-c\C-c" 'compile) -) - -(defvar coq-mode-syntax-table nil - "Syntax table in use in Coq mode buffers.") -(if coq-mode-syntax-table - () - (setq coq-mode-syntax-table (make-syntax-table)) - ; ( is first character of comment start - (modify-syntax-entry ?\( "()1" coq-mode-syntax-table) - ; * is second character of comment start, - ; and first character of comment end - (modify-syntax-entry ?* ". 23" coq-mode-syntax-table) - ; ) is last character of comment end - (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table) - ; quote is a string-like delimiter (for character literals) - (modify-syntax-entry ?' "\"" coq-mode-syntax-table) - ; quote is part of words - (modify-syntax-entry ?' "w" coq-mode-syntax-table) -) - -(defvar coq-mode-indentation 2 - "*Indentation for each extra tab in Coq mode.") - -(defun coq-mode-variables () - (set-syntax-table coq-mode-syntax-table) - (make-local-variable 'paragraph-start) - (setq paragraph-start (concat "^$\\|" page-delimiter)) - (make-local-variable 'paragraph-separate) - (setq paragraph-separate paragraph-start) - (make-local-variable 'paragraph-ignore-fill-prefix) - (setq paragraph-ignore-fill-prefix t) - (make-local-variable 'require-final-newline) - (setq require-final-newline t) - (make-local-variable 'comment-start) - (setq comment-start "(* ") - (make-local-variable 'comment-end) - (setq comment-end " *)") - (make-local-variable 'comment-column) - (setq comment-column 40) - (make-local-variable 'comment-start-skip) - (setq comment-start-skip "(\\*+ *") - (make-local-variable 'parse-sexp-ignore-comments) - (setq parse-sexp-ignore-comments nil) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'coq-indent-command) - (make-local-variable 'font-lock-keywords) - (setq font-lock-defaults '(coq-font-lock-keywords-1))) - -;;; The major mode - -(defun coq-mode () - "Major mode for editing Coq code. -Tab at the beginning of a line indents this line like the line above. -Extra tabs increase the indentation level. -\\{coq-mode-map} -The variable coq-mode-indentation indicates how many spaces are -inserted for each indentation level." - (interactive) - (kill-all-local-variables) - (setq major-mode 'coq-mode) - (setq mode-name "coq") - (use-local-map coq-mode-map) - (coq-mode-variables) - (run-hooks 'coq-mode-hook)) - -;;; Indentation stuff - -(defun coq-in-indentation () - "Tests whether all characters between beginning of line and point -are blanks." - (save-excursion - (skip-chars-backward " \t") - (bolp))) - -(defun coq-indent-command () - "Indent the current line in Coq mode. -When the point is at the beginning of an empty line, indent this line like -the line above. -When the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\), -increase the indentation by one level. -The indentation size is given by the variable coq-mode-indentation. -In all other cases, insert a tabulation (using insert-tab)." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline)) - (previous-indentation - (save-excursion - (if (eq (forward-line -1) 0) (current-indentation) 0)))) - (cond ((and (bolp) - (looking-at "[ \t]*$") - (> previous-indentation 0)) - (indent-to previous-indentation)) - ((coq-in-indentation) - (indent-to (+ current-offset coq-mode-indentation))) - (t - (insert-tab))))) - -(defun coq-unindent-command () - "Decrease indentation by one level in Coq mode. -Works only if the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\). -Does nothing otherwise." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline))) - (if (and (>= current-offset coq-mode-indentation) - (coq-in-indentation)) - (backward-delete-char-untabify coq-mode-indentation)))) - -;;; coq.el ends here - -(provide 'coq) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 74266925..d660f420 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* = 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in for i = 0 to le - 1 do if pdir.[i] = '.' then pdir.[i] <- '/'; done; @@ -107,14 +116,15 @@ let standard opt = print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte"); print "\"\n\n" -let classify_files_by_root var files (inc_i,inc_r) = - if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then +let classify_files_by_root var files (inc_ml,inc_i,inc_r) = + if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) + && not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_i) then begin let absdir_of_files = List.rev_map - (fun x -> Minilib.canonical_path_name (Filename.dirname x)) + (fun x -> CUnix.canonical_path_name (Filename.dirname x)) files in (* files in scope of a -I option (assuming they are no overlapping) *) - let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in + let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml in if has_inc_i then begin printf "%sINC=" var; @@ -123,128 +133,188 @@ let classify_files_by_root var files (inc_i,inc_r) = then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var - ) inc_i; + ) inc_ml; printf "\n"; end; (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> + list_iter_i (fun i (pdir,_,abspdir) -> if List.exists (is_prefix abspdir) absdir_of_files then printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" var i pdir pdir var) - inc_r; + (inc_i@inc_r); end -let install_include_by_root files_var files (inc_i,inc_r) = - try +let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) = + let var_x_absdirs_l = List.rev_map + (fun (v,l) -> (v,List.rev_map (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l)) + var_x_files_l in + let var_filter f g = List.fold_left (fun acc (var,dirs) -> + if f dirs + then (g var)::acc else acc) [] var_x_absdirs_l in (* All files caught by a -R . option (assuming it is the only one) *) - let ldir = match inc_r with - |[(".",t,_)] -> t - |l -> let out = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in - let () = prerr_string "Warning: install rule assumes that -R . _ is the only -R option" in - out in - let pdir = physical_dir_of_logical_dir ldir in - printf "\tfor i in $(%s); do \\\n" files_var; - printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir; - printf "\tdone\n" - with Not_found -> - let absdir_of_files = List.rev_map - (fun x -> Minilib.canonical_path_name (Filename.dirname x)) - files in - let has_inc_i_files = - List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in - let install_inc_i d = - printf "\tinstall -d $(DSTROOT)$(COQLIBINSTALL)/%s; \\\n" d; - printf "\tfor i in $(%sINC); do \\\n" files_var; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" d; + match inc_i@inc_r with + |[(".",t,_)] -> (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l]) + |l -> + try + let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in + let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in + (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l]) + with Not_found -> + ( + (* vars for -Q options *) + Some (var_filter (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) (fun x -> x)), + (* (physical dir, physical dir of logical path,vars) for -R options + (assuming physical dirs are disjoint) *) + if l = [] then + [".","$(INSTALLDEFAULTROOT)",[]] + else + Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) -> + let vars_r = var_filter (List.exists (is_prefix abspdir)) (fun x -> x^string_of_int i) in + let pdir' = physical_dir_of_logical_dir ldir in + (pdir,pdir',vars_r)::out) 1 [] l + ) + +let install_include_by_root perms = + let install_dir for_i (pdir,pdir',vars) = + let b = vars <> [] in + if b then begin + printf "\tcd \"%s\" && for i in " pdir; + print_list " " (List.rev_map (Format.sprintf "$(%s)") vars); + print "; do \\\n"; + printf "\t install -d \"`dirname \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i`\"; \\\n" pdir'; + printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i; \\\n" perms pdir'; + printf "\tdone\n"; + end; + for_i b pdir' in + let install_i = function + |[] -> fun _ _ -> () + |l -> fun b d -> + if not b then printf "\tinstall -d \"$(DSTROOT)\"$(COQLIBINSTALL)/%s; \\\n" d; + print "\tfor i in "; + print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); + print "; do \\\n"; + printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" perms d; printf "\tdone\n" - in - if inc_r = [] then - if has_inc_i_files then - begin - (* Files in the scope of a -I option *) - install_inc_i "$(INSTALLDEFAULTROOT)"; - end else () + in function + |None,l -> List.iter (install_dir (fun _ _ -> ())) l + |Some v_i,l -> List.iter (install_dir (install_i v_i)) l + +let uninstall_by_root = + let uninstall_dir for_i (pdir,pdir',vars) = + printf "\tprintf 'cd \"$${DSTROOT}\"$(COQLIBINSTALL)/%s" pdir'; + if vars <> [] then begin + print " && rm -f "; + print_list " " (List.rev_map (Format.sprintf "$(%s)") vars); + end; + for_i (); + print " && find . -type d -and -empty -delete\\n"; + print "cd \"$${DSTROOT}\"$(COQLIBINSTALL) && "; + printf "find \"%s\" -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" pdir' +in + let uninstall_i = function + |[] -> () + |l -> + print " && \\\\\\nfor i in "; + print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); + print "; do rm -f \"`basename \"$$i\"`\"; done" + in function + |None,l -> List.iter (uninstall_dir (fun _ -> ())) l + |Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l + +let where_put_doc = function + |_,[],[] -> "$(INSTALLDEFAULTROOT)"; + |_,((_,lp,_)::q as inc_i),[] -> + let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in + if (pr <> "") && + ((List.exists (fun(_,b,_) -> b = pr) inc_i) + || pr.[String.length pr - 1] = '.') + then + physical_dir_of_logical_dir pr else - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> - let has_inc_r_files = List.exists (is_prefix abspdir) absdir_of_files in - let pdir' = physical_dir_of_logical_dir ldir in - if has_inc_r_files then - begin - printf "\tcd %s; for i in $(%s%d); do \\\n" pdir files_var i; - printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir'; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir'; - printf "\tdone\n"; - end; - if has_inc_i_files then install_inc_i pdir' - ) inc_r - -let install_doc some_vfiles some_mlifiles (_,inc_r) = - let install_one_kind kind dir = - printf "\tinstall -d $(DSTROOT)$(COQDOCINSTALL)/%s/%s\n" dir kind; - printf "\tfor i in %s/*; do \\\n" kind; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/%s/$$i;\\\n" dir; - print "\tdone\n" in - print "install-doc:\n"; - let () = match inc_r with - |[] -> - if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; - if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; - |(_,lp,_)::q -> - let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in - if (pr <> "") && - ((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.') - then begin - let rt = physical_dir_of_logical_dir pr in - if some_vfiles then install_one_kind "html" rt; - if some_mlifiles then install_one_kind "mlihtml" rt; - end else begin - prerr_string "Warning: -R options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n"; - if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; - if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; - end in - print "\n" + let () = prerr_string "Warning: -Q options don't have a correct common prefix, + install-doc will put anything in $INSTALLDEFAULTROOT\n" in + "$(INSTALLDEFAULTROOT)" + |_,inc_i,((_,lp,_)::q as inc_r) -> + let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in + let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) pr inc_i in + if (pr <> "") && + ((List.exists (fun(_,b,_) -> b = pr) inc_r) + || (List.exists (fun(_,b,_) -> b = pr) inc_i) + || pr.[String.length pr - 1] = '.') + then + physical_dir_of_logical_dir pr + else + let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix, + install-doc will put anything in $INSTALLDEFAULTROOT\n" in + "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function |Project_file.NoInstall -> () |is_install -> + let not_empty = function |[] -> false |_::_ -> true in + let cmofiles = List.rev_append mlpackfiles (List.rev_append mlfiles ml4files) in + let cmifiles = List.rev_append mlifiles cmofiles in + let cmxsfiles = List.rev_append cmofiles mllibfiles in + let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in + let where_what_oth = vars_to_put_by_root + [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + inc in + let doc_dir = where_put_doc inc in let () = if is_install = Project_file.UnspecInstall then print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in - let not_empty = function |[] -> false |_::_ -> true in - let cmofiles = mlpackfiles@mlfiles@ml4files in - let cmifiles = mlifiles@cmofiles in - let cmxsfiles = cmofiles@mllibfiles in if (not_empty cmxsfiles) then begin print "install-natdynlink:\n"; - install_include_by_root "CMXSFILES" cmxsfiles inc; + install_include_by_root "0755" where_what_cmxs; + print "\n"; + end; + if (not_empty cmxsfiles) then begin + print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n"; + printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; + printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; print "\n"; end; print "install:"; if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; print "\n"; - if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; - if (not_empty cmofiles) then - install_include_by_root "CMOFILES" cmofiles inc; - if (not_empty cmifiles) then - install_include_by_root "CMIFILES" cmifiles inc; - if (not_empty mllibfiles) then - install_include_by_root "CMAFILES" mllibfiles inc; + install_include_by_root "0644" where_what_oth; List.iter (fun x -> - printf "\t(cd %s; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) + printf "\t+cd %s && $(MAKE) DSTROOT=\"$(DSTROOT)\" INSTALLDEFAULTROOT=\"$(INSTALLDEFAULTROOT)/%s\" install\n" x x) sds; print "\n"; - install_doc (not_empty vfiles) (not_empty mlifiles) inc + let install_one_kind kind dir = + printf "\tinstall -d \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/%s\n" dir kind; + printf "\tfor i in %s/*; do \\\n" kind; + printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/$$i;\\\n" dir; + print "\tdone\n" in + print "install-doc:\n"; + if not_empty vfiles then install_one_kind "html" doc_dir; + if not_empty mlifiles then install_one_kind "mlihtml" doc_dir; + print "\n"; + let uninstall_one_kind kind dir = + printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir; + printf "\tprintf '&& rm -f $(shell find \"%s\" -maxdepth 1 -and -type f -print)\\n' >> \"$@\"\n" kind; + print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && "; + printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind + in + print "uninstall_me.sh:\n"; + print "\techo '#!/bin/sh' > $@ \n"; + if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; + uninstall_by_root where_what_oth; + if not_empty vfiles then uninstall_one_kind "html" doc_dir; + if not_empty mlifiles then uninstall_one_kind "mlihtml" doc_dir; + print "\tchmod +x $@\n"; + print "\n"; + print "uninstall: uninstall_me.sh\n"; + print "\tsh $<\n\n" let make_makefile sds = if !make_name <> "" then begin printf "%s: %s\n" !makefile_name !make_name; print "\tmv -f $@ $@.bak\n"; - print "\t$(COQBIN)coq_makefile -f $< -o $@\n\n"; + print "\t\"$(COQBIN)coq_makefile\" -f $< -o $@\n\n"; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") + (fun x -> print "\t+cd "; print x; print " && $(MAKE) Makefile\n") sds; print "\n"; end @@ -257,71 +327,78 @@ let clean sds sps = print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; end; if !some_vfile then - print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"; + begin + print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; + print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" + end; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; - print "\t- rm -rf html mlihtml\n"; + print "\t- rm -rf html mlihtml uninstall_me.sh\n"; List.iter - (fun (file,_,_) -> - if not (is_genrule file) then + (fun (file,_,is_phony,_) -> + if not (is_phony || is_genrule file) then (print "\t- rm -rf "; print file; print "\n")) sps; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") + (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n") sds; print "\n"; print "archclean:\n"; print "\trm -f *.cmx *.o\n"; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") + (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n") sds; print "\n"; - print "printenv:\n\t@$(COQBIN)coqtop -config\n"; - print "\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n\t@echo PP =\t$(PP)\n\t@echo COQFLAGS =\t$(COQFLAGS)\n"; - print "\t@echo COQLIBINSTALL =\t$(COQLIBINSTALL)\n\t@echo COQDOCINSTALL =\t$(COQDOCINSTALL)\n\n" + print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n"; + print "\t@echo 'CAMLC =\t$(CAMLC)'\n\t@echo 'CAMLOPTC =\t$(CAMLOPTC)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n"; + print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n" let header_includes () = () let implicit () = section "Implicit rules."; let mli_rules () = - print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.mli.d: %.mli\n"; + print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml4_rules () = - print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "%.ml4.d: %.ml4\n"; - print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; + print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; + print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = - print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.ml.d: %.ml\n"; + print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; + print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let cmxs_rules () = - print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; - print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in + let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *) + print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx +\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; + print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" in let mllib_rules () = - print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "%.mllib.d: %.mllib\n"; - print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; + print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let mlpack_rules () = - print "%.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "%.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "%.mlpack.d: %.mlpack\n"; - print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; + print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; in let v_rules () = - print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "%.g: %.v\n\t$(GALLINA) $<\n\n"; - print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; - print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@\n\n"; - print "%.v.d: %.v\n"; - print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" + print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; + print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; + print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; + print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; + print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; + print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; + print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" in if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); @@ -350,100 +427,121 @@ let variables is_install opt (args,defs) = end; (* Coq executables and relative variables *) if !some_vfile || !some_mlpackfile || !some_mllibfile then - print "COQDEP?=$(COQBIN)coqdep -c\n"; + print "COQDEP?=\"$(COQBIN)coqdep\" -c\n"; if !some_vfile then begin print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQCHKFLAGS?=-silent -o\n"; print "COQDOCFLAGS?=-interpolate -utf8\n"; - print "COQC?=$(COQBIN)coqc\n"; - print "GALLINA?=$(COQBIN)gallina\n"; - print "COQDOC?=$(COQBIN)coqdoc\n"; - print "COQCHK?=$(COQBIN)coqchk\n\n"; + print "COQC?=$(TIMER) \"$(COQBIN)coqc\"\n"; + print "GALLINA?=\"$(COQBIN)gallina\"\n"; + print "COQDOC?=\"$(COQBIN)coqdoc\"\n"; + print "COQCHK?=\"$(COQBIN)coqchk\"\n"; + print "COQMKTOP?=\"$(COQBIN)coqmktop\"\n\n"; end; (* Caml executables and relative variables *) if !some_ml4file || !some_mlfile || !some_mlifile then begin - print "COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \\ - -I $(COQLIB)library -I $(COQLIB)parsing \\ - -I $(COQLIB)pretyping -I $(COQLIB)interp \\ - -I $(COQLIB)proofs -I $(COQLIB)tactics \\ - -I $(COQLIB)toplevel"; + print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\ + -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\ + -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\ + -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\ + -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\ + -I \"$(COQLIB)config\""; List.iter (fun c -> print " \\ - -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n"; + -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; - print "CAMLC?=$(OCAMLC) -c -rectypes\n"; - print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n"; - print "CAMLLINK?=$(OCAMLC) -rectypes\n"; - print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; + print "CAMLC?=$(OCAMLC) -c -rectypes -thread\n"; + print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread\n"; + print "CAMLLINK?=$(OCAMLC) -rectypes -thread\n"; + print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n"; print "GRAMMARS?=grammar.cma\n"; - print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "CAMLP4OPTIONS?=-loc loc\n"; - print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n"; + print "ifeq ($(CAMLP4),camlp5) +CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma +else +CAMLP4EXTEND= +endif\n"; + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\ + $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () | Project_file.UnspecInstall -> section "Install Paths."; print "ifdef USERINSTALL\n"; - print "XDG_DATA_HOME?=$(HOME)/.local/share\n"; + print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; print "else\n"; - print "COQLIBINSTALL=${COQLIB}user-contrib\n"; - print "COQDOCINSTALL=${DOCDIR}user-contrib\n"; + print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; + print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; + print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "endif\n\n" | Project_file.TraditionalInstall -> section "Install Paths."; - print "COQLIBINSTALL=${COQLIB}user-contrib\n"; - print "COQDOCINSTALL=${DOCDIR}user-contrib\n"; + print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; + print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; + print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "\n" | Project_file.UserInstall -> section "Install Paths."; - print "XDG_DATA_HOME?=$(HOME)/.local/share\n"; + print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; + print "COQTOPINSTALL=$(XDG_DATA_HOME)/coq/toploop\n"; print "\n" let parameters () = print ".DEFAULT_GOAL := all\n\n# \n"; print "# This Makefile may take arguments passed as environment variables:\n"; print "# COQBIN to specify the directory where Coq binaries resides;\n"; + print "# TIMECMD set a command to log .v compilation time;\n"; + print "# TIMED if non empty, use the default time command as TIMECMD;\n"; print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n"; print "# DSTROOT to specify a prefix to install path.\n\n"; print "# Here is a hack to make $(eval $(shell works:\n"; print "define donewline\n\n\nendef\n"; print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; - print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n" - -let include_dirs (inc_i,inc_r) = - let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in - let parse_rec_includes l = - List.map (fun (p,l,_) -> - let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l') - l in - let inc_i' = List.filter (fun (_,i) -> not (List.exists (fun (_,_,i') -> is_prefix i' i) inc_r)) inc_i in + print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"; + print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n"; + print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"; + print "vo_to_obj = $(addsuffix .o,\\\n"; + print " $(filter-out Warning: Error:,\\\n"; + print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n" + +let include_dirs (inc_ml,inc_i,inc_r) = + let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in + let parse_includes l = List.map (fun (x,l,_) -> + let l' = if l = "" then "\"\"" else l in + "-Q \"" ^ x ^ "\" " ^ l' ^"") l in + let parse_rec_includes l = List.map (fun (p,l,_) -> + let l' = if l = "" then "\"\"" else l in + "-R \"" ^ p ^ "\" " ^ l' ^"") l in + let str_ml = parse_ml_includes inc_ml in let str_i = parse_includes inc_i in - let str_i' = parse_includes inc_i' in let str_r = parse_rec_includes inc_r in section "Libraries definitions."; if !some_ml4file || !some_mlfile || !some_mlifile then begin - print "OCAMLLIBS?="; print_list "\\\n " str_i; print "\n"; + print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n"; end; if !some_vfile || !some_mllibfile || !some_mlpackfile then begin - print "COQLIBS?="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n"; - print "COQDOCLIBS?="; print_list "\\\n " str_r; print "\n\n"; + print "COQLIBS?="; print_list "\\\n " str_i; + List.iter (fun x -> print "\\\n "; print x) str_r; + List.iter (fun x -> print "\\\n "; print x) str_ml; print "\n"; + print "COQDOCLIBS?="; print_list "\\\n " str_i; + List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n"; end let custom sps = - let pr_path (file,dependencies,com) = + let pr_path (file,dependencies,is_phony,com) = print file; print ": "; print dependencies; print "\n"; - if com <> "" then (print "\t"; print com); print "\n\n" + if com <> "" then (print "\t"; print com; print "\n"); + print "\n" in if sps <> [] then section "Custom targets."; List.iter pr_path sps let subdirs sds = let pr_subdir s = - print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" + print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n" in if sds <> [] then section "Subdirectories."; List.iter pr_subdir sds @@ -470,13 +568,17 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other begin match vfiles with |[] -> () |l -> - print "VOFILES:=$(VFILES:.v=.vo)\n"; + print "VO=vo\n"; + print "VOFILES:=$(VFILES:.v=.$(VO))\n"; classify_files_by_root "VOFILES" l inc; print "GLOBFILES:=$(VFILES:.v=.glob)\n"; - print "VIFILES:=$(VFILES:.v=.vi)\n"; print "GFILES:=$(VFILES:.v=.g)\n"; print "HTMLFILES:=$(VFILES:.v=.html)\n"; - print "GHTMLFILES:=$(VFILES:.v=.g.html)\n" + print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"; + print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n"; + print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; + print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n"; + classify_files_by_root "NATIVEFILES" l inc end; decl_var "ML4FILES" ml4files; decl_var "MLFILES" mlfiles; @@ -566,7 +668,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other end; if !some_vfile then begin - print "spec: $(VIFILES)\n\n"; + print "quick: $(VOFILES:.vo=.vio)\n\n"; + print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n"; + print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n"; print "gallina: $(GFILES)\n\n"; print "html: $(GLOBFILES) $(VFILES)\n"; print "\t- mkdir -p html\n"; @@ -591,13 +695,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other end let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = - let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in - let other_targets = List.map (function x,_,_ -> x) special_targets @ sds in + let other_targets = CList.map_filter + (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None) + sps @ sds in main_targets vfiles mlfiles other_targets inc; print ".PHONY: "; print_list " " - ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" - :: "userinstall" :: "depend" :: "html" :: "validate" :: sds); + ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: + "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" :: + "html" :: "validate" :: + (sds@(CList.map_filter + (fun (n,_,is_phony,_) -> + if is_phony then Some n else None) sps))); print "\n\n"; custom sps; subdirs sds; @@ -628,38 +737,38 @@ let command_line args = print_list args; print "\n#\n\n" -let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((i_inc,r_inc) as l) = +let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l) = let here = Sys.getcwd () in let not_tops =List.for_all (fun s -> s <> Filename.basename s) in - if List.exists (fun (_,x) -> x = here) i_inc - or List.exists (fun (_,_,x) -> is_prefix x here) r_inc - or (not_tops v && not_tops mli && not_tops ml4 && not_tops ml + if List.exists (fun (_,_,x) -> x = here) i_inc + || List.exists (fun (_,_,x) -> is_prefix x here) r_inc + || (not_tops v && not_tops mli && not_tops ml4 && not_tops ml && not_tops mllib && not_tops mlpack) then l else - ((".",here)::i_inc,r_inc) + ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc) let warn_install_at_root_directory - (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_i,inc_r) = - let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in - let inc_top = List.map (fun (p,_,_) -> p) inc_r_top in + (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) = + let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r@inc_i in + let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in - if inc_r = [] || List.exists (fun f -> List.mem (Filename.dirname f) inc_top) files + if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files then - Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" - (if inc_r_top = [] then "" else "with non trivial logical root ") + Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n" + (if inc_top = [] then "" else "with non trivial logical root ") -let check_overlapping_include (_,inc_r) = +let check_overlapping_include (_,inc_i,inc_r) = let pwd = Sys.getcwd () in - let rec aux = function + let aux = function | [] -> () | (pdir,_,abspdir)::l -> if not (is_prefix pwd abspdir) then Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir; List.iter (fun (pdir',_,abspdir') -> - if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; - in aux inc_r + in aux (inc_i@inc_r) let do_makefile args = let has_file var = function @@ -686,7 +795,7 @@ let do_makefile args = else if (Filename.check_suffix f ".mllib") then some_mllibfile := true else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true in - List.iter (fun (_,dependencies,_) -> + List.iter (fun (_,dependencies,_,_) -> List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; let inc = ensure_root_dir targets inc in diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index ca21f706..383a68df 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ]") in + let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>']") in let adapt_delim = function | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c | "\\" -> "{\\char'134}" @@ -88,6 +88,7 @@ let tex_escaped s = | " " -> "~" | "<" -> "{<}" | ">" -> "{>}" + | "'" -> "{\\textquotesingle}" | _ -> assert false in let adapt = function @@ -116,7 +117,7 @@ let insert texfile coq_output result = let next_block k = if !last_read = "" then last_read := input_line c_coq; (* skip k prompts *) - for i = 1 to k do + for _i = 1 to k do last_read := remove_prompt !last_read; done; (* read and return the following lines until a prompt is found *) @@ -170,9 +171,10 @@ let insert texfile coq_output result = if Str.string_match end_coq_example s 0 then begin just_after () end else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if (not first_block) & k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out ("Coq < " ^ s); + let prompt = if k = 0 then "Coq < " else " " in + if !verbose then Printf.printf "%s%s\n" prompt s; + if (not first_block) && k=0 then output_string c_out "\\medskip\n"; + if show_questions then encapsule false c_out (prompt ^ s); if has_match dot_end_line s then begin let bl = next_block (succ k) in if !verbose then List.iter print_endline bl; @@ -209,7 +211,7 @@ let insert texfile coq_output result = (* Process of one TeX file *) -let rm f = try Sys.remove f with _ -> () +let rm f = try Sys.remove f with any -> () let one_file texfile = let inputv = Filename.temp_file "coq_tex" ".v" in @@ -233,9 +235,9 @@ let one_file texfile = insert texfile coq_output result; (* 4. clean up *) rm inputv; rm coq_output - with e -> begin + with reraise -> begin rm inputv; rm coq_output; - raise e + raise reraise end (* Parsing of the command line, check of the Coq command and process diff --git a/tools/coqc.ml b/tools/coqc.ml new file mode 100644 index 00000000..f636ffd8 --- /dev/null +++ b/tools/coqc.ml @@ -0,0 +1,184 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ". +*) + +(* Environment *) + +let environment = Unix.environment () + +let binary = ref "coqtop" +let image = ref "" + +let verbose = ref false + +let rec make_compilation_args = function + | [] -> [] + | file :: fl -> + let file_noext = + if Filename.check_suffix file ".v" then + Filename.chop_suffix file ".v" + else file + in + (if !verbose then "-compile-verbose" else "-compile") + :: file_noext :: (make_compilation_args fl) + +(* compilation of files [files] with command [command] and args [args] *) + +let compile command args files = + let args' = command :: args @ (make_compilation_args files) in + match Sys.os_type with + | "Win32" -> + let pid = + Unix.create_process_env command (Array.of_list args') environment + Unix.stdin Unix.stdout Unix.stderr + in + let status = snd (Unix.waitpid [] pid) in + let errcode = + match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c + in + exit errcode + | _ -> + Unix.execvpe command (Array.of_list args') environment + +let usage () = + Usage.print_usage_coqc () ; + flush stderr ; + exit 1 + +(* parsing of the command line *) +let extra_arg_needed = ref true + +let parse_args () = + let rec parse (cfiles,args) = function + | [] -> + List.rev cfiles, List.rev args + | ("-verbose" | "--verbose") :: rem -> + verbose := true ; parse (cfiles,args) rem + | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem + | "-image" :: [] -> usage () + | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem + | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem + +(* Obsolete options *) + + | "-libdir" :: _ :: rem -> + print_string "Warning: option -libdir deprecated and ignored\n"; + flush stdout; + parse (cfiles,args) rem + | ("-db"|"-debugger") :: rem -> + print_string "Warning: option -db/-debugger deprecated and ignored\n"; + flush stdout; + parse (cfiles,args) rem + +(* Informative options *) + + | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () + + | ("-v"|"--version") :: _ -> Usage.version 0 + + | ("-where") :: _ -> + Envars.set_coqlib (fun x -> x); + print_endline (Envars.coqlib ()); + exit 0 + + | ("-config" | "--config") :: _ -> + Envars.set_coqlib (fun x -> x); + Usage.print_config (); + exit 0 + +(* Options for coqtop : a) options with 0 argument *) + + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time" + |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" + |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" + |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" + |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" + |"-impredicative-set"|"-vm"|"-no-native-compiler" + |"-verbose-compat-notations"|"-no-compat-notations" + |"-indices-matter"|"-quick"|"-color" + |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" + as o) :: rem -> + parse (cfiles,o::args) rem + +(* Options for coqtop : b) options with 1 argument *) + + | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" + |"-load-vernac-source"|"-l"|"-load-vernac-object" + |"-load-ml-source"|"-require"|"-load-ml-object" + |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" + as o) :: rem -> + begin + match rem with + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + +(* Options for coqtop : c) options with 1 argument and possibly more *) + + | ("-I"|"-include" as o) :: rem -> + begin + match rem with + | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem' + | s :: "-as" :: [] -> usage () + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + | "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem + | "-R" :: s :: "-as" :: [] -> usage () + | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem + | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem + | ("-schedule-vio-checking" + |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem -> + let nodash, rem = + CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in + extra_arg_needed := false; + parse (cfiles, List.rev nodash @ s :: o :: args) rem + + | f :: rem -> + if Sys.file_exists f then + parse (f::cfiles,args) rem + else + let fv = f ^ ".v" in + if Sys.file_exists fv then + parse (fv::cfiles,args) rem + else begin + prerr_endline ("coqc: "^f^": no such file or directory") ; + exit 1 + end + in + parse ([],[]) (List.tl (Array.to_list Sys.argv)) + +(* main: we parse the command line, define the command to compile files + * and then call the compilation on each file *) + +let main () = + let cfiles, args = parse_args () in + if cfiles = [] && !extra_arg_needed then begin + prerr_endline "coqc: too few arguments" ; + usage () + end; + let coqtopname = + if !image <> "" then !image + else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension) + in + (* List.iter (compile coqtopname args) cfiles*) + Unix.handle_unix_error (compile coqtopname args) cfiles + +let _ = Printexc.print main () diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 21b4e576..2e0cce6e 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let name = log_dir@[basename] in - let paths = suffixes name in + let paths = if recur then suffixes name else [name] in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () @@ -120,7 +121,7 @@ let traite_Declare f = let s' = basename_noext s in (match search_ml_known s with | Some mldir when not (List.mem s' !decl_list) -> - let fullname = file_name (String.uncapitalize s') mldir in + let fullname = file_name s' mldir in let depl = mL_dep_list s (fullname ^ ".ml") in treat depl; decl_list := s :: !decl_list @@ -156,35 +157,319 @@ let declare_dependencies () = flush stdout) (List.rev !vAccu) +(** DAGs guaranteed to be transitive reductions *) +module DAG (Node : Set.OrderedType) : +sig + type node = Node.t + type t + val empty : t + val add_transitive_edge : node -> node -> t -> t + val iter : (node -> node -> unit) -> t -> unit +end = +struct + type node = Node.t + module NSet = Set.Make(Node) + module NMap = Map.Make(Node) + + (** Associate to a node the set of its neighbours *) + type _t = NSet.t NMap.t + + (** Optimisation: construct the reverse graph at the same time *) + type t = { dir : _t; rev : _t; } + + + let node_equal x y = Node.compare x y = 0 + + let add_edge x y graph = + let set = try NMap.find x graph with Not_found -> NSet.empty in + NMap.add x (NSet.add y set) graph + + let remove_edge x y graph = + let set = try NMap.find x graph with Not_found -> NSet.empty in + let set = NSet.remove y set in + if NSet.is_empty set then NMap.remove x graph + else NMap.add x set graph + + let has_edge x y graph = + let set = try NMap.find x graph with Not_found -> NSet.empty in + NSet.mem y set + + let connected x y graph = + let rec aux rem seen = + if NSet.is_empty rem then false + else + let x = NSet.choose rem in + if node_equal x y then true + else + let rem = NSet.remove x rem in + if NSet.mem x seen then + aux rem seen + else + let seen = NSet.add x seen in + let next = try NMap.find x graph with Not_found -> NSet.empty in + let rem = NSet.union next rem in + aux rem seen + in + aux (NSet.singleton x) NSet.empty + + (** Check whether there is a path from a to b going through the edge + x -> y. *) + let connected_through a b x y graph = + let rec aux rem seen = + if NMap.is_empty rem then false + else + let (n, through) = NMap.choose rem in + if node_equal n b && through then true + else + let rem = NMap.remove n rem in + let is_seen = try Some (NMap.find n seen) with Not_found -> None in + match is_seen with + | None -> + let seen = NMap.add n through seen in + let next = try NMap.find n graph with Not_found -> NSet.empty in + let is_x = node_equal n x in + let push m accu = + let through = through || (is_x && node_equal m y) in + NMap.add m through accu + in + let rem = NSet.fold push next rem in + aux rem seen + | Some false -> + (** The path we took encountered x -> y but not the one in seen *) + if through then aux (NMap.add n true rem) (NMap.add n true seen) + else aux rem seen + | Some true -> aux rem seen + in + aux (NMap.singleton a false) NMap.empty + + let closure x graph = + let rec aux rem seen = + if NSet.is_empty rem then seen + else + let x = NSet.choose rem in + let rem = NSet.remove x rem in + if NSet.mem x seen then + aux rem seen + else + let seen = NSet.add x seen in + let next = try NMap.find x graph with Not_found -> NSet.empty in + let rem = NSet.union next rem in + aux rem seen + in + aux (NSet.singleton x) NSet.empty + + let empty = { dir = NMap.empty; rev = NMap.empty; } + + (** Online transitive reduction algorithm *) + let add_transitive_edge x y graph = + if connected x y graph.dir then graph + else + let dir = add_edge x y graph.dir in + let rev = add_edge y x graph.rev in + let graph = { dir; rev; } in + let ancestors = closure x rev in + let descendents = closure y dir in + let fold_ancestor a graph = + let fold_descendent b graph = + let to_remove = has_edge a b graph.dir in + let to_remove = to_remove && not (node_equal x a && node_equal y b) in + let to_remove = to_remove && connected_through a b x y graph.dir in + if to_remove then + let dir = remove_edge a b graph.dir in + let rev = remove_edge b a graph.rev in + { dir; rev; } + else graph + in + NSet.fold fold_descendent descendents graph + in + NSet.fold fold_ancestor ancestors graph + + let iter f graph = + let iter x set = NSet.iter (fun y -> f x y) set in + NMap.iter iter graph.dir + +end + +module Graph = +struct +(** Dumping a dependency graph **) + +module DAG = DAG(struct type t = string let compare = compare end) + +(** TODO: we should share this code with Coqdep_common *) +let treat_coq_file chan = + let buf = Lexing.from_channel chan in + let deja_vu_v = ref ([]: string list list) + and deja_vu_ml = ref ([] : string list) in + let mark_v_done acc str = + let seen = List.mem str !deja_vu_v in + if not seen then + let () = addQueue deja_vu_v str in + try + let file_str = Hashtbl.find vKnown str in + (canonize file_str, !suffixe) :: acc + with Not_found -> acc + else acc + in + let rec loop acc = + let token = try Some (coq_action buf) with Fin_fichier -> None in + match token with + | None -> acc + | Some action -> + let acc = match action with + | Require strl -> + List.fold_left mark_v_done acc strl + | RequireString s -> + let str = Filename.basename s in + mark_v_done acc [str] + | Declare sl -> + let declare suff dir s = + let base = file_name s dir in + let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in + (escape base, suff ^ opt) + in + let decl acc str = + let s = basename_noext str in + if not (List.mem s !deja_vu_ml) then + let () = addQueue deja_vu_ml s in + match search_mllib_known s with + | Some mldir -> (declare ".cma" mldir s) :: acc + | None -> + match search_ml_known s with + | Some mldir -> (declare ".cmo" mldir s) :: acc + | None -> acc + else acc + in + List.fold_left decl acc sl + | Load str -> + let str = Filename.basename str in + let seen = List.mem [str] !deja_vu_v in + if not seen then + let () = addQueue deja_vu_v [str] in + try + let file_str = Hashtbl.find vKnown [str] in + (canonize file_str, ".v") :: acc + with Not_found -> acc + else acc + | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *) + in + loop acc + in + loop [] + +let treat_coq_file f = + let chan = try Some (open_in f) with Sys_error _ -> None in + match chan with + | None -> [] + | Some chan -> + try + let ans = treat_coq_file chan in + let () = close_in chan in + ans + with Syntax_error (i, j) -> close_in chan; error_cannot_parse f (i, j) + +type graph = + | Element of string + | Subgraph of string * graph list + +let rec insert_graph name path graphs = match path, graphs with + | [] , graphs -> (Element name) :: graphs + | (box :: boxes), (Subgraph (hd, names)) :: tl when hd = box -> + Subgraph (hd, insert_graph name boxes names) :: tl + | _, hd :: tl -> hd :: (insert_graph name path tl) + | (box :: boxes), [] -> [ Subgraph (box, insert_graph name boxes []) ] + +let print_graphs chan graph = + let rec print_aux name = function + | [] -> name + | (Element str) :: tl -> fprintf chan "\"%s\";\n" str; print_aux name tl + | Subgraph (box, names) :: tl -> + fprintf chan "subgraph cluster%n {\nlabel=\"%s\";\n" name box; + let name = print_aux (name + 1) names in + fprintf chan "}\n"; print_aux name tl + in + ignore (print_aux 0 graph) + +let rec pop_common_prefix = function + | [Subgraph (_, graphs)] -> pop_common_prefix graphs + | graphs -> graphs + +let split_path = Str.split (Str.regexp "/") + +let rec pop_last = function + | [] -> [] + | [ x ] -> [] + | x :: xs -> x :: pop_last xs + +let get_boxes path = pop_last (split_path path) + +let insert_raw_graph file = + insert_graph file (get_boxes file) + +let rec get_dependencies name args = + let vdep = treat_coq_file (name ^ ".v") in + let fold (deps, graphs, alseen) (dep, _) = + let dag = DAG.add_transitive_edge name dep deps in + if not (List.mem dep alseen) then + get_dependencies dep (dag, insert_raw_graph dep graphs, dep :: alseen) + else + (dag, graphs, alseen) + in + List.fold_left fold args vdep + +let coq_dependencies_dump chan dumpboxes = + let (deps, graphs, _) = + List.fold_left (fun ih (name, _) -> get_dependencies name ih) + (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu, + List.map fst !vAccu) !vAccu + in + fprintf chan "digraph dependencies {\n"; flush chan; + if dumpboxes then print_graphs chan (pop_common_prefix graphs) + else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu; + DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps; + fprintf chan "}\n" + +end + let usage () = eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] +\n"; eprintf " extra options:\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -exclude-dir f : skip subdirectories named f during -R search\n"; + eprintf " -exclude-dir f : skip subdirectories named 'f' during -R search\n"; + eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; exit 1 +let split_period = Str.split (Str.regexp (Str.quote ".")) + let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll | "-w" :: ll -> option_w := true; parse ll - | "-boot" :: ll -> Flags.boot := true; parse ll + | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll - | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [ln]; parse ll + | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r []; + add_dir add_known r (split_period ln); + parse ll | "-I" :: r :: "-as" :: [] -> usage () - | "-I" :: r :: ll -> add_dir add_known r []; parse ll + | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll + | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll | "-R" :: r :: "-as" :: [] -> usage () - | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll + | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll + | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll | "-R" :: ([] | [_]) -> usage () + | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll + | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () - | "-slash" :: ll -> option_slash := true; parse ll + | "-slash" :: ll -> + Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; + parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () @@ -194,26 +479,42 @@ let coqdep () = parse (List.tl (Array.to_list Sys.argv)); if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) - if !Flags.boot then begin + if !option_boot then begin add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"] + add_rec_dir add_known "plugins" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin + Envars.set_coqlib ~fail:Errors.error; let coqlib = Envars.coqlib () in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in - if Sys.file_exists user then add_rec_dir add_coqlib_known user []; - List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.xdg_dirs; - List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath; + if Sys.file_exists user then add_dir add_coqlib_known user []; + List.iter (fun s -> add_dir add_coqlib_known s []) + (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); + List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath; end; - List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; - List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; - List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu; + List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; + List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; + List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; warning_mult ".mli" iter_mli_known; warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; if !option_c && not !option_D then mL_dependencies (); if not !option_D then coq_dependencies (); - if !option_w || !option_D then declare_dependencies () + if !option_w || !option_D then declare_dependencies (); + begin match !option_dump with + | None -> () + | Some (box, file) -> + let chan = open_out file in + try Graph.coq_dependencies_dump chan box; close_out chan + with e -> close_out chan; raise e + end -let _ = Printexc.catch coqdep () +let _ = + try + coqdep () + with Errors.UserError(s,p) -> + let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in + Pp.msgerrnl pp diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index bcc9f33f..bc3435a6 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* option_slash := true; parse ll | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) @@ -25,20 +24,26 @@ let rec parse = function | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) - add_dir add_known r []; + add_caml_dir r; norec_dirs:=r::!norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep_boot () = + let () = option_boot := true in if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - if !option_c then - add_rec_dir add_known "." [] + if !option_c then begin + add_rec_dir add_known "." []; + add_rec_dir (fun _ -> add_caml_known) "." ["Coq"]; + end else begin add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "plugins" ["Coq"]; + add_caml_dir "tactics"; + add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end; if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 253fb037..2e6a15ce 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* s.[i] = '/' + | "Cygwin" | "Win32" -> + let c = s.[i] in c = '/' || c = '\\' || c = ':' + | _ -> assert false + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || is_dir_sep dirname (l-1) + then dirname ^ filename + else dirname ^ "/" ^ filename (** [get_extension f l] checks whether [f] has one of the extensions listed in [l]. It returns [f] without its extension, alongside with @@ -51,7 +61,7 @@ let rec get_extension f = function let basename_noext filename = let fn = Filename.basename filename in - try Filename.chop_extension fn with _ -> fn + try Filename.chop_extension fn with Invalid_argument _ -> fn (** ML Files specified on the command line. In the entries: - the first string is the basename of the file, without extension nor @@ -76,10 +86,10 @@ let vAccu = ref ([] : (string * string) list) let addQueue q v = q := v :: !q -let safe_hash_add clq q (k,v) = +let safe_hash_add cmp clq q (k,v) = try let v2 = Hashtbl.find q k in - if v<>v2 then + if not (cmp v v2) then let rec add_clash = function (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl | cl::cltl -> cl::add_clash cltl @@ -91,19 +101,24 @@ let safe_hash_add clq q (k,v) = (** Files found in the loadpaths. For the ML files, the string is the basename without extension. - To allow ML source filename to be potentially capitalized, - we perform a double search. *) +let warning_ml_clash x s suff s' suff' = + if suff = suff' then + eprintf + "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + (match s with None -> "." | Some d -> d) + ((match s' with None -> "." | Some d -> d) // x) suff + let mkknown () = - let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in - let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s - and iter f = Hashtbl.iter f h + let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in + let add x s suff = + try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff + with Not_found -> Hashtbl.add h x (s,suff) + and iter f = Hashtbl.iter (fun x (s,_) -> f x s) h and search x = - try Some (Hashtbl.find h (String.uncapitalize x)) - with Not_found -> - try Some (Hashtbl.find h (String.capitalize x)) - with Not_found -> None + try Some (fst (Hashtbl.find h x)) + with Not_found -> None in add, iter, search let add_ml_known, iter_ml_known, search_ml_known = mkknown () @@ -122,7 +137,7 @@ let error_cannot_parse s (i,j) = let warning_module_notfound f s = eprintf "*** Warning: in file %s, library " f; - eprintf "%s.v is required and has not been found in loadpath!\n" + eprintf "%s.v is required and has not been found in the loadpath!\n" (String.concat "." s); flush stderr @@ -142,7 +157,7 @@ let warning_clash file dir = let f = Filename.basename f1 in let d1 = Filename.dirname f1 in let d2 = Filename.dirname f2 in - let dl = List.map Filename.dirname (List.rev fl) in + let dl = List.rev_map Filename.dirname fl in eprintf "*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in " file (String.concat "." dir) f; @@ -265,10 +280,10 @@ let escape = Buffer.clear s'; for i = 0 to String.length s - 1 do let c = s.[i] in - if c = ' ' or c = '#' or c = ':' (* separators and comments *) - or c = '%' (* pattern *) - or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) - or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + if c = ' ' || c = '#' || c = ':' (* separators and comments *) + || c = '%' (* pattern *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 'A' <= s.[1] && s.[1] <= 'Z' || 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) then begin @@ -283,13 +298,16 @@ let escape = done; Buffer.contents s' +let compare_file f1 f2 = + absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2) + let canonize f = let f' = absolute_dir (Filename.dirname f) // Filename.basename f in match List.filter (fun (_,full) -> f' = full) !vAccu with | (f,_) :: _ -> escape f | _ -> escape f -let rec traite_fichier_Coq verbose f = +let rec traite_fichier_Coq suffixe verbose f = try let chan = open_in f in let buf = Lexing.from_channel chan in @@ -305,7 +323,7 @@ let rec traite_fichier_Coq verbose f = addQueue deja_vu_v str; try let file_str = safe_assoc verbose f str in - printf " %s%s" (canonize file_str) !suffixe + printf " %s%s" (canonize file_str) suffixe with Not_found -> if verbose && not (Hashtbl.mem coqlibKnown str) then warning_module_notfound f str @@ -316,7 +334,7 @@ let rec traite_fichier_Coq verbose f = addQueue deja_vu_v [str]; try let file_str = Hashtbl.find vKnown [str] in - printf " %s%s" (canonize file_str) !suffixe + printf " %s%s" (canonize file_str) suffixe with Not_found -> if not (Hashtbl.mem coqlibKnown [str]) then warning_notfound f s @@ -350,7 +368,7 @@ let rec traite_fichier_Coq verbose f = let file_str = Hashtbl.find vKnown [str] in let canon = canonize file_str in printf " %s.v" canon; - traite_fichier_Coq true (canon ^ ".v") + traite_fichier_Coq suffixe true (canon ^ ".v") with Not_found -> () end | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) () @@ -408,7 +426,10 @@ let coq_dependencies () = let ename = escape name in let glob = if !option_noglob then "" else " "^ename^".glob" in printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename; - traite_fichier_Coq true (name ^ ".v"); + traite_fichier_Coq !suffixe true (name ^ ".v"); + printf "\n"; + printf "%s.vio: %s.v" ename ename; + traite_fichier_Coq ".vio" true (name ^ ".v"); printf "\n"; flush stdout) (List.rev !vAccu) @@ -418,18 +439,28 @@ let rec suffixes = function | [name] -> [[name]] | dir::suffix as l -> l::suffixes suffix -let add_known phys_dir log_dir f = - match get_extension f [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with +let add_caml_known phys_dir _ f = + let basename,suff = + get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in + match suff with + | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".mli" -> add_mli_known basename (Some phys_dir) suff + | ".mllib" -> add_mllib_known basename (Some phys_dir) suff + | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff + | _ -> () + +let add_known recur phys_dir log_dir f = + match get_extension f [".v";".vo"] with | (basename,".v") -> let name = log_dir@[basename] in let file = phys_dir//basename in - let paths = suffixes name in + let paths = if recur then suffixes name else [name] in List.iter - (fun n -> safe_hash_add clash_v vKnown (n,file)) paths - | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir) - | (basename,".mli") -> add_mli_known basename (Some phys_dir) - | (basename,".mllib") -> add_mllib_known basename (Some phys_dir) - | (basename,".mlpack") -> add_mlpack_known basename (Some phys_dir) + (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths + | (basename,".vo") when not(!option_boot) -> + let name = log_dir@[basename] in + let paths = if recur then suffixes name else [name] in + List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () (* Visits all the directories under [dir], including [dir], @@ -456,11 +487,18 @@ let rec add_directory recur add_file phys_dir log_dir = done with End_of_file -> closedir dirh +(** -Q semantic: go in subdirs but only full logical paths are known. *) let add_dir add_file phys_dir log_dir = - try add_directory false add_file phys_dir log_dir with Unix_error _ -> () + try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> () +(** -R semantic: go in subdirs and suffixes of logical paths are known. *) let add_rec_dir add_file phys_dir log_dir = - handle_unix_error (add_directory true add_file phys_dir) log_dir + handle_unix_error (add_directory true (add_file true) phys_dir) log_dir + +(** -I semantic: do not go in subdirs. *) +let add_caml_dir phys_dir = + handle_unix_error (add_directory true add_caml_known phys_dir) [] + let rec treat_file old_dirname old_name = let name = Filename.basename old_name diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index b2e01f58..71b96ca0 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a -> unit -val add_ml_known : string -> dir -> unit +val add_ml_known : string -> dir -> string -> unit val iter_ml_known : (string -> dir -> unit) -> unit val search_ml_known : string -> dir option -val add_mli_known : string -> dir -> unit +val add_mli_known : string -> dir -> string -> unit val iter_mli_known : (string -> dir -> unit) -> unit val search_mli_known : string -> dir option -val add_mllib_known : string -> dir -> unit +val add_mllib_known : string -> dir -> string -> unit val search_mllib_known : string -> dir option val vKnown : (string list, string) Hashtbl.t val coqlibKnown : (string list, unit) Hashtbl.t @@ -39,12 +39,15 @@ val canonize : string -> string val mL_dependencies : unit -> unit val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list -val add_known : string -> string list -> string -> unit +val add_known : bool -> string -> string list -> string -> unit +val add_caml_known : string -> string list -> string -> unit val add_directory : bool -> (string -> string list -> string -> unit) -> string -> string list -> unit +val add_caml_dir : string -> unit val add_dir : - (string -> string list -> string -> unit) -> string -> string list -> unit + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val add_rec_dir : - (string -> string list -> string -> unit) -> string -> string list -> unit + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val treat_file : dir -> string -> unit +val error_cannot_parse : string -> int * int -> 'a diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 4806fbb0..b447030a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* " | "." | ".." | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" @@ -174,11 +220,10 @@ and caml_action = parse | _ { caml_action lexbuf } and comment = parse - | "(*" (* "*)" *) - { comment_depth := succ !comment_depth; comment lexbuf } + | "(*" + { comment lexbuf; comment lexbuf } | "*)" - { comment_depth := pred !comment_depth; - if !comment_depth > 0 then comment lexbuf } + { () } | "'" [^ '\\' '\''] "'" { comment lexbuf } | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" @@ -218,7 +263,7 @@ and load_file = parse and require_file = parse | "(*" - { comment_depth := 1; comment lexbuf; require_file lexbuf } + { comment lexbuf; require_file lexbuf } | space+ { require_file lexbuf } | coq_ident @@ -226,7 +271,12 @@ and require_file = parse module_names := [coq_qual_id_tail lexbuf]; let qid = coq_qual_id_list lexbuf in parse_dot lexbuf; - Require qid } + match !from_pre_ident with + None -> + Require qid + | Some from -> + (from_pre_ident := None ; + Require (List.map (fun x -> from @ x) qid)) } | '"' [^'"']* '"' (*'"'*) { let s = Lexing.lexeme lexbuf in parse_dot lexbuf; @@ -248,7 +298,7 @@ and parse_dot = parse and coq_qual_id = parse | "(*" - { comment_depth := 1; comment lexbuf; coq_qual_id lexbuf } + { comment lexbuf; coq_qual_id lexbuf } | space+ { coq_qual_id lexbuf } | coq_ident @@ -264,7 +314,7 @@ and coq_qual_id = parse and coq_qual_id_tail = parse | "(*" - { comment_depth := 1; comment lexbuf; coq_qual_id_tail lexbuf } + { comment lexbuf; coq_qual_id_tail lexbuf } | space+ { coq_qual_id_tail lexbuf } | coq_field @@ -281,7 +331,7 @@ and coq_qual_id_tail = parse and coq_qual_id_list = parse | "(*" - { comment_depth := 1; comment lexbuf; coq_qual_id_list lexbuf } + { comment lexbuf; coq_qual_id_list lexbuf } | space+ { coq_qual_id_list lexbuf } | coq_ident @@ -299,8 +349,7 @@ and modules = parse | space+ { modules lexbuf } | "(*" - { comment_depth := 1; comment lexbuf; - modules lexbuf } + { comment lexbuf; modules lexbuf } | '"' [^'"']* '"' { let lex = (Lexing.lexeme lexbuf) in let str = String.sub lex 1 (String.length lex - 2) in diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index 6a44684d..c3db3a26 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "" && Filename.is_relative f then if not (Sys.file_exists !output_dir) then (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1) else - Filename.concat !output_dir f + !output_dir / f else f @@ -71,17 +73,19 @@ let normalize_filename f = (** A weaker analog of the function in Envars *) let guess_coqlib () = - let file = "states/initial.coq" in + let file = "theories/Init/Prelude.vo" in match Coq_config.coqlib with - | Some coqlib when Sys.file_exists (Filename.concat coqlib file) -> - coqlib + | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib | Some _ | None -> let coqbin = normalize_path (Filename.dirname Sys.executable_name) in let prefix = Filename.dirname coqbin in - let rpath = if Coq_config.local then [] else - (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in - let coqlib = List.fold_left Filename.concat prefix rpath in - if Sys.file_exists (Filename.concat coqlib file) then coqlib + let rpath = + if Coq_config.local then [] + else if Coq_config.arch_is_win32 then ["lib"] + else ["lib/coq"] + in + let coqlib = List.fold_left (/) prefix rpath in + if Sys.file_exists (coqlib / file) then coqlib else prefix let header_trailer = ref true diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index ccd285f1..dbc930f5 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -75,7 +75,7 @@ h4.section { padding-top: 0px; padding-bottom: 0px; font-size : 100%; - font-style : bold; + font-weight : bold; text-decoration : underline; } @@ -86,8 +86,7 @@ h4.section { max-width: 40em; color: black; padding: 10px; - background-color: #90bdff; - border-style: plain} + background-color: #90bdff } .inlinecode { display: inline; @@ -160,8 +159,65 @@ tr.infrulemiddle hr { #footer { font-size: 65%; font-family: sans-serif; } +/* Identifiers: ) */ + .id { display: inline; } +.id[title="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[title="var"] { + color: rgb(40%,0%,40%); +} + +.id[title="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="definition"] { + color: rgb(0%,40%,0%); +} + +.id[title="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[title="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[title="instance"] { + color: rgb(0%,40%,0%); +} + +.id[title="projection"] { + color: rgb(0%,40%,0%); +} + +.id[title="method"] { + color: rgb(0%,40%,0%); +} + +.id[title="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[title="record"] { + color: rgb(0%,0%,80%); +} + +.id[title="class"] { + color: rgb(0%,0%,80%); +} + +.id[title="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +/* Deprecated rules using the 'type' attribute of (not xhtml valid) */ + .id[type="constructor"] { color: rgb(60%,0%,0%); } @@ -261,7 +317,6 @@ tr.infrulemiddle hr { #index #footer { position: absolute; bottom: 0; - text-align: bottom; } .paragraph { diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 9de9a38f..f49f9f00 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -1,5 +1,5 @@ -% This is coqdoc.sty, by Jean-Christophe Filliâtre +% This is coqdoc.sty, by Jean-Christophe Filliâtre % This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc) % % You can modify the following macros to customize the appearance diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli index 390e61d2..4e132ba0 100644 --- a/tools/coqdoc/cpretty.mli +++ b/tools/coqdoc/cpretty.mli @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Cdglobals.coq_module -> unit val detect_subtitle : string -> Cdglobals.coq_module -> string option diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 300d104c..edf7ee8e 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* true | _ -> false - (* saving/restoring the PP state *) type state = { @@ -127,8 +117,6 @@ let without_light = without_ref Cdglobals.light - let show_all f = without_gallina (without_light f) - let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () @@ -251,14 +239,6 @@ with _ -> () - let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:=" - let extract_ident s = - assert (String.length s >= 3); - if Str.string_match extract_ident_re s 0 then - Str.matched_group 1 s - else - String.sub s 1 (String.length s - 3) - let output_indented_keyword s lexbuf = let nbsp,isp = count_spaces s in Output.indentation nbsp; @@ -282,10 +262,8 @@ let firstchar = '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] | (* utf-8 letterlike symbols *) - (* '\206' ([ '\145' - '\183'] | '\187') | *) - (* '\xCF' [ '\x00' - '\xCE' ] | *) - (* utf-8 letterlike symbols *) - '\206' (['\145'-'\161'] | ['\163'-'\187']) | + '\206' (['\145'-'\161'] | ['\163'-'\191']) | + '\207' (['\145'-'\191']) | '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) | '\129' [ '\176'-'\187' ] (* superscripts *) | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) @@ -333,6 +311,7 @@ let def_token = | "Boxed" | "CoFixpoint" | "Record" + | "Variant" | "Structure" | "Scheme" | "Inductive" @@ -345,7 +324,7 @@ let def_token = let decl_token = "Hypothesis" | "Hypotheses" - | "Parameter" + | "Parameter" 's'? | "Axiom" 's'? | "Conjecture" @@ -626,7 +605,7 @@ and coq = parse end else begin - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } @@ -656,17 +635,17 @@ and coq = parse if eol then coq_bol lexbuf else coq lexbuf } | gallina_kw { let s = lexeme lexbuf in - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | notation_kw { let s = lexeme lexbuf in - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol= start_notation_string lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | prog_kw { let s = lexeme lexbuf in - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } @@ -914,11 +893,15 @@ and doc indents = parse and escaped_math_latex = parse | "$" { Output.stop_latex_math () } | eof { Output.stop_latex_math () } + | "*)" + { Output.stop_latex_math (); backtrack lexbuf } | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf } and escaped_latex = parse | "%" { () } | eof { () } + | "*)" + { backtrack lexbuf } | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } and escaped_html = parse @@ -928,12 +911,15 @@ and escaped_html = parse | "##" { Output.html_char '#'; escaped_html lexbuf } | eof { () } + | "*)" + { backtrack lexbuf } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } and verbatim inline = parse | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | ">>" { Output.stop_verbatim inline } + | "*)" { Output.stop_verbatim inline; backtrack lexbuf } | eof { Output.stop_verbatim inline } | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf } @@ -953,11 +939,11 @@ and escaped_coq = parse | "]" { decr brackets; if !brackets > 0 then - (Output.sublexer ']' (lexeme_start lexbuf); escaped_coq lexbuf) + (Output.sublexer_in_doc ']'; escaped_coq lexbuf) else Tokens.flush_sublexer () } | "[" { incr brackets; - Output.sublexer '[' (lexeme_start lexbuf); escaped_coq lexbuf } + Output.sublexer_in_doc '['; escaped_coq lexbuf } | "(*" { Tokens.flush_sublexer (); comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf } @@ -967,7 +953,7 @@ and escaped_coq = parse { Tokens.flush_sublexer () } | (identifier '.')* identifier { Tokens.flush_sublexer(); - Output.ident (lexeme lexbuf) (lexeme_start lexbuf); + Output.ident (lexeme lexbuf) None; escaped_coq lexbuf } | space_nl* { let str = lexeme lexbuf in @@ -979,7 +965,7 @@ and escaped_coq = parse else Output.start_inline_coq ()); escaped_coq lexbuf } | _ - { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf); + { Output.sublexer_in_doc (lexeme_char lexbuf 0); escaped_coq lexbuf } (*s Coq "Comments" command. *) @@ -1078,7 +1064,7 @@ and body_bol = parse | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } and body = parse - | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf} + | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf} | nl+ space* "]]" space* nl { Tokens.flush_sublexer(); if not !formatted then @@ -1147,11 +1133,11 @@ and body = parse else body lexbuf } | "where" { Tokens.flush_sublexer(); - Output.ident (lexeme lexbuf) (lexeme_start lexbuf); + Output.ident (lexeme lexbuf) None; start_notation_string lexbuf } | identifier { Tokens.flush_sublexer(); - Output.ident (lexeme lexbuf) (lexeme_start lexbuf); + Output.ident (lexeme lexbuf) (Some (lexeme_start lexbuf)); body lexbuf } | ".." { Tokens.flush_sublexer(); Output.char '.'; Output.char '.'; diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 8170e173..4a5ff592 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "" | x::_ -> x -let begin_module m = push module_stack m -let begin_section s = push section_stack s - -let end_block id = - (** determines if it ends a module or a section and pops the stack *) - if ((String.compare (head !module_stack) id ) == 0) then - pop module_stack - else if ((String.compare (head !section_stack) id) == 0) then - pop section_stack - else - () - -let make_fullid id = - (** prepends the current module path to an id *) - let path = string_of_stack !module_stack in - if String.length path > 0 then - path ^ "." ^ id - else - id - - (* Coq modules *) let split_sp s = @@ -158,7 +131,7 @@ let find_external_library logicalpath = let rec aux = function | [] -> raise Not_found | (l,u)::rest -> - if String.length logicalpath > String.length l & + if String.length logicalpath > String.length l && String.sub logicalpath 0 (String.length l + 1) = l ^"." then u else aux rest @@ -208,10 +181,6 @@ let sort_entries el = let display_letter c = if c = '*' then "other" else String.make 1 c -let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0 - -let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h [] - let type_name = function | Library -> let ln = !lib_name in @@ -304,9 +273,9 @@ let type_of_string = function | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" | "ex" | "scheme" -> Definition | "prf" | "thm" -> Lemma - | "ind" | "coind" -> Inductive + | "ind" | "variant" | "coind" -> Inductive | "constr" -> Constructor - | "rec" | "corec" -> Record + | "indrec" | "rec" | "corec" -> Record | "proj" -> Projection | "class" -> Class | "meth" -> Method @@ -319,7 +288,7 @@ let type_of_string = function | "mod" | "modtype" -> Module | "tac" -> TacticDefinition | "sec" -> Section - | s -> raise (Invalid_argument ("type_of_string:" ^ s)) + | s -> invalid_arg ("type_of_string:" ^ s) let ill_formed_glob_file f = eprintf "Warning: ill-formed file %s (links will not be available)\n" f @@ -370,9 +339,6 @@ let read_glob vfile f = done) with _ -> ()) | _ -> - try Scanf.sscanf s "not %d %s %s" - (fun loc sp id -> add_def loc loc (type_of_string "not") sp id) - with Scanf.Scan_failure _ -> try Scanf.sscanf s "%s %d:%d %s %s" (fun ty loc1 loc2 sp id -> add_def loc1 loc2 (type_of_string ty) sp id) diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 4c1a445c..69b4e4da 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; + prerr_endline " -Q map physical dir to Coq dir"; prerr_endline " --latin1 set ISO-8859-1 input language"; prerr_endline " --utf8 set UTF-8 input language"; prerr_endline " --charset set HTML charset"; @@ -320,6 +321,10 @@ let parse () = add_path path log; parse_rec rem | "-R" :: ([] | [_]) -> usage () + | "-Q" :: path :: log :: rem -> + add_path path log; parse_rec rem + | "-Q" :: ([] | [_]) -> + usage () | ("-glob-from" | "--glob-from") :: f :: rem -> glob_source := GlobFile f; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> @@ -445,7 +450,7 @@ let gen_mult_files l = if (!header_trailer) then Output.trailer (); close_out_file() end - (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) + (* NB: for latex and texmacs, a separated toc or index is meaningless... *) let read_glob_file vfile f = try Index.read_glob vfile f diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d29c447..ae6e6388 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* () | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n); @@ -383,6 +385,14 @@ module Latex = struct end; last_was_in := false + let sublexer_in_doc c = + if c = '*' && !last_was_in then begin + Tokens.flush_sublexer (); + output_char '*' + end else + Tokens.output_tagged_symbol_char None c; + last_was_in := false + let initialize () = initialize_tex_html (); Tokens.token_tree := token_tree_latex; @@ -399,8 +409,11 @@ module Latex = struct let ident s loc = last_was_in := s = "in"; try - let tag = Index.find (get_module false) loc in - reference (translate s) tag + match loc with + | None -> raise Not_found + | Some loc -> + let tag = Index.find (get_module false) loc in + reference (translate s) tag with Not_found -> if is_tactic s then printf "\\coqdoctac{%s}" (translate s) @@ -522,8 +535,8 @@ module Html = struct printf "\n"; printf "\n\n"; - printf "\n" !charset; - printf "\n"; + printf "\n" !charset; + printf "\n"; printf "%s\n\n\n" !page_title; printf "\n\n
\n\n
\n
\n\n"; printf "
\n\n" @@ -558,7 +571,7 @@ module Html = struct printf "

%s %s

\n\n" ln (get_module true) end - let indentation n = for i = 1 to n do printf " " done + let indentation n = for _i = 1 to n do printf " " done let line_break () = printf "
\n" @@ -573,9 +586,6 @@ module Html = struct | '&' -> printf "&" | c -> output_char c - let raw_string s = - for i = 0 to String.length s - 1 do char s.[i] done - let escaped = let buff = Buffer.create 5 in fun s -> @@ -585,10 +595,24 @@ module Html = struct | '<' -> Buffer.add_string buff "<" | '>' -> Buffer.add_string buff ">" | '&' -> Buffer.add_string buff "&" + | '\'' -> Buffer.add_string buff "´" + | '\"' -> Buffer.add_string buff """ | c -> Buffer.add_char buff c done; Buffer.contents buff + let sanitize_name s = + let rec loop esc i = + if i < 0 then if esc then escaped s else s + else match s.[i] with + | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1) + | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1) + | _ -> + (* This name contains complex characters: + this is probably a notation string, we simply hash it. *) + Digest.to_hex (Digest.string s) + in loop false (String.length s - 1) + let latex_char _ = () let latex_string _ = () @@ -618,19 +642,19 @@ module Html = struct let ident_ref m fid typ s = match find_module m with | Local -> - printf "" m fid; - printf "%s" typ s + printf "" m (sanitize_name fid); + printf "%s" typ s | External m when !externals -> - printf "" m fid; - printf "%s" typ s + printf "" m (sanitize_name fid); + printf "%s" typ s | External _ | Unknown -> - printf "%s" typ s + printf "%s" typ s let reference s r = match r with | Def (fullid,ty) -> - printf "" fullid; - printf "%s" (type_name ty) s + printf "" (sanitize_name fullid); + printf "%s" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s @@ -640,7 +664,7 @@ module Html = struct | Some ref -> reference s ref | None -> if issymbchar then output_string s - else printf "%s" s + else printf "%s" s let sublexer c loc = let tag = @@ -648,6 +672,9 @@ module Html = struct in Tokens.output_tagged_symbol_char tag c + let sublexer_in_doc c = + Tokens.output_tagged_symbol_char None c + let initialize () = initialize_tex_html(); Tokens.token_tree := token_tree_html; @@ -657,16 +684,20 @@ module Html = struct match Tokens.translate s with Some s -> s | None -> escaped s let keyword s loc = - printf "%s" (translate s) + printf "%s" (translate s) let ident s loc = if is_keyword s then begin - printf "%s" (translate s) + printf "%s" (translate s) end else begin - try reference (translate s) (Index.find (get_module false) loc) + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) with Not_found -> if is_tactic s then - printf "%s" (translate s) + printf "%s" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then @@ -818,7 +849,7 @@ module Html = struct "[library]", m ^ ".html", t else sprintf "[%s, in %s]" (type_name t) m m , - sprintf "%s.html#%s" m s, t) + sprintf "%s.html#%s" m (sanitize_name s), t) let format_bytype_index = function | Library, idx -> @@ -827,7 +858,7 @@ module Html = struct Index.map (fun s m -> let text = sprintf "[in %s]" m m in - (text, sprintf "%s.html#%s" m s, t)) idx + (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx (* Impression de la table d'index *) let print_index_table_item i = @@ -923,8 +954,6 @@ module TeXmacs = struct let (preamble : string Queue.t) = in_doc := false; Queue.create () - let push_in_preamble s = Queue.add s preamble - let header () = output_string "(*i This file has been automatically generated with the command \n"; @@ -989,6 +1018,9 @@ module TeXmacs = struct let sublexer c l = if !in_doc then Tokens.output_tagged_symbol_char None c else char c + let sublexer_in_doc c = + char c + let initialize () = Tokens.token_tree := token_tree_texmacs; Tokens.outfun := output_sublexer_string @@ -1045,8 +1077,6 @@ module TeXmacs = struct let paragraph () = printf "\n\n" - let line_break_true () = printf "" - let line_break () = printf "\n" let empty_line_of_code () = printf "\n" @@ -1107,12 +1137,13 @@ module Raw = struct let stop_quote () = printf "\"" let indentation n = - for i = 1 to n do printf " " done + for _i = 1 to n do printf " " done let keyword s loc = raw_ident s let ident s loc = raw_ident s let sublexer c l = char c + let sublexer_in_doc c = char c let initialize () = Tokens.token_tree := ref Tokens.empty_ttree; @@ -1226,6 +1257,7 @@ let char = select Latex.char Html.char TeXmacs.char Raw.char let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer +let sublexer_in_doc = select Latex.sublexer_in_doc Html.sublexer_in_doc TeXmacs.sublexer_in_doc Raw.sublexer_in_doc let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 40fe69f7..c4628dd8 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val nbsp : unit -> unit val char : char -> unit val keyword : string -> loc -> unit -val ident : string -> loc -> unit +val ident : string -> loc option -> unit val sublexer : char -> loc -> unit +val sublexer_in_doc : char -> unit val initialize : unit -> unit val proofbox : unit -> unit diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index 33560fce..a93ae855 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Str.split spaces str + +let (/) = Filename.concat + +(** Which user files do we support (and propagate to ocamlopt) ? +*) +let supported_suffix f = match CUnix.get_extension f with + | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true + | _ -> false + +(** From bytecode extension to native +*) +let native_suffix f = match CUnix.get_extension f with + | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx" + | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa" + | ".a" -> f + | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a") + +(** Transforms a file name in the corresponding Caml module name. +*) +let module_of_file name = + String.capitalize + (try Filename.chop_extension name with Invalid_argument _ -> name) + +(** Run a command [prog] with arguments [args]. + We do not use [Sys.command] anymore, see comment in [CUnix.sys_command]. +*) +let run_command prog args = + match CUnix.sys_command prog args with + | Unix.WEXITED 127 -> failwith ("no such command "^prog) + | Unix.WEXITED n -> n + | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n) + | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n) + + + +(** {6 Coqmktop options} *) + +let opt = ref false +let top = ref false +let echo = ref false +let no_start = ref false + +let is_ocaml4 = Coq_config.caml_version.[0] <> '3' +let is_camlp5 = Coq_config.camlp4 = "camlp5" + + +(** {6 Includes options} *) + +(** Since the Coq core .cma are given with their relative paths + (e.g. "lib/clib.cma"), we only need to include directories mentionned in + the temp main ml file below (for accessing the corresponding .cmi). *) + +let std_includes basedir = + let rebase d = match basedir with None -> d | Some base -> base / d in + ["-I"; rebase "."; + "-I"; rebase "lib"; + "-I"; rebase "toplevel"; + "-I"; rebase "kernel/byterun"; + "-I"; Envars.camlp4lib () ] @ + (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) + +(** For the -R option, visit all directories under [dir] and add + corresponding -I to the [opts] option list (in reversed order) *) +let incl_all_subdirs dir opts = + let l = ref opts in + let add f = l := f :: "-I" :: !l in + let rec traverse dir = + if Sys.file_exists dir && Sys.is_directory dir then + let () = add dir in + let subdirs = try Sys.readdir dir with any -> [||] in + Array.iter (fun f -> traverse (dir/f)) subdirs + in + traverse dir; !l + + +(** {6 Objects to link} *) + +(** NB: dynlink is now always linked, it is used for loading plugins + and compiled vm code (see native-compiler). We now reject platforms + with ocamlopt but no dynlink.cmxa during ./configure, and give + instructions there about how to build a dummy dynlink.cmxa, + cf. dev/dynlink.ml. *) + +(** OCaml + CamlpX libraries *) + +let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] +let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"] +let libobjs = ocaml_libs @ camlp4_libs + +(** Toplevel objects *) + +let ocaml_topobjs = + if is_ocaml4 then + ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"] + else + ["toplevellib.cma"] + +let camlp4_topobjs = + if is_camlp5 then + ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] + else + [ "Camlp4Top.cmo"; + "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo"; + "Camlp4Parsers/Camlp4OCamlParser.cmo"; + "Camlp4Parsers/Camlp4GrammarParser.cmo" ] + +let topobjs = ocaml_topobjs @ camlp4_topobjs + +(** Coq Core objects *) + +let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts) +let core_objs = split_list Tolink.core_objs +let core_libs = split_list Tolink.core_libs + +(** Build the list of files to link and the list of modules names +*) +let files_to_link userfiles = + let top = if !top then topobjs else [] in + let modules = List.map module_of_file (top @ core_objs @ userfiles) in + let objs = libobjs @ top @ core_libs in + let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles + in (modules, objs') + + +(** {6 Parsing of the command-line} *) + +let usage () = + prerr_endline "Usage: coqmktop files\ +\nFlags are:\ +\n -coqlib dir Specify where the Coq object files are\ +\n -camlbin dir Specify where the OCaml binaries are\ +\n -camlp4bin dir Specify where the Camlp4/5 binaries are\ +\n -o exec-file Specify the name of the resulting toplevel\ +\n -boot Run in boot mode\ +\n -echo Print calls to external commands\ +\n -opt Compile in native code\ +\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ +\n -R dir Add recursively dir to OCaml search path\ +\n"; + exit 1 + +let parse_args () = + let rec parse (op,fl) = function + | [] -> List.rev op, List.rev fl + + (* Directories *) + | "-coqlib" :: d :: rem -> + Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem + | "-camlbin" :: d :: rem -> + Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem + | "-camlp4bin" :: d :: rem -> + Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem + | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem + | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage () + + (* Boolean options of coqmktop *) + | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem + | "-opt" :: rem -> opt := true ; parse (op,fl) rem + | "-top" :: rem -> top := true ; parse (op,fl) rem + | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem + | "-echo" :: rem -> echo := true ; parse (op,fl) rem + | ("-v8"|"-full" as o) :: rem -> + Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem + + (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) + | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> + parse (o::op,fl) rem + | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' -> + begin + match rem' with + | a :: rem -> parse (a::o::op,fl) rem + | [] -> usage () + end + + | ("-h"|"-help"|"--help") :: _ -> usage () + | f :: rem when supported_suffix f -> parse (op,f::fl) rem + | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1 + in + parse ([],[]) (List.tl (Array.to_list Sys.argv)) + + +(** {6 Temporary main file} *) + +(** remove the temporary main file +*) +let clean file = + let rm f = if Sys.file_exists f then Sys.remove f in + let basename = Filename.chop_suffix file ".ml" in + if not !echo then begin + rm file; + rm (basename ^ ".o"); + rm (basename ^ ".cmi"); + rm (basename ^ ".cmo"); + rm (basename ^ ".cmx") + end + +(** Initializes the kind of loading in the main program +*) +let declare_loading_string () = + if not !top then + "Mltop.remove ();;" + else + "begin try\ +\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\ +\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\ +\n | Toploop.Directive_none f -> f ()\ +\n | _ -> ()\ +\n end\ +\n with\ +\n | Not_found -> ()\ +\n end;;\ +\n\ +\n let ppf = Format.std_formatter;;\ +\n Mltop.set_top\ +\n {Mltop.load_obj=\ +\n (fun f -> if not (Topdirs.load_file ppf f)\ +\n then Errors.error (\"Could not load plugin \"^f));\ +\n Mltop.use_file=Topdirs.dir_use ppf;\ +\n Mltop.add_dir=Topdirs.dir_directory;\ +\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ +\n" + +(** create a temporary main file to link +*) +let create_tmp_main_file modules = + let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in + try + (* Add the pre-linked modules *) + output_string oc "List.iter Mltop.add_known_module [\""; + output_string oc (String.concat "\";\"" modules); + output_string oc "\"];;\n"; + (* Initializes the kind of loading *) + output_string oc (declare_loading_string()); + (* Start the toplevel loop *) + if not !no_start then output_string oc "Coqtop.start();;\n"; + close_out oc; + main_name + with reraise -> + clean main_name; raise reraise + + +(** {6 Main } *) + +let main () = + let (options, userfiles) = parse_args () in + (* Directories: *) + let () = Envars.set_coqlib ~fail:Errors.error in + let camlbin = Envars.camlbin () in + let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in + (* Which ocaml compiler to invoke *) + let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in + (* Which arguments ? *) + if !opt && !top then failwith "no custom toplevel in native code !"; + let flags = if !opt then [] else Coq_config.vmbyteflags in + let topstart = if !top then [ "topstart.cmo" ] else [] in + let (modules, tolink) = files_to_link userfiles in + let main_file = create_tmp_main_file modules in + try + (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. + - With the coq .cma, we MUST use the -linkall option. *) + let args = + "-linkall" :: "-rectypes" :: flags @ copts @ options @ + (std_includes basedir) @ tolink @ [ main_file ] @ topstart + in + if !echo then begin + let command = String.concat " " (prog::args) in + print_endline command; + print_endline + ("(command length is " ^ + (string_of_int (String.length command)) ^ " characters)"); + flush Pervasives.stdout + end; + let exitcode = run_command prog args in + clean main_file; + exitcode + with reraise -> clean main_file; raise reraise + +let pr_exn = function + | Failure msg -> msg + | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err + | any -> Printexc.to_string any + +let _ = + try exit (main ()) + with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1 diff --git a/tools/coqwc.mll b/tools/coqwc.mll index db927efb..417ec535 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + s, string_of_inet_addr host ^":"^ string_of_int port + | _ -> assert false + +module Queue : sig + type t + val is_empty : t -> bool + val push : int * party -> t -> unit + val pop : t -> int * party + val create : unit -> t +end = struct + type t = (int * party) list ref + let create () = ref [] + let is_empty q = !q = [] + let rec split acc = function + | [] -> List.rev acc, [] + | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | x :: xs -> split (x :: acc) xs + let push (_,{ priority } as item) q = + if priority = Flags.Low then q := !q @ [item] + else + let high, low = split [] !q in + q := high @ (item :: low) + let pop q = match !q with x :: xs -> q := xs; x | _ -> assert false +end + +let read_fd fd s ~off ~len = + let rec loop () = + try Unix.read fd s off len + with Unix.Unix_error(Unix.EAGAIN,_,_) -> loop () + in + loop () + +let really_read_fd fd s off len = + let i = ref 0 in + while !i < len do + let off = off + !i in + let len = len - !i in + let r = read_fd fd s ~off ~len in + if r = 0 then raise End_of_file; + i := !i + r + done + +let raw_input_line fd = + try + let b = Buffer.create 80 in + let s = String.make 1 '\000' in + while s <> "\n" do + really_read_fd fd s 0 1; + if s <> "\n" && s <> "\r" then Buffer.add_string b s; + done; + Buffer.contents b + with Unix.Unix_error _ -> raise End_of_file + +let accept s = + let cs, _ = Unix.accept s in + let cout = Unix.out_channel_of_descr cs in + set_binary_mode_out cout true; + match parse_request (raw_input_line cs) with + | Hello p -> { sock=cs; cout; tokens=0; priority=p } + | _ -> (try Unix.close cs with _ -> ()); raise End_of_file + +let parse s = () + +let parties = ref [] + +let max_tokens = ref 2 +let cur_tokens = ref 0 + +let queue = Queue.create () + +let rec allocate n party = + let extra = min n (!max_tokens - !cur_tokens) in + cur_tokens := !cur_tokens + extra; + party.tokens <- party.tokens + extra; + answer party (Tokens extra) + +and de_allocate n party = + let back = min party.tokens n in + party.tokens <- party.tokens - back; + cur_tokens := min (!cur_tokens - back) !max_tokens; + eventually_dequeue () + +and eventually_dequeue () = + if Queue.is_empty queue || !cur_tokens >= !max_tokens then () + else + let req, party = Queue.pop queue in + if List.exists (fun { sock } -> sock = party.sock) !parties + then allocate req party + else eventually_dequeue () + +let chat s = + let party = + try List.find (fun { sock } -> sock = s) !parties + with Not_found -> Printf.eprintf "Internal error"; exit 1 in + try + match parse_request (raw_input_line party.sock) with + | Get n -> + if !cur_tokens < !max_tokens then allocate n party + else Queue.push (n,party) queue + | TryGet n -> + if !cur_tokens < !max_tokens then allocate n party + else answer party Noluck + | GiveBack n -> de_allocate n party + | Ping -> + answer party (Pong (!cur_tokens,!max_tokens,Unix.getpid ())); + raise End_of_file + | Hello _ -> raise End_of_file + with Failure _ | ParseError | Sys_error _ | End_of_file -> + (try Unix.close party.sock with _ -> ()); + parties := List.filter (fun { sock } -> sock <> s) !parties; + de_allocate party.tokens party; + eventually_dequeue () + +let check_alive s = + match CoqworkmgrApi.connect s with + | Some s -> + let cout = Unix.out_channel_of_descr s in + set_binary_mode_out cout true; + output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request Ping); flush cout; + begin match Unix.select [s] [] [] 1.0 with + | [s],_,_ -> + let cin = Unix.in_channel_of_descr s in + set_binary_mode_in cin true; + begin match parse_response (input_line cin) with + | Pong (n,m,pid) -> n, m, pid + | _ -> raise Not_found + end + | _ -> raise Not_found + end + | _ -> raise Not_found + +let main () = + let args = [ + "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; + "-d",Arg.Set debug, "do not detach (debug)"] in + let usage = + "Prints on stdout an env variable assignement to be picked up by coq\n"^ + "instances in order to limit the maximum number of concurrent workers.\n"^ + "The default value is 2.\n"^ + "Usage:" in + Arg.parse args (fun extra -> + Arg.usage args ("Unexpected argument "^extra^".\n"^usage)) + usage; + try + let sock = Sys.getenv "COQWORKMGR_SOCK" in + if !debug then Printf.eprintf "Contacting %s\n%!" sock; + let cur, max, pid = check_alive sock in + Printf.printf "COQWORKMGR_SOCK=%s\n%!" sock; + Printf.eprintf + "coqworkmgr already up and running (pid=%d, socket=%s, j=%d/%d)\n%!" + pid sock cur max; + exit 0 + with Not_found | Failure _ | Invalid_argument _ | Unix.Unix_error _ -> + if !debug then Printf.eprintf "No running instance. Starting a new one\n%!"; + let master, str = mk_socket_channel () in + if not !debug then begin + let pid = Unix.fork () in + if pid <> 0 then begin + Printf.printf "COQWORKMGR_SOCK=%s\n%!" str; + exit 0 + end else begin + ignore(Unix.setsid ()); + Unix.close Unix.stdin; + Unix.close Unix.stdout; + end; + end else begin + Printf.printf "COQWORKMGR_SOCK=%s\n%!" str; + end; + Sys.catch_break true; + try + while true do + if !debug then + Printf.eprintf "Status: #parties=%d tokens=%d/%d \n%!" + (List.length !parties) !cur_tokens !max_tokens; + let socks = master :: List.map (fun { sock } -> sock) !parties in + let r, _, _ = Unix.select socks [] [] (-1.0) in + List.iter (fun s -> + if s = master then begin + try parties := accept master :: !parties + with _ -> () + end else chat s) + r + done; + exit 0 + with Sys.Break -> + if !parties <> [] then begin + Printf.eprintf "Some coq processes still need me\n%!"; + exit 1; + end else + exit 0 + +let () = main () diff --git a/tools/escape_string.ml b/tools/escape_string.ml deleted file mode 100644 index 50e8faad..00000000 --- a/tools/escape_string.ml +++ /dev/null @@ -1 +0,0 @@ -print_string (String.escaped Sys.argv.(1)) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index a7203dc8..c2b12668 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* exit 1 | _ -> () - -let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (0,true,false,s))); - "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (0,true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (0,false,false,s))); - "INTERP", (fun s -> eval_call (Ide_intf.interp (0,false,true,s))); - "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); - "GOALS", (fun _ -> eval_call (Ide_intf.goals ())); - "HINTS", (fun _ -> eval_call (Ide_intf.hints ())); - "GETOPTIONS", (fun _ -> eval_call (Ide_intf.get_options ())); - "STATUS", (fun _ -> eval_call (Ide_intf.status ())); - "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); - "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s)); - "#", (fun _ -> raise Comment); - ] - -let read_eval_print line = - let lline = String.length line in - let rec find_cmd = function - | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1 - | (cmd,fn) :: cmds -> - let lcmd = String.length cmd in - if lline >= lcmd && String.sub line 0 lcmd = cmd then - let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> "" - in fn arg - else find_cmd cmds +let error s = + prerr_endline ("fake_id: error: "^s); + exit 1 + +type coqtop = { + xml_printer : Xml_printer.t; + xml_parser : Xml_parser.t; +} + +let logger level content = prerr_endline content + +let base_eval_call ?(print=true) ?(fail=true) call coqtop = + if print then prerr_endline (Xmlprotocol.pr_call call); + let xml_query = Xmlprotocol.of_call call in + Xml_printer.print coqtop.xml_printer xml_query; + let rec loop () = + let xml = Xml_parser.parse coqtop.xml_parser in + if Pp.is_message xml then + let message = Pp.to_message xml in + let level = message.Pp.message_level in + let content = message.Pp.message_content in + logger level content; + loop () + else if Feedback.is_feedback xml then + loop () + else (Xmlprotocol.to_answer call xml) in - find_cmd commands + let res = loop () in + if print then prerr_endline (Xmlprotocol.pr_full_value call res); + match res with + | Interface.Fail (_,_,s) when fail -> error s + | Interface.Fail (_,_,s) as x -> prerr_endline s; x + | x -> x + +let eval_call c q = ignore(base_eval_call c q) + +module Parser = struct (* {{{ *) + + exception Err of string + exception More + + type token = + | Tok of string * string + | Top of token list + + type grammar = + | Alt of grammar list + | Seq of grammar list + | Opt of grammar + | Item of (string * (string -> token * int)) + + let eat_rex x = x, fun s -> + if Str.string_match (Str.regexp x) s 0 then begin + let m = Str.match_end () in + let w = String.sub s 0 m in + Tok(x,w), m + end else raise (Err ("Regexp "^x^" not found in: "^s)) + + let eat_balanced c = + let c' = match c with + | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in + let sc, sc' = String.make 1 c, String.make 1 c' in + let name = sc ^ "..." ^ sc' in + let unescape s = + Str.global_replace (Str.regexp ("\\\\"^sc)) sc + (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in + name, fun s -> + if s.[0] = c then + let rec find n m = + if String.length s <= m then raise More; + if s.[m] = c' then + if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1 + else find (n-1) (m+1) + else if s.[m] = c then find (n+1) (m+1) + else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then + find n (m+2) + else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then + find n (m+2) + else find n (m+1) + in find ~-1 0 + else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s)) + + let eat_blanks s = snd (eat_rex "[ \n\t]*") s + + let s = ref "" + + let parse g ic = + let read_more () = s := !s ^ input_line ic ^ "\n" in + let ensure_non_empty n = if n = String.length !s then read_more () in + let cut_after s n = String.sub s n (String.length s - n) in + let rec wrap f n = + try + ensure_non_empty n; + let _, n' = eat_blanks (cut_after !s n) in + ensure_non_empty n'; + let t, m = f (cut_after !s (n+n')) in + let _, m' = eat_blanks (cut_after !s (n+n'+m)) in + t, n+n'+m+m' + with More -> read_more (); wrap f n in + let rec aux n g res : token list * int = + match g with + | Item (_,f) -> + let t, n = wrap f n in + t :: res, n + | Opt g -> + (try let res', n = aux n g [] in Top (List.rev res') :: res, n + with Err _ -> Top [] :: res, n) + | Alt gl -> + let rec fst = function + | [] -> raise (Err ("No more alternatives for: "^cut_after !s n)) + | g :: gl -> + try aux n g res + with Err s -> fst gl in + fst gl + | Seq gl -> + let rec all (res,n) = function + | [] -> res, n + | g :: gl -> all (aux n g res) gl in + all (res,n) gl in + let res, n = aux 0 g [] in + s := cut_after !s n; + List.rev res + + let clean s = Str.global_replace (Str.regexp "\n") "\\n" s + + let rec print g = + match g with + | Item (s,_) -> Printf.sprintf "%s" (clean s) + | Opt g -> Printf.sprintf "[%s]" (print g) + | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) + | Seq gs -> String.concat " " (List.map print gs) + + let rec print_toklist = function + | [] -> "" + | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest + | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest + | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest + +end (* }}} *) + +type sentence = { + name : string; + text : string; + edit_id : int; +} + +let doc : sentence Document.document = Document.create () + +let tip_id () = + try Document.tip doc + with + | Document.Empty -> Stateid.initial + | Invalid_argument _ -> error "add_sentence on top of non assigned tip" + +let add_sentence = + let edit_id = ref 0 in + fun ?(name="") text -> + let tip_id = tip_id () in + decr edit_id; + Document.push doc { name; text; edit_id = !edit_id }; + !edit_id, tip_id + +let print_document () = + let ellipsize s = + Str.global_replace (Str.regexp "^[\n ]*") "" + (if String.length s > 20 then String.sub s 0 17 ^ "..." + else s) in + prerr_endline (Pp.string_of_ppcmds + (Document.print doc + (fun b state_id { name; text } -> + Pp.str (Printf.sprintf "%s[%10s, %3s] %s" + (if b then "*" else " ") + name + (Stateid.to_string (Option.default Stateid.dummy state_id)) + (ellipsize text))))) + +(* This module is the logic a GUI has to implement *) +module GUILogic = struct + + let after_add = function + | Interface.Fail (_,_,s) -> error s + | Interface.Good (id, (Util.Inl (), _)) -> + Document.assign_tip_id doc id + | Interface.Good (id, (Util.Inr tip, _)) -> + Document.assign_tip_id doc id; + Document.unfocus doc; + ignore(Document.cut_at doc tip); + print_document () + + let at id id' _ = Stateid.equal id' id + + let after_edit_at (id,need_unfocus) = function + | Interface.Fail (_,_,s) -> error s + | Interface.Good (Util.Inl ()) -> + if need_unfocus then Document.unfocus doc; + ignore(Document.cut_at doc id); + print_document () + | Interface.Good (Util.Inr (stop_id,(start_id,tip))) -> + if need_unfocus then Document.unfocus doc; + ignore(Document.cut_at doc tip); + Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id); + ignore(Document.cut_at doc id); + print_document () + + let get_id_pred pred = + try Document.find_id doc pred + with Not_found -> error "No state found" + + let get_id id = get_id_pred (fun _ { name } -> name = id) + + let after_fail coq = function + | Interface.Fail (safe_id,_,s) -> + prerr_endline "The command failed as expected"; + let to_id, need_unfocus = + get_id_pred (fun id _ -> Stateid.equal id safe_id) in + after_edit_at (to_id, need_unfocus) + (base_eval_call (Xmlprotocol.edit_at to_id) coq) + | Interface.Good _ -> error "The command was expected to fail but did not" + +end + +open GUILogic + +let eval_print l coq = + let open Parser in + let open Xmlprotocol in + (* prerr_endline ("Interpreting: " ^ print_toklist l); *) + match l with + | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] -> + let eid, tip = add_sentence phrase in + after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] -> + let eid, tip = add_sentence ~name phrase in + after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"GOALS"); ] -> + eval_call (goals ()) coq + | [ Tok(_,"FAILGOALS"); ] -> + after_fail coq (base_eval_call ~fail:false (goals ()) coq) + | [ Tok(_,"EDIT_AT"); Tok(_,id) ] -> + let to_id, need_unfocus = get_id id in + after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) + | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> + eval_call (query (phrase,tip_id())) coq + | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> + let to_id, _ = get_id id in + eval_call (query (phrase, to_id)) coq + | [ Tok(_,"WAIT") ] -> + let phrase = "Stm Wait." in + eval_call (query (phrase,tip_id())) coq + | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> + let to_id, _ = get_id id in + if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" + else prerr_endline "Good tip" + | Tok("#[^\n]*",_) :: _ -> () + | _ -> error "syntax error" + +let grammar = + let open Parser in + let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in + let eat_phrase = eat_balanced '{' in + Alt + [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] + ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "WAIT")] + ; Seq [Item (eat_rex "GOALS")] + ; Seq [Item (eat_rex "FAILGOALS")] + ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] + ; Item (eat_rex "#[^\n]*") + ] + +let read_command inc = Parser.parse grammar inc let usage () = - Printf.printf + error (Printf.sprintf "A fake coqide process talking to a coqtop -ideslave.\n\ - Usage: %s []\n\ - Input syntax is one API call per line, the keyword coming first,\n\ - with the rest of the line as string argument (e.g. INTERP Check plus.)\n\ - Supported API keywords are:\n" (Filename.basename Sys.argv.(0)); - List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands; - exit 1 + Usage: %s (file|-) []\n\ + Input syntax is the following:\n%s\n" + (Filename.basename Sys.argv.(0)) + (Parser.print grammar)) + +module Coqide = Spawn.Sync(struct end) let main = Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let coqtop_name = match Array.length Sys.argv with - | 1 -> "coqtop" - | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1) - | _ -> usage () - in - coqtop := Unix.open_process (coqtop_name^" -ideslave"); + let coqtop_name, coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> "coqtop",[|"-ideslave"|], f + | [| _; f; ct |] -> + let ct = Str.split (Str.regexp " ") ct in + List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f + | _ -> usage () in + let inc = if input_file = "-" then stdin else open_in input_file in + let coq = + let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in + let ip = Xml_parser.make (Xml_parser.SChannel cin) in + let op = Xml_printer.make (Xml_printer.TChannel cout) in + Xml_parser.check_eof ip false; + { xml_printer = op; xml_parser = ip } in + let init () = + match base_eval_call ~print:false (Xmlprotocol.init None) coq with + | Interface.Good id -> + let dir = Filename.dirname input_file in + let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in + let eid, tip = add_sentence ~name:"initial" phrase in + after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) + | Interface.Fail _ -> error "init call failed" in + let finish () = + match base_eval_call (Xmlprotocol.status true) coq with + | Interface.Good _ -> exit 0 + | Interface.Fail (_,_,s) -> error s in + (* The main loop *) + init (); while true do - let l = try read_line () with End_of_file -> exit 0 - in - try read_eval_print l - with - | Comment -> () - | e -> - prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1 + let cmd = try read_command inc with End_of_file -> finish () in + try eval_print cmd coq + with e -> error ("Uncaught exception " ^ Printexc.to_string e) done + +(* vim:set foldmethod=marker: *) diff --git a/tools/gallina-db.el b/tools/gallina-db.el new file mode 100644 index 00000000..baabebb1 --- /dev/null +++ b/tools/gallina-db.el @@ -0,0 +1,240 @@ +;;; gallina-db.el --- coq keywords database utility functions +;; +;; Author: Pierre Courtieu +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; + +;;; We store all information on keywords (tactics or command) in big +;; tables (ex: `coq-tactics-db') From there we get: menus including +;; "smart" commands, completions for command coq-insert-... +;; abbrev tables and font-lock keyword + +;;; real value defined below + +;;; Commentary: +;; + +;;; Code: + +;(require 'proof-config) ; for proof-face-specs, a macro +;(require 'holes) + +(defconst coq-syntax-db nil + "Documentation-only variable, for coq keyword databases. +Each element of a keyword database contains the definition of a \"form\", of the +form: + +(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE) + +MENUNAME is the name of form (or form variant) as it should appear in menus or +completion lists. + +ABBREV is the abbreviation for completion via \\[expand-abbrev]. + +INSERT is the complete text of the form, which may contain holes denoted by +\"#\" or \"@{xxx}\". + +If non-nil the optional STATECH specifies that the command is not state +preserving for coq. + +If non-nil the optional KWREG is the regexp to colorize correponding to the +keyword. ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\"). +*WARNING*: A regexp longer than another one should be put FIRST. For example: + + (\"Module Type\" ... ... t \"Module\\s-+Type\") + (\"Module\" ... ... t \"Module\") + +Is ok because the longer regexp is recognized first. + +If non-nil the optional INSERT-FUN is the function to be called when inserting +the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This +allows writing functions asking for more information to assist the user. + +If non-nil the optional HIDE specifies that this form should not appear in the +menu but only in interactive completions. + +Example of what could be in your emacs init file: + +(defvar coq-user-tactics-db + '( + (\"mytac\" \"mt\" \"mytac # #\" t \"mytac\") + (\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\") + )) + +Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, +will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a +new keyword to colorize." ) + +(defun coq-insert-from-db (db prompt) + "Ask for a keyword, with completion on keyword database DB and insert. +Insert corresponding string with holes at point. If an insertion function is +present for the keyword, call it instead. see `coq-syntax-db' for DB +structure." + (let* ((tac (completing-read (concat prompt " (tab for completion) : ") + db nil nil)) + (infos (cddr (assoc tac db))) + (s (car infos)) ; completion to insert + (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function + (pt (point))) + (if f (funcall f) ; call f if present + (insert (or s tac)) ; insert completion and indent otherwise + (holes-replace-string-by-holes-backward-jump pt) + (indent-according-to-mode)))) + + + +(defun coq-build-regexp-list-from-db (db &optional filter) + "Take a keyword database DB and return the list of regexps for font-lock. +If non-nil Optional argument FILTER is a function applying to each line of DB. +For each line if FILTER returns nil, then the keyword is not added to the +regexp. See `coq-syntax-db' for DB structure." + (let ((l db) (res ())) + (while l + (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing + (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string + ) + ;; TODO delete doublons + (when (and e5 (or (not filter) (funcall filter hd))) + (setq res (nconc res (list e5)))) ; careful: nconc destructive! + (setq l tl))) + res + )) + +;; Computes the max length of strings in a list +(defun max-length-db (db) + "Return the length of the longest first element (menu label) of DB. +See `coq-syntax-db' for DB structure." + (let ((l db) (res 0)) + (while l + (let ((lgth (length (car (car l))))) + (setq res (max lgth res)) + (setq l (cdr l)))) + res)) + + + +(defun coq-build-menu-from-db-internal (db lgth menuwidth) + "Take a keyword database DB and return one insertion submenu. +Argument LGTH is the max size of the submenu. Argument MENUWIDTH is the width +of the largest line in the menu (without abbrev and shortcut specifications). +Used by `coq-build-menu-from-db', which you should probably use instead. See +`coq-syntax-db' for DB structure." + (let ((l db) (res ()) (size lgth) + (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) + (while (and l (> size 0)) + (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing + (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string + (e6 (car-safe tl5)) ; e6 = function for smart insertion + (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu + (entry-with (max (- menuwidth (length e1)) 0)) + (spaces (make-string entry-with ? )) + ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) + ) + (when (not e7) ;; if not hidden + (let ((menu-entry + (vector + ;; menu entry label + (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) + ;;insertion function if present otherwise insert completion + (if e6 e6 `(holes-insert-and-expand ,e3)) + t))) + (setq res (nconc res (list menu-entry)))));; append *in place* + (setq l tl) + (setq size (- size 1)))) + res)) + + +(defun coq-build-title-menu (db size) + "Build a title for the first submenu of DB, of size SIZE. +Return the string made of the first and the SIZE nth first element of DB, +separated by \"...\". Used by `coq-build-menu-from-db'. See `coq-syntax-db' +for DB structure." + (concat (car-safe (car-safe db)) + " ... " + (car-safe (car-safe (nthcdr (- size 1) db))))) + +(defun coq-sort-menu-entries (menu) + (sort menu + '(lambda (x y) (string< + (downcase (elt x 0)) + (downcase (elt y 0)))))) + +(defun coq-build-menu-from-db (db &optional size) + "Take a keyword database DB and return a list of insertion menus for them. +Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB +structure." + ;; sort is destructive for the list, so copy list before sorting + (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) + (wdth (+ 2 (max-length-db db))) + (sz (or size 30)) (lgth (length l))) + (while l + (if (<= lgth sz) + (setq res ;; careful: nconc destructive! + (nconc res (list (cons + (coq-build-title-menu l lgth) + (coq-build-menu-from-db-internal l lgth wdth))))) + (setq res ; careful: nconc destructive! + (nconc res (list (cons + (coq-build-title-menu l sz) + (coq-build-menu-from-db-internal l sz wdth)))))) + (setq l (nthcdr sz l)) + (setq lgth (length l))) + res)) + +(defun coq-build-abbrev-table-from-db (db) + "Take a keyword database DB and return an abbrev table. +See `coq-syntax-db' for DB structure." + (let ((l db) (res ())) + (while l + (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + ) + ;; careful: nconc destructive! + (when e2 + (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) + (setq l tl))) + res)) + + +(defun filter-state-preserving (l) + ; checkdoc-params: (l) + "Not documented." + (not (nth 3 l))) ; fourth argument is nil --> state preserving command + +(defun filter-state-changing (l) + ; checkdoc-params: (l) + "Not documented." + (nth 3 l)) ; fourth argument is nil --> state preserving command + +(defconst coq-solve-tactics-face 'coq-solve-tactics-face + "Expression that evaluates to a face. +Required so that 'proof-solve-tactics-face is a proper facename") + + +;;A new face for tactics which fail when they don't kill the current goal +(defface coq-solve-tactics-face + '((t (:background "red"))) + "Face for names of closing tactics in proof scripts." + :group 'proof-faces) + + + + + +(provide 'gallina-db) + +;;; gallina-db.el ends here + +;** Local Variables: *** +;** fill-column: 80 *** +;** End: *** diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el new file mode 100644 index 00000000..c25abece --- /dev/null +++ b/tools/gallina-syntax.el @@ -0,0 +1,982 @@ +;; gallina-syntax.el Font lock expressions for Coq +;; Copyright (C) 1997-2007 LFCS Edinburgh. +;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Pierre Courtieu + +;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp + +;(require 'proof-syntax) +;(require 'proof-utils) ; proof-locate-executable +(require 'gallina-db) + + + + ;;; keyword databases + + +(defcustom coq-user-tactics-db nil + "User defined tactic information. See `coq-syntax-db' for + syntax. It is not necessary to add your own tactics here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your tactics will be colorized by font-lock + + 2 your tactics will be added to the menu and to completion when + calling \\[coq-insert-tactic] + + 3 you may define an abbreviation for your tactic." + + :type '(repeat sexp) + :group 'coq) + + +(defcustom coq-user-commands-db nil + "User defined command information. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + +(defcustom coq-user-tacticals-db nil + "User defined tactical information. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + +(defcustom coq-user-solve-tactics-db nil + "User defined closing tactics. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + + + +(defcustom coq-user-reserved-db nil + "User defined reserved keywords information. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + + + +(defvar coq-tactics-db + (append + coq-user-tactics-db + '( + ("absurd " "abs" "absurd " t "absurd") + ("apply" "ap" "apply " t "apply") + ("assert by" "assb" "assert ( # : # ) by #" t "assert") + ("assert" "ass" "assert ( # : # )" t) + ;; ("assumption" "as" "assumption" t "assumption") + ("auto with arith" "awa" "auto with arith" t) + ("auto with" "aw" "auto with @{db}" t) + ("auto" "a" "auto" t "auto") + ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) + ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) + ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) + ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") + ("case" "c" "case " t "case") + ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") + ("change in" "chi" "change # in #" t) + ("change with in" "chwi" "change # with # in #" t) + ("change with" "chw" "change # with" t) + ("change" "ch" "change " t "change") + ("clear" "cl" "clear" t "clear") + ("clearbody" "cl" "clearbody" t "clearbody") + ("cofix" "cof" "cofix" t "cofix") + ("coinduction" "coind" "coinduction" t "coinduction") + ("compare" "cmpa" "compare # #" t "compare") + ("compute" "cmpu" "compute" t "compute") + ;; ("congruence" "cong" "congruence" t "congruence") + ("constructor" "cons" "constructor" t "constructor") + ;; ("contradiction" "contr" "contradiction" t "contradiction") + ("cut" "cut" "cut" t "cut") + ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") + ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") + ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") + ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") + ("decompose" "dec" "decompose [#] #" t "decompose") + ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") + ("dependent inversion with" "depinvw" "dependent inversion # with #" t) + ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") + ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t) + ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite") + ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t) + ("destruct as" "desa" "destruct # as #" t) + ("destruct using" "desu" "destruct # using #" t) + ("destruct" "des" "destruct " t "destruct") + ;; ("discriminate" "dis" "discriminate" t "discriminate") + ("discrR" "discrR" "discrR" t "discrR") + ("double induction" "dind" "double induction # #" t "double\\s-+induction") + ("eapply" "eap" "eapply #" t "eapply") + ("eauto with arith" "eawa" "eauto with arith" t) + ("eauto with" "eaw" "eauto with @{db}" t) + ("eauto" "ea" "eauto" t "eauto") + ("econstructor" "econs" "econstructor" t "econstructor") + ("eexists" "eex" "eexists" t "eexists") + ("eleft" "eleft" "eleft" t "eleft") + ("elim using" "elu" "elim # using #" t) + ("elim" "e" "elim #" t "elim") + ("elimtype" "elt" "elimtype" "elimtype") + ("eright" "erig" "eright" "eright") + ("esplit" "esp" "esplit" t "esplit") + ;; ("exact" "exa" "exact" t "exact") + ("exists" "ex" "exists #" t "exists") + ;; ("fail" "fa" "fail" nil) + ;; ("field" "field" "field" t "field") + ("firstorder" "fsto" "firstorder" t "firstorder") + ("firstorder with" "fsto" "firstorder with #" t) + ("firstorder with using" "fsto" "firstorder # with #" t) + ("fold" "fold" "fold #" t "fold") + ;; ("fourier" "four" "fourier" t "fourier") + ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") + ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") + ("generalize" "g" "generalize #" t "generalize") + ("hnf" "hnf" "hnf" t "hnf") + ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id + ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals + ("induction" "ind" "induction #" t "induction") + ("induction using" "indu" "induction # using #" t) + ("injection" "inj" "injection #" t "injection") + ("instantiate" "inst" "instantiate" t "instantiate") + ("intro" "i" "intro" t "intro") + ("intro after" "ia" "intro # after #" t) + ("intros" "is" "intros #" t "intros") + ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) + ("intros until" "isu" "intros until #" t) + ("intuition" "intu" "intuition #" t "intuition") + ("inversion" "inv" "inversion #" t "inversion") + ("inversion in" "invi" "inversion # in #" t) + ("inversion using" "invu" "inversion # using #" t) + ("inversion using in" "invui" "inversion # using # in #" t) + ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") + ("lapply" "lap" "lapply" t "lapply") + ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") + ("left" "left" "left" t "left") + ("linear" "lin" "linear" t "linear") + ("load" "load" "load" t "load") + ("move after" "mov" "move # after #" t "move") + ("omega" "o" "omega" t "omega") + ("pattern" "pat" "pattern" t "pattern") + ("pattern(s)" "pats" "pattern # , #" t) + ("pattern at" "pata" "pattern # at #" t) + ("pose" "po" "pose ( # := # )" t "pose") + ("prolog" "prol" "prolog" t "prolog") + ("quote" "quote" "quote" t "quote") + ("quote []" "quote2" "quote # [#]" t) + ("red" "red" "red" t "red") + ("refine" "ref" "refine" t "refine") + ;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") + ("rename into" "ren" "rename # into #" t "rename") + ("replace with" "rep" "replace # with #" t "replace") + ("replace with in" "repi" "replace # with # in #" t) + ("rewrite <- in" "ri<" "rewrite <- # in #" t) + ("rewrite <-" "r<" "rewrite <- #" t) + ("rewrite in" "ri" "rewrite # in #" t) + ("rewrite" "r" "rewrite #" t "rewrite") + ("right" "rig" "right" t "right") + ;; ("ring" "ring" "ring #" t "ring") + ("set in * |-" "seth" "set ( # := #) in * |-" t) + ("set in *" "set*" "set ( # := #) in *" t) + ("set in |- *" "setg" "set ( # := #) in |- *" t) + ("set in" "seti" "set ( # := #) in #" t) + ("set" "set" "set ( # := #)" t "set") + ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") + ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") + ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") + ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") + ("simpl" "s" "simpl" t "simpl") + ("simpl" "sa" "simpl # at #" t) + ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") + ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") + ("simple induction" "sind" "simple induction" t "simple\\s-+induction") + ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") + ("specialize" "spec" "specialize" t "specialize") + ("split" "sp" "split" t "split") + ("split_Rabs" "spra" "splitRabs" t "split_Rabs") + ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") + ("stepl" "stl" "stepl #" t "stepl") + ("stepl by" "stlb" "stepl # by #" t) + ("stepr" "str" "stepr #" t "stepr") + ("stepr by" "strb" "stepr # by #" t) + ("subst" "su" "subst #" t "subst") + ("symmetry" "sy" "symmetry" t "symmetry") + ("symmetry in" "syi" "symmetry in #" t) + ;; ("tauto" "ta" "tauto" t "tauto") + ("transitivity" "trans" "transitivity #" t "transitivity") + ("trivial" "t" "trivial" t "trivial") + ("trivial with" "tw" "trivial with @{db}" t) + ("unfold" "u" "unfold #" t "unfold") + ("unfold(s)" "us" "unfold # , #" t) + ("unfold in" "unfi" "unfold # in #" t) + ("unfold at" "unfa" "unfold # at #" t) + )) + "Coq tactics information list. See `coq-syntax-db' for syntax. " + ) + +(defvar coq-solve-tactics-db + (append + coq-user-solve-tactics-db + '( + ("assumption" "as" "assumption" t "assumption") + ("by" "by" "by #" t "by") + ("congruence" "cong" "congruence" t "congruence") + ("contradiction" "contr" "contradiction" t "contradiction") + ("decide equality" "deg" "decide equality" t "decide\\s-+equality") + ("discriminate" "dis" "discriminate" t "discriminate") + ("exact" "exa" "exact" t "exact") + ("fourier" "four" "fourier" t "fourier") + ("fail" "fa" "fail" nil) + ("field" "field" "field" t "field") + ("omega" "o" "omega" t "omega") + ("reflexivity" "refl" "reflexivity #" t "reflexivity") + ("ring" "ring" "ring #" t "ring") + ("solve" nil "solve [ # | # ]" nil "solve") + ("tauto" "ta" "tauto" t "tauto") + )) + "Coq tactic(al)s that solve a subgoal." + ) + + +(defvar coq-tacticals-db + (append + coq-user-tacticals-db + '( + ("info" nil "info #" nil "info") + ("first" nil "first [ # | # ]" nil "first") + ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") + ("do" nil "do @{num} @{tac}" nil "do") + ("idtac" nil "idtac") ; also in tactics + ; ("idtac \"" nil "idtac \"#\"") ; also in tactics + ("fail" "fa" "fail" nil "fail") + ; ("fail \"" "fa\"" "fail" nil) ; + ; ("orelse" nil "orelse #" t "orelse") + ("repeat" nil "repeat #" nil "repeat") + ("try" nil "try #" nil "try") + ("progress" nil "progress #" nil "progress") + ("|" nil "[ # | # ]" nil) + ("||" nil "# || #" nil) + )) + "Coq tacticals information list. See `coq-syntax-db' for syntax.") + + + + +(defvar coq-decl-db + '( + ("Axiom" "ax" "Axiom # : #" t "Axiom") + ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") + ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") + ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") + ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") + ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") + ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) + ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") + ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") + ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") + ("Parameter" "par" "Parameter #: #" t "Parameter") + ("Parameters" "par" "Parameter #: #" t "Parameters") + ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") + ("Variable" "v" "Variable #: #." t "Variable") + ("Variables" "vs" "Variables # , #: #." t "Variables") + ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") + ) + "Coq declaration keywords information list. See `coq-syntax-db' for syntax." + ) + +(defvar coq-defn-db + '( + ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") + ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") + ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") + ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful + ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) + ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful + ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) + ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful + ("Definition" "def" "Definition #:# := #." t "Definition");; careful + ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) + ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) + ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) + ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? + ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) + ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) + ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) + ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") + ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") + ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) + ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") + ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") + ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) + ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) + ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") + ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) + ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) + ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) + ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") + ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") + ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) + ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) + ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) + ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) + ("Variant" "indv" "Variant # : # := # : #." t "Variant") + ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t ) + ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t ) + ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) + ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) + ("Let" "Let" "Let # : # := #." t "Let") + ("Ltac" "ltac" "Ltac # := #" t "Ltac") + ("Module :=" "mo" "Module # : # := #." t ) ; careful + ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful + ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful + ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful + ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful + ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful + ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") + ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") + ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) + ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) + ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") + ) + "Coq definition keywords information list. See `coq-syntax-db' for syntax. " + ) + +;; modules and section are indented like goal starters +(defvar coq-goal-starters-db + '( + ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") + ("Chapter" "chp" "Chapter # : #." t "Chapter") + ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") + ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) + ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) + ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful + ("Fact" "fct" "Fact # : #." t "Fact") + ("Goal" nil "Goal #." t "Goal") + ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") + ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") + ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) + ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful + ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful + ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful + ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") + ("Section" "sec" "Section #." t "Section") + ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") + ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") + ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") + ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") + ) + "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " + ) + +;; command that are not declarations, definition or goal starters +(defvar coq-other-commands-db + '( + ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu + ("About" nil "About #." nil "About") + ("Add" nil "Add #." nil "Add" nil t) + ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") + ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") + ("Add Field" nil "Add Field #." t "Add\\s-+Field") + ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") + ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") + ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") + ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") + ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") + ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") + ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") + ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") + ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") + ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") + ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") + ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") + ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") + ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") + ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") + ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") + ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") + ("Cd" nil "Cd #." nil "Cd") + ("Check" nil "Check" nil "Check") + ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") + ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") + ("Comments" nil "Comments #." nil "Comments") + ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) + ("Eval" nil "Eval #." nil "Eval") + ("Export" nil "Export #." t "Export") + ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") + ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") + ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") + ("Extraction" "extr" "Extraction @{id}." nil "Extraction") + ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) + ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") + ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") + ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") + ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") + ("Focus" nil "Focus #." nil "Focus") + ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") + ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") + ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") + ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") + ("Import" nil "Import #." t "Import") + ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") + ("Inspect" nil "Inspect #." nil "Inspect") + ("Locate" nil "Locate" nil "Locate") + ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") + ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") + ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) + ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) + ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) + ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) + ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) + ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) + ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") + ("Notation (simple)" "nots" "Notation # := #." t "Notation") + ("Opaque" nil "Opaque #." nil "Opaque") + ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") + ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") + ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") + ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") + ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) + ("Print" "p" "Print #." nil "Print") + ("Qed" nil "Qed." nil "Qed") + ("Pwd" nil "Pwd." nil "Pwd") + ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") + ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") + ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") + ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") + ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") + ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") + ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") + ("Require Export" nil "Require Export #." t "Require\\s-+Export") + ("Require Import" nil "Require Import #." t "Require\\s-+Import") + ("Require" nil "Require #." t "Require") + ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") + ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") + ("Save" nil "Save." t "Save") + ("Search" nil "Search #" nil "Search") + ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") + ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") + ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") + ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") + ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") + ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") + ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") + ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") + ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") + ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") + ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") + ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") + ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") + ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") + ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") + ("Show" nil "Show #." nil "Show") + ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") + ("Test" nil "Test" nil "Test" nil t) + ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") + ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") + ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") + ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") + ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") + ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") + ("Transparent" nil "Transparent #." nil "Transparent") + ("Unfocus" nil "Unfocus." nil "Unfocus") + ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") + ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") + ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") + ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") + ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") + ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") + ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") + ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") + ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") + ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") + ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") + ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") + ; ("print" "pr" "print #" "print") + ) + "Command that are not declarations, definition or goal starters." + ) + +(defvar coq-commands-db + (append coq-decl-db coq-defn-db coq-goal-starters-db + coq-other-commands-db coq-user-commands-db) + "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " + ) + + +(defvar coq-terms-db + '( + ("fun (1 args)" "f" "fun #:# => #" nil "fun") + ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") + ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") + ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") + ("forall" "fo" "forall #:#,#" nil "forall") + ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") + ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") + ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") + ("if" "if" "if # then # else #" nil "if") + ("let in" "li" "let # := # in #" nil "let") + ("match! (from type)" nil "" nil "match" coq-insert-match) + ("match with" "m" "match # with\n| # => #\nend") + ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") + ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") + ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") + ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") + ) + "Coq terms keywords information list. See `coq-syntax-db' for syntax. " + ) + + + + + + + + ;;; Goals (and module/sections) starters detection + + +;; ----- keywords for font-lock. + +;; FIXME da: this one function breaks the nice configuration of Proof General: +;; would like to have proof-goal-regexp instead. +;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, +;; so it appears more difficult than just a proof-goal-regexp setting. +;; Future improvement may simply to be allow a function value for +;; proof-goal-regexp. + +;; FIXME Pierre: the right way IMHO here would be to set a span +;; property 'goalcommand when coq prompt says it (if the name of +;; current proof has changed). + +;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry +;; for the french: +;;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de +;; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) +;; +;; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable +;; uniquement hors d'un MT +;; - si :=MEXPR est absent, elle demarre un nouveau module interactif +;; - si :=MEXPR est present, elle definit un module +;; (la fonction vernac_define_module dans toplevel/vernacentries) +;; +;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] +;; est valable uniquement dans un MT +;; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module +;; interactif +;; - si (:=MEXPR absent, :MTYP present) +;; ou (:=MEXPR present, :MTYP absent) +;; elle declare un module. +;; (la fonction vernac_declare_module dans toplevel/vernacentries) + +(defun coq-count-match (regexp strg) + "Count the number of (maximum, non overlapping) matching substring + of STRG matching REGEXP. Empty match are counted once." + (let ((nbmatch 0) (str strg)) + (while (and (proof-string-match regexp str) (not (string-equal str ""))) + (incf nbmatch) + (if (= (match-end 0) 0) (setq str (substring str 1)) + (setq str (substring str (match-end 0))))) + nbmatch)) + +;; This function is used for amalgamating a proof into a single +;; goal-save region (proof-goal-command-p used in +;; proof-done-advancing-save in generic/proof-script.el) for coq < +;; 8.0. It is the test when looking backward the start of the proof. +;; It is NOT used for coq > v8.1 +;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and +;; lemma names given in the prompt) + +;; compatibility with v8.0, will delete it some day +(defun coq-goal-command-str-v80-p (str) + "See `coq-goal-command-p'." + (let* ((match (coq-count-match "\\" str)) + (with (coq-count-match "\\" str)) + (letwith (+ (coq-count-match "\\" str) (- with match))) + (affect (coq-count-match ":=" str))) + + (and (proof-string-match coq-goal-command-regexp str) + (not ; + (and + (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) + (not (= letwith affect)))) + (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) + ) + ) + ) + +;; Module and or section openings are detected syntactically. Module +;; *openings* are difficult to detect because there can be Module +;; ...with X := ... . So we need to count :='s to detect real openings. + +;; TODO: have opened section/chapter in the prompt too, and get rid of +;; syntactical tests everywhere +(defun coq-module-opening-p (str) + "Decide whether STR is a module or section opening or not. +Used by `coq-goal-command-p'" + (let* ((match (coq-count-match "\\" str)) + (with (coq-count-match "\\" str)) + (letwith (+ (coq-count-match "\\" str) (- with match))) + (affect (coq-count-match ":=" str))) + (and (proof-string-match "\\`\\(Module\\)\\>" str) + (= letwith affect)) + )) + +(defun coq-section-command-p (str) + (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) + + +(defun coq-goal-command-str-v81-p (str) + "Decide syntactically whether STR is a goal start or not. Use + `coq-goal-command-p-v81' on a span instead if possible." + (coq-goal-command-str-v80-p str) + ) + +;; This is the function that tests if a SPAN is a goal start. All it +;; has to do is look at the 'goalcmd attribute of the span. +;; It also looks if this is not a module start. + +;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs +;; something in the coq prompt telling the name of all opened modules +;; (like for open goals), and use it to set goalcmd --> no more need +;; to look at Modules and section (actually indentation will still +;; need it) +(defun coq-goal-command-p-v81 (span) + "see `coq-goal-command-p'" + (or (span-property span 'goalcmd) + ;; module and section starts are detected here + (let ((str (or (span-property span 'cmd) ""))) + (or (coq-section-command-p str) + (coq-module-opening-p str)) + ))) + +;; In coq > 8.1 This is used only for indentation. +(defun coq-goal-command-str-p (str) + "Decide whether argument is a goal or not. Use + `coq-goal-command-p' on a span instead if posible." + (cond + (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) + (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) + (t (coq-goal-command-str-v80-p str));; this is temporary + )) + +;; This is used for backtracking +(defun coq-goal-command-p (span) + "Decide whether argument is a goal or not." + (cond + (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) + (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) + (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary + )) + +(defvar coq-keywords-save-strict + '("Defined" + "Save" + "Qed" + "End" + "Admitted" + "Abort" + )) + +(defvar coq-keywords-save + (append coq-keywords-save-strict '("Proof")) + ) + +(defun coq-save-command-p (span str) + "Decide whether argument is a Save command or not" + (or (proof-string-match coq-save-command-regexp-strict str) + (and (proof-string-match "\\`Proof\\>" str) + (not (proof-string-match "Proof\\s-*\\(\\.\\|\\\\)" str))) + ) + ) + + +(defvar coq-keywords-kill-goal + '("Abort")) + +;; Following regexps are all state changing +(defvar coq-keywords-state-changing-misc-commands + (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) + +(defvar coq-keywords-goal + (coq-build-regexp-list-from-db coq-goal-starters-db)) + +(defvar coq-keywords-decl + (coq-build-regexp-list-from-db coq-decl-db)) + +(defvar coq-keywords-defn + (coq-build-regexp-list-from-db coq-defn-db)) + + +(defvar coq-keywords-state-changing-commands + (append + coq-keywords-state-changing-misc-commands + coq-keywords-decl ; all state changing + coq-keywords-defn ; idem + coq-keywords-goal)) ; idem + + +;; +(defvar coq-keywords-state-preserving-commands + (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) + +;; concat this is faster that redoing coq-build-regexp-list-from-db on +;; whole commands-db +(defvar coq-keywords-commands + (append coq-keywords-state-changing-commands + coq-keywords-state-preserving-commands) + "All commands keyword.") + +(defvar coq-solve-tactics + (coq-build-regexp-list-from-db coq-solve-tactics-db) + "Keywords for closing tactic(al)s.") + +(defvar coq-tacticals + (coq-build-regexp-list-from-db coq-tacticals-db) + "Keywords for tacticals in a Coq script.") + + + ;; From JF Monin: +(defvar coq-reserved + (append + coq-user-reserved-db + '( + "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" + "return" "struct" "else" "end" "if" "in" "into" "let" "then" + "using" "with" "beta" "delta" "iota" "zeta" "after" "until" + "at" "Sort" "Time")) + "Reserved keywords of Coq.") + + +(defvar coq-state-changing-tactics + (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) + +(defvar coq-state-preserving-tactics + (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) + + +(defvar coq-tactics + (append coq-state-changing-tactics coq-state-preserving-tactics)) + +(defvar coq-retractable-instruct + (append coq-state-changing-tactics coq-keywords-state-changing-commands)) + +(defvar coq-non-retractable-instruct + (append coq-state-preserving-tactics + coq-keywords-state-preserving-commands)) + +(defvar coq-keywords + (append coq-keywords-goal coq-keywords-save coq-keywords-decl + coq-keywords-defn coq-keywords-commands) + "All keywords in a Coq script.") + + + +(defvar coq-symbols + '("|" + "||" + ":" + ";" + "," + "(" + ")" + "[" + "]" + "{" + "}" + ":=" + "=>" + "->" + ".") + "Punctuation Symbols used by Coq.") + +;; ----- regular expressions +(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" + "A regexp indicating that the Coq process has identified an error.") + +(defvar coq-id proof-id) +(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") + +(defvar coq-ids (proof-ids coq-id " ")) + +(defun coq-first-abstr-regexp (paren end) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) + +(defcustom coq-variable-highlight-enable t + "Activates partial bound variable highlighting" + :type 'boolean + :group 'coq) + + +(defvar coq-font-lock-terms + (if coq-variable-highlight-enable + (list + ;; lambda binders + (list (coq-first-abstr-regexp "\\" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) + ;; forall binder + (list (coq-first-abstr-regexp "\\" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + ; (list "\\" + ; (list 0 font-lock-type-face) + ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil + ; (list 0 font-lock-variable-name-face))) + ;; parenthesized binders + (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) + )) + "*Font-lock table for Coq terms.") + + + +;; According to Coq, "Definition" is both a declaration and a goal. +;; It is understood here as being a goal. This is important for +;; recognizing global identifiers, see coq-global-p. +(defconst coq-save-command-regexp-strict + (proof-anchor-regexp + (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) + "\\)"))) +(defconst coq-save-command-regexp + (proof-anchor-regexp + (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) + "\\)"))) +(defconst coq-save-with-hole-regexp + (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) + "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) + +(defconst coq-goal-command-regexp + (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) + +(defconst coq-goal-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) + "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) + +(defconst coq-decl-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) + "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) + +;; (defconst coq-decl-with-hole-regexp +;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) + +(defconst coq-defn-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) + "\\)\\s-+\\(" coq-id "\\)")) + +;; must match: +;; "with f x y :" (followed by = or not) +;; "with f x y (z:" (not followed by =) +;; BUT NOT: +;; "with f ... (x:=" +;; "match ... with .. => " +(defconst coq-with-with-hole-regexp + (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" + coq-id "\\s-*:[^=]\\)")) +;; marche aussi a peu pres +;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) +;;"\\\\|\\\\|\\" +(defvar coq-font-lock-keywords-1 + (append + coq-font-lock-terms + (list + (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) + (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) + (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) + (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) + (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) + (cons "============================" 'font-lock-keyword-face) + (cons "Subtree proved!" 'font-lock-keyword-face) + (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) + (list "^\\([^ \n]+\\) \\(is defined\\)" + (list 2 'font-lock-keyword-face t) + (list 1 'font-lock-function-name-face t)) + + (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) + (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) + (list + (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) + ;; Remove spurious variable and function faces on commas. + '(proof-zap-commas)))) + +(defvar coq-font-lock-keywords coq-font-lock-keywords-1) + +(defun coq-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + + (modify-syntax-entry ?\$ ".") + (modify-syntax-entry ?\/ ".") + (modify-syntax-entry ?\\ ".") + (modify-syntax-entry ?+ ".") + (modify-syntax-entry ?- ".") + (modify-syntax-entry ?= ".") + (modify-syntax-entry ?% ".") + (modify-syntax-entry ?< ".") + (modify-syntax-entry ?> ".") + (modify-syntax-entry ?\& ".") + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + +;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug + (modify-syntax-entry ?\. ".") + + (condition-case nil + ;; Try to use Emacs-21's nested comments. + (modify-syntax-entry ?\* ". 23n") + ;; Revert to non-nested comments if that failed. + (error (modify-syntax-entry ?\* ". 23"))) + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + + +(defconst coq-generic-expression + (mapcar (lambda (kw) + (list (capitalize kw) + (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) + 1)) + (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) + +(provide 'gallina-syntax) + ;;; gallina-syntax.el ends here + +; Local Variables: *** +; indent-tabs-mode: nil *** +; End: *** diff --git a/tools/gallina.el b/tools/gallina.el new file mode 100644 index 00000000..cbc13118 --- /dev/null +++ b/tools/gallina.el @@ -0,0 +1,142 @@ +;; gallina.el --- Coq mode editing commands for Emacs +;; +;; Jean-Christophe Filliatre, march 1995 +;; Shamelessly copied from caml.el, Xavier Leroy, july 1993. +;; +;; modified by Marco Maggesi for gallina-inferior + +; compatibility code for proofgeneral files +(require 'coq-font-lock) +; ProofGeneral files. remember to remove coq version tests in +; gallina-syntax.el +(require 'gallina-syntax) + +(defvar coq-mode-map nil + "Keymap used in Coq mode.") +(if coq-mode-map + () + (setq coq-mode-map (make-sparse-keymap)) + (define-key coq-mode-map "\t" 'coq-indent-command) + (define-key coq-mode-map "\M-\t" 'coq-unindent-command) + (define-key coq-mode-map "\C-c\C-c" 'compile) +) + +(defvar coq-mode-syntax-table nil + "Syntax table in use in Coq mode buffers.") +(if coq-mode-syntax-table + () + (setq coq-mode-syntax-table (make-syntax-table)) + ; ( is first character of comment start + (modify-syntax-entry ?\( "()1" coq-mode-syntax-table) + ; * is second character of comment start, + ; and first character of comment end + (modify-syntax-entry ?* ". 23" coq-mode-syntax-table) + ; ) is last character of comment end + (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table) + ; quote is a string-like delimiter (for character literals) + (modify-syntax-entry ?' "\"" coq-mode-syntax-table) + ; quote is part of words + (modify-syntax-entry ?' "w" coq-mode-syntax-table) +) + +(defvar coq-mode-indentation 2 + "*Indentation for each extra tab in Coq mode.") + +(defun coq-mode-variables () + (set-syntax-table coq-mode-syntax-table) + (make-local-variable 'paragraph-start) + (setq paragraph-start (concat "^$\\|" page-delimiter)) + (make-local-variable 'paragraph-separate) + (setq paragraph-separate paragraph-start) + (make-local-variable 'paragraph-ignore-fill-prefix) + (setq paragraph-ignore-fill-prefix t) + (make-local-variable 'require-final-newline) + (setq require-final-newline t) + (make-local-variable 'comment-start) + (setq comment-start "(* ") + (make-local-variable 'comment-end) + (setq comment-end " *)") + (make-local-variable 'comment-column) + (setq comment-column 40) + (make-local-variable 'comment-start-skip) + (setq comment-start-skip "(\\*+ *") + (make-local-variable 'parse-sexp-ignore-comments) + (setq parse-sexp-ignore-comments nil) + (make-local-variable 'indent-line-function) + (setq indent-line-function 'coq-indent-command) + (make-local-variable 'font-lock-keywords) + (setq font-lock-defaults '(coq-font-lock-keywords-1))) + +;;; The major mode + +(defun coq-mode () + "Major mode for editing Coq code. +Tab at the beginning of a line indents this line like the line above. +Extra tabs increase the indentation level. +\\{coq-mode-map} +The variable coq-mode-indentation indicates how many spaces are +inserted for each indentation level." + (interactive) + (kill-all-local-variables) + (setq major-mode 'coq-mode) + (setq mode-name "coq") + (use-local-map coq-mode-map) + (coq-mode-variables) + (run-hooks 'coq-mode-hook)) + +;;; Indentation stuff + +(defun coq-in-indentation () + "Tests whether all characters between beginning of line and point +are blanks." + (save-excursion + (skip-chars-backward " \t") + (bolp))) + +(defun coq-indent-command () + "Indent the current line in Coq mode. +When the point is at the beginning of an empty line, indent this line like +the line above. +When the point is at the beginning of an indented line +\(i.e. all characters between beginning of line and point are blanks\), +increase the indentation by one level. +The indentation size is given by the variable coq-mode-indentation. +In all other cases, insert a tabulation (using insert-tab)." + (interactive) + (let* ((begline + (save-excursion + (beginning-of-line) + (point))) + (current-offset + (- (point) begline)) + (previous-indentation + (save-excursion + (if (eq (forward-line -1) 0) (current-indentation) 0)))) + (cond ((and (bolp) + (looking-at "[ \t]*$") + (> previous-indentation 0)) + (indent-to previous-indentation)) + ((coq-in-indentation) + (indent-to (+ current-offset coq-mode-indentation))) + (t + (insert-tab))))) + +(defun coq-unindent-command () + "Decrease indentation by one level in Coq mode. +Works only if the point is at the beginning of an indented line +\(i.e. all characters between beginning of line and point are blanks\). +Does nothing otherwise." + (interactive) + (let* ((begline + (save-excursion + (beginning-of-line) + (point))) + (current-offset + (- (point) begline))) + (if (and (>= current-offset coq-mode-indentation) + (coq-in-indentation)) + (backward-delete-char-untabify coq-mode-indentation)))) + +;;; gallina.el ends here + +(provide 'gallina) diff --git a/tools/gallina.ml b/tools/gallina.ml index 2e9a17f6..279919c5 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* &2 + exit 1;; + *) + dir="$dir $1";; + esac + shift +done + +script=`tempfile` +create_script > $script +find $dir -name '*.v' | +while read file; do + mv $file $file.bak + awk -f $script $file.bak > $file +done diff --git a/tools/win32hack.mllib b/tools/win32hack.mllib deleted file mode 100644 index 42395f65..00000000 --- a/tools/win32hack.mllib +++ /dev/null @@ -1 +0,0 @@ -Win32hack_filename \ No newline at end of file diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml deleted file mode 100644 index 74f70686..00000000 --- a/tools/win32hack_filename.ml +++ /dev/null @@ -1,4 +0,0 @@ -(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/". - Let's tweak that... *) - -let _ = Filename.dir_sep.[0] <- '\\' -- cgit v1.2.3