Remove dir-locals and ship suggested helper hooks instead. #6556

SkySkimmer · 2018-01-06T12:08:08Z

Alternative to #1136.

People interested in those functions can copy coqdev.el somewhere and load it, or copy parts of it to their init. Those not interested can just ignore it.

.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.

Zimmi48 · 2018-01-06T15:16:43Z

Copy somewhere, WDYM? Emacs users that are not Emacs expert might need a bit more documentation on how to use this. Can one tweak there .emacs file to load this file without moving it anywhere else? (So as to keep in sync with the potential evolution of this file.)

RalfJung · 2018-02-08T08:58:23Z

I'd be very happy for this to be merged so that I can finally git commit in Coq without annoying warnings by emacs. :)

The label seems wrong though, it seems this needs some additional work by @SkySkimmer to explain somewhere the exact procedure to configure emacs appropriately? I certainly wouldn't know where "somewhere" is. ;-)

Zimmi48 · 2018-02-08T09:19:05Z

I talked to @letouzey who would be favorable to merging this as well.

SkySkimmer · 2018-02-08T15:11:11Z

TBH I was waiting for someone to say they were interested in this approach before doing more work on it.

RalfJung · 2018-02-08T16:13:04Z

Fair enough :)

SkySkimmer · 2018-02-08T16:26:22Z

Copy somewhere, WDYM? Emacs users that are not Emacs expert might need a bit more documentation on how to use this. Can one tweak there .emacs file to load this file without moving it anywhere else? (So as to keep in sync with the potential evolution of this file.)

It's just a regular emacs package (although a very Coq developer specific one), you put it in the load path (or add to the load path to include it) and (require 'coqdev) or (load "coqdev").

Zimmi48 · 2018-02-09T08:32:10Z

OK so for instance:

(add-to-list 'load-path "~/coq/dev/tools/")
(require 'coqdev)

Can you put this in the comments at the top of the file? And also mention the existence of this file in the relevant section of dev/README? It would probably be worth checking whether the other two Emacs files in this directory still make sense BTW and merge this into coqdev.el if they do...

SkySkimmer · 2018-02-11T21:03:26Z

It would probably be worth checking whether the other two Emacs files in this directory still make sense BTW and merge this into coqdev.el if they do...

The backtrace regex is very mergeable, objects.el not so much IMO. objects.el came up in #819 but I didn't remove it due to inertia. If it should be removed let's do it in another PR.

Zimmi48 · 2018-02-12T13:23:20Z

I am very satisfied by the documentation and completely incompetent when it comes to reviewing Elisp. @JasonGross: would you do it?

SkySkimmer · 2018-02-13T00:06:08Z

I am very satisfied by the documentation and completely incompetent when it comes to reviewing Elisp. @JasonGross: would you do it?

Maybe we could get comments from PG people? @Matafou @cpitclaudel I don't know who else is there.

Matafou · 2018-02-13T10:38:01Z

LGTM. Good solution.

cpitclaudel

OK, I took a look.

cpitclaudel · 2018-02-13T13:32:51Z

dev/tools/coqdev.el

+(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))))


You want to shell-quote-argument on dir, in case it contains spaces.

cpitclaudel · 2018-02-13T13:33:14Z

dev/tools/coqdev.el

+
+(defun coqdev-setup-compile-command ()
+  "Setup `compilate-command' for Coq development."
+  (when-let ((dir (coqdev-default-directory)))


when-let is Emacs 25+, but the default is still 24.5 on Debian and Ubuntu

cpitclaudel · 2018-02-13T13:33:27Z

dev/tools/coqdev.el

+    (expand-file-name dir)))
+
+(defun coqdev-setup-compile-command ()
+  "Setup `compilate-command' for Coq development."


compile-command, I think, not compilate

cpitclaudel · 2018-02-13T13:33:48Z

dev/tools/coqdev.el

+
+(defun coqdev-default-directory ()
+  "Return the Coq repository containing `default-directory'."
+  (when-let ((dir (locate-dominating-file default-directory "META.coq")))


when-let is Emacs 25+, but the default is still 24.5 on Debian and Ubuntu

cpitclaudel · 2018-02-13T13:34:31Z

dev/tools/coqdev.el

+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"))))


expand-file-name is usually better than concat

concat is shorter and we already expanded in coqdev-default-directory, is there still some use we can get out of expand-file-name?

Not too much. I don't think expand-file-name is guaranteed to return a path ending with a "/", but in practice it likely does in most cases.

cpitclaudel · 2018-02-13T13:35:18Z

dev/tools/coqdev.el

+  (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)


I'm not sure that hack-local-variables-hook is the best to use here. Maybe just tuareg-mode-hook? Or am I missing something?

I'm not sure that hack-local-variables-hook is the best to use here. Maybe just tuareg-mode-hook? Or am I missing something?

ocamldebug reads ocamldebug-command-name after moving to the ocamldebug buffer (creating it if it doesn't already exist). If newly created the buffer is in fundamental-mode at that time. So setting the variable only in ocaml files won't have an effect.

I see, thanks. That sounds like an ocamldebug bug.
In that case, since that hook will run in al buffer, it might be better to check the buffer's name before running the actual body of the function.

cpitclaudel · 2018-02-13T13:35:46Z

dev/tools/coqdev.el

+(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"))))


Same here: when-let, concat, and hack-local-variables

cpitclaudel · 2018-02-13T13:36:08Z

dev/tools/coqdev.el

+;; 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)


What is this for?

For a couple files ((C)Morphisms.v and some test suite files) there are file local arguments which we don't want to override, but we don't want to false positive detect the presence of file local arguments when PG set them from _CoqProject in another file (eg the files in Init/, or some 3rd party file).

Yup, I understand the buffer-local part; but why do you set it to nil?

In case PG modified it before us.

cpitclaudel · 2018-02-13T13:37:20Z

dev/tools/coqdev.el

+;; are recognized and can be jumped from easily in the *compilation*
+;; buffer.
+(defvar compilation-error-regexp-alist-alist)
+(defvar compilation-error-regexp-alist)


You need a to require the file that defines these variables; defvar-ing them is not enough to be able to change them.

You need a to require the file that defines these variables; defvar-ing them is not enough to be able to change them.

How about (with-eval-after-load 'compile ...)?

I'd go for (require 'compile), but the with-eval-after-load form works fine too.

(and alist-alist)

SkySkimmer · 2018-02-13T14:54:30Z

I'm going to leave the concat and hack-local-variables barring further comments.

cpitclaudel · 2018-02-13T16:37:07Z

dev/tools/coqdev.el

+;; following to your init:
+
+;; (add-to-list 'load-path "/path/to/coqdev/")
+;; (require 'coqdev)


No need to add the full path, I think; unless you have > 1 files, it's enough to pass the file name to `require'.

herbelin · 2018-02-13T19:50:42Z

Hi, seeing emacs expert gathered in this thread, may I bounce on the discussion to ask whether someone would have a solution for making C-x C-a C-b work in emacs when ocamldebugging packed modules (either with Tuareg's ocamldebug.el - as reported here - or with the camldebug.el file released with OCaml, but after all, why not also with an ad hoc emacs file for Coq developers such as discussed in this PR).

This seems a bit tricky to do since emacs has to send something like break @ MyModule.MyFile # 324. to ocamldebug, where MyModule is the name of the pack, and there seems to be no canonical way to get this name in general.

In the case of Coq however, the name of the module is the basename of the .mlpack file lying in the same directory as the current directory and which mentions the module name corresponding to the current .ml file in its list of modules to include, e.g. Ground_plugin when debugging say file plugins/firstorder/sequent.ml, since Sequent occurs in plugins/firstorder/ground_plugin.mlpack. This is why I wondered if maybe, even if a generic Tuareg-level or OCaml-level solution is difficult to get, at least something could be done at the level of coqdev.el??

maximedenes · 2018-02-19T09:02:11Z

@SkySkimmer Do you consider this ready or do you plan to address @cpitclaudel 's comments?

SkySkimmer · 2018-02-19T09:06:59Z

I think it's ready.

…tead.

Remove dir-locals and ship suggested helper hooks instead.

568dffc

.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.

SkySkimmer added kind: infrastructure CI, build tools, development tools. needs: review part: tools Coqdoc, coq_makefile, etc. labels Jan 6, 2018

SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Feb 10, 2018

coqdev.el: add installation instructions.

e4529a4

SkySkimmer removed the needs: progress Work in progress: awaiting action from the author. label Feb 11, 2018

Merge anomaly-traces-parser.el into coqdev.el.

20e654c

SkySkimmer mentioned this pull request Feb 11, 2018

Generate .dir-locals.el at configuration time. #1136

Closed

Zimmi48 added this to the 8.8 milestone Feb 11, 2018

Zimmi48 requested a review from JasonGross February 12, 2018 13:23

Zimmi48 removed the needs: review label Feb 13, 2018

cpitclaudel reviewed Feb 13, 2018

View reviewed changes

SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Feb 13, 2018

SkySkimmer added 3 commits February 13, 2018 15:33

coqdev.el: stop using when-let for emacs<25 compatibility.

9997f9a

coqdev.el: shell-quote-argument the directory for make -C

fbe9d25

coqdev.el: fix "compilate"-command typo

d5c7711

SkySkimmer force-pushed the no-dir-locals branch from b4bfc61 to d5c7711 Compare February 13, 2018 14:33

coqdev.el: wait for 'compile to touch compilation-error-regexp-alist

d9cb50d

(and alist-alist)

SkySkimmer removed the needs: progress Work in progress: awaiting action from the author. label Feb 13, 2018

cpitclaudel reviewed Feb 13, 2018

View reviewed changes

maximedenes merged commit d9cb50d into coq:master Feb 19, 2018

maximedenes added a commit that referenced this pull request Feb 19, 2018

Merge PR #6556: Remove dir-locals and ship suggested helper hooks ins…

8e9d142

…tead.

SkySkimmer deleted the no-dir-locals branch February 19, 2018 10:33

Remove dir-locals and ship suggested helper hooks instead. #6556

Remove dir-locals and ship suggested helper hooks instead. #6556

Conversation

SkySkimmer commented Jan 6, 2018

Zimmi48 commented Jan 6, 2018

RalfJung commented Feb 8, 2018

Zimmi48 commented Feb 8, 2018

SkySkimmer commented Feb 8, 2018

RalfJung commented Feb 8, 2018

SkySkimmer commented Feb 8, 2018

Zimmi48 commented Feb 9, 2018 • edited Loading

SkySkimmer commented Feb 11, 2018

Zimmi48 commented Feb 12, 2018 • edited Loading

SkySkimmer commented Feb 13, 2018

Matafou commented Feb 13, 2018

cpitclaudel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

SkySkimmer commented Feb 13, 2018

Choose a reason for hiding this comment

herbelin commented Feb 13, 2018

maximedenes commented Feb 19, 2018

SkySkimmer commented Feb 19, 2018

Zimmi48 commented Feb 9, 2018 •

edited

Loading

Zimmi48 commented Feb 12, 2018 •

edited

Loading