diff options
Diffstat (limited to 'test-suite')
46 files changed, 265 insertions, 136 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache.test-suite Binary files differindex 046cb067c5..046cb067c5 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache.test-suite diff --git a/test-suite/Makefile b/test-suite/Makefile index dece21885c..d4ad438d61 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -115,12 +115,13 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ coqdoc ssr primitive/uint63 primitive/float ltac2 # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS) -PREREQUISITELOG = prerequisite/admit.v.log \ - prerequisite/make_local.v.log prerequisite/make_notation.v.log \ - prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \ - prerequisite/module_bug7192.v.log +.csdp.cache: .csdp.cache.test-suite + cp $< $@ + chmod u+w $@ + +PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) .csdp.cache ####################################################################### # Phony targets @@ -191,6 +192,7 @@ summary: $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ + $(call summary_dir, "Output tests with coqchk", output-coqchk); \ $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ @@ -284,8 +286,8 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) # ML files from unit-test framework, not containing tests -UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) -UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) +UNIT_SRCFILES:=$(shell find ./unit-tests/src -name '*.ml') +UNIT_ALLMLFILES:=$(shell find ./unit-tests -name '*.ml') UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) @@ -315,11 +317,6 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test -unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK) - $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \ - -I unit-tests/src $(UNIT_LINK) $< -o $<.test; - $(HIDE)./$<.test ####################################################################### # Other generic tests @@ -466,6 +463,43 @@ $(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISI fi; \ } > "$@" +output-coqchk: $(addsuffix .log,$(wildcard output-coqchk/*.v)) +$(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ + echo $(call log_intro,$<); \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ + fi; \ + } > "$@" + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ + echo $(call log_intro,$<); \ + output=$*.out.real; \ + export LC_CTYPE=C; \ + export LANG=C; \ + $(coqchk) -o -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1 \ + | sed 's/File "[^"]*"/File "stdin"/' \ + > $$output; \ + diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + rm $$output; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ + fi; \ + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi + .PHONY: approve-output approve-output: output output-coqtop $(HIDE)for f in output/*.out.real; do \ @@ -478,6 +512,7 @@ approve-output: output output-coqtop output/MExtraction.out: ../plugins/micromega/micromega.ml $(SHOW) GEN $@ $(HIDE) cp $< $@ + $(HIDE) chmod u+w $@ $(HIDE) echo >> $@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out diff --git a/test-suite/bugs/closed/bug_12233.v b/test-suite/bugs/closed/bug_12233.v new file mode 100644 index 0000000000..3cbf084594 --- /dev/null +++ b/test-suite/bugs/closed/bug_12233.v @@ -0,0 +1,5 @@ +Theorem thm (A:Prop) (H:exists m:nat, True) : True. +destruct H as ([|],?). +assert A. +Show Proof. (* was raising Not_found since 8.7 *) +Abort. diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 30be5e6456..ab89e12592 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -9,10 +9,18 @@ cd _test || exit 1 mkdir -p src mkdir -p theories/sub -cp ../../template/theories/sub/testsub.v theories/sub -cp ../../template/theories/test.v theories -cp ../../template/src/test.mlg src -cp ../../template/src/test_aux.mli src -cp ../../template/src/test.mli src -cp ../../template/src/test_plugin.mlpack src -cp ../../template/src/test_aux.ml src +cp_file() { + local _TARGET=$1 + cp ../../template/$_TARGET $_TARGET + chmod u+w $_TARGET +} + +# We chmod +w as to fix the case where the sources are read-only, as +# for example when using Dune's cache. +cp_file theories/sub/testsub.v +cp_file theories/test.v +cp_file src/test.mlg +cp_file src/test_aux.mli +cp_file src/test.mli +cp_file src/test_plugin.mlpack +cp_file src/test_aux.ml diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 541b307b5e..85aeab2c69 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -3,4 +3,4 @@ 0m00.47s | 394716 ko | Total Time / Peak Mem | 0m00.45s | 394392 ko || +0m00.01s || 324 ko | +4.44% | +0.08% ----------------------------------------------------------------------------------------------------------------------------- 0m00.42s | 394716 ko | Fast.vo | 0m00.02s | 57164 ko || +0m00.40s || 337552 ko | +1999.99% | +590.49% -0m00.05s | 57124 ko | Slow.vo | 0m00.43s | 394392 ko || -0m00.38s || -337268 ko | -88.37% | -85.51%
\ No newline at end of file +0m00.05s | 57124 ko | Slow.vo | 0m00.43s | 394392 ko || -0m00.38s || -337268 ko | -88.37% | -85.51% diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired index 71e4ee0b32..ed5454b480 100644 --- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -1,9 +1,9 @@ After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- - 0m14.06s | Total | 0m00.72s || +0m13.34s | +1854.02% + 0m15.00s | Total | 0m00.72s || +0m14.28s | +1983.61% ---------------------------------------------------------------------------------------------------- -0m13.582s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.353s || +0m13.22s | +3747.59% -0m00.335s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.225s || +0m00.11s | +48.88% -0m00.152s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.142s || +0m00.01s | +7.04% +0m14.578s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.356s || +0m14.22s | +3994.94% +0m00.284s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.225s || +0m00.05s | +26.22% + 0m00.14s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.139s || +0m00.00s | +0.71% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected index e7d289858b..948e28fbc6 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected index 36f86e0e1e..ea36822c8d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected index 6415223693..b6c21a3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected @@ -23,4 +23,4 @@ 3m22.96s | 3302508 ko | Specific/NISTP256/AMD64/femul | 3m37.80s | 3307052 ko || -0m14.84s || -4544 ko | -6.81% | -0.13% 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09% 3m01.77s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s | 1656912 ko || -0m26.16s || -67396 ko | -12.58% | -4.06% - 4m16.77s | 1617000 ko | Specific/X25519/C64/ladderstep | 5m16.83s | 1621500 ko || -1m00.06s || -4500 ko | -18.95% | -0.27%
\ No newline at end of file + 4m16.77s | 1617000 ko | Specific/X25519/C64/ladderstep | 5m16.83s | 1621500 ko || -1m00.06s || -4500 ko | -18.95% | -0.27% 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 index 36f86e0e1e..ea36822c8d 100644 --- 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 @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected index 84d20f484a..a964c29da8 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected index 7576dca88b..59af8c3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected index 1173a6fe29..5ee974c9f3 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected @@ -23,4 +23,4 @@ 3m09.62s | 3302508 ko | Specific/NISTP256/AMD64/femul | 3m22.52s | 3307052 ko || -0m12.90s || -4544 ko | -6.36% | -0.13% 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09% 2m48.52s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s | 1656912 ko || -0m24.42s || -67396 ko | -12.66% | -4.06% - 4m01.34s | 1617000 ko | Specific/X25519/C64/ladderstep | 4m59.49s | 1621500 ko || -0m58.15s || -4500 ko | -19.41% | -0.27%
\ No newline at end of file + 4m01.34s | 1617000 ko | Specific/X25519/C64/ladderstep | 4m59.49s | 1621500 ko || -0m58.15s || -4500 ko | -19.41% | -0.27% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected index 7576dca88b..59af8c3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected index 94122d8190..317497c68a 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline 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 index 94122d8190..317497c68a 100644 --- 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 @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected index 6104c78380..ee9fca7eb4 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected @@ -304,4 +304,4 @@ 0m00.04s | 54440 ko | bedrock2/deps/coqutil/src/dlet 0m00.04s | 54804 ko | bedrock2/deps/coqutil/src/sanity 0m00.04s | 56096 ko | bedrock2/deps/riscv-coq/src/Utility/MMIOTrace - 0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal
\ No newline at end of file + 0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal 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 index 76b0a35cb2..37f144b19b 100644 --- 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 @@ -26,4 +26,4 @@ 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 + 0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A 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 index 1e27d5d12b..a77215b67d 100644 --- 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 @@ -26,4 +26,4 @@ 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 + 0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected index 2a2d2c1b2f..9d6231f2ce 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected @@ -23,4 +23,4 @@ 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected index 7e4cfaec1c..4864c1aaf7 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected @@ -23,4 +23,4 @@ 0m27.81s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m28.91s | 756216 ko || -0m01.10s || -136 ko | -3.80% | -0.01% 0m22.81s | 766300 ko | Specific/X25519/C64/feadd | 0m23.43s | 766168 ko || -0m00.62s || 132 ko | -2.64% | +0.01% 0m11.15s | 687760 ko | Specific/X25519/C64/Synthesis | 0m11.23s | 687812 ko || -0m00.08s || -52 ko | -0.71% | -0.00% - 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00%
\ No newline at end of file + 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected index 7842f91f1f..27d3a9c683 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected @@ -23,4 +23,4 @@ 0m43.34s | 793376 ko | Specific/NISTP256/AMD64/fesub | 0m43.78s | 799668 ko || -0m00.43s || -6292 ko | -1.00% | -0.78% 0m39.72s | 825448 ko | Specific/X25519/C64/femul | 0m42.98s | 839624 ko || -0m03.25s || -14176 ko | -7.58% | -1.68% 3m01.77s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s | 1656912 ko || -0m26.16s || -67396 ko | -12.58% | -4.06% - 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09%
\ No newline at end of file + 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected index 7e4cfaec1c..4864c1aaf7 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected @@ -23,4 +23,4 @@ 0m27.81s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m28.91s | 756216 ko || -0m01.10s || -136 ko | -3.80% | -0.01% 0m22.81s | 766300 ko | Specific/X25519/C64/feadd | 0m23.43s | 766168 ko || -0m00.62s || 132 ko | -2.64% | +0.01% 0m11.15s | 687760 ko | Specific/X25519/C64/Synthesis | 0m11.23s | 687812 ko || -0m00.08s || -52 ko | -0.71% | -0.00% - 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00%
\ No newline at end of file + 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected index ea116a804f..48e168657c 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected @@ -23,4 +23,4 @@ 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected index 128f140662..fc26998b8f 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected @@ -23,4 +23,4 @@ 0m25.50s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m26.41s | 756216 ko || -0m00.91s || -136 ko | -3.44% | -0.01% 0m20.93s | 766300 ko | Specific/X25519/C64/feadd | 0m21.41s | 766168 ko || -0m00.48s || 132 ko | -2.24% | +0.01% 0m10.37s | 687760 ko | Specific/X25519/C64/Synthesis | 0m10.30s | 687812 ko || +0m00.06s || -52 ko | +0.67% | -0.00% - 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00%
\ No newline at end of file + 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected index 79dc49892f..1fcdb84025 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected @@ -23,4 +23,4 @@ 0m39.59s | 793376 ko | Specific/NISTP256/AMD64/fesub | 0m40.09s | 799668 ko || -0m00.50s || -6292 ko | -1.24% | -0.78% 0m36.32s | 825448 ko | Specific/X25519/C64/femul | 0m39.50s | 839624 ko || -0m03.17s || -14176 ko | -8.05% | -1.68% 2m48.52s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s | 1656912 ko || -0m24.42s || -67396 ko | -12.66% | -4.06% - 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09%
\ No newline at end of file + 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected index 128f140662..fc26998b8f 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected @@ -23,4 +23,4 @@ 0m25.50s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m26.41s | 756216 ko || -0m00.91s || -136 ko | -3.44% | -0.01% 0m20.93s | 766300 ko | Specific/X25519/C64/feadd | 0m21.41s | 766168 ko || -0m00.48s || 132 ko | -2.24% | +0.01% 0m10.37s | 687760 ko | Specific/X25519/C64/Synthesis | 0m10.30s | 687812 ko || +0m00.06s || -52 ko | +0.67% | -0.00% - 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00%
\ No newline at end of file + 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00% diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v index 3d2a875e38..32c8a7cbe7 100644 --- a/test-suite/ltac2/notations.v +++ b/test-suite/ltac2/notations.v @@ -1,6 +1,8 @@ From Ltac2 Require Import Ltac2. From Coq Require Import ZArith String List. +(** * Test cases for the notation system itself *) + Open Scope Z_scope. Check 1 + 1 : Z. @@ -22,3 +24,9 @@ Lemma maybe : list bool. Proof. refine (sl ["left" =? "right"]). Qed. + +(** * Test cases for specific notations with special contexts *) + +(** ** Test eval ... in / reduction tactics *) + +(** Moved to test-suite/output/ltac2_notations_eval_in.v so that the output can be checked s*) diff --git a/test-suite/misc/redirect_printing.out b/test-suite/misc/redirect_printing.out new file mode 100644 index 0000000000..4f45c4d4c2 --- /dev/null +++ b/test-suite/misc/redirect_printing.out @@ -0,0 +1,2 @@ +nat_ind + : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n diff --git a/test-suite/misc/redirect_printing.sh b/test-suite/misc/redirect_printing.sh new file mode 100755 index 0000000000..7da17407f3 --- /dev/null +++ b/test-suite/misc/redirect_printing.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +$coqc misc/redirect_printing.v +diff -u redirect_test.out misc/redirect_printing.out diff --git a/test-suite/misc/redirect_printing.v b/test-suite/misc/redirect_printing.v new file mode 100644 index 0000000000..2f9096bcb8 --- /dev/null +++ b/test-suite/misc/redirect_printing.v @@ -0,0 +1,2 @@ +Set Printing Width 999999. +Redirect "redirect_test" Check nat_ind. diff --git a/test-suite/output-coqchk/bug_5030.out b/test-suite/output-coqchk/bug_5030.out new file mode 100644 index 0000000000..bef45bf2f6 --- /dev/null +++ b/test-suite/output-coqchk/bug_5030.out @@ -0,0 +1,14 @@ + +CONTEXT SUMMARY +=============== + +* Theory: Set is predicative + +* Axioms: <none> + +* Constants/Inductives relying on type-in-type: <none> + +* Constants/Inductives relying on unsafe (co)fixpoints: <none> + +* Inductives whose positivity is assumed: <none> + diff --git a/test-suite/output-coqchk/bug_5030.v b/test-suite/output-coqchk/bug_5030.v new file mode 100644 index 0000000000..543784e3c9 --- /dev/null +++ b/test-suite/output-coqchk/bug_5030.v @@ -0,0 +1,10 @@ +Module Type testt. +Parameter proof : True. +End testt. + +Module Export test : testt. +Definition proof := I. +End test. + +Lemma true : True. +Proof. apply proof. Qed. diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out index dd8189c56f..539ec9b2bf 100644 --- a/test-suite/output/FloatExtraction.out +++ b/test-suite/output/FloatExtraction.out @@ -1,16 +1,18 @@ File "stdin", line 25, characters 8-12: Warning: The constant 0.01 is not a binary64 floating-point value. A closest -value will be used and unambiguously printed 0.01. [inexact-float,parsing] +value 0x1.47ae147ae147bp-7 will be used and unambiguously printed 0.01. +[inexact-float,parsing] File "stdin", line 25, characters 20-25: Warning: The constant -0.01 is not a binary64 floating-point value. A closest -value will be used and unambiguously printed -0.01. [inexact-float,parsing] +value -0x1.47ae147ae147bp-7 will be used and unambiguously printed -0.01. +[inexact-float,parsing] File "stdin", line 25, characters 27-35: Warning: The constant 1.7e+308 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed 1.6999999999999999e+308. -[inexact-float,parsing] +closest value 0x1.e42d130773b76p+1023 will be used and unambiguously printed +1.6999999999999999e+308. [inexact-float,parsing] File "stdin", line 25, characters 37-46: Warning: The constant -1.7e-308 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed +closest value -0x0.c396c98f8d899p-1022 will be used and unambiguously printed -1.7000000000000002e-308. [inexact-float,parsing] (** val infinity : Float64.t **) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 4a5a700879..0b18e9a3d2 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -6,13 +6,13 @@ : float File "stdin", line 9, characters 6-13: Warning: The constant 2.5e123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed 2.4999999999999999e+123. -[inexact-float,parsing] +closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed +2.4999999999999999e+123. [inexact-float,parsing] 2.4999999999999999e+123%float : float File "stdin", line 10, characters 7-16: Warning: The constant -2.5e-123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed +closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed -2.5000000000000001e-123. [inexact-float,parsing] (-2.5000000000000001e-123)%float : float @@ -28,13 +28,13 @@ closest value will be used and unambiguously printed : float File "stdin", line 19, characters 6-13: Warning: The constant 2.5e123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed 2.4999999999999999e+123. -[inexact-float,parsing] +closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed +2.4999999999999999e+123. [inexact-float,parsing] 2.4999999999999999e+123 : float File "stdin", line 20, characters 7-16: Warning: The constant -2.5e-123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed +closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed -2.5000000000000001e-123. [inexact-float,parsing] -2.5000000000000001e-123 : float @@ -56,16 +56,24 @@ closest value will be used and unambiguously printed : float File "stdin", line 30, characters 6-11: Warning: The constant 1e309 is not a binary64 floating-point value. A closest -value will be used and unambiguously printed infinity. +value infinity will be used and unambiguously printed infinity. [inexact-float,parsing] infinity : float File "stdin", line 31, characters 6-12: Warning: The constant -1e309 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed neg_infinity. -[inexact-float,parsing] +closest value neg_infinity will be used and unambiguously printed +neg_infinity. [inexact-float,parsing] neg_infinity : float +0x1p-1 + : float +0.5 + : float +0x1p-1 + : float +0.5 + : float 2 : nat 2%float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 36ffc27239..d3eb6d2e4c 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -30,6 +30,15 @@ Check -0xb.2cp-2. Check 1e309. Check -1e309. +Set Printing All. +Check 0.5. +Unset Printing All. +Check 0.5. +Unset Printing Float. +Check 0.5. +Set Printing Float. +Check 0.5. + Open Scope nat_scope. Check 2. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 190c34262f..ca4858d7a7 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,17 +7,17 @@ bli : Type Axioms: bli : Type Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Closed under the global context Closed under the global context Axioms: diff --git a/test-suite/output/ltac2_notations_eval_in.out b/test-suite/output/ltac2_notations_eval_in.out new file mode 100644 index 0000000000..15e43b7fb9 --- /dev/null +++ b/test-suite/output/ltac2_notations_eval_in.out @@ -0,0 +1,21 @@ +- : constr = +constr:((fix add (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (add p m) + end) (1 + 2) 3) +- : constr = constr:(S (0 + 2 + 3)) +- : constr = constr:(6) +- : constr = constr:(1 + 2 + 3) +- : constr = constr:(6) +- : constr = constr:(1 + 2 + 3) +- : constr = constr:(1 + 2 + 3) +- : constr = constr:(6) +- : constr = constr:(1 + 2 + 3) +- : constr = constr:(1 + 2 + 3) +- : constr = constr:(6) +- : constr = constr:(1 + 2 + 3) +- : constr = constr:(1 + 2 + 3) +- : constr list = [constr:(0 <> 0); constr:(0 = 0 -> False); +constr:((fun P : Prop => P -> False) (0 = 0)); constr:( +0 <> 0)] diff --git a/test-suite/output/ltac2_notations_eval_in.v b/test-suite/output/ltac2_notations_eval_in.v new file mode 100644 index 0000000000..4a11e7cae0 --- /dev/null +++ b/test-suite/output/ltac2_notations_eval_in.v @@ -0,0 +1,42 @@ +From Ltac2 Require Import Ltac2. +From Coq Require Import ZArith. + +(** * Test eval ... in / reduction tactics *) + +(** The below test cases test if the notation syntax works - not the tactics as such *) + +Ltac2 Eval (eval red in (1+2+3)). + +Ltac2 Eval (eval hnf in (1+2+3)). + +Ltac2 Eval (eval simpl in (1+2+3)). + +Ltac2 Eval (eval simpl Z.add in (1+2+3)). + +Ltac2 Eval (eval cbv in (1+2+3)). + +Ltac2 Eval (eval cbv delta [Z.add] beta iota in (1+2+3)). + +Ltac2 Eval (eval cbv delta [Z.add Pos.add] beta iota in (1+2+3)). + +Ltac2 Eval (eval cbn in (1+2+3)). + +Ltac2 Eval (eval cbn delta [Z.add] beta iota in (1+2+3)). + +Ltac2 Eval (eval cbn delta [Z.add Pos.add] beta iota in (1+2+3)). + +Ltac2 Eval (eval lazy in (1+2+3)). + +Ltac2 Eval (eval lazy delta [Z.add] beta iota in (1+2+3)). + +Ltac2 Eval (eval lazy delta [Z.add Pos.add] beta iota in (1+2+3)). + +(* The example for [fold] in the reference manual *) + +Ltac2 Eval ( + let t1 := '(~0=0) in + let t2 := eval unfold not in $t1 in + let t3 := eval pattern (0=0) in $t2 in + let t4 := eval fold not in $t3 in + [t1; t2; t3; t4] +). diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index c86548440b..97b4e39168 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq812. +Import Coq.Compat.Coq813. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index a1c1209db6..c06dd6e450 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..f408e95d2e --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 00f4747e3e..83010f2149 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml deleted file mode 100644 index 3082acdf1f..0000000000 --- a/test-suite/unit-tests/ide/lex_tests.ml +++ /dev/null @@ -1,50 +0,0 @@ -open Utest - -let log_out_ch = open_log_out_ch __FILE__ - -let lex s = - let n = - let last = String.length s - 1 in - if s.[last] = '.' then Some last else None in - let stop = ref None in - let f i _ = assert(!stop = None); stop := Some i in - begin try Coq_lex.delimit_sentences f s - with Coq_lex.Unterminated -> () end; - if n <> !stop then begin - let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in - Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop) - end; - n = !stop - -let i2s i = "test at line: " ^ string_of_int i - -let tests = [ - - mk_bool_test (i2s __LINE__) "no quotation" @@ lex - "foo.+1 bar." - ; - mk_bool_test (i2s __LINE__) "quotation" @@ lex - "foo constr:(xxx)." - ; - mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex - "foo constr:(xxx. yyy)." - ; - mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex - "foo constr:((xxx. (foo.+1 ) \")\" yyy))." - ; - mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex - "foo constr:[xxx. (foo.+1 ) \")\" yyy]." - ; - mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex - "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]." - ; - mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex - "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]." - ; - mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex - "bar:{{ foo {{ hello. }} }}." - ; - -] - -let _ = run_tests __FILE__ log_out_ch tests diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index d0b8d21b69..60267cd859 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -76,11 +76,14 @@ let _ = add_test "tokenize_string/diff_mode in lexer" t open Pp +let write_diffs_option s = + Goptions.set_string_option_value Proof_diffs.opt_name s + (* example that was failing from #8922 *) let t () = - Proof_diffs.write_diffs_option "removed"; + write_diffs_option "removed"; ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1"); - Proof_diffs.write_diffs_option "on" + write_diffs_option "on" let _ = add_test "shorten_diff_span failure from #8922" t (* note pp_to_string concatenates adjacent strings, could become one token, @@ -181,7 +184,7 @@ let _ = if false then add_test "diff_pp/add_diff_tags token containing white spa let add_entries map idents rhs_pp = let make_entry() = { idents; rhs_pp; done_ = false } in - List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;; + List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents;; let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps @@ -194,11 +197,11 @@ let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (fl let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["a"]; ["b"]] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["a"] (str " : foo"); add_entries o_hyp_map ["b"] (str " : bar car"); let n_line_idents = [ ["b"]; ["a"]] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["b"] (str " : car"); add_entries n_hyp_map ["a"] (str " : foo bar"); let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ])); @@ -224,11 +227,11 @@ let _ = add_test "diff_hyps simple diffs" t let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["a"]; ["c"; "d"]] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["a"] (str " : nat"); add_entries o_hyp_map ["c"; "d"] (str " : int"); let n_line_idents = [ ["a"; "b"]; ["d"]] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["a"; "b"] (str " : nat"); add_entries n_hyp_map ["d"] (str " : int"); let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ])); @@ -264,12 +267,12 @@ DIFFS let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["a"]; ["b"]; ["c"]] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["a"] (str " : foo"); add_entries o_hyp_map ["b"] (str " : bar"); add_entries o_hyp_map ["c"] (str " : nat"); let n_line_idents = [ ["b"; "a"; "c"] ] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat"); let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))])); flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))])); @@ -302,10 +305,10 @@ DIFFS let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["b"; "a"; "c"] ] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat"); let n_line_idents = [ ["a"]; ["b"]; ["c"]] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["a"] (str " : foo"); add_entries n_hyp_map ["b"] (str " : bar"); add_entries n_hyp_map ["c"] (str " : nat"); |