The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

Dear Coq users, 

Here are a few lines that you can insert in your .emacs. In defines
the functions : 

  coq-find-file
  coq-find-file-read-only

That search a file in the $COQTOP subtrees, and completes the suffixe
.ml, .mli, .ml4 or .v if not given. For example 

M-x coq-find-file       and then      term 

opens $COQTOP/src/constr/term.ml. That tool can be useful when
developing tactics in Coq.

The following functions are also defined :

        gml
        gmli 
        gml4
        gv

They do a grep in all the .ml files (resp. .mli, .ml4 or .v) of the
$COQTOP subdirectories for the given regular expressions.

Best regards
-- 
Patrick.Loiseleur AT lri.fr

===========================================================================
(defvar coq-load-path (let ((coqtop (getenv "COQTOP")))
  (cons (concat coqtop "/")
  (cons (concat coqtop "/doc/")
  (cons (concat coqtop "/doc/library/")
  (cons (concat coqtop "/doc/omega/")
  (cons (concat coqtop "/src/")
  (cons (concat coqtop "/src/config/")
  (cons (concat coqtop "/src/constr/")
  (cons (concat coqtop "/src/env/")
  (cons (concat coqtop "/src/launch/")
  (cons (concat coqtop "/src/lib/")
  (cons (concat coqtop "/src/lib/stream-pp/")
  (cons (concat coqtop "/src/lib/util/")
  (cons (concat coqtop "/src/link/")
  (cons (concat coqtop "/src/man/")
  (cons (concat coqtop "/src/meta/")
  (cons (concat coqtop "/src/parsing/")
  (cons (concat coqtop "/src/proofs/")
  (cons (concat coqtop "/src/syntax/")
  (cons (concat coqtop "/src/tactics/")
  (cons (concat coqtop "/src/typing/")
  (cons (concat coqtop "/states/")
  (cons (concat coqtop "/tactics/")
  (cons (concat coqtop "/tactics/contrib/")
  (cons (concat coqtop "/tactics/contrib/polynom/")
  (cons (concat coqtop "/tactics/contrib/extraction/")
  (cons (concat coqtop "/tactics/contrib/linear/")
  (cons (concat coqtop "/tactics/contrib/natural/")
  (cons (concat coqtop "/tactics/contrib/omega/")
  (cons (concat coqtop "/tactics/contrib/reflexion/")
  (cons (concat coqtop "/tactics/tcc/")
  (cons (concat coqtop "/tactics/programs/")
  (cons (concat coqtop "/tactics/programs/gop/")
  (cons (concat coqtop "/theories/")
  (cons (concat coqtop "/theories/ARITH/")
  (cons (concat coqtop "/theories/BOOL/")
  (cons (concat coqtop "/theories/DEMOS/")
  (cons (concat coqtop "/theories/DEMOS/OMEGA/")
  (cons (concat coqtop "/theories/DEMOS/OMEGA/ARITH-OMEGA/")
  (cons (concat coqtop "/theories/DEMOS/PROGRAMS/")
  (cons (concat coqtop "/theories/INIT/")
  (cons (concat coqtop "/theories/LISTS/")
  (cons (concat coqtop "/theories/LOGIC/")
  (cons (concat coqtop "/theories/RELATIONS/")
  (cons (concat coqtop "/theories/RELATIONS/WELLFOUNDED/")
  (cons (concat coqtop "/theories/SETS/")
  (cons (concat coqtop "/theories/SORTING/")
  (cons (concat coqtop "/theories/TESTS/")
  (cons (concat coqtop "/theories/ZARITH/")
  (cons (concat coqtop "/theories/ZARITH/WITH-OMEGA/")
  (cons (concat coqtop "/tools/")
  (cons (concat coqtop "/tools/camlp4/")
  (cons (concat coqtop "/tools/coq-tex/")
  (cons (concat coqtop "/tools/coqdep/")
  (cons (concat coqtop "/tools/do_Makefile/")
  (cons (concat coqtop "/tools/emacs/")
  (cons (concat coqtop "/tools/filters/")
  (cons (concat coqtop "/tools/gallina/")
  (cons (concat coqtop "/tools/coqinstall/") nil
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(defun coq-find-file (filename)
   "Find and open a file in the $COQTOP subdirectories"
  (interactive "sFind a coq file: ")
  (catch 'answer
    (mapcar
     '(lambda (dir)
        (mapcar
         '(lambda (suf)
            (let ((try (concat dir (concat filename suf))))
              (and (file-readable-p try)
                   (null (file-directory-p try))
                   (progn
                     (find-file try)
                     (throw 'answer try)))))
         '(".ml" ".ml4" ".mli" ".v" "")))
     coq-load-path)
    (message "No file %s in coqtop subdirectories" filename)
    nil))

(defun coq-find-file-read-only (filename)
   "Find and open READ-ONLY a file in the $COQTOP subdirectories"
  (interactive "sFind a coq file read-only: ")
  (catch 'answer
    (mapcar
     '(lambda (dir)
        (mapcar
         '(lambda (suf)
            (let ((try (concat dir (concat filename suf))))
              (and (file-readable-p try)
                   (null (file-directory-p try))
                   (progn
                     (find-file-read-only try)
                     (throw 'answer try)))))
         '(".ml" ".ml4" ".mli" ".v" "")))
     coq-load-path)
    (message "No file %s in coqtop subdirectories" filename)
    nil))

(defun grepcoq (file-pattern pattern)
  "Does grep pattern in all files whose name matches file-pattern in
    $COQTOP subdirectories"
  (shell-command (concat (concat "find " 
                         (getenv "COQTOP") 
                         " -name "
                         file-pattern
                         " -exec grep -n \""
                         pattern 
                         "\" {} \\; -print"))))

(defun gml (pattern)
  "Does a grep in all ml files of the $COQTOP subdirectories"
  (interactive "sGrep in Coq ml files the regexp: ")
  (grepcoq "\\*.ml" pattern))

(defun gmli (pattern)
  "Does a grep in all mli files of the $COQTOP subdirectories"
  (interactive "sGrep in Coq mli files the regexp: ")
  (grepcoq "\\*.mli" pattern))

(defun gml4 (pattern)
  "Does a grep in all ml4 files of the $COQTOP subdirectories"
  (interactive "sGrep in Coq ml4 files the regexp: ")
  (grepcoq "\\*.ml4" pattern))

(defun gv (pattern)
  "Does a grep in all ml files of the $COQTOP subdirectories"
  (interactive "sGrep in Coq vernac files the regexp: ")
  (grepcoq "\\*.v" pattern))