From 7cde26b20cab22d2a82f6bb50e852bbb5688d610 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 14 Dec 2020 22:27:36 +0100 Subject: add auto compile test to trigger two bugs for dependees in state ready See also the committed test.el. The test is not completely robust, it needs to be improved in the future. --- ci/compile-tests/006-ready-dependee/Makefile | 28 ++++++ ci/compile-tests/006-ready-dependee/a.v.orig | 38 ++++++++ ci/compile-tests/006-ready-dependee/b.v.orig | 23 +++++ ci/compile-tests/006-ready-dependee/c.v.orig | 23 +++++ ci/compile-tests/006-ready-dependee/d.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/e.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/f.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/g.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/h.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/i.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/j.v.orig | 15 ++++ ci/compile-tests/006-ready-dependee/k.v.orig | 21 +++++ ci/compile-tests/006-ready-dependee/test.el | 130 +++++++++++++++++++++++++++ 13 files changed, 368 insertions(+) create mode 100644 ci/compile-tests/006-ready-dependee/Makefile create mode 100644 ci/compile-tests/006-ready-dependee/a.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/b.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/c.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/d.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/e.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/f.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/g.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/h.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/i.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/j.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/k.v.orig create mode 100644 ci/compile-tests/006-ready-dependee/test.el diff --git a/ci/compile-tests/006-ready-dependee/Makefile b/ci/compile-tests/006-ready-dependee/Makefile new file mode 100644 index 00000000..fe014bfc --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/Makefile @@ -0,0 +1,28 @@ +# This file is part of Proof General. +# +# © Copyright 2020 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 d.v e.v f.v g.v h.v i.v j.v k.v + +.PHONY: test +test: + $(MAKE) clean + $(MAKE) $(TEST_SOURCES) + emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l test.el -f ert-run-tests-batch-and-exit + +%.v: %.v.orig + cp $< $@ + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux $(TEST_SOURCES) diff --git a/ci/compile-tests/006-ready-dependee/a.v.orig b/ci/compile-tests/006-ready-dependee/a.v.orig new file mode 100644 index 00000000..8e4300e8 --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/a.v.orig @@ -0,0 +1,38 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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 21 *) +Require Export b. +Require Export c. +(* This is line 24 *) + + +(* This is line 27 *) +Definition sum : nat := 9. + + +(* This is line 31 *) +Lemma x : b + c + k = sum. +Proof using. + unfold b, c, k, sum in *. + simpl. + trivial. +Qed. +(* This is line 38 *) diff --git a/ci/compile-tests/006-ready-dependee/b.v.orig b/ci/compile-tests/006-ready-dependee/b.v.orig new file mode 100644 index 00000000..0354f635 --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/b.v.orig @@ -0,0 +1,23 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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 d. + +(* This is line 22 *) +Definition b : nat := 2. diff --git a/ci/compile-tests/006-ready-dependee/c.v.orig b/ci/compile-tests/006-ready-dependee/c.v.orig new file mode 100644 index 00000000..3d2e542c --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/c.v.orig @@ -0,0 +1,23 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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 k. + +(* This is line 22 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/006-ready-dependee/d.v.orig b/ci/compile-tests/006-ready-dependee/d.v.orig new file mode 100644 index 00000000..2f9825cb --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/d.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export e. diff --git a/ci/compile-tests/006-ready-dependee/e.v.orig b/ci/compile-tests/006-ready-dependee/e.v.orig new file mode 100644 index 00000000..0589d31b --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/e.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export f. diff --git a/ci/compile-tests/006-ready-dependee/f.v.orig b/ci/compile-tests/006-ready-dependee/f.v.orig new file mode 100644 index 00000000..32c9287b --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/f.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export g. diff --git a/ci/compile-tests/006-ready-dependee/g.v.orig b/ci/compile-tests/006-ready-dependee/g.v.orig new file mode 100644 index 00000000..73b210c1 --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/g.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export h. diff --git a/ci/compile-tests/006-ready-dependee/h.v.orig b/ci/compile-tests/006-ready-dependee/h.v.orig new file mode 100644 index 00000000..5db2c3ca --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/h.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export i. diff --git a/ci/compile-tests/006-ready-dependee/i.v.orig b/ci/compile-tests/006-ready-dependee/i.v.orig new file mode 100644 index 00000000..09135c38 --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/i.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export j. diff --git a/ci/compile-tests/006-ready-dependee/j.v.orig b/ci/compile-tests/006-ready-dependee/j.v.orig new file mode 100644 index 00000000..62702b4f --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/j.v.orig @@ -0,0 +1,15 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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. + *) + +Require Export k. diff --git a/ci/compile-tests/006-ready-dependee/k.v.orig b/ci/compile-tests/006-ready-dependee/k.v.orig new file mode 100644 index 00000000..7405e2c9 --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/k.v.orig @@ -0,0 +1,21 @@ +(* This file is part of Proof General. + * + * © Copyright 2020 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 20 *) +Definition k : nat := 4. diff --git a/ci/compile-tests/006-ready-dependee/test.el b/ci/compile-tests/006-ready-dependee/test.el new file mode 100644 index 00000000..280c008a --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/test.el @@ -0,0 +1,130 @@ +;; This file is part of Proof General. +;; +;; © Copyright 2020 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 recompilation and ancestor registration for the case a +;; dependency is in state ready already. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a +;; / \ +;; b c +;; | |____________ +;; d \ +;; | | +;; e--f--g--h--i--j--k +;; +;; The idea is that the coqdep chain from b to j takes so long, that k +;; has been compiled and is in state ready before the coqdep results +;; from j are processed. This works - unless the disk cache is cold. +;; If it works the test triggers two bugs. First, k is locked with the +;; require command of c. Second, the modification time of k is not +;; propagated to j, such that the whole chain from j to b is not +;; recompiled after k has changed. + + +;;; set configuration +(cct-configure-proof-general) + +;;; Data and utility functions + +(defconst b-ancestors '("./b.v" "./d.v" "./e.v" "./f.v" "./g.v" + "./h.v" "./i.v" "./j.v" "./k.v") + "Ancestors of b.v.") + +(defconst c-ancestors '("./c.v") + "Ancestors of c.v.") + +(defconst all-ancestors (append b-ancestors c-ancestors) + "All ancestors.") + +(defconst all-compiled-ancestors + (mapcar 'cct-library-vo-of-v-file all-ancestors) + "All vo ancestors files.") + +(defun cct-replace-last-word (line word) + "Replace last word in line LINE with WORD. +In current buffer, go to the end of line LINE and one word +backward. Replace the word there with WORD." + (cct-goto-line line) + (end-of-line) + (backward-word) + (kill-word 1) + (insert word)) + +(defun cct-check-main-buffer (vo-times new-sum recompiled-files + other-locked-files) + "Perform various checks for recompilation in buffer a.v. +Combine all the following tests in this order: +- line 21 in a.v is unlocked +- after replacing the sum on line 28 with NEW-SUM, a.v can be + processed until line 38 +- files in VO-TIMES not listed in RECOMPILED-FILES have the same + last change time as in VO-TIMES +- files in RECOMPILED-FILES have a newer change time +- the spans in line 22 and 23 hold the ancestors of b and c, respectively. +- all the buffers in OTHER-LOCKED-FILES are locked until line 18." + (let (splitted) + (set-buffer "a.v") + (cct-check-locked 21 'unlocked) + (cct-replace-last-word 28 new-sum) + (cct-process-to-line 38) + (cct-check-locked 37 'locked) + (setq splitted (cct-split-change-times vo-times recompiled-files)) + (cct-unmodified-change-times (car splitted)) + (cct-older-change-times (cdr splitted)) + (cct-locked-ancestors 22 b-ancestors) + (cct-locked-ancestors 23 c-ancestors) + (mapc + (lambda (b) + (set-buffer b) + (cct-check-locked 18 'locked)) + other-locked-files))) + + +;;; The test itself + +(ert-deftest cct-change-recompile () + "Test successful recompilation for a dependency in state ready." + ;; :expected-result :failed + ;;(setq coq--debug-auto-compilation t) + (find-file "a.v") + + ;; 1. process original content - compile everything + (message "\n1. process original content - compile everything\n") + (cct-process-to-line 38) + (cct-check-locked 37 'locked) + (cct-locked-ancestors 22 b-ancestors) + (cct-locked-ancestors 23 c-ancestors) + + (let ((vo-times (cct-record-change-times all-compiled-ancestors)) + other-locked-files) + + ;; 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) + (cct-check-main-buffer vo-times "9" nil nil) + + ;; 3. change k and process again - everything should be compiled + (message "\n3. change k and process again - everything should be compiled\n") + (find-file "k.v") + (push "k.v" other-locked-files) + (cct-check-locked 21 'locked) + (cct-replace-last-word 21 "5") + (cct-check-main-buffer + vo-times "10" + '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./g.vo" + "./h.vo" "./i.vo" "./j.v" "./k.v") + other-locked-files) + )) -- cgit v1.2.3