diff options
Diffstat (limited to 'test-suite')
29 files changed, 329 insertions, 19 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index ae426f0daf..61e75fa5d3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -92,7 +92,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ coqdoc # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log @@ -156,6 +156,7 @@ summary: $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ + $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ @@ -498,6 +499,26 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) fi; \ } > "$@" +# coqwc : test output + +coqwc : $(patsubst %.v,%.v.log,$(wildcard coqwc/*.v)) + +coqwc/%.v.log : coqwc/%.v + $(HIDE){ \ + echo $(call log_intro,$<); \ + tmpoutput=`mktemp /tmp/coqwc.XXXXXX`; \ + $(BIN)coqwc $< 2>&1 > $$tmpoutput; \ + diff -u --strip-trailing-cr coqwc/$*.out $$tmpoutput 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + fi; \ + rm $$tmpoutput; \ + } > "$@" + # coq_makefile coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) diff --git a/test-suite/bugs/closed/4852.v b/test-suite/bugs/closed/4852.v new file mode 100644 index 0000000000..5068ed9b95 --- /dev/null +++ b/test-suite/bugs/closed/4852.v @@ -0,0 +1,54 @@ +(** BZ 4852 : unsatisfactory Extraction Implicit for a fixpoint defined via wf *) + +Require Import Coq.Lists.List. +Import ListNotations. +Require Import Omega. + +Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf. + +Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) := + let R := fresh in + let E := fresh in + remember term as R eqn:E; + revert E; revert Hs; + induction R as [R H] using wfi_lt; + intros; subst R. + +Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws. + +Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega. + +Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'"). + +Definition split_acc (ls : list nat) : forall acc1 acc2, + (|acc1| = |acc2| \/ |acc1| = S (|acc2|)) -> + { lss : list nat * list nat | + let '(ls1, ls2) := lss in |ls1++ls2| = |ls++acc1++acc2| /\ (|ls1| = |ls2| \/ |ls1| = S (|ls2|))}. +Proof. + induction ls as [|a ls IHls]. all:intros acc1 acc2 H. + { exists (acc1, acc2). cbn. intuition reflexivity. } + destruct (IHls (a::acc2) acc1) as [[ls1 ls2] (H1 & H2)]. 1:solve_nat. + exists (ls1, ls2). cbn. intuition solve_nat. +Defined. + +Definition join(ls : list nat) : { rls : list nat | |rls| = |ls| }. +Proof. + wfinduction (|ls|) on ls as IH. + case (split_acc ls [] []). 1:solve_nat. + intros (ls1 & ls2) (H1 & H2). + destruct ls2 as [|a ls2]. + - exists ls1. solve_nat. + - unshelve eelim (IH _ _ ls1 eq_refl). 1:solve_nat. intros rls1 H3. + unshelve eelim (IH _ _ ls2 eq_refl). 1:solve_nat. intros rls2 H4. + exists (a :: rls1 ++ rls2). solve_nat. +Defined. + +Require Import ExtrOcamlNatInt. +Extract Inlined Constant length => "List.length". +Extract Inlined Constant app => "List.append". + +Extraction Inline wfi_lt. +Extraction Implicit wfi_lt [1 3]. +Recursive Extraction join. (* was: Error: An implicit occurs after extraction *) +Extraction TestCompile join. + diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v new file mode 100644 index 0000000000..55ef7abe40 --- /dev/null +++ b/test-suite/bugs/closed/5692.v @@ -0,0 +1,38 @@ +Set Primitive Projections. +Require Import ZArith ssreflect. + +Module Test3. + +Set Primitive Projections. + +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure group := Something { + group_car :> Type; + group_op : group_car -> group_car -> group_car; + group_neg : group_car -> group_car; + group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y) +}. + +Coercion group_sg (X : group) : semigroup := + SemiGroup (group_car X) (group_op X). +Canonical Structure group_sg. + +Axiom group_neg_op : forall (X : group) (x y : X), + group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y). + +Canonical Structure Z_sg := SemiGroup Z Z.add . +Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr. + +Lemma foo (x y : Z) : + sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) = + group_neg Z_group (sg_op Z_sg x y). +Proof. + rewrite -group_neg_op. + reflexivity. +Qed. + +End Test3. diff --git a/test-suite/bugs/closed/5741.v b/test-suite/bugs/closed/5741.v new file mode 100644 index 0000000000..f6598f192d --- /dev/null +++ b/test-suite/bugs/closed/5741.v @@ -0,0 +1,4 @@ +(* Check no anomaly in info_trivial *) + +Goal True. +info_trivial. diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v new file mode 100644 index 0000000000..0d0f2eed44 --- /dev/null +++ b/test-suite/bugs/closed/5757.v @@ -0,0 +1,76 @@ +(* Check that resolved status of evars follows "restrict" *) + +Axiom H : forall (v : nat), Some 0 = Some v -> True. +Lemma L : True. +eapply H with _; +match goal with + | |- Some 0 = Some ?v => change (Some (0+0) = Some v) +end. +Abort. + +(* The original example *) + +Set Default Proof Using "Type". + +Module heap_lang. + +Inductive expr := + | InjR (e : expr). + +Inductive val := + | InjRV (v : val). + +Bind Scope val_scope with val. + +Fixpoint of_val (v : val) : expr := + match v with + | InjRV v => InjR (of_val v) + end. + +Fixpoint to_val (e : expr) : option val := None. + +End heap_lang. +Export heap_lang. + +Module W. +Inductive expr := + | Val (v : val) + (* Sums *) + | InjR (e : expr). + +Fixpoint to_expr (e : expr) : heap_lang.expr := + match e with + | Val v => of_val v + | InjR e => heap_lang.InjR (to_expr e) + end. + +End W. + + + +Section Tests. + + Context (iProp: Type). + Context (WPre: expr -> Prop). + + Context (tac_wp_alloc : + forall (e : expr) (v : val), + to_val e = Some v -> WPre e). + + Lemma push_atomic_spec (x: val) : + WPre (InjR (of_val x)). + Proof. +(* This works. *) +eapply tac_wp_alloc with _. +match goal with + | |- to_val ?e = Some ?v => + change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v) +end. +Undo. Undo. +(* This is fixed *) +eapply tac_wp_alloc with _; +match goal with + | |- to_val ?e = Some ?v => + change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v) +end. +Abort. diff --git a/test-suite/bugs/closed/5765.v b/test-suite/bugs/closed/5765.v new file mode 100644 index 0000000000..343ab49357 --- /dev/null +++ b/test-suite/bugs/closed/5765.v @@ -0,0 +1,3 @@ +(* 'pat binder not (yet?) allowed in parameters of inductive types *) + +Fail Inductive X '(a,b) := x. diff --git a/test-suite/bugs/closed/5769.v b/test-suite/bugs/closed/5769.v new file mode 100644 index 0000000000..42573aad87 --- /dev/null +++ b/test-suite/bugs/closed/5769.v @@ -0,0 +1,20 @@ +(* Check a few naming heuristics based on types *) +(* was buggy for types names _something *) + +Inductive _foo :=. +Lemma bob : (sigT (fun x : nat => _foo)) -> _foo. +destruct 1. +exact _f. +Abort. + +Inductive _'Foo :=. +Lemma bob : (sigT (fun x : nat => _'Foo)) -> _'Foo. +destruct 1. +exact _'f. +Abort. + +Inductive ____ :=. +Lemma bob : (sigT (fun x : nat => ____)) -> ____. +destruct 1. +exact x0. +Abort. diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 803fe8029a..c4bd11c57d 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -2,6 +2,7 @@ set -e set -o pipefail export PATH=$COQBIN:$PATH +export LC_ALL=C rm -rf theories src Makefile Makefile.conf tmp git clean -dfx || true diff --git a/test-suite/coqwc/BZ5637.out b/test-suite/coqwc/BZ5637.out new file mode 100644 index 0000000000..f0b5e4f7eb --- /dev/null +++ b/test-suite/coqwc/BZ5637.out @@ -0,0 +1,2 @@ + spec proof comments + 5 0 0 coqwc/BZ5637.v diff --git a/test-suite/coqwc/BZ5637.v b/test-suite/coqwc/BZ5637.v new file mode 100644 index 0000000000..6428b10ff8 --- /dev/null +++ b/test-suite/coqwc/BZ5637.v @@ -0,0 +1,5 @@ +Local Obligation Tactic := idtac. +Definition a := 1. +Definition b := 1. +Definition c := 1. +Definition d := 1. diff --git a/test-suite/coqwc/BZ5756.out b/test-suite/coqwc/BZ5756.out new file mode 100644 index 0000000000..039d1e5008 --- /dev/null +++ b/test-suite/coqwc/BZ5756.out @@ -0,0 +1,2 @@ + spec proof comments + 3 0 2 coqwc/BZ5756.v diff --git a/test-suite/coqwc/BZ5756.v b/test-suite/coqwc/BZ5756.v new file mode 100644 index 0000000000..ccb12076a3 --- /dev/null +++ b/test-suite/coqwc/BZ5756.v @@ -0,0 +1,3 @@ +Definition myNextValue := 0. (* OK *) +Definition x := myNextValue. (* not OK *) +Definition y := 0. diff --git a/test-suite/coqwc/false.out b/test-suite/coqwc/false.out new file mode 100644 index 0000000000..14c5713f6d --- /dev/null +++ b/test-suite/coqwc/false.out @@ -0,0 +1,2 @@ + spec proof comments + 3 3 1 coqwc/false.v diff --git a/test-suite/coqwc/false.v b/test-suite/coqwc/false.v new file mode 100644 index 0000000000..640f9ea7f0 --- /dev/null +++ b/test-suite/coqwc/false.v @@ -0,0 +1,8 @@ +Axiom x : nat. + +Definition foo (x : nat) := x + 1. + +Lemma bar : False. + idtac. + idtac. (* truth is overrated *) +Admitted. diff --git a/test-suite/coqwc/next-obligation.out b/test-suite/coqwc/next-obligation.out new file mode 100644 index 0000000000..7a0fd777c1 --- /dev/null +++ b/test-suite/coqwc/next-obligation.out @@ -0,0 +1,2 @@ + spec proof comments + 1 7 0 coqwc/next-obligation.v diff --git a/test-suite/coqwc/next-obligation.v b/test-suite/coqwc/next-obligation.v new file mode 100644 index 0000000000..786df98913 --- /dev/null +++ b/test-suite/coqwc/next-obligation.v @@ -0,0 +1,10 @@ +(* make sure all proof lines are counted *) + +Goal True. + Next Obligation. + idtac. + Next Obligation. + idtac. + Next Obligation. + idtac. +Qed. diff --git a/test-suite/coqwc/theorem.out b/test-suite/coqwc/theorem.out new file mode 100644 index 0000000000..d01507bf78 --- /dev/null +++ b/test-suite/coqwc/theorem.out @@ -0,0 +1,2 @@ + spec proof comments + 1 9 2 coqwc/theorem.v diff --git a/test-suite/coqwc/theorem.v b/test-suite/coqwc/theorem.v new file mode 100644 index 0000000000..901c9074fd --- /dev/null +++ b/test-suite/coqwc/theorem.v @@ -0,0 +1,10 @@ +Theorem foo : True. +Proof. + idtac. (* comment *) + idtac. + idtac. + idtac. (* comment *) + idtac. + idtac. + auto. +Qed. diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh new file mode 100755 index 0000000000..13e264c09c --- /dev/null +++ b/test-suite/misc/deps-utf8.sh @@ -0,0 +1,17 @@ +# Check reading directories matching non pure ascii idents +# See bug #5715 (utf-8 working on macos X and linux) +# Windows is still not compliant +a=`uname` +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +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 +S=$? +if [ $R = 0 -a $S = 0 ]; then + exit 0 +else + exit 1 +fi +fi diff --git a/test-suite/misc/deps/αβ/γδ.v b/test-suite/misc/deps/αβ/γδ.v new file mode 100644 index 0000000000..f43a2d6571 --- /dev/null +++ b/test-suite/misc/deps/αβ/γδ.v @@ -0,0 +1,4 @@ +Theorem simple : forall A, A -> A. +Proof. +auto. +Qed. diff --git a/test-suite/misc/deps/αβ/εζ.v b/test-suite/misc/deps/αβ/εζ.v new file mode 100644 index 0000000000..e7fd25c0d1 --- /dev/null +++ b/test-suite/misc/deps/αβ/εζ.v @@ -0,0 +1 @@ +Require Import γδ. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 65efe228af..6ef75dd135 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -124,3 +124,7 @@ return (1, 2, 3, 4) : nat !!! _ _ : nat, True : (nat -> Prop) * ((nat -> Prop) * Prop) +((*1).2).3 + : nat +*(1.2) + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index ea372ad1a3..8c7bbe5917 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -190,3 +190,10 @@ Check 1+1+1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). Check !!! (x y:nat), True. + +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out index a5b55a9993..2761b87b02 100644 --- a/test-suite/output/auto.out +++ b/test-suite/output/auto.out @@ -18,3 +18,5 @@ Debug: 1 depth=5 Debug: 1.1 depth=4 simple apply or_intror Debug: 1.1.1 depth=4 intro Debug: 1.1.1.1 depth=4 exact H +(* info trivial: *) +exact I (in core). diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v index a77b7b82e6..92917cdfc7 100644 --- a/test-suite/output/auto.v +++ b/test-suite/output/auto.v @@ -9,3 +9,7 @@ info_eauto. Undo. debug eauto. Qed. + +Goal True. +info_trivial. +Qed. diff --git a/test-suite/output/ltac_extra_args.out b/test-suite/output/ltac_extra_args.out new file mode 100644 index 0000000000..77e799d359 --- /dev/null +++ b/test-suite/output/ltac_extra_args.out @@ -0,0 +1,8 @@ +The command has indeed failed with message: +Illegal tactic application: got 1 extra argument. +The command has indeed failed with message: +Illegal tactic application: got 2 extra arguments. +The command has indeed failed with message: +Illegal tactic application: got 1 extra argument. +The command has indeed failed with message: +Illegal tactic application: got 2 extra arguments. diff --git a/test-suite/output/ltac_extra_args.v b/test-suite/output/ltac_extra_args.v new file mode 100644 index 0000000000..4caf619fee --- /dev/null +++ b/test-suite/output/ltac_extra_args.v @@ -0,0 +1,10 @@ +Ltac foo := idtac. +Ltac bar H := idtac. + +Goal True. +Proof. + Fail foo H. + Fail foo H H'. + Fail bar H H'. + Fail bar H H' H''. +Abort. diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v deleted file mode 100644 index b3e41ab1fb..0000000000 --- a/test-suite/success/qed_export.v +++ /dev/null @@ -1,18 +0,0 @@ -Lemma a : True. -Proof. -assert True as H. - abstract (trivial) using exported_seff. -exact H. -Fail Qed exporting a_subproof. -Qed exporting exported_seff. -Check ( exported_seff : True ). - -Lemma b : True. -Proof. -assert True as H. - abstract (trivial) using exported_seff2. -exact H. -Qed. - -Fail Check ( exported_seff2 : True ). - diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v index 672222bdd6..a4fa544cd9 100644 --- a/test-suite/success/unshelve.v +++ b/test-suite/success/unshelve.v @@ -9,3 +9,11 @@ unshelve (refine (F _ _ _ _)). + exact (@eq_refl bool true). + exact (@eq_refl unit tt). Qed. + +(* This was failing in 8.6, because of ?a:nat being wrongly duplicated *) + +Goal (forall a : nat, a = 0 -> True) -> True. +intros F. +unshelve (eapply (F _);clear F). +2:reflexivity. +Qed. |