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