diff options
Diffstat (limited to 'test-suite')
32 files changed, 253 insertions, 47 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 928a77cb8e..1db97f43c5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -187,14 +187,6 @@ summary.log: $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" -# if not on travis we can get the log files (they're just there for a -# local build, and downloadable on GitLab) -PRINT_LOGS?= -TRAVIS?= # special because we want to print travis_fold directives -ifdef APPVEYOR -PRINT_LOGS:=APPVEYOR -endif #APPVEYOR - report: summary.log $(HIDE)bash report.sh diff --git a/test-suite/bugs/closed/bug_2001.v b/test-suite/bugs/closed/bug_2001.v index 652c65706a..31c62b7b36 100644 --- a/test-suite/bugs/closed/bug_2001.v +++ b/test-suite/bugs/closed/bug_2001.v @@ -1,12 +1,10 @@ (* Automatic computing of guard in "Theorem with"; check that guard is not computed when the user explicitly indicated it *) -Unset Automatic Introduction. - Inductive T : Set := | v : T. -Definition f (s:nat) (t:T) : nat. +Definition f : forall (s:nat) (t:T), nat. fix f 2. intros s t. refine diff --git a/test-suite/bugs/closed/bug_4771.v b/test-suite/bugs/closed/bug_4771.v new file mode 100644 index 0000000000..e25e5a1be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_4771.v @@ -0,0 +1,21 @@ +(* The following code used to trigger an anomaly in functor substitutions *) + +Module Type Foo. + +Parameter Inline t : nat. + +End Foo. + +Module F(X : Foo). + +Tactic Notation "foo" ref(x) := idtac. + +Ltac g := foo X.t. + +End F. + +Module N. +Definition t := 0 + 0. +End N. + +Module K := F(N). diff --git a/test-suite/bugs/closed/gh6165.v b/test-suite/bugs/closed/bug_6165.v index b87a7caaf2..b87a7caaf2 100644 --- a/test-suite/bugs/closed/gh6165.v +++ b/test-suite/bugs/closed/bug_6165.v diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/bug_6384.v index cec84642fb..cec84642fb 100644 --- a/test-suite/bugs/closed/gh6384.v +++ b/test-suite/bugs/closed/bug_6384.v diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/bug_6385.v index 3bbb664f4f..3bbb664f4f 100644 --- a/test-suite/bugs/closed/gh6385.v +++ b/test-suite/bugs/closed/bug_6385.v diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v index e88a3704d8..28a9ffc7bd 100644 --- a/test-suite/bugs/closed/bug_6661.v +++ b/test-suite/bugs/closed/bug_6661.v @@ -53,8 +53,6 @@ Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. exact x. Defined. -Unset Automatic Introduction. - Definition idfun (T : UU) := λ t:T, t. Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. diff --git a/test-suite/bugs/closed/bug_8224.v b/test-suite/bugs/closed/bug_8224.v new file mode 100644 index 0000000000..42dd47d48c --- /dev/null +++ b/test-suite/bugs/closed/bug_8224.v @@ -0,0 +1,9 @@ +(* Checking that terms are evar-free before being grounded *) + +(* This used to raise an anomaly in 8.9 beta *) + +Fail Fixpoint restrict f n := + match n with + | O => nil + | S n => cons (f n) (restrict f n) + end. diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v new file mode 100644 index 0000000000..9be1936cdf --- /dev/null +++ b/test-suite/bugs/closed/bug_8791.v @@ -0,0 +1,9 @@ +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. + +Definition A := 42. + +Instance foo (A: Type): Inhabited (list A). +Check A. +Abort. + +Fail Instance foo (A : nat) (A : Type) : Inhabited nat. diff --git a/test-suite/bugs/closed/bug_8885.v b/test-suite/bugs/closed/bug_8885.v new file mode 100644 index 0000000000..9d86c08d71 --- /dev/null +++ b/test-suite/bugs/closed/bug_8885.v @@ -0,0 +1,8 @@ +From Coq Require Import Cyclic31. + +Definition Nat `(int31) := nat. +Definition Zero (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _: digits) := 0. + +Check (eq_refl (int31_rect Nat Zero 1) : 0 = 0). +Check (eq_refl (int31_rect Nat Zero 1) <: 0 = 0). +Check (eq_refl (int31_rect Nat Zero 1) <<: 0 = 0). diff --git a/test-suite/bugs/closed/bug_8908.v b/test-suite/bugs/closed/bug_8908.v new file mode 100644 index 0000000000..9c85839b75 --- /dev/null +++ b/test-suite/bugs/closed/bug_8908.v @@ -0,0 +1,8 @@ +Record foo : Type := + { fooA : Type; fooB : Type }. +Definition id {A : Type} (a : A) := a. +Definition untypable : Type. + unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y). + exact foo. + constructor. exact unit. exact unit. +Defined. diff --git a/test-suite/coq-makefile/camldep/_CoqProject b/test-suite/coq-makefile/camldep/_CoqProject new file mode 100644 index 0000000000..0b7ebd14e4 --- /dev/null +++ b/test-suite/coq-makefile/camldep/_CoqProject @@ -0,0 +1,4 @@ +-Q . Foo +-I src +src/file1.mlg +src/file2.ml diff --git a/test-suite/coq-makefile/camldep/run.sh b/test-suite/coq-makefile/camldep/run.sh new file mode 100755 index 0000000000..aa62ee56eb --- /dev/null +++ b/test-suite/coq-makefile/camldep/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +set -e +export PATH=$COQBIN:$PATH +export LC_ALL=C + +rm -rf _test +mkdir _test +cp _CoqProject _test/ +cd _test +mkdir src + +echo '{ let foo = () }' > src/file1.mlg +echo 'let bar = File1.foo' > src/file2.ml +coq_makefile -f _CoqProject -o Makefile +make src/file2.cmx +[ -f src/file2.cmx ] diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 6d8ce7c5d7..047f4cd080 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -15,7 +15,7 @@ let evil t f = let tc = mkConst tc in let fe = Declare.definition_entry - ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) ~types:(Term.mkArrow tc tu) (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) in diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh new file mode 100755 index 0000000000..96bdee2fc2 --- /dev/null +++ b/test-suite/misc/quick-include.sh @@ -0,0 +1,5 @@ +#!/bin/sh +set -e + +$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v +$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v diff --git a/test-suite/misc/quick-include/file1.v b/test-suite/misc/quick-include/file1.v new file mode 100644 index 0000000000..fa48e240cb --- /dev/null +++ b/test-suite/misc/quick-include/file1.v @@ -0,0 +1,18 @@ + +Module Type E. End E. + +Module M. + Lemma x : True. + Proof. trivial. Qed. +End M. + + +Module Type T. + Lemma x : True. + Proof. trivial. Qed. +End T. + +Module F(A:E). + Lemma x : True. + Proof. trivial. Qed. +End F. diff --git a/test-suite/misc/quick-include/file2.v b/test-suite/misc/quick-include/file2.v new file mode 100644 index 0000000000..ab10dfd8de --- /dev/null +++ b/test-suite/misc/quick-include/file2.v @@ -0,0 +1,6 @@ + +From QuickInclude Require file1. + +Module M. Include file1.M. End M. +Module T. Include file1.T. End T. +Module F. Include file1.F. End F. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 46784d1897..d25ad5dca8 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -17,3 +17,7 @@ end : Expr -> Expr [(1 + 1)] : Expr +Let "x" e1 e2 + : expr +Let "x" e1 e2 + : expr diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 6bdbf1bed5..7800e91ee5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -70,3 +70,27 @@ Notation "( x )" := x (in custom expr at level 0, x at level 2). Check [1 + 1]. End C. + +(* An example of interaction between coercion and notations from + Robbert Krebbers. *) + +Require Import String. + +Module D. + +Inductive expr := + | Var : string -> expr + | Lam : string -> expr -> expr + | App : expr -> expr -> expr. + +Notation Let x e1 e2 := (App (Lam x e2) e1). + +Parameter e1 e2 : expr. + +Check (Let "x" e1 e2). + +Coercion App : expr >-> Funclass. + +Check (Let "x" e1 e2). + +End D. diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out new file mode 100644 index 0000000000..c42e15e4e8 --- /dev/null +++ b/test-suite/output/PrintUnivsSubgraph.out @@ -0,0 +1,5 @@ +Prop < Set +Set < i + < j +i < j + diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v new file mode 100644 index 0000000000..ec9cf44d4f --- /dev/null +++ b/test-suite/output/PrintUnivsSubgraph.v @@ -0,0 +1,9 @@ + +Universes i j k l. + +Definition foo : Type@{j} := Type@{i}. + +Definition baz : Type@{k} := Type@{l}. + +Print Universes Subgraph(i j). +(* should print [i < j], not [l < k] (and not prelude universes) *) diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 49c292c501..4d3f7419e6 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -41,8 +41,7 @@ Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] Polymorphic bar@{u} = nat : Wrap@{u} Set -(* u |= Set < u - *) +(* u |= Set < u *) bar is universe polymorphic Polymorphic foo@{u UnivBinders.17 v} = @@ -79,8 +78,9 @@ mono The command has indeed failed with message: Universe u already exists. Monomorphic bobmorane = -let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(tt.u,ff.u)} +let tt := Type@{UnivBinders.32} in +let ff := Type@{UnivBinders.34} in tt -> ff + : Type@{max(UnivBinders.31,UnivBinders.33)} bobmorane is not universe polymorphic The command has indeed failed with message: @@ -150,6 +150,11 @@ Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} For inseccstr: Argument scope is [type_scope] +Polymorphic insec2@{u} = Prop + : Type@{Set+1} +(* u |= *) + +insec2 is universe polymorphic Polymorphic inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) @@ -171,26 +176,26 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i UnivBinders.55 UnivBinders.56} : -Type@{UnivBinders.55} -> Type@{i} -(* i UnivBinders.55 UnivBinders.56 |= *) +axfoo@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.56} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.55 UnivBinders.56} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.55 UnivBinders.56 |= *) +axbar@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i} +axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i} +axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 56474a0723..582a5e969a 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,4 +1,5 @@ -(* coq-prog-args: ("-top" "UnivBinders") *) +(* -*- coq-prog-args: ("-top" "UnivBinders"); -*- *) + Set Universe Polymorphism. Set Printing Universes. (* Unset Strict Universe Declaration. *) @@ -73,19 +74,10 @@ Module SecLet. (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) Unset Strict Universe Declaration. Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) - Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *) + Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) Definition bobmorane := tt -> ff. End foo. - Print bobmorane. (* - bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} = - let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(UnivBinders.15,ff.u)} - (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15 - ff.v < ff.u - *) - - bobmorane is universe polymorphic - *) + Print bobmorane. End SecLet. (* fun x x => foo is nonsense with local binders *) @@ -130,6 +122,12 @@ End SomeSec. Print insec. Print insecind. +Section SomeSec2. + Universe u. + Definition insec2@{} := Prop. +End SomeSec2. +Print insec2. + Module SomeMod. Definition inmod@{u} := Type@{u}. Print inmod. diff --git a/test-suite/report.sh b/test-suite/report.sh index 05f39b4b02..c5e698232f 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -24,7 +24,7 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$TRAVIS" ] || [ -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 @@ -40,12 +40,13 @@ if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then else printf '\n' fi done + printed_logs=1 fi if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; - if [ -z "$TRAVIS" ] && [ -z "$PRINT_LOGS" ]; then + if [ -z "$printed_logs" ]; then echo 'To print details of failed tests, rerun with environment variable PRINT_LOGS=1' echo 'eg "make report PRINT_LOGS=1" from the test suite directory"' echo 'See README.md in the test suite directory for more information.' diff --git a/test-suite/ssr/case_TC.v b/test-suite/ssr/case_TC.v new file mode 100644 index 0000000000..78ed374432 --- /dev/null +++ b/test-suite/ssr/case_TC.v @@ -0,0 +1,18 @@ +From Coq Require Import ssreflect. +From Coq Require Import ssrbool. + +Set Printing All. +Set Debug Ssreflect. + +Class Class := { sort : Type ; op : sort -> bool }. +Coercion sort : Class >-> Sortclass. +Arguments op [_] _. + +Section Section. + Context (A B: Class) (a: A). + + Goal op a || ~~ op a. + by case: op. + Abort. + +End Section. diff --git a/test-suite/ssr/case_TC2.v b/test-suite/ssr/case_TC2.v new file mode 100644 index 0000000000..37504d662d --- /dev/null +++ b/test-suite/ssr/case_TC2.v @@ -0,0 +1,20 @@ +From Coq Require Import Bool ssreflect. + +Set Printing All. +Set Debug Ssreflect. + +Class Class := { sort : Type ; op : sort -> bool }. +Coercion sort : Class >-> Sortclass. +Arguments op [_] _. + +Lemma opP (A: Class) (a: A) : reflect True (op a). +Proof. Admitted. + +Section Section. + Context (A B: Class) (a: A). + + Goal is_true (op a). + by case: opP. + Abort. + +End Section. diff --git a/test-suite/ssr/case_TC3.v b/test-suite/ssr/case_TC3.v new file mode 100644 index 0000000000..92e166e85d --- /dev/null +++ b/test-suite/ssr/case_TC3.v @@ -0,0 +1,21 @@ +From Coq Require Import Utf8 Bool ssreflect. + +Set Printing All. +Set Debug Ssreflect. + +Class Class sort := { op : sort → bool }. +Arguments op {_ _}. +Hint Mode Class !. + +Lemma opP A (C: Class A) (a: A) : reflect True (op a). +Proof. Admitted. +Arguments op {_ _}. + +Section Section. + Context A B (CA : Class A) (CB : Class B) (a: A). + + Goal is_true (op a). + by case: opP. + Abort. + +End Section. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index efb32ef6f7..81c9763ccd 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -50,8 +50,6 @@ End folding. (* Check definition by tactics *) -Set Automatic Introduction. - Inductive even : nat -> Type := | even_O : even 0 | even_S : forall n, odd n -> even (S n) diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v index f851d8c7d9..de5987c4f7 100644 --- a/test-suite/success/Require.v +++ b/test-suite/success/Require.v @@ -1,3 +1,8 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) + Require Import Coq.Arith.Plus. Require Coq.Arith.Minus. Locate Library Coq.Arith.Minus. + +(* Check that Init didn't get exported by the import above *) +Fail Check nat. diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v index 0a0812711c..1140a537fc 100644 --- a/test-suite/success/autointros.v +++ b/test-suite/success/autointros.v @@ -1,5 +1,3 @@ -Set Automatic Introduction. - Inductive even : nat -> Prop := | even_0 : even 0 | even_odd : forall n, odd n -> even (S n) diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v index 7c298c98b6..1bc565cbb5 100644 --- a/test-suite/success/unidecls.v +++ b/test-suite/success/unidecls.v @@ -1,4 +1,4 @@ -(* coq-prog-args: ("-top" "unidecls") *) +(* -*- coq-prog-args: ("-top" "unidecls"); -*- *) Set Printing Universes. Module decls. @@ -46,12 +46,12 @@ Universe secfoo. Section Foo'. Fail Universe secfoo. Universe secfoo2. - Check Type@{Foo'.secfoo2}. + Fail Check Type@{Foo'.secfoo2}. + Check Type@{secfoo2}. Constraint secfoo2 < a. End Foo'. Check Type@{secfoo2}. -Fail Check Type@{Foo'.secfoo2}. Fail Check eq_refl : Type@{secfoo2} = Type@{a}. (** Below, u and v are global, fixed universes *) diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index 526cefec44..7f9e6cc6e0 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -71,6 +71,13 @@ let _ = add_test "tokenize_string examples" t open Pp +(* example that was failing from #8922 *) +let t () = + Proof_diffs.write_diffs_option "removed"; + ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1"); + Proof_diffs.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, e.g. str " a" ++ str "b " will give a token "ab" *) (* checks background is present and correct *) |