diff options
Diffstat (limited to 'ci/compile-tests/007-slow-require')
26 files changed, 978 insertions, 0 deletions
diff --git a/ci/compile-tests/007-slow-require/Makefile b/ci/compile-tests/007-slow-require/Makefile new file mode 100644 index 00000000..b99eebc1 --- /dev/null +++ b/ci/compile-tests/007-slow-require/Makefile @@ -0,0 +1,35 @@ +# This file is part of Proof General. +# +# © Copyright 2021 Hendrik Tews +# +# Authors: Hendrik Tews +# Maintainer: Hendrik Tews <hendrik@askra.de> +# +# 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:=\ + a1.v b1.v c1.v d1.v \ + a2.v b2.v c2.v d2.v \ + a3.v b3.v c3.v d3.v \ + a4.v b4.v c4.v d4.v \ + a5.v b5.v c5.v d5.v \ + a6.v b6.v c6.v d6.v + +.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/007-slow-require/a1.v.orig b/ci/compile-tests/007-slow-require/a1.v.orig new file mode 100644 index 00000000..6b3e3349 --- /dev/null +++ b/ci/compile-tests/007-slow-require/a1.v.orig @@ -0,0 +1,41 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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 b1. +Require Export (* coqdep-delay 2 *) c1. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) diff --git a/ci/compile-tests/007-slow-require/a2.v.orig b/ci/compile-tests/007-slow-require/a2.v.orig new file mode 100644 index 00000000..60ac1279 --- /dev/null +++ b/ci/compile-tests/007-slow-require/a2.v.orig @@ -0,0 +1,41 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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 b2. +Require Export c2. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) diff --git a/ci/compile-tests/007-slow-require/a3.v.orig b/ci/compile-tests/007-slow-require/a3.v.orig new file mode 100644 index 00000000..8337b2ad --- /dev/null +++ b/ci/compile-tests/007-slow-require/a3.v.orig @@ -0,0 +1,41 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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 2 *) b3. +Require Export c3. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) diff --git a/ci/compile-tests/007-slow-require/a4.v.orig b/ci/compile-tests/007-slow-require/a4.v.orig new file mode 100644 index 00000000..fd5d4b60 --- /dev/null +++ b/ci/compile-tests/007-slow-require/a4.v.orig @@ -0,0 +1,41 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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 b4. +Require Export c4. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) diff --git a/ci/compile-tests/007-slow-require/a5.v.orig b/ci/compile-tests/007-slow-require/a5.v.orig new file mode 100644 index 00000000..b6d7edbb --- /dev/null +++ b/ci/compile-tests/007-slow-require/a5.v.orig @@ -0,0 +1,41 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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 b5. +Require Export c5. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) diff --git a/ci/compile-tests/007-slow-require/a6.v.orig b/ci/compile-tests/007-slow-require/a6.v.orig new file mode 100644 index 00000000..a9bb279f --- /dev/null +++ b/ci/compile-tests/007-slow-require/a6.v.orig @@ -0,0 +1,41 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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 b6. +Require Export c6. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) diff --git a/ci/compile-tests/007-slow-require/b1.v.orig b/ci/compile-tests/007-slow-require/b1.v.orig new file mode 100644 index 00000000..926bed1d --- /dev/null +++ b/ci/compile-tests/007-slow-require/b1.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d1. + +(* This is line 27 *) +Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/b2.v.orig b/ci/compile-tests/007-slow-require/b2.v.orig new file mode 100644 index 00000000..b9cff7ea --- /dev/null +++ b/ci/compile-tests/007-slow-require/b2.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d2. + +(* 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 new file mode 100644 index 00000000..51ab7a2f --- /dev/null +++ b/ci/compile-tests/007-slow-require/b3.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d3. + +(* This is line 27 *) +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 new file mode 100644 index 00000000..fd8d331e --- /dev/null +++ b/ci/compile-tests/007-slow-require/b4.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 2 + * coqc-delay 0 + *) + +Require Export d4. + +(* This is line 27 *) +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 new file mode 100644 index 00000000..3fec38a3 --- /dev/null +++ b/ci/compile-tests/007-slow-require/b5.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d5. + +(* This is line 27 *) +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 new file mode 100644 index 00000000..2b957e6e --- /dev/null +++ b/ci/compile-tests/007-slow-require/b6.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d6. + +(* This is line 27 *) +Definition b : nat := 2. diff --git a/ci/compile-tests/007-slow-require/c1.v.orig b/ci/compile-tests/007-slow-require/c1.v.orig new file mode 100644 index 00000000..9df47c9b --- /dev/null +++ b/ci/compile-tests/007-slow-require/c1.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d1. + +(* This is line 26 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/007-slow-require/c2.v.orig b/ci/compile-tests/007-slow-require/c2.v.orig new file mode 100644 index 00000000..b8db7474 --- /dev/null +++ b/ci/compile-tests/007-slow-require/c2.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 2 + * coqc-delay 0 + *) + +Require Export d2. + +(* This is line 26 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/007-slow-require/c3.v.orig b/ci/compile-tests/007-slow-require/c3.v.orig new file mode 100644 index 00000000..04b225ab --- /dev/null +++ b/ci/compile-tests/007-slow-require/c3.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d3. + +(* This is line 26 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/007-slow-require/c4.v.orig b/ci/compile-tests/007-slow-require/c4.v.orig new file mode 100644 index 00000000..400a8a6c --- /dev/null +++ b/ci/compile-tests/007-slow-require/c4.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d4. + +(* This is line 26 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/007-slow-require/c5.v.orig b/ci/compile-tests/007-slow-require/c5.v.orig new file mode 100644 index 00000000..2fa5a612 --- /dev/null +++ b/ci/compile-tests/007-slow-require/c5.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d5. + +(* This is line 26 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/007-slow-require/c6.v.orig b/ci/compile-tests/007-slow-require/c6.v.orig new file mode 100644 index 00000000..fd0289bf --- /dev/null +++ b/ci/compile-tests/007-slow-require/c6.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 2 + * coqc-delay 0 + *) + +Require Export d6. + +(* This is line 26 *) +Definition c : nat := 3. diff --git a/ci/compile-tests/007-slow-require/d1.v.orig b/ci/compile-tests/007-slow-require/d1.v.orig new file mode 100644 index 00000000..fec95787 --- /dev/null +++ b/ci/compile-tests/007-slow-require/d1.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + + + +(* This is line 26 *) +Definition d : nat := 4. diff --git a/ci/compile-tests/007-slow-require/d2.v.orig b/ci/compile-tests/007-slow-require/d2.v.orig new file mode 100644 index 00000000..fec95787 --- /dev/null +++ b/ci/compile-tests/007-slow-require/d2.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + + + +(* This is line 26 *) +Definition d : nat := 4. diff --git a/ci/compile-tests/007-slow-require/d3.v.orig b/ci/compile-tests/007-slow-require/d3.v.orig new file mode 100644 index 00000000..fec95787 --- /dev/null +++ b/ci/compile-tests/007-slow-require/d3.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + + + +(* This is line 26 *) +Definition d : nat := 4. diff --git a/ci/compile-tests/007-slow-require/d4.v.orig b/ci/compile-tests/007-slow-require/d4.v.orig new file mode 100644 index 00000000..fec95787 --- /dev/null +++ b/ci/compile-tests/007-slow-require/d4.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + + + +(* This is line 26 *) +Definition d : nat := 4. diff --git a/ci/compile-tests/007-slow-require/d5.v.orig b/ci/compile-tests/007-slow-require/d5.v.orig new file mode 100644 index 00000000..d2fae3f6 --- /dev/null +++ b/ci/compile-tests/007-slow-require/d5.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 2 + * coqc-delay 0 + *) + + + +(* This is line 26 *) +Definition d : nat := 4. diff --git a/ci/compile-tests/007-slow-require/d6.v.orig b/ci/compile-tests/007-slow-require/d6.v.orig new file mode 100644 index 00000000..b60d54a6 --- /dev/null +++ b/ci/compile-tests/007-slow-require/d6.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * 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. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay + * coqc-delay 4 + *) + + + +(* This is line 26 *) +Definition d : nat := 4. diff --git a/ci/compile-tests/007-slow-require/runtest.el b/ci/compile-tests/007-slow-require/runtest.el new file mode 100644 index 00000000..52c2f392 --- /dev/null +++ b/ci/compile-tests/007-slow-require/runtest.el @@ -0,0 +1,211 @@ +;; This file is part of Proof General. +;; +;; © Copyright 2021 Hendrik Tews +;; +;; Authors: Hendrik Tews +;; Maintainer: Hendrik Tews <hendrik@askra.de> +;; +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; +;; Coq Compile Tests (cct) -- +;; ert tests for parallel background compilation for Coq +;; +;; Test two require jobs with different delays such that +;; coq-par-retire-top-level-job happens when the other require job is +;; 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. +;; +;; The dependencies are the same in all projects: +;; +;; a +;; / \ +;; b c +;; \ / +;; d +;; +;; Test 1 delays coqdep on require c, such that queue kickoff happens +;; in state 'enqueued-coqdep, the dependency link d->c is created when +;; d is ready and kickoff-queue-maybe on require c happens when +;; require b is in state 'ready. +;; +;; Test 2 delays coqdep on c, such that queue kickoff happens in state +;; 'waiting-dep. +;; +;; Test 3 delays coqdep on require b, such that kickoff-queue-maybe on +;; require c happens when require b is in state 'enqueued-coqdep and +;; queue kickoff happens in state 'waiting-queue. +;; +;; Test 4 delays coqdep on b, such that kickoff-queue-maybe on require +;; c happens when require b is in state 'waiting-dep. +;; +;; Test 5 delays coqdep on d, such that the second dependency on d is +;; created when d is in state enqueued-coqdep. +;; +;; Test 6 delays coqdep on c for 2 seconds and coqc on d for 4 +;; seconds, such that the dependency link d->c is created when d is in +;; state enqueued-coqc. + +;; 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 pre-b-ancestors '("./b" "./d") + "Ancestors of b without suffixes.") + +(defconst pre-c-ancestors '("./c") + "Ancestors of c without suffixes.") + +(defconst pre-all-ancestors (append pre-b-ancestors pre-c-ancestors) + "All ancestors without suffixes.") + +(defun b-ancestors (n) + "Ancestors of b for part N." + (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-b-ancestors)) + +(defun c-ancestors (n) + "Ancestors of c for part N." + (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-c-ancestors)) + +(defun all-ancestors (n) + "All ancestors for part N." + (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-all-ancestors)) + +(defun all-compiled-ancestors (n) + "All vo ancestor files for part N." + (mapcar 'cct-library-vo-of-v-file (all-ancestors n))) + +(defun check-main-buffer (n vo-times new-sum recompiled-files + other-locked-files) + "Perform various checks in buffer aN.v. +See `cct-generic-check-main-buffer'." + (cct-generic-check-main-buffer + (format "a%d.v" n) ; main-buf + 25 ; main-unlocked + 41 ; main-locked + 31 ; main-sum-line + new-sum + vo-times + recompiled-files + `((25 . ,(b-ancestors n)) (26 . ,(c-ancestors n))) ; require-ancestors + other-locked-files + 27 ; other-locked-line + )) + + +;;; Define the test + +(defun test-slow-require (n) + "Test part N of slow require job tests. +XXX Test a setting where the second require job is still in state +'enqueued-coqdep when the first one finishes." + (let* + ;; .v file names are used as file and as buffer names + ((av (format "a%d.v" n)) + (bv (format "b%d.v" n)) + (cv (format "c%d.v" n)) + (dv (format "d%d.v" n)) + ;; .vo names compared with ancestors, they need a "./" prefix + (bvo (concat "./" (cct-library-vo-of-v-file bv))) + (cvo (concat "./" (cct-library-vo-of-v-file cv))) + (dvo (concat "./" (cct-library-vo-of-v-file dv))) + vo-times other-locked-files) + + ;; (setq cct--debug-tests t) + ;; (setq coq--debug-auto-compilation t) + (find-file av) + (message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s" + coq-dependency-analyzer + coq-compiler + (getenv "PATH") + exec-path) + + ;; 1. process original content - compile everything + (message "\n%d.1. process original content - compile everything\n" n) + ;;(setq coq--debug-auto-compilation t) + (cct-process-to-line 42) + (cct-check-locked 41 'locked) + (cct-locked-ancestors 25 (b-ancestors n)) + (cct-locked-ancestors 26 (c-ancestors n)) + + ;; (cl-assert nil nil "exit") + + (setq vo-times (cct-record-change-times (all-compiled-ancestors n))) + ;; 2. retract and process again - nothing should be compiled + (message "\n%d.2. retract and process again - nothing should be compiled\n" + n) + (cct-process-to-line 24) + (check-main-buffer n vo-times "9" nil nil) + + ;; 3. change d and process again - b and c should be compiled + (message "\n%d.3. change d and process again - b and c should be compiled\n" + n) + (find-file dv) + (push dv other-locked-files) + (cct-check-locked 23 'locked) + (cct-replace-last-word 27 "5") + (check-main-buffer n vo-times "10" (list bvo cvo dvo) + other-locked-files) + + ;; 4. change b and process again - only b should be compiled + (message "\n%d.4. change b and process again - only b should be compiled\n" + n) + (setq vo-times (cct-record-change-times (all-compiled-ancestors n))) + (find-file bv) + (push bv other-locked-files) + (cct-check-locked 23 'locked) + (cct-replace-last-word 27 "4") + (check-main-buffer n vo-times "12" (list bvo) other-locked-files) + + ;; 5. change c and process again - only c should be compiled + (message "\n%d.5. change c and process again - only c should be compiled\n" + n) + (setq vo-times (cct-record-change-times (all-compiled-ancestors n))) + (find-file cv) + (push cv other-locked-files) + (cct-check-locked 23 'locked) + (cct-replace-last-word 27 "8") + (check-main-buffer n vo-times "17" (list cvo) other-locked-files) + + ;; 6. delete d and process again - b and c should be compiled + (message "\n%d.6. delete d and process again - b and c should be compiled\n" + n) + (setq vo-times (cct-record-change-times (all-compiled-ancestors n))) + (delete-file dvo) + (set-buffer av) + (cct-process-to-line 24) + (check-main-buffer n vo-times "17" (list bvo cvo dvo) + other-locked-files) + + ;; 7. delete b and process again - only b should be compiled + (message "\n%d.7. delete b and process again - only b should be compiled\n" + n) + (setq vo-times (cct-record-change-times (all-compiled-ancestors n))) + (delete-file bvo) + (set-buffer av) + (cct-process-to-line 24) + (check-main-buffer n vo-times "17" (list bvo) other-locked-files) + + ;; 8. delete c and process again - only c should be compiled + (message "\n%d.8. delete c and process again - only c should be compiled\n" + n) + (setq vo-times (cct-record-change-times (all-compiled-ancestors n))) + (delete-file cvo) + (set-buffer av) + (cct-process-to-line 24) + (check-main-buffer n vo-times "17" (list cvo) other-locked-files) + )) + + +(ert-deftest cct-slow-require-1 () (test-slow-require 1)) +(ert-deftest cct-slow-require-2 () (test-slow-require 2)) +(ert-deftest cct-slow-require-3 () (test-slow-require 3)) +(ert-deftest cct-slow-require-4 () (test-slow-require 4)) +(ert-deftest cct-slow-require-5 () (test-slow-require 5)) +(ert-deftest cct-slow-require-6 () (test-slow-require 6)) |