diff options
Diffstat (limited to 'test-suite')
26 files changed, 467 insertions, 32 deletions
diff --git a/test-suite/bugs/closed/bug_11114.v b/test-suite/bugs/closed/bug_11114.v new file mode 100644 index 0000000000..dd981279db --- /dev/null +++ b/test-suite/bugs/closed/bug_11114.v @@ -0,0 +1,17 @@ +Require Extraction. + +Inductive t (sig: list nat) := +| T (k: nat). + +Record pkg := + { _sig: list nat; + _t : t _sig }. + +Definition map (f: nat -> nat) (p: pkg) := + {| _sig := p.(_sig); + _t := match p.(_t) with + | T _ k => T p.(_sig) (f k) + end |}. + +Extraction Implicit Build_pkg [_sig]. +Extraction TestCompile map. diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v new file mode 100644 index 0000000000..bb43edbe74 --- /dev/null +++ b/test-suite/bugs/closed/bug_9517.v @@ -0,0 +1,19 @@ +Declare Custom Entry expr. +Declare Custom Entry stmt. +Notation "x" := x (in custom stmt, x ident). +Notation "x" := x (in custom expr, x ident). + +Notation "1" := 1 (in custom expr). + +Notation "! x = y !" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr). +Notation "? x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr). +Notation "x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr). + +Notation "stmt:( s )" := s (s custom stmt). +Check stmt:(! _ = _ !). +Check stmt:(? _ = _). +Check stmt:(_ = _). +Check stmt:(! 1 = 1 !). +Check stmt:(? 1 = 1). +Check stmt:(1 = 1). +Check stmt:(_ = 1). diff --git a/test-suite/bugs/closed/bug_9521.v b/test-suite/bugs/closed/bug_9521.v new file mode 100644 index 0000000000..0464c62c09 --- /dev/null +++ b/test-suite/bugs/closed/bug_9521.v @@ -0,0 +1,23 @@ +(* Example from #9521 *) + +Module A. + +Declare Custom Entry expr. +Notation "expr0:( s )" := s (s custom expr at level 0). +Notation "#" := 0 (in custom expr at level 1). +Check expr0:(#). (* Should not be an anomaly "unknown level 0" *) + +End A. + +(* Another example from a comment at #11561 *) + +Module B. + +Declare Custom Entry special. +Declare Custom Entry expr. +Notation "## x" := (S x) (in custom expr at level 10, x custom special at level 10). +Notation "[ e ]" := e (e custom expr at level 10). +Notation "1" := 1 (in custom special). +Check [ ## 1 ]. + +End B. diff --git a/test-suite/bugs/closed/bug_9640.v b/test-suite/bugs/closed/bug_9640.v new file mode 100644 index 0000000000..4dc0bead7b --- /dev/null +++ b/test-suite/bugs/closed/bug_9640.v @@ -0,0 +1,23 @@ +(* Similar to #9521 (was an anomaly unknown level 150 *) + +Module A. + +Declare Custom Entry expr. +Notation "p" := (p) (in custom expr at level 150, p constr, right associativity). +Notation "** X" := (X) (at level 200, X custom expr at level 150). +Lemma t : ** True. +Abort. + +End A. + +(* Similar to #9517, #9519, #11331 *) + +Module B. + +Declare Custom Entry expr. +Notation "p" := (p) (in custom expr at level 100, p constr (* at level 200 *)). +Notation "** X" := (X) (at level 200, X custom expr at level 150). +Lemma t : ** True. +Abort. + +End B. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh index 4a50759bdb..a6f35db17c 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh @@ -5,6 +5,10 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log +"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-user.log -diff -u time-of-build-both.log.expected time-of-build-both.log || exit $? +diff -u time-of-build-both-user.log.expected time-of-build-both-user.log || exit $? + +"$COQLIB"/tools/make-both-time-files.py --real time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-real.log + +diff -u time-of-build-both-real.log.expected time-of-build-both-real.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected new file mode 100644 index 0000000000..ea600b000e --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected @@ -0,0 +1,26 @@ +After | File Name | Before || Change | % Change +---------------------------------------------------------------------------------------------- +20m46.07s | Total | 23m06.30s || -2m20.23s | -10.11% +---------------------------------------------------------------------------------------------- +4m16.77s | Specific/X25519/C64/ladderstep | 5m16.83s || -1m00.06s | -18.95% +3m01.77s | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s || -0m26.16s | -12.58% +2m35.79s | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s || -0m23.42s | -13.06% +3m22.96s | Specific/NISTP256/AMD64/femul | 3m37.80s || -0m14.84s | -6.81% +0m39.72s | Specific/X25519/C64/femul | 0m42.98s || -0m03.25s | -7.58% +0m38.19s | Specific/NISTP256/AMD64/feadd | 0m40.48s || -0m02.28s | -5.65% +0m34.35s | Specific/X25519/C64/freeze | 0m36.42s || -0m02.07s | -5.68% +0m33.08s | Specific/X25519/C64/fesquare | 0m35.23s || -0m02.14s | -6.10% +0m31.00s | Specific/NISTP256/AMD64/feopp | 0m32.08s || -0m01.07s | -3.36% +0m27.81s | Specific/NISTP256/AMD64/fenz | 0m28.91s || -0m01.10s | -3.80% +0m27.11s | Specific/X25519/C64/fecarry | 0m28.85s || -0m01.74s | -6.03% +0m24.71s | Specific/X25519/C64/fesub | 0m26.11s || -0m01.39s | -5.36% +0m49.44s | Specific/solinas32_2e255m765_13limbs/Synthesis | 0m49.50s || -0m00.06s | -0.12% +0m43.34s | Specific/NISTP256/AMD64/fesub | 0m43.78s || -0m00.43s | -1.00% +0m40.13s | Specific/solinas32_2e255m765_12limbs/Synthesis | 0m39.53s || +0m00.60s | +1.51% +0m22.81s | Specific/X25519/C64/feadd | 0m23.43s || -0m00.62s | -2.64% +0m13.45s | Specific/NISTP256/AMD64/Synthesis | 0m13.74s || -0m00.29s | -2.11% +0m11.15s | Specific/X25519/C64/Synthesis | 0m11.23s || -0m00.08s | -0.71% +0m07.33s | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s || -0m00.07s | -0.94% +0m01.93s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s || +0m00.19s | +11.56% +0m01.85s | Specific/Framework/SynthesisFramework | 0m01.95s || -0m00.09s | -5.12% +0m01.38s | Compilers/Z/Bounds/Pipeline | 0m01.18s || +0m00.19s | +16.94%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected index 159e645512..159e645512 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh index 4f39b3ce7e..d4614749e7 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh @@ -5,6 +5,10 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-user.log -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? +diff -u time-of-build-pretty-user.log.expected time-of-build-pretty-user.log || exit $? + +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-real.log + +diff -u time-of-build-pretty-real.log.expected time-of-build-pretty-real.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected index b9739ddb1d..b9739ddb1d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected new file mode 100644 index 0000000000..b9739ddb1d --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected @@ -0,0 +1,26 @@ +Time | File Name +---------------------------------------------------------- +19m16.04s | Total +---------------------------------------------------------- +4m01.34s | Specific/X25519/C64/ladderstep +3m09.62s | Specific/NISTP256/AMD64/femul +2m48.52s | Specific/solinas32_2e255m765_13limbs/femul +2m23.70s | Specific/solinas32_2e255m765_12limbs/femul +0m45.75s | Specific/solinas32_2e255m765_13limbs/Synthesis +0m39.59s | Specific/NISTP256/AMD64/fesub +0m36.92s | Specific/solinas32_2e255m765_12limbs/Synthesis +0m36.32s | Specific/X25519/C64/femul +0m35.40s | Specific/NISTP256/AMD64/feadd +0m31.50s | Specific/X25519/C64/freeze +0m30.13s | Specific/X25519/C64/fesquare +0m28.51s | Specific/NISTP256/AMD64/feopp +0m25.50s | Specific/NISTP256/AMD64/fenz +0m24.99s | Specific/X25519/C64/fecarry +0m22.65s | Specific/X25519/C64/fesub +0m20.93s | Specific/X25519/C64/feadd +0m12.55s | Specific/NISTP256/AMD64/Synthesis +0m10.37s | Specific/X25519/C64/Synthesis +0m07.18s | Compilers/Z/Bounds/Pipeline/Definition +0m01.72s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics +0m01.67s | Specific/Framework/SynthesisFramework +0m01.19s | Compilers/Z/Bounds/Pipeline
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected new file mode 100644 index 0000000000..726c19a2e2 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected @@ -0,0 +1,29 @@ +After | Code | Before || Change | % Change +----------------------------------------------------------------------------------------------------------- +0m01.23s | Total | 0m01.28s || -0m00.04s | -3.50% +----------------------------------------------------------------------------------------------------------- +0m00.53s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).] | 0m00.566s || -0m00.03s | -6.36% +0m00.4s | Chars 285-289 ~ 305-309 [Qed.] | 0m00.411s || -0m00.01s | -2.67% +0m00.194s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.192s || +0m00.00s | +1.04% +0m00.114s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.] | 0m00.114s || +0m00.00s | +0.00% +0m00.s | Chars 065-075 ~ 065-075 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 078-086 ~ 078-086 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 078-090 ~ 078-090 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 087-091 ~ 091-095 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 092-102 ~ 096-106 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 105-113 ~ 109-117 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 105-117 ~ 109-121 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 114-118 ~ 122-126 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 119-129 ~ 127-137 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 132-140 ~ 140-148 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 132-144 ~ 140-152 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 141-145 ~ 153-157 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 146-156 ~ 158-168 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 159-167 ~ 171-179 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 159-171 ~ 171-183 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 168-172 ~ 184-188 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected new file mode 100644 index 0000000000..f6be1d936d --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected @@ -0,0 +1,29 @@ +After | Code | Before || Change | % Change +----------------------------------------------------------------------------------------------------------- +0m01.14s | Total | 0m01.15s || -0m00.00s | -0.77% +----------------------------------------------------------------------------------------------------------- +0m00.504s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).] | 0m00.528s || -0m00.02s | -4.54% +0m00.384s | Chars 285-289 ~ 305-309 [Qed.] | 0m00.4s || -0m00.01s | -4.00% +0m00.172s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.156s || +0m00.01s | +10.25% +0m00.083s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.] | 0m00.072s || +0m00.01s | +15.27% +0m00.004s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | ∞ +0m00.s | Chars 065-075 ~ 065-075 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 078-086 ~ 078-086 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 078-090 ~ 078-090 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 087-091 ~ 091-095 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 092-102 ~ 096-106 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 105-113 ~ 109-117 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 105-117 ~ 109-121 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 114-118 ~ 122-126 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 119-129 ~ 127-137 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 132-140 ~ 140-148 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 132-144 ~ 140-152 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 141-145 ~ 153-157 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 146-156 ~ 158-168 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 159-167 ~ 171-179 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 159-171 ~ 171-183 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 168-172 ~ 184-188 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in new file mode 100644 index 0000000000..c58e7d82d1 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in @@ -0,0 +1,20 @@ +Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.083u,0.032s) +Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.194 secs (0.172u,0.023s) +Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 78 - 86 [exact~I.] 0. secs (0.u,0.s) +Chars 87 - 91 [Qed.] 0. secs (0.u,0.s) +Chars 92 - 102 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 105 - 113 [exact~I.] 0. secs (0.u,0.s) +Chars 114 - 118 [Qed.] 0. secs (0.u,0.s) +Chars 119 - 129 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 132 - 140 [exact~I.] 0. secs (0.u,0.s) +Chars 141 - 145 [Qed.] 0. secs (0.u,0.s) +Chars 146 - 156 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 159 - 167 [exact~I.] 0. secs (0.u,0.s) +Chars 168 - 172 [Qed.] 0. secs (0.u,0.s) +Chars 173 - 183 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 186 - 194 [exact~I.] 0. secs (0.u,0.s) +Chars 195 - 199 [Qed.] 0. secs (0.u,0.s) +Chars 200 - 257 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.004u,0.s) +Chars 260 - 284 [(vm_compute;~reflexivity).] 0.53 secs (0.504u,0.024s) +Chars 285 - 289 [Qed.] 0.4 secs (0.384u,0.016s) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in new file mode 100644 index 0000000000..b49c1b1cb7 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in @@ -0,0 +1,20 @@ +Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.072u,0.044s) +Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.192 secs (0.156u,0.035s) +Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 78 - 90 [constructor.] 0. secs (0.u,0.s) +Chars 91 - 95 [Qed.] 0. secs (0.u,0.s) +Chars 96 - 106 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 109 - 121 [constructor.] 0. secs (0.u,0.s) +Chars 122 - 126 [Qed.] 0. secs (0.u,0.s) +Chars 127 - 137 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 140 - 152 [constructor.] 0. secs (0.u,0.004s) +Chars 153 - 157 [Qed.] 0. secs (0.u,0.s) +Chars 158 - 168 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 171 - 183 [constructor.] 0. secs (0.u,0.s) +Chars 184 - 188 [Qed.] 0. secs (0.u,0.s) +Chars 189 - 199 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 202 - 214 [constructor.] 0. secs (0.u,0.s) +Chars 215 - 219 [Qed.] 0. secs (0.u,0.s) +Chars 220 - 277 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.u,0.s) +Chars 280 - 304 [(vm_compute;~reflexivity).] 0.566 secs (0.528u,0.039s) +Chars 305 - 309 [Qed.] 0.411 secs (0.4u,0.008s) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v new file mode 100644 index 0000000000..7141065b52 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v @@ -0,0 +1,20 @@ +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5. + vm_compute; reflexivity. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v new file mode 100644 index 0000000000..e152689ee4 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v @@ -0,0 +1,20 @@ +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5. + vm_compute; reflexivity. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh new file mode 100755 index 0000000000..980bf9cf01 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 foo.v.after-timing.in foo.v.before-timing.in foo-real.v.timing.diff || exit $? + +diff -u foo-real.v.timing.diff.expected foo-real.v.timing.diff || exit $? + +"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 --user foo.v.after-timing.in foo.v.before-timing.in foo-user.v.timing.diff || exit $? + +diff -u foo-user.v.timing.diff.expected foo-user.v.timing.diff || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index cfacf738a3..4b5acb9168 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -10,3 +10,4 @@ export COQLIB ./001-correct-diff-sorting-order/run.sh ./002-single-file-sorting/run.sh ./003-non-utf8/run.sh +./004-per-file-fuzz/run.sh diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 5f22eb5d7c..ef7667936c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -1,4 +1,4 @@ -compose (C:=nat) S +compose S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) @@ -12,3 +12,8 @@ map id' (1 :: nil) : list nat map (id'' (A:=nat)) (1 :: nil) : list nat +fix f (x : nat) : option nat := match x with + | 0 => None + | S _ => x + end + : nat -> option nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 306532c0df..a7c4399e38 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x. Check map (@id'' nat) (1::nil). +Module MatchBranchesInContext. + +Set Implicit Arguments. +Set Contextual Implicit. + +Inductive option A := None | Some (a:A). +Coercion some_nat := @Some nat. +Check fix f x := match x with 0 => None | n => some_nat n end. + +End MatchBranchesInContext. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f65696e464..e121b5e86c 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -71,3 +71,39 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". +Entry constr:expr is +[ "201" RIGHTA + [ "{"; constr:operconstr LEVEL "200"; "}" ] ] + +fun x : nat => [ x ] + : nat -> nat +fun x : nat => [x] + : nat -> nat +∀ x : nat, x = x + : Prop +File "stdin", line 219, characters 0-160: +Warning: Notation "∀ _ .. _ , _" was already defined with a different format +in scope type_scope. [notation-incompatible-format,parsing] +∀x : nat,x = x + : Prop +File "stdin", line 232, characters 0-60: +Warning: Notation "_ %%% _" was already defined with a different format. +[notation-incompatible-format,parsing] +File "stdin", line 236, characters 0-64: +Warning: Notation "_ %%% _" was already defined with a different format. +[notation-incompatible-format,parsing] +File "stdin", line 241, characters 0-62: +Warning: Lonely notation "_ %%%% _" was already defined with a different +format. [notation-incompatible-format,parsing] +3 %% 4 + : nat +3 %% 4 + : nat +3 %% 4 + : nat +File "stdin", line 269, characters 0-61: +Warning: The format modifier is irrelevant for only parsing rules. +[irrelevant-format-only-parsing,parsing] +File "stdin", line 273, characters 0-63: +Warning: The only parsing modifier has no effect in Reserved Notation. +[irrelevant-reserved-notation-only-parsing,parsing] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4de6ce19b4..1cf0d919b1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -184,3 +184,92 @@ Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). End M. + +Module Bug11331. + +Declare Custom Entry expr. +Notation "{ p }" := (p) (in custom expr at level 201, p constr). +Print Custom Grammar expr. + +End Bug11331. + +Module Bug_6082. + +Declare Scope foo. +Notation "[ x ]" := (S x) (format "[ x ]") : foo. +Open Scope foo. +Check fun x => S x. + +Declare Scope bar. +Notation "[ x ]" := (S x) (format "[ x ]") : bar. +Open Scope bar. + +Check fun x => S x. + +End Bug_6082. + +Module Bug_7766. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' ∀ x .. y ']' , P") : type_scope. + +Check forall (x : nat), x = x. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "∀ x .. y , P") : type_scope. + +Check forall (x : nat), x = x. + +End Bug_7766. + +Module N. + +(* Other tests about generic and specific formats *) + +Reserved Notation "x %%% y" (format "x %%% y", at level 35). +Reserved Notation "x %%% y" (format "x %%% y", at level 35). + +(* Not using the reserved format, we warn *) + +Notation "x %%% y" := (x+y) (format "x %%% y", at level 35). + +(* Same scope (here lonely): we warn *) + +Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35). +Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35). + +(* Test if the format for a specific notation becomes the default + generic format or if the generic format, in the absence of a + Reserved Notation, is the one canonically obtained from the + notation *) + +Declare Scope foo_scope. +Declare Scope bar_scope. +Declare Scope bar'_scope. +Notation "x %% y" := (x+y) (at level 47, format "x %% y") : foo_scope. +Open Scope foo_scope. +Check 3 %% 4. + +(* No scope, we inherit the initial format *) + +Notation "x %% y" := (x*y) : bar_scope. (* Inherit the format *) +Open Scope bar_scope. +Check 3 %% 4. + +(* Different scope and no reserved notation, we don't warn *) + +Notation "x %% y" := (x*y) (at level 47, format "x %% y") : bar'_scope. +Open Scope bar'_scope. +Check 3 %% 4. + +(* Warn for combination of "only parsing" and "format" *) + +Notation "###" := 0 (at level 0, only parsing, format "###"). + +(* In reserved notation, warn only for the "only parsing" *) + +Reserved Notation "##" (at level 0, only parsing, format "##"). + +End N. diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index 83dd2f40fb..c5b4d6f291 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -6,13 +6,13 @@ where ?B : [ |- Type] p 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b -p 0 0 (B:=bool) +p 0 0 : forall b : bool, 0 = 0 /\ b = b -p 0 0 (B:=bool) +p 0 0 : forall b : bool, 0 = 0 /\ b = b -p (A:=nat) +p : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b -p (A:=nat) +p : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b @p nat 0 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b @@ -44,16 +44,16 @@ p : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b f x true : 0 = 0 /\ true = true -f x (B:=bool) +f x : forall b : bool, 0 = 0 /\ b = b -f x (B:=bool) +f x : forall b : bool, 0 = 0 /\ b = b @f nat : forall a1 a2 : nat, T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b @f : forall (A : Type) (a1 a2 : A), @@ -62,16 +62,16 @@ f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b x.(f) true : 0 = 0 /\ true = true -x.(f) (B:=bool) +x.(f) : forall b : bool, 0 = 0 /\ b = b -x.(f) (B:=bool) +x.(f) : forall b : bool, 0 = 0 /\ b = b @f nat : forall a1 a2 : nat, T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b @f : forall (A : Type) (a1 a2 : A), @@ -218,7 +218,7 @@ p 0 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -p 0 0 (B:=bool) +p 0 0 : forall b : bool, 0 = 0 /\ b = b p 0 0 true : 0 = 0 /\ true = true diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 505dc52ebe..113384e9cf 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -75,7 +75,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". -File "stdin", line 202, characters 2-72: +File "stdin", line 203, characters 2-72: Warning: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index c306b15ef3..22aff36d67 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -123,6 +123,7 @@ Module Test6. Export Scopes. Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). End Notations. + Set Printing Coercions. Check let v := 0%wnat in v : wnat. Check wrap O. Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 651247937d..e2b4694fff 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,23 +1,22 @@ -Module Att. - #[uniform] Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. - Check (list : Type -> Type). - Check (cons : forall A, A -> list A -> list A). -End Att. - Set Uniform Inductive Parameters. Inductive list (A : Type) := -| nil : list -| cons : A -> list -> list. + | nil : list + | cons : A -> list -> list. Check (list : Type -> Type). Check (cons : forall A, A -> list A -> list A). Inductive list2 (A : Type) (A' := prod A A) := -| nil2 : list2 -| cons2 : A' -> list2 -> list2. + | nil2 : list2 + | cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). -#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). +Inductive list3 | A := nil3 | cons3 : A -> list3 (A * A)%type -> list3 A. + +Unset Uniform Inductive Parameters. + +Inductive list4 A | := nil4 | cons4 : A -> list4 -> list4. + +Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. |