Any interest in having a Coq 'compile-command?

[Ptival]

I don't know how uniform people's environments are, but for all my projects I have something along the lines of:

`- root
  `- _CoqProject
  `- Makefile
  `- Makefile.coq
  `- dir1
  `- dir2

Now when in emacs, it'd be nice to do M-x compile and run something like either: make -C /path/to/root/ or cd ../../until/root/ && make

I'm not sure whether this feature is already provided and I missed it, or whether you judge it too specific to my kind of project structure and not general enough, or is it a bad idea for some other reason? :-)

[cpitclaudel]

Proof General already has a feature to compile on demand; did you try that? Otherwise, I think it's a more general thing than PG. I have this in my .emacs:

(defun ~/compile ()
  "Same as `compile', with bells and whistles.
Add -C if command is make and a Makefile can be found, and always
run in comint mode."
  (interactive)
  (let* ((command (eval compile-command))
         (makefile-dir (locate-dominating-file default-directory "Makefile"))
         (is-default-dir (or (null makefile-dir)
                             (string= (expand-file-name default-directory)
                                      (expand-file-name makefile-dir)))))
    (when (string-match "make \\(?:-C \\([^'\" ]+\\|\"[^\"]+\"\\|'[^']+'\\)\\)?" command)
      (setq command (replace-match (if (not is-default-dir)
                                       (format "make -C %S " makefile-dir)
                                     "make ")
                                   nil t command)))
    (let ((current-prefix-arg (cons 4 nil))
          (compile-command command))
      (call-interactively #'compile))))