diff options
Diffstat (limited to 'test-suite')
35 files changed, 646 insertions, 19 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index ae426f0da..61e75fa5d 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 000000000..5068ed9b9 --- /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 000000000..55ef7abe4 --- /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 000000000..f6598f192 --- /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/5749.v b/test-suite/bugs/closed/5749.v new file mode 100644 index 000000000..81bfe351c --- /dev/null +++ b/test-suite/bugs/closed/5749.v @@ -0,0 +1,18 @@ +(* Checking computation of free vars of a term for generalization *) + +Definition Decision := fun P : Prop => {P} + {~ P}. +Class SetUnfold (P Q : Prop) : Prop := Build_SetUnfold { set_unfold : P <-> Q +}. + +Section Filter_Help. + + Context {A: Type}. + Context (fold_right : forall A B : Type, (B -> A -> A) -> A -> list B -> A). + Definition lType2 := (sigT (fun (P : A -> Prop) => forall a, Decision (P +a))). + Definition test (X: lType2) := let (x, _) := X in x. + + Global Instance foo `{fhl1 : list lType2} m Q: + SetUnfold (Q) + (fold_right _ _ (fun (s : lType2) => let (P, _) := s in and (P +m)) (Q) (fhl1)). diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v new file mode 100644 index 000000000..6d0e21f5d --- /dev/null +++ b/test-suite/bugs/closed/5750.v @@ -0,0 +1,3 @@ +(* Check printability of the hole of the context *) +Goal 0 = 0. +match goal with |- context c [0] => idtac c end. diff --git a/test-suite/bugs/closed/5755.v b/test-suite/bugs/closed/5755.v new file mode 100644 index 000000000..e07fdcf83 --- /dev/null +++ b/test-suite/bugs/closed/5755.v @@ -0,0 +1,16 @@ +(* Sections taking care of let-ins for inductive types *) + +Section Foo. + +Inductive foo (A : Type) (x : A) (y := x) (y : A) := Foo. + +End Foo. + +Section Foo2. + +Variable B : Type. +Variable b : B. +Let c := b. +Inductive foo2 (A : Type) (x : A) (y := x) (y : A) := Foo2 : c=c -> foo2 A x y. + +End Foo2. diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v new file mode 100644 index 000000000..0d0f2eed4 --- /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 000000000..343ab4935 --- /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 000000000..42573aad8 --- /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/complexity/constructor.v b/test-suite/complexity/constructor.v new file mode 100644 index 000000000..c5e195382 --- /dev/null +++ b/test-suite/complexity/constructor.v @@ -0,0 +1,216 @@ +(* Checks that constructor does not repeat the reduction of the conclusion *) +(* Expected time < 3.00s *) + +(* Note: on i7 2.2GZ, time decreases from 85s to 0.1s *) + +Inductive T : bool -> Prop := +| C000 : T true | C001 : T true | C002 : T true | C003 : T true | C004 : T true +| C005 : T true | C006 : T true | C007 : T true | C008 : T true | C009 : T true +| C010 : T true | C011 : T true | C012 : T true | C013 : T true | C014 : T true +| C015 : T true | C016 : T true | C017 : T true | C018 : T true | C019 : T true +| C020 : T true | C021 : T true | C022 : T true | C023 : T true | C024 : T true +| C025 : T true | C026 : T true | C027 : T true | C028 : T true | C029 : T true +| C030 : T true | C031 : T true | C032 : T true | C033 : T true | C034 : T true +| C035 : T true | C036 : T true | C037 : T true | C038 : T true | C039 : T true +| C040 : T true | C041 : T true | C042 : T true | C043 : T true | C044 : T true +| C045 : T true | C046 : T true | C047 : T true | C048 : T true | C049 : T true +| C050 : T true | C051 : T true | C052 : T true | C053 : T true | C054 : T true +| C055 : T true | C056 : T true | C057 : T true | C058 : T true | C059 : T true +| C060 : T true | C061 : T true | C062 : T true | C063 : T true | C064 : T true +| C065 : T true | C066 : T true | C067 : T true | C068 : T true | C069 : T true +| C070 : T true | C071 : T true | C072 : T true | C073 : T true | C074 : T true +| C075 : T true | C076 : T true | C077 : T true | C078 : T true | C079 : T true +| C080 : T true | C081 : T true | C082 : T true | C083 : T true | C084 : T true +| C085 : T true | C086 : T true | C087 : T true | C088 : T true | C089 : T true +| C090 : T true | C091 : T true | C092 : T true | C093 : T true | C094 : T true +| C095 : T true | C096 : T true | C097 : T true | C098 : T true | C099 : T true +| C100 : T true | C101 : T true | C102 : T true | C103 : T true | C104 : T true +| C105 : T true | C106 : T true | C107 : T true | C108 : T true | C109 : T true +| C110 : T true | C111 : T true | C112 : T true | C113 : T true | C114 : T true +| C115 : T true | C116 : T true | C117 : T true | C118 : T true | C119 : T true +| C120 : T true | C121 : T true | C122 : T true | C123 : T true | C124 : T true +| C125 : T true | C126 : T true | C127 : T true | C128 : T true | C129 : T true +| C130 : T true | C131 : T true | C132 : T true | C133 : T true | C134 : T true +| C135 : T true | C136 : T true | C137 : T true | C138 : T true | C139 : T true +| C140 : T true | C141 : T true | C142 : T true | C143 : T true | C144 : T true +| C145 : T true | C146 : T true | C147 : T true | C148 : T true | C149 : T true +| C150 : T true | C151 : T true | C152 : T true | C153 : T true | C154 : T true +| C155 : T true | C156 : T true | C157 : T true | C158 : T true | C159 : T true +| C160 : T true | C161 : T true | C162 : T true | C163 : T true | C164 : T true +| C165 : T true | C166 : T true | C167 : T true | C168 : T true | C169 : T true +| C170 : T true | C171 : T true | C172 : T true | C173 : T true | C174 : T true +| C175 : T true | C176 : T true | C177 : T true | C178 : T true | C179 : T true +| C180 : T true | C181 : T true | C182 : T true | C183 : T true | C184 : T true +| C185 : T true | C186 : T true | C187 : T true | C188 : T true | C189 : T true +| C190 : T true | C191 : T true | C192 : T true | C193 : T true | C194 : T true +| C195 : T true | C196 : T true | C197 : T true | C198 : T true | C199 : T true +| C200 : T true | C201 : T true | C202 : T true | C203 : T true | C204 : T true +| C205 : T true | C206 : T true | C207 : T true | C208 : T true | C209 : T true +| C210 : T true | C211 : T true | C212 : T true | C213 : T true | C214 : T true +| C215 : T true | C216 : T true | C217 : T true | C218 : T true | C219 : T true +| C220 : T true | C221 : T true | C222 : T true | C223 : T true | C224 : T true +| C225 : T true | C226 : T true | C227 : T true | C228 : T true | C229 : T true +| C230 : T true | C231 : T true | C232 : T true | C233 : T true | C234 : T true +| C235 : T true | C236 : T true | C237 : T true | C238 : T true | C239 : T true +| C240 : T true | C241 : T true | C242 : T true | C243 : T true | C244 : T true +| C245 : T true | C246 : T true | C247 : T true | C248 : T true | C249 : T true +| C250 : T true | C251 : T true | C252 : T true | C253 : T true | C254 : T true +| C255 : T true | C256 : T true | C257 : T true | C258 : T true | C259 : T true +| C260 : T true | C261 : T true | C262 : T true | C263 : T true | C264 : T true +| C265 : T true | C266 : T true | C267 : T true | C268 : T true | C269 : T true +| C270 : T true | C271 : T true | C272 : T true | C273 : T true | C274 : T true +| C275 : T true | C276 : T true | C277 : T true | C278 : T true | C279 : T true +| C280 : T true | C281 : T true | C282 : T true | C283 : T true | C284 : T true +| C285 : T true | C286 : T true | C287 : T true | C288 : T true | C289 : T true +| C290 : T true | C291 : T true | C292 : T true | C293 : T true | C294 : T true +| C295 : T true | C296 : T true | C297 : T true | C298 : T true | C299 : T true +| C300 : T true | C301 : T true | C302 : T true | C303 : T true | C304 : T true +| C305 : T true | C306 : T true | C307 : T true | C308 : T true | C309 : T true +| C310 : T true | C311 : T true | C312 : T true | C313 : T true | C314 : T true +| C315 : T true | C316 : T true | C317 : T true | C318 : T true | C319 : T true +| C320 : T true | C321 : T true | C322 : T true | C323 : T true | C324 : T true +| C325 : T true | C326 : T true | C327 : T true | C328 : T true | C329 : T true +| C330 : T true | C331 : T true | C332 : T true | C333 : T true | C334 : T true +| C335 : T true | C336 : T true | C337 : T true | C338 : T true | C339 : T true +| C340 : T true | C341 : T true | C342 : T true | C343 : T true | C344 : T true +| C345 : T true | C346 : T true | C347 : T true | C348 : T true | C349 : T true +| C350 : T true | C351 : T true | C352 : T true | C353 : T true | C354 : T true +| C355 : T true | C356 : T true | C357 : T true | C358 : T true | C359 : T true +| C360 : T true | C361 : T true | C362 : T true | C363 : T true | C364 : T true +| C365 : T true | C366 : T true | C367 : T true | C368 : T true | C369 : T true +| C370 : T true | C371 : T true | C372 : T true | C373 : T true | C374 : T true +| C375 : T true | C376 : T true | C377 : T true | C378 : T true | C379 : T true +| C380 : T true | C381 : T true | C382 : T true | C383 : T true | C384 : T true +| C385 : T true | C386 : T true | C387 : T true | C388 : T true | C389 : T true +| C390 : T true | C391 : T true | C392 : T true | C393 : T true | C394 : T true +| C395 : T true | C396 : T true | C397 : T true | C398 : T true | C399 : T true +| C400 : T true | C401 : T true | C402 : T true | C403 : T true | C404 : T true +| C405 : T true | C406 : T true | C407 : T true | C408 : T true | C409 : T true +| C410 : T true | C411 : T true | C412 : T true | C413 : T true | C414 : T true +| C415 : T true | C416 : T true | C417 : T true | C418 : T true | C419 : T true +| C420 : T true | C421 : T true | C422 : T true | C423 : T true | C424 : T true +| C425 : T true | C426 : T true | C427 : T true | C428 : T true | C429 : T true +| C430 : T true | C431 : T true | C432 : T true | C433 : T true | C434 : T true +| C435 : T true | C436 : T true | C437 : T true | C438 : T true | C439 : T true +| C440 : T true | C441 : T true | C442 : T true | C443 : T true | C444 : T true +| C445 : T true | C446 : T true | C447 : T true | C448 : T true | C449 : T true +| C450 : T true | C451 : T true | C452 : T true | C453 : T true | C454 : T true +| C455 : T true | C456 : T true | C457 : T true | C458 : T true | C459 : T true +| C460 : T true | C461 : T true | C462 : T true | C463 : T true | C464 : T true +| C465 : T true | C466 : T true | C467 : T true | C468 : T true | C469 : T true +| C470 : T true | C471 : T true | C472 : T true | C473 : T true | C474 : T true +| C475 : T true | C476 : T true | C477 : T true | C478 : T true | C479 : T true +| C480 : T true | C481 : T true | C482 : T true | C483 : T true | C484 : T true +| C485 : T true | C486 : T true | C487 : T true | C488 : T true | C489 : T true +| C490 : T true | C491 : T true | C492 : T true | C493 : T true | C494 : T true +| C495 : T true | C496 : T true | C497 : T true | C498 : T true | C499 : T true +| C500 : T true | C501 : T true | C502 : T true | C503 : T true | C504 : T true +| C505 : T true | C506 : T true | C507 : T true | C508 : T true | C509 : T true +| C510 : T true | C511 : T true | C512 : T true | C513 : T true | C514 : T true +| C515 : T true | C516 : T true | C517 : T true | C518 : T true | C519 : T true +| C520 : T true | C521 : T true | C522 : T true | C523 : T true | C524 : T true +| C525 : T true | C526 : T true | C527 : T true | C528 : T true | C529 : T true +| C530 : T true | C531 : T true | C532 : T true | C533 : T true | C534 : T true +| C535 : T true | C536 : T true | C537 : T true | C538 : T true | C539 : T true +| C540 : T true | C541 : T true | C542 : T true | C543 : T true | C544 : T true +| C545 : T true | C546 : T true | C547 : T true | C548 : T true | C549 : T true +| C550 : T true | C551 : T true | C552 : T true | C553 : T true | C554 : T true +| C555 : T true | C556 : T true | C557 : T true | C558 : T true | C559 : T true +| C560 : T true | C561 : T true | C562 : T true | C563 : T true | C564 : T true +| C565 : T true | C566 : T true | C567 : T true | C568 : T true | C569 : T true +| C570 : T true | C571 : T true | C572 : T true | C573 : T true | C574 : T true +| C575 : T true | C576 : T true | C577 : T true | C578 : T true | C579 : T true +| C580 : T true | C581 : T true | C582 : T true | C583 : T true | C584 : T true +| C585 : T true | C586 : T true | C587 : T true | C588 : T true | C589 : T true +| C590 : T true | C591 : T true | C592 : T true | C593 : T true | C594 : T true +| C595 : T true | C596 : T true | C597 : T true | C598 : T true | C599 : T true +| C600 : T true | C601 : T true | C602 : T true | C603 : T true | C604 : T true +| C605 : T true | C606 : T true | C607 : T true | C608 : T true | C609 : T true +| C610 : T true | C611 : T true | C612 : T true | C613 : T true | C614 : T true +| C615 : T true | C616 : T true | C617 : T true | C618 : T true | C619 : T true +| C620 : T true | C621 : T true | C622 : T true | C623 : T true | C624 : T true +| C625 : T true | C626 : T true | C627 : T true | C628 : T true | C629 : T true +| C630 : T true | C631 : T true | C632 : T true | C633 : T true | C634 : T true +| C635 : T true | C636 : T true | C637 : T true | C638 : T true | C639 : T true +| C640 : T true | C641 : T true | C642 : T true | C643 : T true | C644 : T true +| C645 : T true | C646 : T true | C647 : T true | C648 : T true | C649 : T true +| C650 : T true | C651 : T true | C652 : T true | C653 : T true | C654 : T true +| C655 : T true | C656 : T true | C657 : T true | C658 : T true | C659 : T true +| C660 : T true | C661 : T true | C662 : T true | C663 : T true | C664 : T true +| C665 : T true | C666 : T true | C667 : T true | C668 : T true | C669 : T true +| C670 : T true | C671 : T true | C672 : T true | C673 : T true | C674 : T true +| C675 : T true | C676 : T true | C677 : T true | C678 : T true | C679 : T true +| C680 : T true | C681 : T true | C682 : T true | C683 : T true | C684 : T true +| C685 : T true | C686 : T true | C687 : T true | C688 : T true | C689 : T true +| C690 : T true | C691 : T true | C692 : T true | C693 : T true | C694 : T true +| C695 : T true | C696 : T true | C697 : T true | C698 : T true | C699 : T true +| C700 : T true | C701 : T true | C702 : T true | C703 : T true | C704 : T true +| C705 : T true | C706 : T true | C707 : T true | C708 : T true | C709 : T true +| C710 : T true | C711 : T true | C712 : T true | C713 : T true | C714 : T true +| C715 : T true | C716 : T true | C717 : T true | C718 : T true | C719 : T true +| C720 : T true | C721 : T true | C722 : T true | C723 : T true | C724 : T true +| C725 : T true | C726 : T true | C727 : T true | C728 : T true | C729 : T true +| C730 : T true | C731 : T true | C732 : T true | C733 : T true | C734 : T true +| C735 : T true | C736 : T true | C737 : T true | C738 : T true | C739 : T true +| C740 : T true | C741 : T true | C742 : T true | C743 : T true | C744 : T true +| C745 : T true | C746 : T true | C747 : T true | C748 : T true | C749 : T true +| C750 : T true | C751 : T true | C752 : T true | C753 : T true | C754 : T true +| C755 : T true | C756 : T true | C757 : T true | C758 : T true | C759 : T true +| C760 : T true | C761 : T true | C762 : T true | C763 : T true | C764 : T true +| C765 : T true | C766 : T true | C767 : T true | C768 : T true | C769 : T true +| C770 : T true | C771 : T true | C772 : T true | C773 : T true | C774 : T true +| C775 : T true | C776 : T true | C777 : T true | C778 : T true | C779 : T true +| C780 : T true | C781 : T true | C782 : T true | C783 : T true | C784 : T true +| C785 : T true | C786 : T true | C787 : T true | C788 : T true | C789 : T true +| C790 : T true | C791 : T true | C792 : T true | C793 : T true | C794 : T true +| C795 : T true | C796 : T true | C797 : T true | C798 : T true | C799 : T true +| C800 : T true | C801 : T true | C802 : T true | C803 : T true | C804 : T true +| C805 : T true | C806 : T true | C807 : T true | C808 : T true | C809 : T true +| C810 : T true | C811 : T true | C812 : T true | C813 : T true | C814 : T true +| C815 : T true | C816 : T true | C817 : T true | C818 : T true | C819 : T true +| C820 : T true | C821 : T true | C822 : T true | C823 : T true | C824 : T true +| C825 : T true | C826 : T true | C827 : T true | C828 : T true | C829 : T true +| C830 : T true | C831 : T true | C832 : T true | C833 : T true | C834 : T true +| C835 : T true | C836 : T true | C837 : T true | C838 : T true | C839 : T true +| C840 : T true | C841 : T true | C842 : T true | C843 : T true | C844 : T true +| C845 : T true | C846 : T true | C847 : T true | C848 : T true | C849 : T true +| C850 : T true | C851 : T true | C852 : T true | C853 : T true | C854 : T true +| C855 : T true | C856 : T true | C857 : T true | C858 : T true | C859 : T true +| C860 : T true | C861 : T true | C862 : T true | C863 : T true | C864 : T true +| C865 : T true | C866 : T true | C867 : T true | C868 : T true | C869 : T true +| C870 : T true | C871 : T true | C872 : T true | C873 : T true | C874 : T true +| C875 : T true | C876 : T true | C877 : T true | C878 : T true | C879 : T true +| C880 : T true | C881 : T true | C882 : T true | C883 : T true | C884 : T true +| C885 : T true | C886 : T true | C887 : T true | C888 : T true | C889 : T true +| C890 : T true | C891 : T true | C892 : T true | C893 : T true | C894 : T true +| C895 : T true | C896 : T true | C897 : T true | C898 : T true | C899 : T true +| C900 : T true | C901 : T true | C902 : T true | C903 : T true | C904 : T true +| C905 : T true | C906 : T true | C907 : T true | C908 : T true | C909 : T true +| C910 : T true | C911 : T true | C912 : T true | C913 : T true | C914 : T true +| C915 : T true | C916 : T true | C917 : T true | C918 : T true | C919 : T true +| C920 : T true | C921 : T true | C922 : T true | C923 : T true | C924 : T true +| C925 : T true | C926 : T true | C927 : T true | C928 : T true | C929 : T true +| C930 : T true | C931 : T true | C932 : T true | C933 : T true | C934 : T true +| C935 : T true | C936 : T true | C937 : T true | C938 : T true | C939 : T true +| C940 : T true | C941 : T true | C942 : T true | C943 : T true | C944 : T true +| C945 : T true | C946 : T true | C947 : T true | C948 : T true | C949 : T true +| C950 : T true | C951 : T true | C952 : T true | C953 : T true | C954 : T true +| C955 : T true | C956 : T true | C957 : T true | C958 : T true | C959 : T true +| C960 : T true | C961 : T true | C962 : T true | C963 : T true | C964 : T true +| C965 : T true | C966 : T true | C967 : T true | C968 : T true | C969 : T true +| C970 : T true | C971 : T true | C972 : T true | C973 : T true | C974 : T true +| C975 : T true | C976 : T true | C977 : T true | C978 : T true | C979 : T true +| C980 : T true | C981 : T true | C982 : T true | C983 : T true | C984 : T true +| C985 : T true | C986 : T true | C987 : T true | C988 : T true | C989 : T true +| C990 : T true | C991 : T true | C992 : T true | C993 : T true | C994 : T true +| C995 : T true | C996 : T true | C997 : T true | C998 : T true | C999 : T true +| C1000 : T false. + +Fixpoint expand (n : nat) : Prop := + match n with + | O => T false + | S n => expand n + end. + +Example Expand : expand 2500. +Time constructor. (* ~0.45 secs *) diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 803fe8029..c4bd11c57 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 000000000..f0b5e4f7e --- /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 000000000..6428b10ff --- /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 000000000..039d1e500 --- /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 000000000..ccb12076a --- /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 000000000..14c5713f6 --- /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 000000000..640f9ea7f --- /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 000000000..7a0fd777c --- /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 000000000..786df9891 --- /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 000000000..d01507bf7 --- /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 000000000..901c9074f --- /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 000000000..13e264c09 --- /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 000000000..f43a2d657 --- /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 000000000..e7fd25c0d --- /dev/null +++ b/test-suite/misc/deps/αβ/εζ.v @@ -0,0 +1 @@ +Require Import γδ. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 128bc7767..904ff68aa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,3 +4,9 @@ bar@{u} = nat *) bar is universe polymorphic +foo@{u Top.8 v} = +Type@{Top.8} -> Type@{v} -> Type@{u} + : Type@{max(u+1, Top.8+1, v+1)} +(* u Top.8 v |= *) + +foo is universe polymorphic diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index d9e89e43c..8656ff1a3 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,7 +1,13 @@ Set Universe Polymorphism. Set Printing Universes. +Unset Strict Universe Declaration. Class Wrap A := wrap : A. Instance bar@{u} : Wrap@{u} Set. Proof nat. Print bar. + +(* The universes in the binder come first, then the extra universes in + order of appearance. *) +Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. +Print foo. diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out index a5b55a999..2761b87b0 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 a77b7b82e..92917cdfc 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 000000000..77e799d35 --- /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 000000000..4caf619fe --- /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/Inductive.v b/test-suite/success/Inductive.v index f746def5c..06f807f29 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -183,3 +183,20 @@ Module PolyNoLowerProp. Fail Check Foo True : Prop. End PolyNoLowerProp. + +(* Test building of elimination scheme with noth let-ins and + non-recursively uniform parameters *) + +Module NonRecLetIn. + + Unset Implicit Arguments. + + Inductive Ind (b:=2) (a:nat) (c:=1) : Type := + | Base : Ind a + | Rec : Ind (S a) -> Ind a. + + Check Ind_rect (fun n (b:Ind n) => b = b) + (fun n => eq_refl) + (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). + +End NonRecLetIn. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index ecc988507..7eaafc354 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -156,6 +156,52 @@ Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d. End structures. + +Module binders. + + Definition mynat@{|} := nat. + + Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}. + exact A. + Defined. + + Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). + exact A. + Fail Defined. + Abort. + + Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). + exact A. + Defined. + + Check moreu@{_ _ _ _}. + + Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A. + + (* By default constraints are extensible *) + Polymorphic Definition morec@{i j} (A : Type@{i}) : Type@{j} := A. + Check morec@{_ _}. + + (* Handled in proofs as well *) + Lemma bar@{i j | } : Type@{i}. + exact Type@{j}. + Fail Defined. + Abort. + + Lemma bar@{i j| i < j} : Type@{j}. + Proof. + exact Type@{i}. + Qed. + + Lemma barext@{i j|+} : Type@{j}. + Proof. + exact Type@{i}. + Qed. + +End binders. + Section cats. Local Set Universe Polymorphism. Require Import Utf8. diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v deleted file mode 100644 index b3e41ab1f..000000000 --- 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 672222bdd..a4fa544cd 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. |