From 568dffcc32cfdec78e7824fa6875d892fb9cfd5a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 6 Jan 2018 12:26:49 +0100 Subject: Remove dir-locals and ship suggested helper hooks instead. .dir-locals led to issues with unsafe local variable warnings. With this method the user is opting in to running this code so there are no warnings. --- .dir-locals.el | 37 -------------------------- dev/README | 4 +++ dev/tools/coqdev.el | 69 +++++++++++++++++++++++++++++++++++++++++++++++++ plugins/.dir-locals.el | 4 --- theories/.dir-locals.el | 4 --- 5 files changed, 73 insertions(+), 45 deletions(-) delete mode 100644 .dir-locals.el create mode 100644 dev/tools/coqdev.el delete mode 100644 plugins/.dir-locals.el delete mode 100644 theories/.dir-locals.el diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index e32ce14a4..000000000 --- a/.dir-locals.el +++ /dev/null @@ -1,37 +0,0 @@ -;; EMACS CONFIGURATION FOR COQ DEVELOPPERS This configuration will be -;; executed for each opened file under coq root directory. -((nil - . ((eval - . (progn - ;; coq root directory (ending with slash) - (let ((coq-root-directory (when buffer-file-name - (locate-dominating-file - buffer-file-name - ".dir-locals.el"))) - (coq-project-find-file - (and (boundp 'coq-project-find-file) coq-project-find-file))) - ;; coq tags file and coq debugger executable - (set (make-local-variable 'tags-file-name) - (concat coq-root-directory "TAGS")) - (setq camldebug-command-name (concat coq-root-directory - "dev/ocamldebug-coq")) - - ;; Setting the compilation directory to coq root. This is - ;; mutually exclusive with the setting of default-directory - ;; below. Also setting the path for next error. - (unless coq-project-find-file - (set (make-local-variable 'compile-command) - (concat "make -C " coq-root-directory)) - (set (make-local-variable 'compilation-search-path) - (cons coq-root-directory nil))) - - ;; Set default directory to coq root ONLY IF variable - ;; coq-project-find-file is non nil. This should remain a - ;; user preference and not be set by default. This setting - ;; is redundant with compile-command above as M-x compile - ;; always CD's to default directory. To enable it add this - ;; to your emacs config: (setq coq-project-find-file t) - (when coq-project-find-file - (setq default-directory coq-root-directory)))) - )) - )) diff --git a/dev/README b/dev/README index b446c3e97..f97e2a769 100644 --- a/dev/README +++ b/dev/README @@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- +coqdev.el: helper customizations for everyday Coq development, eg + making `compile' work in subdirectories + objects.el: various development utilities at emacs level + anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el new file mode 100644 index 000000000..581995d46 --- /dev/null +++ b/dev/tools/coqdev.el @@ -0,0 +1,69 @@ +;;; coqdev.el --- Emacs helpers for Coq development -*- lexical-binding:t -*- + +;; Copyright (C) 2018 The Coq Development Team + +;; Maintainer: coqdev@inria.fr + +;;; Commentary: + +;; Helpers to set compilation commands, proof general variables, etc +;; for Coq development + +;; You can disable individual features without editing this file by +;; using `remove-hook', for instance +;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +;;; Code: + +(require 'subr-x) + +(defun coqdev-default-directory () + "Return the Coq repository containing `default-directory'." + (when-let ((dir (locate-dominating-file default-directory "META.coq"))) + (expand-file-name dir))) + +(defun coqdev-setup-compile-command () + "Setup `compilate-command' for Coq development." + (when-let ((dir (coqdev-default-directory))) + (setq-local compile-command (concat "make -C " dir)))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +(defvar camldebug-command-name) ; from camldebug.el (caml package) +(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package) +(defun coqdev-setup-camldebug () + "Setup ocamldebug for Coq development. + +Specifically `camldebug-command-name' and `ocamldebug-command-name'." + (when-let ((dir (coqdev-default-directory))) + (setq-local camldebug-command-name (concat dir "dev/ocamldebug-coq")) + (setq-local ocamldebug-command-name (concat dir "dev/ocamldebug-coq")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug) + +(defun coqdev-setup-tags () + "Setup `tags-file-name' for Coq development." + (when-let ((dir (coqdev-default-directory))) + (setq-local tags-file-name (concat dir "TAGS")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-tags) + +(defvar coq-prog-args) +(defvar coq-prog-name) + +;; Lets us detect whether there are file local variables +;; even though PG sets it with `setq' when there's a _Coqproject. +;; Also makes sense generally, so might make it into PG someday. +(make-variable-buffer-local 'coq-prog-args) +(setq-default coq-prog-args nil) + +(defun coqdev-setup-proofgeneral () + "Setup Proofgeneral variables for Coq development. + +Note that this function is executed before _Coqproject is read if it exists." + (when-let ((dir (coqdev-default-directory))) + (unless coq-prog-args ; In case there are file-local variables + (setq coq-prog-args `("-coqlib" ,dir + "-R" ,(concat dir "plugins") "Coq" + "-R" ,(concat dir "theories") "Coq"))) + (setq-local coq-prog-name (concat dir "bin/coqtop")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) + +(provide 'coqdev) diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/plugins/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/theories/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) -- cgit v1.2.3 From e4529a4349110c2edb6bd08f873175db71363a84 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 11 Feb 2018 21:55:17 +0100 Subject: coqdev.el: add installation instructions. --- dev/tools/coqdev.el | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 581995d46..f5a0feffa 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -13,6 +13,22 @@ ;; using `remove-hook', for instance ;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) +;;; Installation: + +;; To use this, with coqdev.el located at /path/to/coqdev.el, add the +;; following to your init: + +;; (add-to-list 'load-path "/path/to/coqdev/") +;; (require 'coqdev) + +;; If you load this file from a git repository, checking out an old +;; commit will make it disappear and cause errors for your Emacs +;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; check out a malicious commit Emacs startup would allow it to run +;; arbitrary code, to avoid this you can copy coqdev.el to any +;; location and adjust the load path accordingly (of course if you run +;; ./configure to compile Coq it is already too late). + ;;; Code: (require 'subr-x) @@ -67,3 +83,4 @@ Note that this function is executed before _Coqproject is read if it exists." (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) (provide 'coqdev) +;;; coqdev ends here -- cgit v1.2.3 From 20e654c5b1995e04d103e099bc806d27f797b640 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 11 Feb 2018 21:58:31 +0100 Subject: Merge anomaly-traces-parser.el into coqdev.el. --- dev/tools/anomaly-traces-parser.el | 28 ---------------------------- dev/tools/coqdev.el | 16 ++++++++++++++++ 2 files changed, 16 insertions(+), 28 deletions(-) delete mode 100644 dev/tools/anomaly-traces-parser.el diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el deleted file mode 100644 index 68f54266f..000000000 --- a/dev/tools/anomaly-traces-parser.el +++ /dev/null @@ -1,28 +0,0 @@ -;; This Elisp snippet adds a regexp parser for the format of Anomaly -;; backtraces (coqc -bt ...), to the error parser of the Compilation -;; mode (C-c C-c: "Compile command: ..."). Once the -;; coq-change-error-alist-for-backtraces function has run, file -;; locations in traces are recognized and can be jumped from easily -;; from the *compilation* buffer. - -;; You can just copy everything below to your .emacs and this will be -;; enabled from any compilation command launched from an OCaml file. - -(defun coq-change-error-alist-for-backtraces () - "Hook to change the compilation-error-regexp-alist variable, to - search the coq backtraces for error locations" - (interactive) - (add-to-list - 'compilation-error-regexp-alist-alist - '(coq-backtrace - "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ - lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ - \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" - 2 (3 . 4) (5 . 6))) - (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) - -;; this Anomaly parser should be available when one is hacking -;; on the *OCaml* code of Coq (adding bugs), so we enable it -;; through the OCaml mode hooks. -(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces) -(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index f5a0feffa..31cde7584 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -82,5 +82,21 @@ Note that this function is executed before _Coqproject is read if it exists." (setq-local coq-prog-name (concat dir "bin/coqtop")))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) +;; This Elisp snippet adds a regexp parser for the format of Anomaly +;; backtraces (coqc -bt ...), to the error parser of the Compilation +;; mode (C-c C-c: "Compile command: ..."). File locations in traces +;; are recognized and can be jumped from easily in the *compilation* +;; buffer. +(defvar compilation-error-regexp-alist-alist) +(defvar compilation-error-regexp-alist) +(add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ + lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ + \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" + 2 (3 . 4) (5 . 6))) +(add-to-list 'compilation-error-regexp-alist 'coq-backtrace) + (provide 'coqdev) ;;; coqdev ends here -- cgit v1.2.3 From 9997f9aec01abdb59852ec5706ef36ce56311109 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 13 Feb 2018 15:24:10 +0100 Subject: coqdev.el: stop using when-let for emacs<25 compatibility. --- dev/tools/coqdev.el | 37 ++++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 31cde7584..20613a4cf 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -31,17 +31,15 @@ ;;; Code: -(require 'subr-x) - (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (when-let ((dir (locate-dominating-file default-directory "META.coq"))) - (expand-file-name dir))) + (let ((dir (locate-dominating-file default-directory "META.coq"))) + (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () "Setup `compilate-command' for Coq development." - (when-let ((dir (coqdev-default-directory))) - (setq-local compile-command (concat "make -C " dir)))) + (let ((dir (coqdev-default-directory))) + (when dir (setq-local compile-command (concat "make -C " dir))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) (defvar camldebug-command-name) ; from camldebug.el (caml package) @@ -50,15 +48,18 @@ "Setup ocamldebug for Coq development. Specifically `camldebug-command-name' and `ocamldebug-command-name'." - (when-let ((dir (coqdev-default-directory))) - (setq-local camldebug-command-name (concat dir "dev/ocamldebug-coq")) - (setq-local ocamldebug-command-name (concat dir "dev/ocamldebug-coq")))) + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local camldebug-command-name + (concat dir "dev/ocamldebug-coq")) + (setq-local ocamldebug-command-name + (concat dir "dev/ocamldebug-coq"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug) (defun coqdev-setup-tags () "Setup `tags-file-name' for Coq development." - (when-let ((dir (coqdev-default-directory))) - (setq-local tags-file-name (concat dir "TAGS")))) + (let ((dir (coqdev-default-directory))) + (when dir (setq-local tags-file-name (concat dir "TAGS"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-tags) (defvar coq-prog-args) @@ -74,12 +75,14 @@ Specifically `camldebug-command-name' and `ocamldebug-command-name'." "Setup Proofgeneral variables for Coq development. Note that this function is executed before _Coqproject is read if it exists." - (when-let ((dir (coqdev-default-directory))) - (unless coq-prog-args ; In case there are file-local variables - (setq coq-prog-args `("-coqlib" ,dir - "-R" ,(concat dir "plugins") "Coq" - "-R" ,(concat dir "theories") "Coq"))) - (setq-local coq-prog-name (concat dir "bin/coqtop")))) + (let ((dir (coqdev-default-directory))) + (when dir + (unless coq-prog-args + (setq coq-prog-args + `("-coqlib" ,dir "-R" ,(concat dir "plugins") + "Coq" "-R" ,(concat dir "theories") + "Coq"))) + (setq-local coq-prog-name (concat dir "bin/coqtop"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) ;; This Elisp snippet adds a regexp parser for the format of Anomaly -- cgit v1.2.3 From fbe9d252ef31f49a75225b8c71be56a38bc51a3d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 13 Feb 2018 15:26:40 +0100 Subject: coqdev.el: shell-quote-argument the directory for make -C --- dev/tools/coqdev.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 20613a4cf..01334690c 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -39,7 +39,7 @@ (defun coqdev-setup-compile-command () "Setup `compilate-command' for Coq development." (let ((dir (coqdev-default-directory))) - (when dir (setq-local compile-command (concat "make -C " dir))))) + (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir)))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) (defvar camldebug-command-name) ; from camldebug.el (caml package) -- cgit v1.2.3 From d5c771138a3b2ce753f458396d82eef9a4557e20 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 13 Feb 2018 15:27:13 +0100 Subject: coqdev.el: fix "compilate"-command typo --- dev/tools/coqdev.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 01334690c..4252458cd 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -37,7 +37,7 @@ (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () - "Setup `compilate-command' for Coq development." + "Setup `compile-command' for Coq development." (let ((dir (coqdev-default-directory))) (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir)))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) -- cgit v1.2.3 From d9cb50d8f9b2bb16ddf7c27c146e09d7de33b90f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 13 Feb 2018 15:51:25 +0100 Subject: coqdev.el: wait for 'compile to touch compilation-error-regexp-alist (and alist-alist) --- dev/tools/coqdev.el | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 4252458cd..8c55be283 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -92,14 +92,15 @@ Note that this function is executed before _Coqproject is read if it exists." ;; buffer. (defvar compilation-error-regexp-alist-alist) (defvar compilation-error-regexp-alist) -(add-to-list - 'compilation-error-regexp-alist-alist - '(coq-backtrace - "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ +(with-eval-after-load 'compile + (add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" - 2 (3 . 4) (5 . 6))) -(add-to-list 'compilation-error-regexp-alist 'coq-backtrace) + 2 (3 . 4) (5 . 6))) + (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) (provide 'coqdev) ;;; coqdev ends here -- cgit v1.2.3