diff options
Diffstat (limited to 'test-suite')
26 files changed, 298 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 78d90aad8..ae426f0da 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -85,8 +85,10 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed +INTERACTIVE := interactive + VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ - output-modulo-time interactive micromega $(COMPLEXITY) modules stm \ + output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc # All subsystems diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v new file mode 100644 index 000000000..77bf169e1 --- /dev/null +++ b/test-suite/bugs/closed/5245.v @@ -0,0 +1,18 @@ +Set Primitive Projections. + +Record foo := Foo { + foo_car : Type; + foo_rel : foo_car -> foo_car -> Prop +}. +Arguments foo_rel : simpl never. + +Definition foo_fun {A B} := Foo (A -> B) (fun f g => forall x, f x = g x). + +Goal @foo_rel foo_fun (fun x : nat => x) (fun x => x). +Proof. +intros x; exact eq_refl. +Undo. +progress hnf; intros; exact eq_refl. +Undo. +unfold foo_rel. intros x. exact eq_refl. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5434.v b/test-suite/bugs/closed/5434.v new file mode 100644 index 000000000..5d2460fac --- /dev/null +++ b/test-suite/bugs/closed/5434.v @@ -0,0 +1,18 @@ +(* About binders which remain unnamed after typing *) + +Global Set Asymmetric Patterns. + +Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : +@sig A P) : @sig A Q + := let 'exist a p := x in exist Q a (f a p). +Axioms (feBW' : Type) (g : Prop -> Prop) (f' : feBW' -> Prop). +Definition foo := @proj2_sig_map feBW' (fun H => True = f' _) (fun H => + g True = g (f' H)) + (fun (a : feBW') (p : (fun H : feBW' => True = + f' H) a) => @f_equal Prop Prop g True (f' a) p). +Print foo. +Goal True. + lazymatch type of foo with + | sig (fun a : ?A => ?P) -> _ + => pose (fun a : A => a = a /\ P = P) + end. diff --git a/test-suite/bugs/closed/5683.v b/test-suite/bugs/closed/5683.v new file mode 100644 index 000000000..b5c6a48ec --- /dev/null +++ b/test-suite/bugs/closed/5683.v @@ -0,0 +1,71 @@ +Require Import Program.Tactics. +Require Import FunctionalExtensionality. + +Inductive Succ A := +| Succ_O : Succ A +| Succ_S : A -> Succ A. +Arguments Succ_O {A}. +Arguments Succ_S {A} _. + +Inductive Zero : Type :=. + +Inductive ty := +| ty_nat : ty +| ty_arr : ty -> ty -> ty. + +Inductive term A := +| term_abs : ty -> term (Succ A) -> term A +| term_app : term A -> term A -> term A +| term_var : A -> term A +| term_nat : nat -> term A. +Arguments term_abs {A} _ _. +Arguments term_app {A} _ _. +Arguments term_var {A} _. +Arguments term_nat {A} _. + +Class Functor F := +{ + ret : forall {A}, A -> F A; + fmap : forall {A B}, (A -> B) -> F A -> F B; + fmap_id : forall {A} (fa : F A), fmap (@id A) fa = fa; + fmap_compose : forall {A B C} (fa : F A) (g : B -> C) (h : A -> B), fmap (fun +a => g (h a)) fa = fmap g (fmap h fa) +}. + +Class Monad M `{Functor M} := +{ + bind : forall {A B}, M A -> (A -> M B) -> M B; + ret_left_id : forall {A B} (a : A) (f : A -> M B), bind (ret a) f = f a; + ret_right_id : forall {A} (m : M A), bind m ret = m; + bind_assoc : forall {A B C} (m : M A) (f : A -> M B) (g : B -> M C), bind +(bind m f) g = bind m (fun x => bind (f x) g) +}. + +Instance Succ_Functor : Functor Succ. +Proof. + unshelve econstructor. + - intros A B f fa. + destruct fa. + + apply Succ_O. + + apply Succ_S. tauto. + - intros. apply Succ_S. assumption. + - intros A [|a]; reflexivity. + - intros A B C [|a] g h; reflexivity. +Defined. + +(* Anomaly: Not an arity *) +Program Fixpoint term_bind {A B} (tm : term A) (f : A -> term B) : term B := + let Succ_f (var : Succ A) := + match var with + | Succ_O => term_var Succ_O + | Succ_S var' => _ + end in + match tm with + | term_app tm1 tm2 => term_app (term_bind tm1 f) (term_bind tm2 f) + | term_abs ty body => term_abs ty (term_bind body Succ_f) + | term_var a => f a + | term_nat n => term_nat n + end. +Next Obligation. + intros. +Admitted. diff --git a/test-suite/bugs/closed/5697.v b/test-suite/bugs/closed/5697.v new file mode 100644 index 000000000..c653f992a --- /dev/null +++ b/test-suite/bugs/closed/5697.v @@ -0,0 +1,19 @@ +Set Primitive Projections. + +Record foo : Type := Foo { foo_car: nat }. + +Goal forall x y : nat, x <> y -> Foo x <> Foo y. +Proof. +intros. +intros H'. +congruence. +Qed. + +Record bar (A : Type) : Type := Bar { bar_car: A }. + +Goal forall x y : nat, x <> y -> Bar nat x <> Bar nat y. +Proof. +intros. +intros H'. +congruence. +Qed. diff --git a/test-suite/bugs/closed/5713.v b/test-suite/bugs/closed/5713.v new file mode 100644 index 000000000..9daf9647f --- /dev/null +++ b/test-suite/bugs/closed/5713.v @@ -0,0 +1,15 @@ +(* Checking that classical_right/classical_left work in an empty context *) + +Require Import Classical. + +Parameter A:Prop. + +Goal A \/ ~A. +classical_right. +assumption. +Qed. + +Goal ~A \/ A. +classical_left. +assumption. +Qed. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 1feff7479..dc5a500db 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 1feff7479..dc5a500db 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local new file mode 100644 index 000000000..0f4a7d995 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package foo diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META new file mode 100644 index 000000000..ff5f1c7c9 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/META @@ -0,0 +1,4 @@ +archive(byte)="foo.cma" +archive(native)="foo.cmxa" +linkopts="-linkall" +requires="str" diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile new file mode 100644 index 000000000..1615bfd06 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile @@ -0,0 +1,14 @@ +-include ../../Makefile.conf + +CO="$(COQMF_OCAMLFIND)" opt +CB="$(COQMF_OCAMLFIND)" ocamlc + +all: + $(CO) -c foolib.ml + $(CO) -a foolib.cmx -o foo.cmxa + $(CB) -c foolib.ml + $(CB) -a foolib.cmo -o foo.cma + $(CB) -c foo.mli # empty .mli file, to be understood + +clean: + rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml new file mode 100644 index 000000000..81306fb89 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml @@ -0,0 +1,2 @@ +let foo () = + assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3) diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh new file mode 100755 index 000000000..5b24df639 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +if which cygpath 2>/dev/null; then + # the only way I found to pass OCAMLPATH on win is to have it contain + # only one entry + export OCAMLPATH=`cygpath -w $PWD/findlib` +fi +make -C findlib/foo clean +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +cat Makefile.local +make -C findlib/foo +make +make byte diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 51669f28f..03df9cf05 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 51669f28f..03df9cf05 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 3bec11cb7..89bafe9ad 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -18,6 +18,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out new file mode 100644 index 000000000..0e05660d6 --- /dev/null +++ b/test-suite/coqdoc/bug5700.html.out @@ -0,0 +1,50 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug5700</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug5700</h1> + +<div class="code"> +</div> + +<div class="doc"> +<pre>foo (* bar *) </pre> + +</div> +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="const1"><span class="id" title="definition">const1</span></a> := 1.<br/> + +<br/> +</div> + +<div class="doc"> +<pre>more (* nested (* comments *) within verbatim *) </pre> + +</div> +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="const2"><span class="id" title="definition">const2</span></a> := 2.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out new file mode 100644 index 000000000..33990cb89 --- /dev/null +++ b/test-suite/coqdoc/bug5700.tex.out @@ -0,0 +1,24 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug5700}{Library }{Coqdoc.bug5700} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{verbatim}foo (* bar *) \end{verbatim} + \begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol +\coqdocemptyline +\end{coqdoccode} +\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} + \begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v new file mode 100644 index 000000000..839034a48 --- /dev/null +++ b/test-suite/coqdoc/bug5700.v @@ -0,0 +1,5 @@ +(** << foo (* bar *) >> *) +Definition const1 := 1. + +(** << more (* nested (* comments *) within verbatim *) >> *) +Definition const2 := 2. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 9d106d2da..7bcd7b041 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with | 1 => 1 end = p : forall x : nat, x = x -> Prop +bar 0 + : nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b9985a594..fe6c05c39 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. +(* Check bug 5693 *) + +Module M. +Definition A := 0. +Definition bar (a b : nat) := plus a b. +Notation "" := A (format "", only printing). +Check (bar A 0). +End M. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e5dbfcb4b..65efe228a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -122,3 +122,5 @@ return (1, 2, 3, 4) : nat * nat * nat * nat {{ 1 | 1 // 1 }} : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b1015137d..ea372ad1a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4). Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). 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. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 837f2efd0..4d04f2cf9 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -142,3 +142,8 @@ Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing). Reserved Notation "x === y" (at level 50). Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x where "x === y" := (EQ x y). + +(* Check that strictly ident or _ are coerced to a name *) + +Fail Check {x@{u},y|x=x}. +Fail Check {?[n],y|0=0}. |