From d05b614f6e231cfc24a5c560cc5c8ede8c872d8e Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 1 Apr 2021 21:22:20 +0200 Subject: [PATCH 1/6] improve test documentation and fix some line numbers --- ci/compile-tests/007-slow-require/Makefile | 5 +++++ ci/compile-tests/007-slow-require/b1.v.orig | 2 +- ci/compile-tests/007-slow-require/b3.v.orig | 2 +- ci/compile-tests/007-slow-require/b4.v.orig | 2 +- ci/compile-tests/007-slow-require/b5.v.orig | 2 +- ci/compile-tests/007-slow-require/b6.v.orig | 2 +- ci/compile-tests/007-slow-require/runtest.el | 6 +++++- 7 files changed, 15 insertions(+), 6 deletions(-) diff --git a/ci/compile-tests/007-slow-require/Makefile b/ci/compile-tests/007-slow-require/Makefile index b99eebc1d..c23f8d55c 100644 --- a/ci/compile-tests/007-slow-require/Makefile +++ b/ci/compile-tests/007-slow-require/Makefile @@ -19,6 +19,11 @@ TEST_SOURCES:=\ a5.v b5.v c5.v d5.v \ a6.v b6.v c6.v d6.v +# This test uses ../bin/compile-test-start-delayed to start certain +# commands with specified delays to check carfully constructed +# internal states. compile-test-start-delayed outputs diagnostics on +# file descriptor 9, which bypasses emacs and is joined with stderr of +# the current make. Open file descriptor 9 here. .PHONY: test test: $(MAKE) clean diff --git a/ci/compile-tests/007-slow-require/b1.v.orig b/ci/compile-tests/007-slow-require/b1.v.orig index 926bed1da..2f9cf6d99 100644 --- a/ci/compile-tests/007-slow-require/b1.v.orig +++ b/ci/compile-tests/007-slow-require/b1.v.orig @@ -23,5 +23,5 @@ Require Export d1. -(* This is line 27 *) +(* This is line 26 *) Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/b3.v.orig b/ci/compile-tests/007-slow-require/b3.v.orig index 51ab7a2f9..5b2668c00 100644 --- a/ci/compile-tests/007-slow-require/b3.v.orig +++ b/ci/compile-tests/007-slow-require/b3.v.orig @@ -23,5 +23,5 @@ Require Export d3. -(* This is line 27 *) +(* This is line 26 *) Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/b4.v.orig b/ci/compile-tests/007-slow-require/b4.v.orig index fd8d331ea..5b49fd50f 100644 --- a/ci/compile-tests/007-slow-require/b4.v.orig +++ b/ci/compile-tests/007-slow-require/b4.v.orig @@ -23,5 +23,5 @@ Require Export d4. -(* This is line 27 *) +(* This is line 26 *) Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/b5.v.orig b/ci/compile-tests/007-slow-require/b5.v.orig index 3fec38a35..cd4a7b711 100644 --- a/ci/compile-tests/007-slow-require/b5.v.orig +++ b/ci/compile-tests/007-slow-require/b5.v.orig @@ -23,5 +23,5 @@ Require Export d5. -(* This is line 27 *) +(* This is line 26 *) Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/b6.v.orig b/ci/compile-tests/007-slow-require/b6.v.orig index 2b957e6ef..826bdacf2 100644 --- a/ci/compile-tests/007-slow-require/b6.v.orig +++ b/ci/compile-tests/007-slow-require/b6.v.orig @@ -23,5 +23,5 @@ Require Export d6. -(* This is line 27 *) +(* This is line 26 *) Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/runtest.el b/ci/compile-tests/007-slow-require/runtest.el index 52c2f392c..df9dbc312 100644 --- a/ci/compile-tests/007-slow-require/runtest.el +++ b/ci/compile-tests/007-slow-require/runtest.el @@ -17,7 +17,11 @@ ;; in each possible state. For specifying the different delays there ;; are 6 mini projects, one for each test in this file. Each project ;; consists of four files, a1.v, b1.v, c1.v and d1.v for the first one -;; and a6.v, b6.v, c6.v and d6.v for the sixth one. +;; and a6.v, b6.v, c6.v and d6.v for the sixth one. Each project is +;; one ert test, described further below. In each project or test, the +;; top level require commands are asserted and retracted several times +;; with changes in different files to test (almost) all possible +;; internal state combinations. ;; ;; The dependencies are the same in all projects: ;; From 3285f0c2c92dd62b6d98209b833a1ded82dd7573 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 1 Apr 2021 21:47:44 +0200 Subject: [PATCH 2/6] add test for default-directory This test exhibits a bug in background compilation that became apparent when working on tramp support: Strange things may happen when the user changes the current buffer, because part of the code may then run with an incorrect default-directory. Introduce hooks before and after busy waiting in the cct library. --- ci/compile-tests/008-default-dir/Makefile | 34 ++++++ ci/compile-tests/008-default-dir/a.v.orig | 40 +++++++ ci/compile-tests/008-default-dir/b.v.orig | 23 ++++ ci/compile-tests/008-default-dir/c.v.orig | 23 ++++ ci/compile-tests/008-default-dir/runtest.el | 111 ++++++++++++++++++++ ci/compile-tests/README.md | 26 ++++- ci/compile-tests/cct-lib.el | 20 +++- coq/coq-par-compile.el | 25 +++-- 8 files changed, 291 insertions(+), 11 deletions(-) create mode 100644 ci/compile-tests/008-default-dir/Makefile create mode 100644 ci/compile-tests/008-default-dir/a.v.orig create mode 100644 ci/compile-tests/008-default-dir/b.v.orig create mode 100644 ci/compile-tests/008-default-dir/c.v.orig create mode 100644 ci/compile-tests/008-default-dir/runtest.el diff --git a/ci/compile-tests/008-default-dir/Makefile b/ci/compile-tests/008-default-dir/Makefile new file mode 100644 index 000000000..5890dddb6 --- /dev/null +++ b/ci/compile-tests/008-default-dir/Makefile @@ -0,0 +1,34 @@ +# This file is part of Proof General. +# +# © Copyright 2021 Hendrik Tews +# +# Authors: Hendrik Tews +# Maintainer: Hendrik Tews +# +# License: GPL (GNU GENERAL PUBLIC LICENSE) + + +# This test modifies some .v files during the test. The original +# versions are in .v.orig files. They are moved to the corresponding +# .v files before the test starts. +TEST_SOURCES:= a.v b.v c.v + +# This test uses ../bin/compile-test-start-delayed to start certain +# commands with specified delays to check carfully constructed +# internal states. compile-test-start-delayed outputs diagnostics on +# file descriptor 9, which bypasses emacs and is joined with stderr of +# the current make. Open file descriptor 9 here. +.PHONY: test +test: + $(MAKE) clean + $(MAKE) $(TEST_SOURCES) + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit \ + 9>&1 + +%.v: %.v.orig + cp $< $@ + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux $(TEST_SOURCES) diff --git a/ci/compile-tests/008-default-dir/a.v.orig b/ci/compile-tests/008-default-dir/a.v.orig new file mode 100644 index 000000000..3f019f160 --- /dev/null +++ b/ci/compile-tests/008-default-dir/a.v.orig @@ -0,0 +1,40 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews + * + * License: GPL (GNU GENERAL PUBLIC LICENSE) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +(* The test script relies on absolute line numbers. + * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING. + *) + +(* The delay for coqdep is specified in comments with key coqdep-delay, + * see compile-test-start-delayed. + *) + + +(* This is line 24 *) +Require Export (* coqdep-delay 1 *) b. +(* This is line 26 *) + + +(* This is line 29 *) +Definition sum : nat := 5. + + +(* This is line 33 *) +Lemma x : b + c = sum. +Proof using. + unfold b, c, sum in *. + simpl. + trivial. +Qed. +(* This is line 40 *) diff --git a/ci/compile-tests/008-default-dir/b.v.orig b/ci/compile-tests/008-default-dir/b.v.orig new file mode 100644 index 000000000..1713dba97 --- /dev/null +++ b/ci/compile-tests/008-default-dir/b.v.orig @@ -0,0 +1,23 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews + * + * License: GPL (GNU GENERAL PUBLIC LICENSE) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +(* The test script relies on absolute line numbers. + * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING. + *) + + +Require Export c. + +(* This is line 22 *) +Definition b : nat := 2. diff --git a/ci/compile-tests/008-default-dir/c.v.orig b/ci/compile-tests/008-default-dir/c.v.orig new file mode 100644 index 000000000..dfd8e8f1d --- /dev/null +++ b/ci/compile-tests/008-default-dir/c.v.orig @@ -0,0 +1,23 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews + * + * License: GPL (GNU GENERAL PUBLIC LICENSE) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +(* The test script relies on absolute line numbers. + * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING. + *) + + + + +(* This is line 22 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/008-default-dir/runtest.el b/ci/compile-tests/008-default-dir/runtest.el new file mode 100644 index 000000000..c0cfe3af5 --- /dev/null +++ b/ci/compile-tests/008-default-dir/runtest.el @@ -0,0 +1,111 @@ +;; This file is part of Proof General. +;; +;; © Copyright 2021 Hendrik Tews +;; +;; Authors: Hendrik Tews +;; Maintainer: Hendrik Tews +;; +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; +;; Coq Compile Tests (cct) -- +;; ert tests for parallel background compilation for Coq +;; +;; Test that default-directory is correctly set independently of the +;; current buffer in the foreground. +;; +;; The dependencies in this test are: +;; +;; a +;; | +;; b +;; | +;; c +;; + + +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + +;;; set configuration +(cct-configure-proof-general) +(configure-delayed-coq) + +(defconst all-ancestors '("./b.v" "./c.v") + "All ancestors.") + +(defconst all-compiled-ancestors + (mapcar 'cct-library-vo-of-v-file all-ancestors) + "All vo ancestors files.") + +(defun check-main-buffer (vo-times new-sum recompiled-files + other-locked-files) + "Perform various checks in buffer a.v. +See `cct-generic-check-main-buffer'." + (cct-generic-check-main-buffer + "a.v" ; main-buf + 24 ; main-unlocked + 40 ; main-locked + 30 ; main-sum-line + new-sum + vo-times + recompiled-files + `((25 . ,all-ancestors)) ; require-ancestors + other-locked-files + 23 ; other-locked-line + )) + + +;;; The test itself + +(ert-deftest test-default-dir () + "`default-directory' test. +Test that `default-directory' is correctly set independently of the +current buffer in the foreground." + (let (vo-times av-buffer ci-buffer other-locked-files) + + ;; (setq cct--debug-tests t) + ;; (setq coq--debug-auto-compilation t) + (find-file "a.v") + (setq av-buffer (current-buffer)) + + (message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s" + coq-dependency-analyzer + coq-compiler + (getenv "PATH") + exec-path) + + (find-file "../..") + (setq ci-buffer (current-buffer)) + + (add-hook 'cct-before-busy-waiting-hook (lambda () (set-buffer ci-buffer))) + (add-hook 'cct-after-busy-waiting-hook (lambda () (set-buffer av-buffer))) + + ;; 1. process original content - compile everything + (message "\n1. process original content - compile everything\n") + (check-main-buffer vo-times "5" nil other-locked-files) + (setq vo-times (cct-record-change-times all-compiled-ancestors)) + + ;; 2. retract and process again - nothing should be compiled + (message "\n2. retract and process again - nothing should be compiled\n") + (cct-process-to-line 21) + (check-main-buffer vo-times "5" nil other-locked-files) + + ;; 3. change b and process again - only b should get compiled + (message "\n3. change b and process again - only b should get compiled\n") + (find-file "b.v") + (push "b.v" other-locked-files) + (cct-check-locked 23 'locked) + (cct-replace-last-word 23 "3") + (check-main-buffer vo-times "6" '("./b.vo") other-locked-files) + + ;; 4. change c and process again - b and c should get compiled + (message "\n4. change c and process again - b and c should get compiled\n") + (find-file "c.v") + (push "c.v" other-locked-files) + (cct-check-locked 23 'locked) + (cct-replace-last-word 23 "5") + (check-main-buffer vo-times "8" '("./b.vo" "./c.vo") other-locked-files) + + )) diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md index 084911256..0a0ca5dc3 100644 --- a/ci/compile-tests/README.md +++ b/ci/compile-tests/README.md @@ -9,7 +9,31 @@ Each test comes with a hand-crafted set of Coq source files that implement a particular dependency tree. Therefore, most of the tests have a subdirectory on their own. -Tests currently missing: +# Overview of existing tests + +All tests are for parallel background compilation. + +001-mini-project +: test compilation for a simple project +002-require-no-dependencies +: Test a require that does not produce any dependencies. +003-require-error +: coqdep fails on a require +004-dependency-cycle +: dependency cycle +005-change-recompile +: test that the right files are recompiled when changes are made +006-ready-dependee +: dependency in state ready +007-slow-require +: test almost all internal state combinations with delay on + coqdep and coqc +008-default-dir +: test that the default/current directory is set correctly + independent of user/emacs changing the current buffer + +# Tests currently missing + - unlock checks for ancestors of failed jobs in different cases - a job depending on a failed dependee, where the dependee has been finished before diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el index 740b04c1a..e573f5c65 100644 --- a/ci/compile-tests/cct-lib.el +++ b/ci/compile-tests/cct-lib.el @@ -1,6 +1,6 @@ ;; This file is part of Proof General. ;; -;; © Copyright 2020 Hendrik Tews +;; © Copyright 2020 - 2021 Hendrik Tews ;; ;; Authors: Hendrik Tews ;; Maintainer: Hendrik Tews @@ -38,6 +38,13 @@ (defvar cct--debug-tests nil "Set to t to get more output during test runs.") +(defvar cct-before-busy-waiting-hook nil + "Hooks run by ‘cct-process-to-line’ before busy waiting.") + +(defvar cct-after-busy-waiting-hook nil + "Hooks run by ‘cct-process-to-line’ after busy waiting.") + + (defmacro cct-implies (p q) "Short-circuit logical implication. Evaluate Q only if P is non-nil." @@ -109,12 +116,16 @@ backward. Replace the word there with WORD." (insert word)) (defun cct-process-to-line (line) - "Assert/retract to line LINE and wait until processing completed." + "Assert/retract to line LINE and wait until processing completed. +Runs `cct-before-busy-waiting-hook' and +`cct-after-busy-waiting-hook' before and after busy waiting for +the prover. In many tests these hooks are not used." (when cct--debug-tests (message "assert/retrect to line %d in buffer %s" line (buffer-name))) (cct-goto-line line) (proof-goto-point) + (run-hooks 'cct-before-busy-waiting-hook) (while (or proof-second-action-list-active (consp proof-action-list)) ;; (message "wait for coq/compilation with %d items queued\n" ;; (length proof-action-list)) @@ -122,7 +133,8 @@ backward. Replace the word there with WORD." ;; accept-process-output without timeout returns rather quickly, ;; apparently most times without process output or any other event ;; to process. - (accept-process-output nil 0.1))) + (accept-process-output nil 0.1)) + (run-hooks 'cct-after-busy-waiting-hook)) (defun cct-get-vanilla-span (line) "Get THE vanilla span for line LINE, report an error if there is none. @@ -158,7 +170,7 @@ region of the buffer and signals a test failure if not." (let ((locked (eq locked-state 'locked))) (when cct--debug-tests (message (concat "check lock state in buffer %s: line %d should be %s;\n" - "\tlocked-span: %s ends at char %s in line %d") + "\tlocked-span: %s ends at char %s in line %s") (buffer-name) line (if locked "locked" "unlocked") proof-locked-span diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index a38964dd0..c88664cd9 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -983,10 +983,13 @@ function and reported appropriately." (process-get process 'coq-compilation-job)))) (let (exit-status) (when coq--debug-auto-compilation - (message "%s %s: process status changed to %s" - (get (process-get process 'coq-compilation-job) 'name) - (process-name process) - event)) + (message + "%s %s: process status changed to %s (default-dir %s curr buf %s)" + (get (process-get process 'coq-compilation-job) 'name) + (process-name process) + event + default-directory + (buffer-name))) (cond ((eq (process-status process) 'exit) (setq exit-status (process-exit-status process))) @@ -1145,6 +1148,9 @@ therefore delete a file if it might be in the way. Sets the (if vio-obj-time (time-less-p vio-obj-time src-time) "-") (if vo-obj-time (coq-par-time-less vo-obj-time dep-time) "-") (if vio-obj-time (coq-par-time-less vio-obj-time dep-time) "-"))) + ;; the source file must exist + (cl-assert src-time nil + "internal error - cannot find src file I") ;; Compute first the max of vo-obj-time and vio-obj-time and remember ;; which of both is newer. This is only meaningful if at least one of ;; the .vo or .vio file exists. @@ -1295,12 +1301,19 @@ the 'second-stage property on job to 'vok if necessary." (vos-obj-time (nth 5 (file-attributes vos-file))) result) (when coq--debug-auto-compilation - (message "%s: compare mod times: vos mod %s, src mod %s, youngest dep %s" + (message + (concat "%s: compare mod times: vos mod %s, src mod %s, youngest dep %s\n" + "\tsrc file %s in %s") (get job 'name) (if vos-obj-time (current-time-string vos-obj-time) "-") (if src-time (current-time-string src-time) "-") (if (eq dep-time 'just-compiled) "just compiled" - (current-time-string dep-time)))) + (current-time-string dep-time)) + (get job 'src-file) + default-directory)) + ;; the source file must exist + (cl-assert src-time nil + "internal error - cannot find src file II") (if (or (eq dep-time 'just-compiled) ; a dep has been just compiled (not vos-obj-time) ; neither vos nor vo present ;; src younger than vos? From 95caa6f106e6283ecc9342055ef26527909c29a7 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 1 Apr 2021 21:35:20 +0200 Subject: [PATCH 3/6] Fix default-directory problem in background compilation --- coq/coq-par-compile.el | 93 +++++++++++++++++++++++------------------- 1 file changed, 50 insertions(+), 43 deletions(-) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index c88664cd9..5c616abb8 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -905,40 +905,39 @@ file to be deleted when the process does not finish successfully." (process-name (format "pro-%s" coq--par-next-id)) process) (setq coq--par-next-id (1+ coq--par-next-id)) - (with-current-buffer (or proof-script-buffer (current-buffer)) - (when coq--debug-auto-compilation - (message "%s %s: start %s %s in %s" - (get job 'name) process-name - command (mapconcat 'identity arguments " ") - default-directory)) - (condition-case err - ;; If the command is wrong, start-process aborts with an - ;; error. However, in Emacs 23.4.1. it will leave a process - ;; behind, which is in a very strange state: running with no - ;; pid. Emacs 24.2 fixes this. - (setq process (apply 'start-process process-name - nil ; no process buffer - command arguments)) - (error - (when coq--debug-auto-compilation - (message "%s %s: error in start process, %s" - (get job 'name) process-name - (if file-rm - (format "rm %s" file-rm) - "no file removal"))) - (when file-rm - (ignore-errors (delete-file file-rm))) - (signal 'coq-compile-error-command-start - (list (cons command arguments) (nth 2 err))))) - (set-process-filter process 'coq-par-process-filter) - (set-process-sentinel process 'coq-par-process-sentinel) - (set-process-query-on-exit-flag process nil) - (setq coq--current-background-jobs (1+ coq--current-background-jobs)) - (process-put process 'coq-compilation-job job) - (process-put process 'coq-process-continuation continuation) - (process-put process 'coq-process-command (cons command arguments)) - (process-put process 'coq-process-output "") - (process-put process 'coq-process-rm file-rm)))) + (when coq--debug-auto-compilation + (message "%s %s: start %s %s in %s" + (get job 'name) process-name + command (mapconcat 'identity arguments " ") + default-directory)) + (condition-case err + ;; If the command is wrong, start-process aborts with an + ;; error. However, in Emacs 23.4.1. it will leave a process + ;; behind, which is in a very strange state: running with no + ;; pid. Emacs 24.2 fixes this. + (setq process (apply 'start-process process-name + nil ; no process buffer + command arguments)) + (error + (when coq--debug-auto-compilation + (message "%s %s: error in start process, %s" + (get job 'name) process-name + (if file-rm + (format "rm %s" file-rm) + "no file removal"))) + (when file-rm + (ignore-errors (delete-file file-rm))) + (signal 'coq-compile-error-command-start + (list (cons command arguments) (nth 2 err))))) + (set-process-filter process 'coq-par-process-filter) + (set-process-sentinel process 'coq-par-process-sentinel) + (set-process-query-on-exit-flag process nil) + (setq coq--current-background-jobs (1+ coq--current-background-jobs)) + (process-put process 'coq-compilation-job job) + (process-put process 'coq-process-continuation continuation) + (process-put process 'coq-process-command (cons command arguments)) + (process-put process 'coq-process-output "") + (process-put process 'coq-process-rm file-rm))) (defun coq-par-process-sentinel (process event) "Sentinel for all kinds of Coq background compilation processes. @@ -981,7 +980,10 @@ function and reported appropriately." (get (process-get process 'coq-compilation-job) 'name))) (coq-par-second-stage-enqueue (process-get process 'coq-compilation-job)))) - (let (exit-status) + ;; process was not killed explicitly by us + (let (exit-status + (default-directory + (get (process-get process 'coq-compilation-job) 'current-dir))) (when coq--debug-auto-compilation (message "%s %s: process status changed to %s (default-dir %s curr buf %s)" @@ -1840,7 +1842,7 @@ synchronously or asynchronously." (coq-par-start-task new-job) (coq-par-job-enqueue new-job))) -(defun coq-par-job-init-common (coq-load-path type) +(defun coq-par-job-init-common (coq-load-path type current-dir) "Common initialization for 'require and 'file jobs. Create a new job of type TYPE and initialize all common fields of require and file jobs that need an initialization different from @@ -1851,6 +1853,7 @@ nil." (put new-job 'coqc-dependency-count 0) (put new-job 'type type) (put new-job 'state 'enqueued-coqdep) + (put new-job 'current-dir current-dir) ;; The ancestor modification time is not really needed in require ;; jobs, however, if the field is present, we can treat require ;; and file jobs more uniformely. @@ -1859,7 +1862,8 @@ nil." (put new-job 'load-path coq-load-path) new-job)) -(defun coq-par-create-require-job (coq-load-path require-items require-span) +(defun coq-par-create-require-job (coq-load-path require-items require-span + current-dir) "Create a new require job for REQUIRE-SPAN. Create a new require job and initialize its fields. COQ-LOAD-PATH is the load path configured for the current scripting buffer, @@ -1875,10 +1879,9 @@ not search the current directory. This function is called synchronously when asserting. The new require job is neither started nor enqueued here - the caller must do this." - (let ((new-job (coq-par-job-init-common coq-load-path 'require))) + (let ((new-job (coq-par-job-init-common coq-load-path 'require current-dir))) (put new-job 'require-span require-span) (put new-job 'queueitems require-items) - (put new-job 'current-dir default-directory) (when coq--debug-auto-compilation (let* ((require-item (car require-items)) (require-command (mapconcat 'identity (nth 1 require-item) " "))) @@ -1890,7 +1893,8 @@ must do this." ;; there was some error and it was not used anywhere back then, but ;; job is now needed as a dependency of some other file? ;; XXX what happens if the job exists and is failed? -(defun coq-par-create-file-job (module-vo-file coq-load-path dep-src-file) +(defun coq-par-create-file-job (module-vo-file coq-load-path dep-src-file + current-dir) "Create a new file job for MODULE-VO-FILE. DEP-SRC-FILE is the source file whose coqdep output we are just processing and which depends on MODULE-VO-FILE. This argument is @@ -1907,7 +1911,7 @@ If a new job is created it is started or enqueued right away." (cond ((gethash module-vo-file coq--compilation-object-hash)) (t - (let ((new-job (coq-par-job-init-common coq-load-path 'file))) + (let ((new-job (coq-par-job-init-common coq-load-path 'file current-dir))) ;; fields 'required-obj-file and obj-mod-time are implicitely set to nil (put new-job 'vo-file module-vo-file) (put new-job 'src-file (coq-library-src-of-vo-file module-vo-file)) @@ -2090,7 +2094,8 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (unless (coq-compile-ignore-file dep-vo-file) (let* ((dep-job (coq-par-create-file-job dep-vo-file (get job 'load-path) - (get job 'src-file))) + (get job 'src-file) + (get job 'current-dir))) (dep-time (get dep-job 'youngest-coqc-dependency))) (when (get dep-job 'failed) (setq dependee-failed t)) @@ -2220,7 +2225,9 @@ This function is called synchronously when asserting." `(lambda () (coq-unlock-all-ancestors-of-span ,span))) ;; create a new require job and maintain coq--last-compilation-job - (setq new-job (coq-par-create-require-job coq-load-path require-items span)) + (setq new-job + (coq-par-create-require-job coq-load-path require-items span + default-directory)) (when coq--last-compilation-job (coq-par-add-queue-dependency coq--last-compilation-job new-job)) (setq coq--last-compilation-job new-job) From b30765337532a8c7926e6b7003c1e7062e1089b5 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 4 Apr 2021 11:39:18 +0200 Subject: [PATCH 4/6] extend default-directory test to second stage --- ci/compile-tests/008-default-dir/runtest.el | 44 ++++++++++++++++--- .../bin/compile-test-start-delayed | 3 ++ ci/compile-tests/bin/coqc-delayed | 2 +- ci/compile-tests/bin/coqdep-delayed | 2 +- ci/compile-tests/cct-lib.el | 43 +++++++++++++++++- 5 files changed, 85 insertions(+), 9 deletions(-) diff --git a/ci/compile-tests/008-default-dir/runtest.el b/ci/compile-tests/008-default-dir/runtest.el index c0cfe3af5..7b9c9f853 100644 --- a/ci/compile-tests/008-default-dir/runtest.el +++ b/ci/compile-tests/008-default-dir/runtest.el @@ -63,18 +63,21 @@ See `cct-generic-check-main-buffer'." "`default-directory' test. Test that `default-directory' is correctly set independently of the current buffer in the foreground." - (let (vo-times av-buffer ci-buffer other-locked-files) + (let (vo-times av-buffer ci-buffer other-locked-files + vok-times vos-vio-files) ;; (setq cct--debug-tests t) ;; (setq coq--debug-auto-compilation t) (find-file "a.v") (setq av-buffer (current-buffer)) - (message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s" - coq-dependency-analyzer - coq-compiler - (getenv "PATH") - exec-path) + (message + "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s\ndetected coq version: %s" + coq-dependency-analyzer + coq-compiler + (getenv "PATH") + exec-path + coq-autodetected-version) (find-file "../..") (setq ci-buffer (current-buffer)) @@ -99,6 +102,7 @@ current buffer in the foreground." (cct-check-locked 23 'locked) (cct-replace-last-word 23 "3") (check-main-buffer vo-times "6" '("./b.vo") other-locked-files) + (setq vo-times (cct-record-change-times all-compiled-ancestors)) ;; 4. change c and process again - b and c should get compiled (message "\n4. change c and process again - b and c should get compiled\n") @@ -107,5 +111,33 @@ current buffer in the foreground." (cct-check-locked 23 'locked) (cct-replace-last-word 23 "5") (check-main-buffer vo-times "8" '("./b.vo" "./c.vo") other-locked-files) + (setq vo-times (cct-record-change-times all-compiled-ancestors)) + ;; 5. change b and c and reprocess with vos-and-vok/quick-and-vio2vo + (message + "\n5. change b and c and reprocess with vos-and-vok/quick-and-vio2vo\n") + (if (coq--post-v811) + (setq coq-compile-vos 'vos-and-vok + vos-vio-files '("./b.vos" "./c.vos") + vok-times (cct-record-change-times '("./b.vok" "./c.vok"))) + (setq coq-compile-quick 'quick-and-vio2vo + vos-vio-files '("./b.vio" "./c.vio"))) + + (set-buffer "b.v") + (cct-check-locked 23 'locked) + (cct-replace-last-word 23 "7") + (set-buffer "c.v") + (cct-check-locked 23 'unlocked) + (cct-replace-last-word 23 "10") + (check-main-buffer nil "17" nil other-locked-files) + + (cct-files-are-readable vos-vio-files) + ;; this will switch to a different default-directory, see the + ;; hooks above + (cct-wait-for-second-stage) + (if (coq--post-v811) + (progn + (cct-older-change-times vok-times) + (cct-unmodified-change-times vo-times)) + (cct-older-change-times vo-times)) )) diff --git a/ci/compile-tests/bin/compile-test-start-delayed b/ci/compile-tests/bin/compile-test-start-delayed index f528f4d1d..a35a98bd9 100755 --- a/ci/compile-tests/bin/compile-test-start-delayed +++ b/ci/compile-tests/bin/compile-test-start-delayed @@ -37,6 +37,9 @@ fi key="$1" file="${@: -1}" + +#echo key $key file "\"$file\"" + shift delay=$(sed -ne "/$key/ s/.*$key \([0-9]*\).*/\1/p" $file) diff --git a/ci/compile-tests/bin/coqc-delayed b/ci/compile-tests/bin/coqc-delayed index 26c92805c..dcbe9d59c 100755 --- a/ci/compile-tests/bin/coqc-delayed +++ b/ci/compile-tests/bin/coqc-delayed @@ -1,3 +1,3 @@ #!/bin/bash -exec compile-test-start-delayed coqc-delay coqc "$*" +exec compile-test-start-delayed coqc-delay coqc "$@" diff --git a/ci/compile-tests/bin/coqdep-delayed b/ci/compile-tests/bin/coqdep-delayed index f123770a0..76fc4efcc 100755 --- a/ci/compile-tests/bin/coqdep-delayed +++ b/ci/compile-tests/bin/coqdep-delayed @@ -1,3 +1,3 @@ #!/bin/bash -exec compile-test-start-delayed coqdep-delay coqdep "$*" +exec compile-test-start-delayed coqdep-delay coqdep "$@" diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el index e573f5c65..98b71ea79 100644 --- a/ci/compile-tests/cct-lib.el +++ b/ci/compile-tests/cct-lib.el @@ -136,6 +136,27 @@ the prover. In many tests these hooks are not used." (accept-process-output nil 0.1)) (run-hooks 'cct-after-busy-waiting-hook)) +(defun cct-wait-for-second-stage () + "Wait until second stage compilation is complete. +Runs `cct-before-busy-waiting-hook' and +`cct-after-busy-waiting-hook' before and after busy waiting." + (run-hooks 'cct-before-busy-waiting-hook) + (when cct--debug-tests + (message + "%s start waiting for vok/vio2vo timer %s 2nd-stage-in-progress %s" + (current-time-string) + coq--par-second-stage-delay-timer + coq--par-second-stage-in-progress)) + (while (or coq--par-second-stage-delay-timer + coq--par-second-stage-in-progress) + (accept-process-output nil 0.5) + (when cct--debug-tests + (message "%s wait for vok/vio2vo timer %s 2nd-stage-in-progress %s" + (current-time-string) + coq--par-second-stage-delay-timer + coq--par-second-stage-in-progress))) + (run-hooks 'cct-after-busy-waiting-hook)) + (defun cct-get-vanilla-span (line) "Get THE vanilla span for line LINE, report an error if there is none. PG uses a number of overlapping and non-overlapping spans (read @@ -212,7 +233,7 @@ Used to check that FILE has not been changed since TIME was recorded before." (let ((file-time (nth 5 (file-attributes file)))) (when cct--debug-tests - (message "file %s should be unchanged, recorded time: %s now: %s\n" + (message "file %s should be unchanged, recorded time: %s now: %s" file (format-time-string "%H:%M:%S.%3N" time) (format-time-string "%H:%M:%S.%3N" file-time))) @@ -241,6 +262,14 @@ changed since FILE-TIME-ASSOC has been recorded." (defun cct-file-newer (file time) "Check that FILE exists and its modification time is more recent than TIME." (let ((file-time (nth 5 (file-attributes file)))) + (when cct--debug-tests + (message "file %s in %s should be changed, recorded time: %s now: %s" + file + default-directory + (if time (format-time-string "%H:%M:%S.%3N" time) "---") + (if file-time + (format-time-string "%H:%M:%S.%3N" file-time) + "---"))) (should (and file-time (time-less-p time file-time))))) (defun cct-older-change-times (file-time-assoc) @@ -251,11 +280,23 @@ times as returned by `cct-record-change-times' or FILE-TIME-ASSOC do exist and that their modification time is more recent than in the association list, i.e., they have been updated or changed since recording the time in the association." + (when cct--debug-tests + (message "Files should have been changed: %s" + (mapconcat + (lambda (file-time) (car file-time)) + file-time-assoc + ", "))) (mapc (lambda (file-time-cons) (cct-file-newer (car file-time-cons) (cdr file-time-cons))) file-time-assoc)) +(defun cct-files-are-readable (files) + "Check that FILES exist and are readable." + (when cct--debug-tests + (message "Files should exist and be readable: %s" files)) + (mapc (lambda (fname) (should (file-readable-p fname))) files)) + (defun cct-generic-check-main-buffer (main-buf main-unlocked main-locked main-sum-line new-sum vo-times recompiled-files require-ancestors From e782e646f3512442428bd17fba16a13826b8e681 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 4 Apr 2021 21:57:27 +0200 Subject: [PATCH 5/6] fix default directory problem for second stage start --- ci/compile-tests/README.md | 8 +- .../bin/compile-test-start-delayed | 13 ++- coq/coq-par-compile.el | 81 +++++++++++++++---- 3 files changed, 85 insertions(+), 17 deletions(-) diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md index 0a0ca5dc3..7c939741b 100644 --- a/ci/compile-tests/README.md +++ b/ci/compile-tests/README.md @@ -30,7 +30,8 @@ All tests are for parallel background compilation. coqdep and coqc 008-default-dir : test that the default/current directory is set correctly - independent of user/emacs changing the current buffer + independent of user/emacs changing the current buffer during + first and second stage compilation # Tests currently missing @@ -43,3 +44,8 @@ All tests are for parallel background compilation. in state waiting-queue - coq-par-create-file-job finds a failed job - all tests in all quick and all vos variants +- test two coq-par-kickoff-queue-from-action-list entries being + active at the same time: assert one region, let compilation + fail, assert second region, while first region is still busy, + this should fail in some weird way, because failed is not + propagated diff --git a/ci/compile-tests/bin/compile-test-start-delayed b/ci/compile-tests/bin/compile-test-start-delayed index a35a98bd9..50ae7a03a 100755 --- a/ci/compile-tests/bin/compile-test-start-delayed +++ b/ci/compile-tests/bin/compile-test-start-delayed @@ -20,7 +20,8 @@ function usage(){ Start program prog with arguments args with some delay. There must be at least one argument in args and the last one must be - a file. The delay is taken from a line in that file that + a file or something that becomes a file when ".v" is appended. + The delay is taken from a line in that file that contains the key, followed by a space and the delay in seconds (maybe somewhere in the middle of the line). The file must contain at most one line containing key. When there is no line @@ -42,6 +43,16 @@ file="${@: -1}" shift +# vio2vo needs a module name or a .vio file on the command line +# support only module names for now +if [ ! -f "$file" ] ; then + if [ -f "$file.v" ] ; then + file="$file.v" + else + exit 22 + fi +fi + delay=$(sed -ne "/$key/ s/.*$key \([0-9]*\).*/\1/p" $file) if [ -z "$delay" ] ; then diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 5c616abb8..0cecd9cba 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -84,6 +84,7 @@ ;; 4- using -quick and the handling of .vo/.vio prerequisites for Coq < 8.11 ;; 5- using -vos for Coq >= 8.11 ;; 6- running vio2vo or -vok to check proofs +;; 7- default-directory / current directory ;; ;; ;; For 1- where to put the Require command and the items that follow it: @@ -228,6 +229,21 @@ ;; `coq--par-second-stage-start-id' and only acts if that is still the ;; current value when the callback is executed. ;; +;; +;; For 7- default-directory / current directory +;; +;; `default-directory' determines the current directory for background +;; processes. In a sentinel or process filter, default-directory is +;; taken from the current buffer, which is basically random. Starting +;; with a wrong current directory will cause compilation failures. +;; Therefore all entry points of this library must set +;; default-directory. Entry points are coq-par-process-sentinel, the +;; functions started from timer and those started from an empty entry +;; in `proof-action-list'. To set default-directory in these cases, I +;; record default-directory in 'current-dir inside +;; `coq-par-preprocess-require-commands' and then pass it on to all +;; jobs created. +;; ;; ;; Properties of compilation jobs ;; @@ -297,8 +313,10 @@ ;; 'visited - used in the dependency cycle detection to mark ;; visited jobs ;; 'current-dir - current directory or default-directory of the buffer -;; that contained the require command. Only present in -;; require jobs. Only needed for 8.4 compatibility. +;; that contained the require command. Passed recursively +;; to all jobs. Used to set default-directory in the +;; sentinel and other functions, because it can otherwise +;; be more or less random. ;; 'temp-require-file - temporary file name just containing the require ;; command of a require job for determining the files ;; needed for that require. Must be deleted after @@ -521,14 +539,22 @@ their SOURCE binding." "Insert X in queue QUEUE." (push x (car queue))) +(defun coq-par-queue-reverse-if-needed (queue) + "Reorganize QUEUE, such that the pop-end contains something. +Of course only if necessary and possible." + (unless (cdr queue) + (setcdr queue (nreverse (car queue))) + (setcar queue nil))) + +(defun coq-par-queue-head (queue) + "Return the head of QUEUE, if any, without removing it." + (coq-par-queue-reverse-if-needed queue) + (cadr queue)) + (defun coq-par-dequeue (queue) "Dequeue the next item from QUEUE." - (let ((res (pop (cdr queue)))) - (unless res - (setcdr queue (nreverse (car queue))) - (setcar queue nil) - (setq res (pop (cdr queue)))) - res)) + (coq-par-queue-reverse-if-needed queue) + (pop (cdr queue))) (defun coq-par-queue-length (queue) "Length of QUEUE." @@ -573,6 +599,10 @@ Use `coq-par-second-stage-enqueue', (when coq--debug-auto-compilation (message "%s: enqueue job in second stage queue" (get job 'name)))) +(defun coq-par-second-stage-head () + "Return the head of the second stage queue, if any, without removing it." + (coq-par-queue-head coq--par-second-stage-queue)) + (defun coq-par-second-stage-dequeue () "Dequeue the next job from the second stage queue." (let ((res (coq-par-dequeue coq--par-second-stage-queue))) @@ -1037,7 +1067,10 @@ function and reported appropriately." ;;; second stage compilation (vio2vo and vok) (defun coq-par-run-second-stage-queue () - "Start delayed second stage compilation (vio2vo or vok)." + "Start delayed second stage compilation (vio2vo or vok). +Set `default-directory' from the 'current-dir property of the +head of the second stage queue, such that processes started here +run with the right current directory." ;; XXX this assert can be triggered - just start a compilation ;; shortly before the timer triggers (cl-assert (not coq--last-compilation-job) @@ -1046,9 +1079,12 @@ function and reported appropriately." (when coq--debug-auto-compilation (message "Start second stage processing for %d jobs" (coq-par-second-stage-queue-length))) - (when (> (coq-par-second-stage-queue-length) 0) - (setq coq--par-second-stage-in-progress t) - (coq-par-start-jobs-until-full))) + (let ((head (coq-par-second-stage-head)) + default-directory) + (when head + (setq default-directory (get head 'current-dir)) + (setq coq--par-second-stage-in-progress t) + (coq-par-start-jobs-until-full)))) (defun coq-par-require-processed (race-counter) "Callback for `proof-action-list' to signal completion of the last Require. @@ -1098,6 +1134,11 @@ item will be processed as comment and only the callback will be called." (message "%s -> %s: add coqc dependency" (get dependee 'name) (get dependant 'name)))) +;; XXX need to propagate 'failed from dependee to dependant +;; Relevant, if user asserts second region when for the first one +;; compilation has failed already, but the queue region is still +;; processing. What happens with coq--par-delayed-last-job and the +;; delayed coq-par-kickoff-queue-maybe call? (defun coq-par-add-queue-dependency (dependee dependant) "Add queue dependency from require job DEPENDEE to require job DEPENDANT. The require item of DEPENDANT comes after those of DEPENDEE. @@ -1433,6 +1474,14 @@ jobs when they transition from 'waiting-queue to 'ready: ;; resetting queueitems is on the save side in any case (put job 'queueitems nil)))) +(defun coq-par-kickoff-queue-from-action-list (job) + "Trigger `coq-par-kickoff-queue-maybe' from action list. +Simple wrapper around `coq-par-kickoff-queue-maybe' to set +`default-directory' when entering background compilation +functions from `proof-action-list'." + (let ((default-directory (get job 'current-dir))) + (coq-par-kickoff-queue-maybe job))) + (defun coq-par-kickoff-queue-maybe (job) "Transition require job JOB to 'waiting-queue and maybe to 'ready. This function can only be called for require jobs. It further @@ -1496,7 +1545,8 @@ retired and transition to 'ready. This means: (setq coq--par-delayed-last-job t) (proof-add-to-queue (list (coq-par-callback-queue-item - `(lambda (span) (coq-par-kickoff-queue-maybe ',job)))) + `(lambda (span) + (coq-par-kickoff-queue-from-action-list ',job)))) 'advancing)) (put job 'state 'ready) (when coq--debug-auto-compilation @@ -1873,8 +1923,9 @@ following the REQUIRE-SPAN, they are temporarily stored in the new require job outside of `proof-action-list'. The current directory (from `default-directory') is stored in -property 'current-dir for <8.5 compatibility, where coqdep did -not search the current directory. +property 'current-dir and propagated to all dependend jobs. This +is used to set `default-directory' when entering background +compilation from a sentinel or elsewhere. This function is called synchronously when asserting. The new require job is neither started nor enqueued here - the caller From 70ff03799f6f21424643d4e25d1f1bbb596a5cee Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 5 Apr 2021 22:32:35 +0200 Subject: [PATCH 6/6] enable compilation for remote files via tramp tramp support is not complete with this patch, but works if used with care. There are a few assertions that quick user interactions can trigger. Automatic background compilation via tramp is very slow, because tramp opens a new connection with all overhead for each asynchronous coqdep and coqc invocation. With this patch, tramp support only works for Emacs version 26 or later, because it uses make-nearby-temp-file. Modifications: - switch to functions that properly deal with remote or magic files - protect sentinels against multiple instances running interleaved, which suddenly happens under tramp - recognize the error when coqdep cannot access a file Fixes #104 and fixes #203. --- coq/coq-par-compile.el | 252 +++++++++++++++++++++++++++++++++++------ 1 file changed, 216 insertions(+), 36 deletions(-) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 0cecd9cba..5b59ed78e 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -85,6 +85,7 @@ ;; 5- using -vos for Coq >= 8.11 ;; 6- running vio2vo or -vok to check proofs ;; 7- default-directory / current directory +;; 8- sentinels running interleaved ;; ;; ;; For 1- where to put the Require command and the items that follow it: @@ -243,6 +244,27 @@ ;; record default-directory in 'current-dir inside ;; `coq-par-preprocess-require-commands' and then pass it on to all ;; jobs created. +;; +;; +;; For 8- sentinels running interleaved +;; +;; Sentinels (and also process filters) run only when emacs waits +;; inside certain functions. The functions in this library start +;; asynchronous background processes but do not perform such waiting. +;; From this one could naively infer that invocations of +;; `coq-par-process-sentinel' can never run interleaved. This is +;; indeed the case when working with local files only (as contrast to +;; remote files in the sense of Tramp). However, when working with +;; remote files (possibly via Tramp), a lot of normal system functions +;; (`file-attributes', `file-truename', and so on) run as synchronous +;; processes that wait for the remote side. Without precautions +;; several sentinels may then run interleaved. To avoid this, the +;; sentinel and other functions entering this library must aquire the +;; `coq--par-process-sentinels' lock. When the lock is busy, newly +;; incoming sentinels wait in `coq--par-sentinel-queue'. Before +;; exiting a function that aquired the lock, one runs +;; `coq-par-run-queued-sentinels' to run all waiting sentinels and to +;; release the lock. ;; ;; ;; Properties of compilation jobs @@ -479,6 +501,12 @@ which is otherwise started when `coq--last-compilation-job' has not been retired but no compilation process is running in the background.") +(defvar coq--par-process-sentinels nil + "Lock for entering `coq-par-process-sentinel' and other functions. +This lock needs to be taken before entering functions in this +library that modify the internal state of compilation jobs. When +the lock is busy, sentinels must queue in `coq--par-sentinel-queue'.") + ;;; utility functions @@ -617,6 +645,36 @@ Use `coq-par-second-stage-enqueue', (coq-par-queue-length coq--par-second-stage-queue)) +;;; queue for process sentinels + +(defvar coq--par-sentinel-queue (coq-par-new-queue) + "Queue of waiting sentinels. +To be executed when the currently running sentinel finishes. Use +`coq-par-sentinel-enqueue' and `coq-par-sentinel-dequeue' to +access the queue.") + +(defun coq-par-sentinel-enqueue (process event) + "Insert the sentinel arguments PROCESS and EVENT in the sentinel queue." + (coq-par-enqueue coq--par-sentinel-queue (cons process event)) + (when coq--debug-auto-compilation + (message "%s %s: enqueue sentinel" + (get (process-get process 'coq-compilation-job) 'name) + (process-name process)))) + +(defun coq-par-sentinel-dequeue () + "Dequeue the next pair of sentinel arguments from the sentinel queue. +Returns a cons of process and event arguments for +`coq--par-process-sentinels'." + (let ((res (coq-par-dequeue coq--par-sentinel-queue))) + (when coq--debug-auto-compilation + (if res + (message "%s %s: dequeue sentinel" + (get (process-get (car res) 'coq-compilation-job) 'name) + (process-name (car res))) + (message "sentinel queue empty"))) + res)) + + ;;; error symbols ;; coq-compile-error-coqdep @@ -783,13 +841,28 @@ or .vos files must be done elsewhere." ;; (message "analyse coqdep output \"%s\"" output)) (if (or (not (eq status 0)) + ;; when a file on the command line is missing, coqdep drops it, + ;; possibly outputting nothing + (equal output "") + ;; when a dependency is missing coqdep outputs a warning with status 0 (string-match coq-coqdep-error-regexp output)) (progn ;; display the error - (coq-compile-display-error (mapconcat 'identity command " ") output t) - (if (eq status 0) - "unsatisfied dependencies" - (format "coqdep exist status %d" status))) + (coq-compile-display-error + (mapconcat 'identity command " ") + (if (equal output "") + "No coqdep output - file probably inaccessible" + output) + t) + ;; give back a string to signal error - the string content + ;; will only become visible during debugging + (cond + ((not (eq status 0)) + (format "coqdep exit status %d" status)) + ((equal output "") + "no coqdep output") + (t + "unsatisfied dependencies"))) ;; In 8.5, coqdep produces two lines. Match with .* here to ;; extract only a part of the first line. ;; We could match against (concat "^[^:]*" obj-file "[^:]*: \\(.*\\)") @@ -810,8 +883,9 @@ or .vos files must be done elsewhere." Return t if some process was killed." ;; need to first mark processes as killed, because delete process ;; starts running sentinels in the order processes terminated, so - ;; after the first delete-process we see sentinentels of non-killed + ;; after the first delete-process we see sentinels of non-killed ;; processes running + ;; XXX maybe the two stage kill is not needed anymore because of sentinel lock (let ((kill-needed)) (mapc (lambda (process) @@ -849,7 +923,10 @@ Used for unlocking ancestors on compilation errors." "Kill all background compilation, cleanup internal state and unlock ancestors. This is the common core of `coq-par-emergency-cleanup' and `coq-par-user-interrupt'. Returns t if there actually was a -background job that was killed." +background job that was killed. This function does not cleanup +the sentinel lock and the sentinel queue, because this function +might get called from inside `coq-par-process-sentinel-wrapper', +which is protected by the sentinel lock." (let (proc-killed) (when coq--debug-auto-compilation (message "kill all jobs and cleanup state")) @@ -945,7 +1022,7 @@ file to be deleted when the process does not finish successfully." ;; error. However, in Emacs 23.4.1. it will leave a process ;; behind, which is in a very strange state: running with no ;; pid. Emacs 24.2 fixes this. - (setq process (apply 'start-process process-name + (setq process (apply 'start-file-process process-name nil ; no process buffer command arguments)) (error @@ -970,7 +1047,75 @@ file to be deleted when the process does not finish successfully." (process-put process 'coq-process-rm file-rm))) (defun coq-par-process-sentinel (process event) - "Sentinel for all kinds of Coq background compilation processes. + "Sentinel for all processes started by `coq-par-start-process'. +Depending on the sentinel lock `coq--par-process-sentinels', +directly execute the sentinel functionality or queue it. If the +lock is taken here, run all sentinels that queued during the run +time of this sentinel at the end." + (if coq--par-process-sentinels + (coq-par-sentinel-enqueue process event) + (cl-assert (not (coq-par-sentinel-dequeue)) nil + "sentinel queue non-empty when sentinel lock is free") + (setq coq--par-process-sentinels t) + (unwind-protect + (coq-par-process-sentinel-wrapper process event) + (coq-par-run-queued-sentinels)))) + +(defun coq-par-run-queued-sentinels () + "Run all queued sentinels and free the lock `coq--par-process-sentinels'. +Ensure sentinel queue is empty and sentinel lock is free, even in +case of error. This function should run _after_ killing all +processes in an emergency cleanup, for instance in an unwind +protect around the error handler that triggers the cleanup in +case of error. Oherwise the queue and the lock will be left +behind." + (let (process-event) + (cl-assert coq--par-process-sentinels nil + "sentinel lock not busy before clearing sentinel queue") + (unwind-protect + ;; In case of an error in one of the queued sentinels, none of + ;; the following sentinels and no sentinel for all the killed + ;; jobs will run. This will leave all 'coq-process-rm content + ;; behind, in the worst case partially written vo or vio + ;; files. XXX consider to make at least one attempt to clean + ;; up 'coq-process-rm stuff after an error. + (while (setq process-event (coq-par-sentinel-dequeue)) + (coq-par-process-sentinel-wrapper + (car process-event) (cdr process-event))) + ;; In case of normal termination the queue is empty at this + ;; point, reinitializing it only wastes a cons cell. In case of + ;; abnormal termination cleanup is essential. + (setq coq--par-sentinel-queue (coq-par-new-queue)) + (setq coq--par-process-sentinels nil)))) + +(defun coq-par-process-sentinel-wrapper (process event) + "Exception and debug status wrapper around `coq-par-process-sentinel-internal'. +The funcion must not be called without acquiring the sentinel lock +`coq--par-process-sentinels' first." + (condition-case err + (progn + (when coq--debug-auto-compilation + (message "%s %s: enter sentinel" + (get (process-get process 'coq-compilation-job) 'name) + (process-name process))) + (cl-assert coq--par-process-sentinels nil + "sentinel lock not busy before entering real sentinel") + (coq-par-process-sentinel-internal process event) + (when coq--debug-auto-compilation + (message "%s %s: leave sentinel normally" + (get (process-get process 'coq-compilation-job) 'name) + (process-name process)))) + (error + (message "%s %s: leave sentinel abnormally" + (get (process-get process 'coq-compilation-job) 'name) + (process-name process)) + (signal (car err) (cdr err))))) + +(defun coq-par-process-sentinel-internal (process event) + "Real functionality of the sentinel for all compilation processes. +This function must not be called when a different instance is +still running. + Runs when process PROCESS terminated because of EVENT. It determines the exit status and calls the continuation function that has been registered with that process. Normal compilation @@ -1071,20 +1216,30 @@ function and reported appropriately." Set `default-directory' from the 'current-dir property of the head of the second stage queue, such that processes started here run with the right current directory." + ;; XXX protect this function against escaping exceptions and clean + ;; up, if this happens similar to sentinel and + ;; coq-par-preprocess-require-commands ;; XXX this assert can be triggered - just start a compilation ;; shortly before the timer triggers (cl-assert (not coq--last-compilation-job) nil "normal compilation and second stage in parallel 1") (setq coq--par-second-stage-delay-timer nil) (when coq--debug-auto-compilation - (message "Start second stage processing for %d jobs" + (message "Kickoff second stage processing for %d jobs" (coq-par-second-stage-queue-length))) (let ((head (coq-par-second-stage-head)) default-directory) (when head (setq default-directory (get head 'current-dir)) + ;; XXX fix this to ensure this cannot fire + (cl-assert (not coq--par-process-sentinels) nil + "sentinel lock busy when starting second stage") + (setq coq--par-process-sentinels t) (setq coq--par-second-stage-in-progress t) - (coq-par-start-jobs-until-full)))) + (coq-par-start-jobs-until-full) + (coq-par-run-queued-sentinels) + (when coq--debug-auto-compilation + (message "Leave second stage kickoff"))))) (defun coq-par-require-processed (race-counter) "Callback for `proof-action-list' to signal completion of the last Require. @@ -1346,12 +1501,13 @@ the 'second-stage property on job to 'vok if necessary." (when coq--debug-auto-compilation (message (concat "%s: compare mod times: vos mod %s, src mod %s, youngest dep %s\n" - "\tsrc file %s in %s") + "\tvos %s src %s in %s") (get job 'name) (if vos-obj-time (current-time-string vos-obj-time) "-") (if src-time (current-time-string src-time) "-") (if (eq dep-time 'just-compiled) "just compiled" (current-time-string dep-time)) + vos-file (get job 'src-file) default-directory)) ;; the source file must exist @@ -1479,8 +1635,16 @@ jobs when they transition from 'waiting-queue to 'ready: Simple wrapper around `coq-par-kickoff-queue-maybe' to set `default-directory' when entering background compilation functions from `proof-action-list'." + ;; XXX protect this function against escaping exceptions and clean + ;; up, if this happens similar to sentinel and + ;; coq-par-preprocess-require-commands (let ((default-directory (get job 'current-dir))) - (coq-par-kickoff-queue-maybe job))) + ;; XXX fix this to ensure this cannot fire + (cl-assert (not coq--par-process-sentinels) nil + "sentinel lock busy when kickoff queue from action list") + (setq coq--par-process-sentinels t) + (coq-par-kickoff-queue-maybe job) + (coq-par-run-queued-sentinels))) (defun coq-par-kickoff-queue-maybe (job) "Transition require job JOB to 'waiting-queue and maybe to 'ready. @@ -1650,7 +1814,8 @@ transition is triggered for DEPENDANT. For 'file jobs this is This function must be called for failed jobs to complete all necessary transitions." - ;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time) + ;; (message "%s: CPDCD state %s with time %s" + ;; (get dependant 'name) (get dependant 'state) dependee-time) (cl-assert (eq (get dependant 'state) 'waiting-dep) nil "wrong state of parent dependant job") (when (coq-par-time-less (get dependant 'youngest-coqc-dependency) @@ -1759,7 +1924,14 @@ was queued." (coq-load-path-include-current nil) (require-command (mapconcat 'identity (nth 1 (car (get job 'queueitems))) " ")) - (temp-file (make-temp-file "ProofGeneral-coq" nil ".v"))) + temp-file temp-file-local-part) + (if (fboundp 'make-nearby-temp-file) + ;; make-nearby-temp-file was introduced in 26.1 + (progn + (setq temp-file (make-nearby-temp-file "ProofGeneral-coq" nil ".v")) + (setq temp-file-local-part (file-local-name temp-file))) + (setq temp-file (make-temp-file "ProofGeneral-coq" nil ".v")) + (setq temp-file-local-part temp-file)) (put job 'temp-require-file temp-file) (with-temp-file temp-file (insert require-command)) (when coq--debug-auto-compilation @@ -1768,7 +1940,7 @@ was queued." (get job 'temp-require-file))) (coq-par-start-process coq-dependency-analyzer - (coq-par-coqdep-arguments (get job 'temp-require-file) load-path) + (coq-par-coqdep-arguments temp-file-local-part load-path) 'coq-par-process-coqdep-result job (get job 'temp-require-file)))) @@ -2383,27 +2555,35 @@ does the error checking/reporting for `coq-par-preprocess-require-commands-internal', which does all the work. This function is called synchronously when asserting." (when coq-compile-before-require - (condition-case err - (coq-par-preprocess-require-commands-internal) - (coq-compile-error - (coq-par-emergency-cleanup) - (message "%s %s" (get (car err) 'error-message) (cdr err))) - (coq-unclassifiable-version - (coq-par-emergency-cleanup) - (if (equal (cdr err) "trunk") - (message - (concat "your Coq version \"trunk\" is too unspecific for " - "Proof General; please customize coq-pinned-version")) - (message "%s \"%s\"; consider customizing coq-pinned-version" - (get (car err) 'error-message) (cdr err)))) - (file-error - (coq-par-emergency-cleanup) - (message "Error: %s" (mapconcat 'identity (cdr err) ": "))) - (error - (message "Unexpected error during parallel compilation: %s" - err) - (coq-par-emergency-cleanup) - (signal (car err) (cdr err)))))) + (unwind-protect + (condition-case err + (progn + ;; XXX transform the synchronously called functions here + ;; such that this assert cannot be triggered any more + (cl-assert (not coq--par-process-sentinels) nil + "sentinel lock busy when entering compilation") + (setq coq--par-process-sentinels t) + (coq-par-preprocess-require-commands-internal)) + (coq-compile-error + (coq-par-emergency-cleanup) + (message "%s %s" (get (car err) 'error-message) (cdr err))) + (coq-unclassifiable-version + (coq-par-emergency-cleanup) + (if (equal (cdr err) "trunk") + (message + (concat "your Coq version \"trunk\" is too unspecific for " + "Proof General; please customize coq-pinned-version")) + (message "%s \"%s\"; consider customizing coq-pinned-version" + (get (car err) 'error-message) (cdr err)))) + (file-error + (coq-par-emergency-cleanup) + (message "Error: %s" (mapconcat 'identity (cdr err) ": "))) + (error + (message "Unexpected error during parallel compilation: %s" + err) + (coq-par-emergency-cleanup) + (signal (car err) (cdr err)))) + (coq-par-run-queued-sentinels)))) (provide 'coq-par-compile)