diff options
Diffstat (limited to 'test-suite')
42 files changed, 123 insertions, 86 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 37091a49e5..111bd52a33 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -38,14 +38,15 @@ LIB := .. BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS) coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc +coqtop := $(BIN)coqtop -batch -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite coqtopbyte := $(BIN)coqtop.byte -coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source -coqtopcompile := $(coqtop) -async-proofs-cache force -compile +coqc_interactive := $(coqc) -async-proofs-cache force +coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force coqdep := $(BIN)coqdep -coqlib $(LIB) VERBOSE?= @@ -60,12 +61,8 @@ SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1))))) -# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop -has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) -get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload)) get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1))) - bogomips:= ifneq (,$(wildcard /proc/cpuinfo)) sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc @@ -209,7 +206,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...still active"; \ @@ -231,7 +228,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -297,7 +294,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ @@ -316,7 +313,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -342,7 +339,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -367,7 +364,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -392,7 +389,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -431,7 +428,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out echo $(call log_intro,$<); \ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -486,7 +483,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ + res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ @@ -517,7 +514,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_success); \ echo " $<...still wished"; \ @@ -531,7 +528,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG # Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v - $(HIDE)$(coqtop) -R modules Mods -compile $< + $(HIDE)$(coqc) -R modules Mods $< ####################################################################### # Miscellaneous tests @@ -550,7 +547,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) echo $(call log_intro,$<); \ export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ - export coqtop="$(coqtop)"; \ + export coqtop="$(coqc_boot)"; \ export coqdep="$(coqdep)"; \ export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ @@ -591,7 +588,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) @echo "TEST $<" $(HIDE){ \ $(coqc) -quick -R vio vio $* 2>&1 && \ - $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \ + $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \ $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index 3e3a987a7c..b80e0bb0e4 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn} Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}. Global Instance FunctorApplicationDash C D (F : Functor C D) -: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0. +: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}. Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B) -: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100. +: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}. Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope. diff --git a/test-suite/bugs/closed/bug_3324.v b/test-suite/bugs/closed/bug_3324.v index 45dbb57aa2..dae0d4c024 100644 --- a/test-suite/bugs/closed/bug_3324.v +++ b/test-suite/bugs/closed/bug_3324.v @@ -6,7 +6,7 @@ Module ETassi. Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}. Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). - Global Instance isset_hProp : IsHSet hProp | 0. + Global Instance isset_hProp : IsHSet hProp | 0 := {}. Check (eq_refl _ : setT (default_HSet _ _) = hProp). Check (eq_refl _ : setT _ = hProp). @@ -22,7 +22,7 @@ Module JGross. Definition Unit_hp:hProp:=(hp Unit admit). Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). - Global Instance isset_hProp : IsHSet hProp | 0. + Global Instance isset_hProp : IsHSet hProp | 0 := {}. Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h. Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True. diff --git a/test-suite/bugs/closed/bug_3454.v b/test-suite/bugs/closed/bug_3454.v index e4cd60cb24..0a01adec33 100644 --- a/test-suite/bugs/closed/bug_3454.v +++ b/test-suite/bugs/closed/bug_3454.v @@ -32,14 +32,14 @@ Local Instance isequiv_tgt_compose A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) (@compose A {xy : B * B & fst xy = snd xy} B - (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)). + (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)) := {}. (* Toplevel input, characters 220-223: *) (* Error: Cannot infer this placeholder. *) Local Instance isequiv_tgt_compose' A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) - (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)). + (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)) := {}. (* Toplevel input, characters 221-232: *) (* Error: *) (* In environment *) @@ -52,7 +52,7 @@ Local Instance isequiv_tgt_compose'' A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) - (fun s => s.(projT1)))). + (fun s => s.(projT1)))) := {}. (* Toplevel input, characters 15-241: Error: Cannot infer an internal placeholder of type "Type" in environment: diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v index 9d37d1a2d0..07b759afb5 100644 --- a/test-suite/bugs/closed/bug_3682.v +++ b/test-suite/bugs/closed/bug_3682.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. Class Foo. Definition bar `{Foo} (x : Set) := Set. -Instance: Foo. +Instance: Foo := {}. Definition bar1 := bar nat. Definition bar2 := bar ltac:(admit). diff --git a/test-suite/bugs/closed/bug_4782.v b/test-suite/bugs/closed/bug_4782.v index be17a96f15..c08195d502 100644 --- a/test-suite/bugs/closed/bug_4782.v +++ b/test-suite/bugs/closed/bug_4782.v @@ -15,8 +15,8 @@ Record T := { dom : Type }. Definition pairT A B := {| dom := (dom A * dom B)%type |}. Class C (A:Type). Parameter B:T. -Instance c (A:T) : C (dom A). -Instance cn : C (dom B). +Instance c (A:T) : C (dom A) := {}. +Instance cn : C (dom B) := {}. Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. Set Typeclasses Debug. Goal forall (A:T) (x:dom A), pairT A A = pairT A A. diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v index 41a1251ca5..696812dee1 100644 --- a/test-suite/bugs/closed/bug_4798.v +++ b/test-suite/bugs/closed/bug_4798.v @@ -1,3 +1,5 @@ +(* DO NOT MODIFY THIS FILE DIRECTLY *) +(* It is autogenerated by dev/tools/update-compat.py. *) Check match 2 with 0 => 0 | S n => n end. Notation "|" := 1 (compat "8.7"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v index 5838dcd8a7..9aefb10172 100644 --- a/test-suite/bugs/closed/bug_4836.v +++ b/test-suite/bugs/closed/bug_4836.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *) +(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *) diff --git a/test-suite/bugs/closed/bug_5401.v b/test-suite/bugs/closed/bug_5401.v index 95193b993b..466e669d00 100644 --- a/test-suite/bugs/closed/bug_5401.v +++ b/test-suite/bugs/closed/bug_5401.v @@ -5,7 +5,7 @@ Parameter P : nat -> Type. Parameter v : forall m, P m. Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0. Class U (R : P 0) (m : forall x, P x) : Prop. -Instance w : U (f _ (fun _ => v _)) v. +Instance w : U (f _ (fun _ => v _)) v := {}. Print HintDb typeclass_instances. End A. diff --git a/test-suite/bugs/closed/bug_7811.v b/test-suite/bugs/closed/bug_7811.v index fee330f22d..155f3285b7 100644 --- a/test-suite/bugs/closed/bug_7811.v +++ b/test-suite/bugs/closed/bug_7811.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) +(* -*- mode: coq; coq-prog-args: ("-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) (* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *) (* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3 coqtop version 8.8.0 (May 2018) *) diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v index 8a7e9c37b0..a89837dd12 100644 --- a/test-suite/bugs/closed/bug_9166.v +++ b/test-suite/bugs/closed/bug_9166.v @@ -1,3 +1,5 @@ +(* DO NOT MODIFY THIS FILE DIRECTLY *) +(* It is autogenerated by dev/tools/update-compat.py. *) Set Warnings "+deprecated". Notation bar := option (compat "8.7"). diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v index c5e1953829..31217ca75e 100644 --- a/test-suite/complexity/constructor.v +++ b/test-suite/complexity/constructor.v @@ -214,3 +214,4 @@ Fixpoint expand (n : nat) : Prop := Example Expand : expand 2500. Time constructor. (* ~0.45 secs *) +Qed. diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v index 86698fa872..c2c566930b 100644 --- a/test-suite/complexity/f_equal.v +++ b/test-suite/complexity/f_equal.v @@ -12,3 +12,4 @@ end. Goal stupid 23 = stupid 23. Timeout 5 Time f_equal. +Abort. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index a76fa19d3c..298a07c1c4 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -111,3 +111,4 @@ Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 -> Proof. intros. Timeout 10 Time injection H. +Abort. diff --git a/test-suite/complexity/ring.v b/test-suite/complexity/ring.v index 51f7c4dabc..2d585ce5c5 100644 --- a/test-suite/complexity/ring.v +++ b/test-suite/complexity/ring.v @@ -5,3 +5,4 @@ Require Import ZArith. Open Scope Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. +Abort. diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index 04fa59075b..1c119b8e42 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -50,3 +50,4 @@ Infix "+" := Zadd : Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. +Abort. diff --git a/test-suite/complexity/setoid_rewrite.v b/test-suite/complexity/setoid_rewrite.v index 2e3b006ef0..10b270ccad 100644 --- a/test-suite/complexity/setoid_rewrite.v +++ b/test-suite/complexity/setoid_rewrite.v @@ -8,3 +8,4 @@ Variable f : nat -> Prop. Goal forall U:Prop, f 100 <-> U. intros U. Timeout 5 Time setoid_replace U with False. +Abort. diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v index d2ea527516..0c9915c84e 100644 --- a/test-suite/complexity/unification.v +++ b/test-suite/complexity/unification.v @@ -49,3 +49,4 @@ Goal )))) . Timeout 2 Time try refine (refl_equal _). +Abort. diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake new file mode 100644 index 0000000000..aa68fad39e --- /dev/null +++ b/test-suite/ide/debug_ltac.fake @@ -0,0 +1,2 @@ +FAILADD { Debug On. } +ADD { Set Debug On. } diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh index 86bc50b5cd..70071b9d60 100755 --- a/test-suite/misc/4722.sh +++ b/test-suite/misc/4722.sh @@ -4,12 +4,12 @@ set -e # create test files mkdir -p misc/4722 ln -sf toto misc/4722/tata -touch misc/4722.v +touch misc/bug_4722.v # run test -$coqtop "-R" "misc/4722" "Foo" -top Top -load-vernac-source misc/4722.v +$coqc "-R" "misc/4722" "Foo" -top Top misc/bug_4722.v # clean up test files rm misc/4722/tata rmdir misc/4722 -rm misc/4722.v +rm misc/bug_4722.v diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh index 0ca2c97d24..5fc171649e 100755 --- a/test-suite/misc/7704.sh +++ b/test-suite/misc/7704.sh @@ -4,4 +4,4 @@ set -e export PATH=$BIN:$PATH -${coqtop#"$BIN"} -compile misc/aux7704.v +${coqc#"$BIN"} misc/aux7704.v diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v index 6fdcf67684..1c95211a71 100644 --- a/test-suite/misc/aux7704.v +++ b/test-suite/misc/aux7704.v @@ -1,4 +1,3 @@ - Goal True /\ True. Proof. split. diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index a15a8fbee9..8523358303 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -3,4 +3,4 @@ rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v $coqc -R misc/deps/B A misc/deps/B/B.v -$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v +$coqc -R misc/deps/B A -R misc/deps/A A misc/deps/checksum.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 6bb2ba2da0..551515b0d6 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -10,12 +10,12 @@ R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 -$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 +$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 S=$? if [ $R = 0 ] && [ $S = 0 ]; then - printf "coqdep and coqtop agree\n" + printf "coqdep and coqc agree\n" exit 0 else - printf "coqdep and coqtop disagree\n" + printf "coqdep and coqc disagree\n" exit 1 fi diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh index acb45b2292..af69370ce4 100755 --- a/test-suite/misc/deps-utf8.sh +++ b/test-suite/misc/deps-utf8.sh @@ -8,7 +8,7 @@ rm -f misc/deps/théorèmes/*.v tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX) $coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v R=$? -$coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v +$coqc -R misc/deps AlphaBêta misc/deps/αβ/εζ.v S=$? if [ $R = 0 ] && [ $S = 0 ]; then exit 0 diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v index 7658ce718e..440fe46003 100644 --- a/test-suite/output/FunExt.v +++ b/test-suite/output/FunExt.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-async-proofs" "no") -*- *) Require Import FunctionalExtensionality. (* Basic example *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 94016e170b..7a64b7eb45 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,5 +45,9 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +myAnd1 True True + : Prop +r 2 3 + : Prop Notation Cn := Foo.FooCn -Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn +Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 309115848f..90babf9c55 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -165,6 +165,22 @@ Check ##. End H. +(* Fixing bugs reported by G. Gonthier in #9207 *) + +Module I. + +Definition myAnd A B := A /\ B. +Notation myAnd1 A := (myAnd A). +Check myAnd1 True True. + +Set Warnings "-auto-template". + +Record Pnat := {inPnat :> nat -> Prop}. +Axiom r : nat -> Pnat. +Check r 2 3. + +End I. + (* Fixing a bug reported by G. Gonthier in #9207 *) Module J. diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v index cd667bbd00..a53b52396f 100644 --- a/test-suite/output/RecognizePluginWarning.v +++ b/test-suite/output/RecognizePluginWarning.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) +(* -*- mode: coq; coq-prog-args: ("-w" "extraction-logical-axiom") -*- *) (* Test that mentioning a warning defined in plugins works. The failure mode here is that these result in a warning about unknown warnings, since the diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v index 60faac8dd9..c875051bdc 100644 --- a/test-suite/output/Show.v +++ b/test-suite/output/Show.v @@ -5,7 +5,7 @@ Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). Proof. intros. - induction n as [| n']. + induction n as [| n']. induction m as [| m']. Show. Admitted. diff --git a/test-suite/output/UnclosedBlocks.v b/test-suite/output/UnclosedBlocks.v index 854bd6a6d5..b9ba579246 100644 --- a/test-suite/output/UnclosedBlocks.v +++ b/test-suite/output/UnclosedBlocks.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-compile" "UnclosedBlocks.v") *) Module Foo. Module Closed. End Closed. diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v index c6e0054641..618b8fd42f 100644 --- a/test-suite/output/UsePluginWarning.v +++ b/test-suite/output/UsePluginWarning.v @@ -1,5 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) - +(* -*- mode: coq; coq-prog-args: ("-w" "-extraction-logical-axiom") -*- *) Require Extraction. Axiom foo : Prop. diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v index 5f1926f142..5f7e3ab9dd 100644 --- a/test-suite/output/simpl.v +++ b/test-suite/output/simpl.v @@ -11,3 +11,4 @@ Undo. simpl (0 + _). Show. Undo. +Abort. diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v index 179dec3fb0..c987d66c5f 100644 --- a/test-suite/output/unifconstraints.v +++ b/test-suite/output/unifconstraints.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-async-proofs" "no") -*- *) (* Set Printing Existential Instances. *) Unset Solve Unification Constraints. Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat. diff --git a/test-suite/report.sh b/test-suite/report.sh index cef615266b..71aac029ea 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -24,21 +24,11 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$TRAVIS" ] || [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do - if [ -n "$TRAVIS" ]; then - # ${foo////.} replaces every / by . in $foo - printf 'travis_fold:start:coq.logs.%s\n' "${file////.}"; - else printf '%s\n' "$file" - fi - + printf '%s\n' "$file" cat "$file" - - if [ -n "$TRAVIS" ]; then - # ${foo////.} replaces every / by . in $foo - printf 'travis_fold:end:coq.logs.%s\n' "${file////.}"; - else printf '\n' - fi + printf '\n' done printed_logs=1 fi diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v new file mode 100644 index 0000000000..528f33f30d --- /dev/null +++ b/test-suite/ssr/ipat_replace.v @@ -0,0 +1,17 @@ +Require Import ssreflect. + +Lemma test : True. +Proof. +have H : True. + by []. +have {}H : True. + by apply: H. +by apply: H. +Qed. + +Lemma test2 (H : True) : False -> False -> False. +Proof. +move=> {}W. +move=> {}H. +by apply: H. +Qed. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 9086621344..3888cafed3 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -14,7 +14,7 @@ Module onlyclasses. Module RJung. Class Foo (x : nat). - Instance foo x : x = 2 -> Foo x. + Instance foo x : x = 2 -> Foo x := {}. Hint Extern 0 (_ = _) => reflexivity : typeclass_instances. Typeclasses eauto := debug. Check (_ : Foo 2). @@ -63,7 +63,7 @@ End RefineVsNoTceauto. Module Leivantex2PR339. (** Was a bug preventing to find hints associated with no pattern *) Class Bar := {}. - Instance bar1 (t:Type) : Bar. + Instance bar1 (t:Type) : Bar := {}. Hint Extern 0 => exact True : typeclass_instances. Typeclasses eauto := debug. Goal Bar. @@ -222,10 +222,10 @@ Module IterativeDeepening. Class B. Class C. - Instance: B -> A | 0. - Instance: C -> A | 0. - Instance: C -> B -> A | 0. - Instance: A -> A | 0. + Instance: B -> A | 0 := {}. + Instance: C -> A | 0 := {}. + Instance: C -> B -> A | 0 := {}. + Instance: A -> A | 0 := {}. Goal C -> A. intros. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 5477c83316..62a66daf7d 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -51,7 +51,7 @@ Qed. Class B (A : Type). Class I. -Instance i : I. +Instance i : I := {}. Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y. Class D (f : nat -> nat -> nat). @@ -59,7 +59,7 @@ Definition ftest (x y : nat) := x + y. Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f). Admitted. Module Instnopat. - Local Instance: B nat. + Local Instance: B nat := {}. (* pattern_of_constr -> B nat *) (* exact hint *) Check (_ : B nat). @@ -72,7 +72,7 @@ Module Instnopat. eauto with typeclass_instances. Qed. - Local Instance: D ftest. + Local Instance: D ftest := {}. Local Hint Resolve flipD | 0 : typeclass_instances. (* pattern: D (flip _) *) Fail Timeout 1 Check (_ : D _). (* loops applying flipD *) @@ -80,7 +80,7 @@ Module Instnopat. End Instnopat. Module InstnopatApply. - Local Instance: I -> B nat. + Local Instance: I -> B nat := {}. (* pattern_of_constr -> B nat *) (* apply hint *) Check (_ : B nat). @@ -116,7 +116,7 @@ Module InstPat. Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances. Module withftest. - Local Instance: D ftest. + Local Instance: D ftest := {}. Check (_ : D _). (* D_instance_0 : D ftest *) diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 730b367d60..cea7d92c0b 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -149,10 +149,10 @@ Module IterativeDeepening. Class B. Class C. - Instance: B -> A | 0. - Instance: C -> A | 0. - Instance: C -> B -> A | 0. - Instance: A -> A | 0. + Instance: B -> A | 0 := {}. + Instance: C -> A | 0 := {}. + Instance: C -> B -> A | 0 := {}. + Instance: A -> A | 0 := {}. Goal C -> A. intros. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index d1d384659b..573912c7cd 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -263,7 +263,7 @@ Abort. (* This one was working in 8.4 (because of full conv on closed arguments) *) Class E. -Instance a:E. +Instance a:E := {}. Goal forall h : E -> nat -> nat, h (id a) 0 = h a 0. intros. destruct (h _). diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index c44747379f..5b616ccc33 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -9,11 +9,11 @@ (************************************************************************) Class A (A : Type). - Instance an: A nat. + Instance an: A nat := {}. Class B (A : Type) (a : A). -Instance bn0: B nat 0. -Instance bn1: B nat 1. +Instance bn0: B nat 0 := {}. +Instance bn1: B nat 1 := {}. Goal A nat. Proof. @@ -39,7 +39,7 @@ Proof. eexists. eexists. typeclasses eauto. Defined. -Instance ab: A bool. (* Backtrack on A instance *) +Instance ab: A bool := {}. (* Backtrack on A instance *) Goal exists (T : Type) (t : T), A T /\ B T t. Proof. eexists. eexists. typeclasses eauto. @@ -51,7 +51,7 @@ Hint Extern 0 { x : ?A & _ } => unshelve class_apply @existT : typeclass_instances. Existing Class sigT. Set Typeclasses Debug. -Instance can: C an 0. +Instance can: C an 0 := {}. (* Backtrack on instance implementation *) Goal exists (T : Type) (t : T), { x : A T & C x t }. Proof. @@ -59,7 +59,7 @@ Proof. Defined. Class D T `(a: A T). - Instance: D _ an. + Instance: D _ an := {}. Goal exists (T : Type), { x : A T & D T x }. Proof. eexists. typeclasses eauto. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 79467e549c..351481b0b6 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop. Axiom SetoidS1 : Setoid_Theory S1 eqS1. Add Setoid S1 eqS1 SetoidS1 as S1setoid. -Instance eqS1_default : DefaultRelation eqS1. +Instance eqS1_default : DefaultRelation eqS1 := {}. Axiom eqS1': S1 -> S1 -> Prop. Axiom SetoidS1' : Setoid_Theory S1 eqS1'. @@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8. Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. -Instance eqS1_test8_default : DefaultRelation eqS1_test8. +Instance eqS1_test8_default : DefaultRelation eqS1_test8 := {}. Axiom f_test8 : S2 -> S1_test8. Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted. |