diff options
Diffstat (limited to 'test-suite/misc')
-rwxr-xr-x | test-suite/misc/4722.sh | 15 | ||||
-rw-r--r-- | test-suite/misc/berardi_test.v | 153 | ||||
-rwxr-xr-x | test-suite/misc/coqc_dash_o.sh | 15 | ||||
-rw-r--r-- | test-suite/misc/coqc_dash_o.v | 1 | ||||
-rwxr-xr-x | test-suite/misc/deps-checksum.sh | 5 | ||||
-rwxr-xr-x | test-suite/misc/deps-order.sh | 20 | ||||
-rwxr-xr-x | test-suite/misc/deps-utf8.sh | 17 | ||||
-rw-r--r-- | test-suite/misc/deps/αβ/γδ.v | 4 | ||||
-rw-r--r-- | test-suite/misc/deps/αβ/εζ.v | 1 | ||||
-rwxr-xr-x | test-suite/misc/exitstatus.sh | 7 | ||||
-rw-r--r-- | test-suite/misc/exitstatus/illtyped.v | 1 | ||||
-rwxr-xr-x | test-suite/misc/printers.sh | 3 | ||||
-rwxr-xr-x | test-suite/misc/universes.sh | 8 |
13 files changed, 97 insertions, 153 deletions
diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh new file mode 100755 index 00000000..86bc50b5 --- /dev/null +++ b/test-suite/misc/4722.sh @@ -0,0 +1,15 @@ +#!/bin/sh +set -e + +# create test files +mkdir -p misc/4722 +ln -sf toto misc/4722/tata +touch misc/4722.v + +# run test +$coqtop "-R" "misc/4722" "Foo" -top Top -load-vernac-source misc/4722.v + +# clean up test files +rm misc/4722/tata +rmdir misc/4722 +rm misc/4722.v diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v deleted file mode 100644 index a64db4da..00000000 --- a/test-suite/misc/berardi_test.v +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file formalizes Berardi's paradox which says that in - the calculus of constructions, excluded middle (EM) and axiom of - choice (AC) imply proof irrelevance (PI). - Here, the axiom of choice is not necessary because of the use - of inductive types. -<< -@article{Barbanera-Berardi:JFP96, - author = {F. Barbanera and S. Berardi}, - title = {Proof-irrelevance out of Excluded-middle and Choice - in the Calculus of Constructions}, - journal = {Journal of Functional Programming}, - year = {1996}, - volume = {6}, - number = {3}, - pages = {519-525} -} ->> *) - -Set Implicit Arguments. - -Section Berardis_paradox. - -(** Excluded middle *) -Hypothesis EM : forall P:Prop, P \/ ~ P. - -(** Conditional on any proposition. *) -Definition IFProp (P B:Prop) (e1 e2:P) := - match EM B with - | or_introl _ => e1 - | or_intror _ => e2 - end. - -(** Axiom of choice applied to disjunction. - Provable in Coq because of dependent elimination. *) -Lemma AC_IF : - forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), - (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). -Proof. -intros P B e1 e2 Q p1 p2. -unfold IFProp. -case (EM B); assumption. -Qed. - - -(** We assume a type with two elements. They play the role of booleans. - The main theorem under the current assumptions is that [T=F] *) -Variable Bool : Prop. -Variable T : Bool. -Variable F : Bool. - -(** The powerset operator *) -Definition pow (P:Prop) := P -> Bool. - - -(** A piece of theory about retracts *) -Section Retracts. - -Variables A B : Prop. - -Record retract : Prop := - {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. - -Record retract_cond : Prop := - {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. - - -(** The dependent elimination above implies the axiom of choice: *) -Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. -Proof. -intros r. -case r; simpl. -trivial. -Qed. - -End Retracts. - -(** This lemma is basically a commutation of implication and existential - quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) - which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) - -Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). -Proof. -intros A B. -destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; - destruct hf; auto. -Qed. - - -(** The paradoxical set *) -Definition U := forall P:Prop, pow P. - -(** Bijection between [U] and [(pow U)] *) -Definition f (u:U) : pow U := u U. - -Definition g (h:pow U) : U := - fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). - -(** We deduce that the powerset of [U] is a retract of [U]. - This lemma is stated in Berardi's article, but is not used - afterwards. *) -Lemma retract_pow_U_U : retract (pow U) U. -Proof. -exists g f. -intro a. -unfold f, g; simpl. -apply AC. -exists (fun x:pow U => x) (fun x:pow U => x). -trivial. -Qed. - -(** Encoding of Russel's paradox *) - -(** The boolean negation. *) -Definition Not_b (b:Bool) := IFProp (b = T) F T. - -(** the set of elements not belonging to itself *) -Definition R : U := g (fun u:U => Not_b (u U u)). - - -Lemma not_has_fixpoint : R R = Not_b (R R). -Proof. -unfold R at 1. -unfold g. -rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). -trivial. -exists (fun x:pow U => x) (fun x:pow U => x); trivial. -Qed. - - -Theorem classical_proof_irrelevence : T = F. -Proof. -generalize not_has_fixpoint. -unfold Not_b. -apply AC_IF. -intros is_true is_false. -elim is_true; elim is_false; trivial. - -intros not_true is_true. -elim not_true; trivial. -Qed. - -End Berardis_paradox. diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh new file mode 100755 index 00000000..0ae7873f --- /dev/null +++ b/test-suite/misc/coqc_dash_o.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash + +DOUT=misc/tmp_coqc_dash_o/ +OUT=${DOUT}coqc_dash_o.vo + + +mkdir -p "${DOUT}" +rm -f "${OUT}" +$coqc misc/coqc_dash_o.v -o "${OUT}" +if [ ! -f "${OUT}" ]; then + printf "coqc -o not working" + exit 1 +fi +rm -fr "${DOUT}" +exit 0 diff --git a/test-suite/misc/coqc_dash_o.v b/test-suite/misc/coqc_dash_o.v new file mode 100644 index 00000000..7426dff1 --- /dev/null +++ b/test-suite/misc/coqc_dash_o.v @@ -0,0 +1 @@ +Definition x := nat. diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh new file mode 100755 index 00000000..e07612b8 --- /dev/null +++ b/test-suite/misc/deps-checksum.sh @@ -0,0 +1,5 @@ +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 diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh new file mode 100755 index 00000000..299f4946 --- /dev/null +++ b/test-suite/misc/deps-order.sh @@ -0,0 +1,20 @@ +# Check that both coqdep and coqtop/coqc supports -R +# Check that both coqdep and coqtop/coqc takes the later -R +# See bugs 2242, 2337, 2339 +rm -f misc/deps/lib/*.vo misc/deps/client/*.vo +tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput +diff -u --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1 +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 +S=$? +if [ $R = 0 -a $S = 0 ]; then + printf "coqdep and coqtop agree\n" + exit 0 +else + printf "coqdep and coqtop disagree\n" + exit 1 +fi diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh new file mode 100755 index 00000000..13e264c0 --- /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 00000000..f43a2d65 --- /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 00000000..e7fd25c0 --- /dev/null +++ b/test-suite/misc/deps/αβ/εζ.v @@ -0,0 +1 @@ +Require Import γδ. diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh new file mode 100755 index 00000000..cea1de86 --- /dev/null +++ b/test-suite/misc/exitstatus.sh @@ -0,0 +1,7 @@ +$coqtop -load-vernac-source misc/exitstatus/illtyped.v +N=$? +$coqc misc/exitstatus/illtyped.v +P=$? +printf "On ill-typed input, coqtop returned $N.\n" +printf "On ill-typed input, coqc returned $P.\n" +if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v new file mode 100644 index 00000000..df6bbb38 --- /dev/null +++ b/test-suite/misc/exitstatus/illtyped.v @@ -0,0 +1 @@ +Check S S. diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh new file mode 100755 index 00000000..28e7dc36 --- /dev/null +++ b/test-suite/misc/printers.sh @@ -0,0 +1,3 @@ +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" +if [ $? = 0 ]; then exit 1; else exit 0; fi + diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh new file mode 100755 index 00000000..d87a8603 --- /dev/null +++ b/test-suite/misc/universes.sh @@ -0,0 +1,8 @@ +# Sort universes for the whole standard library +EXPECTED_UNIVERSES=4 # Prop is not counted +$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 +$coqc -R misc/universes Universes misc/universes/universes 2>&1 +mv universes.txt misc/universes +N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` +printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi |