diff options
| -rw-r--r-- | coq/coq.el | 119 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 15 |
2 files changed, 109 insertions, 25 deletions
@@ -1102,12 +1102,9 @@ Currently this doesn't take the loadpath into account." ;; - Bug: never stopping busy cursor ;; - Bug: coq not running for the first comment after switching ;; - modify behavior of locked ancestors, see proof-span-read-only -;; - display coqdep errors in the recompile-response buffer -;; - use a variable for the recompile-response buffer ;; - fix problem with partial library names ;; - clean old multiple file stuff ;; - fix places marked with XXX -;; - enable next-error in recompile-response buffers ;; user options and variables @@ -1282,6 +1279,13 @@ identifier and should therefore not be matched by this regexp.") (defvar coq-compile-history nil "History of external Coq compilation commands.") +(defvar coq-compile-response-buffer-name "*coq-compile-response*" + "Name of the buffer to display error messages from coqc and coqdep.") + +(defvar coq-compile-response-buffer nil + "Buffer to display error messages from coqc and coqdep.") + + ;; basic utilities (defun time-less-or-equal (time-1 time-2) @@ -1403,7 +1407,43 @@ FILE should be an absolute file name. It can be nil if (cons "-I" (cons (file-name-directory file) result)))) result)) -(defun coq-get-library-dependencies (lib-src-file) +(defun coq-init-compile-response-buffer (command) + "Initialize the buffer for the compilation output. +If `coq-compile-response-buffer' exists, empty it. Otherwise +create a buffer with name `coq-compile-response-buffer-name', put +it into `compilation-mode' and store it in +`coq-compile-response-buffer' for later use. Argument COMMAND is +the command whose output will appear in the buffer." + (if (bufferp coq-compile-response-buffer) + (let ((inhibit-read-only t)) + (with-current-buffer coq-compile-response-buffer + (erase-buffer))) + (setq coq-compile-response-buffer + (get-buffer-create coq-compile-response-buffer-name)) + (with-current-buffer coq-compile-response-buffer + (compilation-mode))) + ;; I don't really care if somebody gets the right mode when + ;; he saves and reloads this buffer. However, error messages in + ;; the first line are not found for some reason ... + (let ((inhibit-read-only t)) + (with-current-buffer coq-compile-response-buffer + (insert "-*- mode: compilation; -*-\n\n" command "\n")))) + +(defun coq-display-compile-response-buffer () + "Display the errors in `coq-compile-response-buffer'." + (with-current-buffer coq-compile-response-buffer + ;; fontification enables the error messages + (let ((font-lock-verbose nil)) ; shut up font-lock messages + (font-lock-fontify-buffer))) + ;; Make it so the next C-x ` will use this buffer. + (setq next-error-last-buffer coq-compile-response-buffer) + (let ((window (display-buffer coq-compile-response-buffer))) + (if proof-shrink-windows-tofit + (save-excursion + (save-selected-window + (proof-resize-window-tofit window)))))) + +(defun coq-get-library-dependencies (lib-src-file &optional command-intro) "Compute dependencies of LIB-SRC-FILE. Invoke \"coq-dep\" on lib-src-file and parse the output to compute the compiled coq library object files on which @@ -1413,6 +1453,11 @@ the core of the error message. If the return value is a list no error occurred and the returned list is the (possibly empty) list of file names LIB-SRC-FILE depends on. +If an error occurs this funtion displays the +`coq-compile-response-buffer' with the complete command and its +output. The optional argument COMMAND-INTRO is only used in the +error case. It is prepended to the displayed command. + LIB-SRC-FILE should be an absolute file name. If it is, the dependencies are absolute too and the simplified treatment of `coq-load-path-include-current' in `coq-include-options' won't @@ -1427,34 +1472,44 @@ break." (setq coqdep-output (buffer-string))) ;(message "coqdep output on %s: %s" lib-src-file coqdep-output) (if (string-match "^\\*\\*\\* Warning" coqdep-output) - "unsatisfied dependencies" + (let* ((this-command (cons coq-dependency-analyzer coqdep-arguments)) + (full-command (if command-intro + (cons command-intro this-command) + this-command))) + ;; display the error + (coq-init-compile-response-buffer + (mapconcat 'identity full-command " ")) + (let ((inhibit-read-only t)) + (with-current-buffer coq-compile-response-buffer + (insert coqdep-output))) + (coq-display-compile-response-buffer) + "unsatisfied dependencies") (if (string-match ": \\(.*\\)$" coqdep-output) (cdr-safe (split-string (match-string 1 coqdep-output))) ())))) (defun coq-compile-library (src-file) "Recompile coq library SRC-FILE. -Display errors in buffer *coq-auto-compile-response*." +Display errors in buffer `coq-compile-response-buffer'." (message "Recompile %s" src-file) - (with-current-buffer (get-buffer-create "*coq-auto-compile-response*") - (erase-buffer)) (let ((coqc-arguments (nconc (coq-include-options src-file) (list src-file))) coqc-status) + (coq-init-compile-response-buffer + (mapconcat 'identity (cons coq-compiler coqc-arguments) " ")) ;(message "call coqc arg list: %s" coqc-arguments) (setq coqc-status (apply 'call-process - coq-compiler nil "*coq-auto-compile-response*" t coqc-arguments)) + coq-compiler nil coq-compile-response-buffer t coqc-arguments)) ; (if (eq coqc-status 0) ; (message "compilation %s OK, output |%s|" src-file ; (with-current-buffer proof-response-buffer ; (buffer-string)))) (unless (eq coqc-status 0) - (let ((terminated-text - (if (numberp coqc-status) - "terminated with exit status" - "was terminated by signal"))) - (display-buffer "*coq-auto-compile-response*") + (coq-display-compile-response-buffer) + (let ((terminated-text (if (numberp coqc-status) + "terminated with exit status" + "was terminated by signal"))) (error "ERROR: Recompiling coq library %s %s %s" src-file terminated-text coqc-status))))) @@ -1601,12 +1656,14 @@ therefore the customizations for `compile' do not apply." span (coq-library-src-of-obj-file absolute-module-obj-file))))) -(defun coq-map-module-id-to-obj-file (module-id) +(defun coq-map-module-id-to-obj-file (module-id span) "Map MODULE-ID to the appropriate coq object file. The mapping depends of course on `coq-load-path'. The current implementation invokes coqdep with a one-line require command. This is probably slower but much simpler than modelling coq file -loading inside ProofGeneral. +loading inside ProofGeneral. Argument SPAN is only used for error +handling. It provides the location information of MODULE-ID for a +decent error message. A peculiar consequence of the current implementation is that this function returns () if MODULE-ID comes from the standard library." @@ -1616,15 +1673,37 @@ function returns () if MODULE-ID comes from the standard library." coq-load-path)) (coq-load-path-include-current nil) (temp-require-file (make-temp-file "ProofGeneral-coq" nil ".v")) + (coq-string (concat "Require " module-id ".")) result) (unwind-protect (progn (with-temp-file temp-require-file - (insert "Require " module-id ".")) - (setq result (coq-get-library-dependencies temp-require-file))) + (insert coq-string)) + (setq result + (coq-get-library-dependencies + temp-require-file + (concat "echo \"" coq-string "\" > " temp-require-file)))) (delete-file temp-require-file)) (if (stringp result) - (error "Cannot find library %s in loadpath" module-id)) + ;; Error handling: coq-get-library-dependencies was not able to + ;; translate module-id into a file name. We insert now a faked error + ;; message into coq-compile-response-buffer to make next-error happy. + (let ((error-message + (format "Cannot find library %s in loadpath" module-id)) + (inhibit-read-only t)) + ;; Writing a message into coq-compile-response-buffer for next-error + ;; does currently not work. We do have exact position information + ;; about the span, but we don't know how much white space there is + ;; between the start of the span and the start of the command string. + ;; (with-current-buffer coq-compile-response-buffer + ;; (insert + ;; (format "File \"%s\", line %d\n%s.\n" + ;; (buffer-file-name (span-buffer span)) + ;; (with-current-buffer (span-buffer span) + ;; (line-number-at-pos (span-start span))) + ;; error-message))) + ;; (coq-display-compile-response-buffer) + (error error-message))) (assert (<= (length result) 1) "Internal error in coq-map-module-id-to-obj-file") (car-safe result))) @@ -1646,7 +1725,7 @@ the coq-obj-hash, which is used during internal compilation (see `coq-make-lib-up-to-date'). This way one hash will be used for all \"Require\" commands added at once to the queue." - (let ((module-obj-file (coq-map-module-id-to-obj-file module-id))) + (let ((module-obj-file (coq-map-module-id-to-obj-file module-id span))) ;; coq-map-module-id-to-obj-file currently returns () for ;; standard library modules! (when module-obj-file diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 6715c48b..e2795818 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4109,9 +4109,18 @@ The compilation command must be customized in @code{coq-compile-command} and the flag @code{coq-confirm-external-compilation-command} determines whether the user must confirm the compilation command. The output -of the compilation appears in the @code{*compilation*} buffer and +of the compilation appears then in the @code{*compilation*} +buffer. + +When Proof General compiles itself, output is only shown in case +of errors. It then appears in the buffer +@code{*coq-compile-response*}. Both with internal and external +compilation one can use @code{C-x `} (bound to @code{next-error}, @inforef{Compilation Mode,,emacs}) to jump to error locations. +Note however, that @code{coqdep} does not produce error messages +with location information, so @code{C-x `} cannot work for errors +from @code{coqdep}. Proof General cannot know if some library files have been updated outside of Proof General, therefore, it must perform the @@ -4377,10 +4386,6 @@ addressed in the next release: @item Support @code{Declare ML Module} commands. @item -Properly display errors from @code{coqdep} and @code{coqc}, -enable @code{C-x `} (@code{M-x next-error}) for these error -messages. -@item Improved undo behaviour for locked ancestors. @item Integrate with older options for multiple file support, such as, |