diff options
Diffstat (limited to 'test-suite/misc')
40 files changed, 335 insertions, 0 deletions
diff --git a/test-suite/misc/.gitignore b/test-suite/misc/.gitignore new file mode 100644 index 0000000000..a4083e9314 --- /dev/null +++ b/test-suite/misc/.gitignore @@ -0,0 +1,2 @@ +4722/ +4722.v diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh new file mode 100755 index 0000000000..86bc50b5cd --- /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/7595.sh b/test-suite/misc/7595.sh new file mode 100755 index 0000000000..836e354ee9 --- /dev/null +++ b/test-suite/misc/7595.sh @@ -0,0 +1,5 @@ +#!/bin/sh +set -e + +$coqc -R misc/7595 Test misc/7595/base.v +$coqc -R misc/7595 Test misc/7595/FOO.v diff --git a/test-suite/misc/7595/FOO.v b/test-suite/misc/7595/FOO.v new file mode 100644 index 0000000000..30c957d3b1 --- /dev/null +++ b/test-suite/misc/7595/FOO.v @@ -0,0 +1,39 @@ +Require Import Test.base. + +Lemma dec_stable `{Decision P} : ¬¬P → P. +Proof. firstorder. Qed. + +(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the +components is double negated, it will try to remove the double negation. *) +Tactic Notation "destruct_decide" constr(dec) "as" ident(H) := + destruct dec as [H|H]; + try match type of H with + | ¬¬_ => apply dec_stable in H + end. +Tactic Notation "destruct_decide" constr(dec) := + let H := fresh in destruct_decide dec as H. + + +(** * Monadic operations *) +Instance option_guard: MGuard option := λ P dec A f, + match dec with left H => f H | _ => None end. + +(** * Tactics *) +Tactic Notation "case_option_guard" "as" ident(Hx) := + match goal with + | H : context C [@mguard option _ ?P ?dec] |- _ => + change (@mguard option _ P dec) with (λ A (f : P → option A), + match @decide P dec with left H' => f H' | _ => None end) in *; + destruct_decide (@decide P dec) as Hx + | |- context C [@mguard option _ ?P ?dec] => + change (@mguard option _ P dec) with (λ A (f : P → option A), + match @decide P dec with left H' => f H' | _ => None end) in *; + destruct_decide (@decide P dec) as Hx + end. +Tactic Notation "case_option_guard" := + let H := fresh in case_option_guard as H. + +(* This proof failed depending on the name of the module. *) +Lemma option_guard_True {A} P `{Decision P} (mx : option A) : + P → (guard P; mx) = mx. +Proof. intros. case_option_guard. reflexivity. contradiction. Qed. diff --git a/test-suite/misc/7595/base.v b/test-suite/misc/7595/base.v new file mode 100644 index 0000000000..6a6b7b79d9 --- /dev/null +++ b/test-suite/misc/7595/base.v @@ -0,0 +1,28 @@ +From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. +Set Default Proof Using "Type". +Export ListNotations. +From Coq.Program Require Export Basics Syntax. +Global Generalizable All Variables. + +(** * Type classes *) +(** ** Decidable propositions *) +(** This type class by (Spitters/van der Weegen, 2011) collects decidable +propositions. *) +Class Decision (P : Prop) := decide : {P} + {¬P}. +Hint Mode Decision ! : typeclass_instances. +Arguments decide _ {_} : simpl never, assert. + +(** ** Proof irrelevant types *) +(** This type class collects types that are proof irrelevant. That means, all +elements of the type are equal. We use this notion only used for propositions, +but by universe polymorphism we can generalize it. *) +Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y. +Hint Mode ProofIrrel ! : typeclass_instances. + +Class MGuard (M : Type → Type) := + mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A. +Arguments mguard _ _ _ !_ _ _ / : assert. +Notation "'guard' P ; z" := (mguard P (λ _, z)) + (at level 20, z at level 200, only parsing, right associativity) . +Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z)) + (at level 20, z at level 200, only parsing, right associativity) . diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh new file mode 100755 index 0000000000..0ca2c97d24 --- /dev/null +++ b/test-suite/misc/7704.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +set -e + +export PATH=$BIN:$PATH + +${coqtop#"$BIN"} -compile misc/aux7704.v diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v new file mode 100644 index 0000000000..6fdcf67684 --- /dev/null +++ b/test-suite/misc/aux7704.v @@ -0,0 +1,6 @@ + +Goal True /\ True. +Proof. + split. + par:exact I. +Qed. diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh new file mode 100755 index 0000000000..0ae7873fd9 --- /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 0000000000..7426dff1a0 --- /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 0000000000..a15a8fbee9 --- /dev/null +++ b/test-suite/misc/deps-checksum.sh @@ -0,0 +1,6 @@ +#!/bin/sh +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 0000000000..6bb2ba2da0 --- /dev/null +++ b/test-suite/misc/deps-order.sh @@ -0,0 +1,21 @@ +#!/bin/sh +# 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 ] && [ $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 0000000000..acb45b2292 --- /dev/null +++ b/test-suite/misc/deps-utf8.sh @@ -0,0 +1,18 @@ +#!/bin/sh +# 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" ] || [ "$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 ] && [ $S = 0 ]; then + exit 0 +else + exit 1 +fi +fi diff --git a/test-suite/misc/deps/A/A.v b/test-suite/misc/deps/A/A.v new file mode 100644 index 0000000000..49aaf4a79e --- /dev/null +++ b/test-suite/misc/deps/A/A.v @@ -0,0 +1 @@ +Definition b := true. diff --git a/test-suite/misc/deps/B/A.v b/test-suite/misc/deps/B/A.v new file mode 100644 index 0000000000..c01a30dca5 --- /dev/null +++ b/test-suite/misc/deps/B/A.v @@ -0,0 +1 @@ +Definition b := false. diff --git a/test-suite/misc/deps/B/B.v b/test-suite/misc/deps/B/B.v new file mode 100644 index 0000000000..f3cda70a9d --- /dev/null +++ b/test-suite/misc/deps/B/B.v @@ -0,0 +1,7 @@ +Require A. + +Definition c := A.b. +Lemma foo : c = false. +Proof. +reflexivity. +Qed. diff --git a/test-suite/misc/deps/checksum.v b/test-suite/misc/deps/checksum.v new file mode 100644 index 0000000000..450045e4bf --- /dev/null +++ b/test-suite/misc/deps/checksum.v @@ -0,0 +1,2 @@ +Require Import A. +Fail Require Import B. diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v new file mode 100644 index 0000000000..6296941862 --- /dev/null +++ b/test-suite/misc/deps/client/bar.v @@ -0,0 +1,11 @@ +(* We assume the file compiled with -R ../lib lib -R . client *) +(* foo alone should refer to client.foo because -R . client comes last *) + +Require Import foo. +Goal a = 1. +reflexivity. +Qed. +Require Import lib.foo. +Goal a = 0. +reflexivity. +Qed. diff --git a/test-suite/misc/deps/client/foo.v b/test-suite/misc/deps/client/foo.v new file mode 100644 index 0000000000..fc82069e5b --- /dev/null +++ b/test-suite/misc/deps/client/foo.v @@ -0,0 +1 @@ +Definition a := 1. diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out new file mode 100644 index 0000000000..5b79349fc2 --- /dev/null +++ b/test-suite/misc/deps/deps.out @@ -0,0 +1 @@ +misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo diff --git a/test-suite/misc/deps/lib/foo.v b/test-suite/misc/deps/lib/foo.v new file mode 100644 index 0000000000..b745fbd482 --- /dev/null +++ b/test-suite/misc/deps/lib/foo.v @@ -0,0 +1 @@ +Definition a := 0. 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/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh new file mode 100755 index 0000000000..a327f4248b --- /dev/null +++ b/test-suite/misc/exitstatus.sh @@ -0,0 +1,8 @@ +#!/bin/sh +$coqtop -load-vernac-source misc/exitstatus/illtyped.v +N=$? +$coqc misc/exitstatus/illtyped.v +P=$? +printf "On ill-typed input, coqtop returned %s.\n" "$N" +printf "On ill-typed input, coqc returned %s.\n" "$P" +if [ $N = 1 ] && [ $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 0000000000..df6bbb389c --- /dev/null +++ b/test-suite/misc/exitstatus/illtyped.v @@ -0,0 +1 @@ +Check S S. diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh new file mode 100755 index 0000000000..e066ac039b --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/poly-capture-global-univs/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs + +if make; then + >&2 echo 'Should have failed!' + exit 1 +fi diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore new file mode 100644 index 0000000000..2a6a6bc68d --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/.gitignore @@ -0,0 +1,2 @@ +/Makefile* +/src/evil.ml diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject new file mode 100644 index 0000000000..e5dc3cff56 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Evil +-I src + +src/evil.mlg +src/evilImpl.ml +src/evilImpl.mli +src/evil_plugin.mlpack +theories/evil.v + diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg new file mode 100644 index 0000000000..edd22b1d29 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -0,0 +1,10 @@ +{ +open Stdarg +open EvilImpl +} + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> { evil x y } +END diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml new file mode 100644 index 0000000000..047f4cd080 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -0,0 +1,22 @@ +open Names + +let evil t f = + let open Univ in + let open Entries in + let open Decl_kinds in + let open Constr in + let k = IsDefinition Definition in + let u = Level.var 0 in + let tu = mkType (Universe.make u) in + let te = Declare.definition_entry + ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu + in + let tc = Declare.declare_constant t (DefinitionEntry te, k) in + let tc = mkConst tc in + + let fe = Declare.definition_entry + ~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 + ignore (Declare.declare_constant f (DefinitionEntry fe, k)) diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli new file mode 100644 index 0000000000..97c7e3dadd --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli @@ -0,0 +1,2 @@ + +val evil : Names.Id.t -> Names.Id.t -> unit diff --git a/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack new file mode 100644 index 0000000000..0093328a40 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack @@ -0,0 +1,2 @@ +EvilImpl +Evil diff --git a/test-suite/misc/poly-capture-global-univs/theories/evil.v b/test-suite/misc/poly-capture-global-univs/theories/evil.v new file mode 100644 index 0000000000..7fd98c2773 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/theories/evil.v @@ -0,0 +1,13 @@ + +Declare ML Module "evil_plugin". + +Evil T f. (* <- if this doesn't fail then the rest goes through *) + +Definition g : Type -> Set := f. + +Require Import Hurkens. + +Lemma absurd : False. +Proof. + exact (TypeNeqSmallType.paradox (g Type) eq_refl). +Qed. diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh new file mode 100755 index 0000000000..ef3f056d89 --- /dev/null +++ b/test-suite/misc/printers.sh @@ -0,0 +1,2 @@ +#!/bin/sh +if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi 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/misc/universes.sh b/test-suite/misc/universes.sh new file mode 100755 index 0000000000..ef61ca6241 --- /dev/null +++ b/test-suite/misc/universes.sh @@ -0,0 +1,9 @@ +#!/bin/sh +# 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 diff --git a/test-suite/misc/universes/build_all_stdlib.sh b/test-suite/misc/universes/build_all_stdlib.sh new file mode 100755 index 0000000000..2d2e6f863b --- /dev/null +++ b/test-suite/misc/universes/build_all_stdlib.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +echo "Require $(find ../../../theories ../../../plugins -type f -name "*.v" | \ + sed 's/^.*\/theories\///' | sed 's/^.*\/plugins\///' | sed 's/\.v$//' | sed 's/\//./g') ." diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune new file mode 100644 index 0000000000..58bba300d2 --- /dev/null +++ b/test-suite/misc/universes/dune @@ -0,0 +1,8 @@ +(rule + (targets all_stdlib.v) + (deps + (source_tree ../../../theories) + (source_tree ../../../plugins)) + (action + (with-outputs-to all_stdlib.v + (run ./build_all_stdlib.sh)))) diff --git a/test-suite/misc/universes/universes.v b/test-suite/misc/universes/universes.v new file mode 100644 index 0000000000..b7c7ed812f --- /dev/null +++ b/test-suite/misc/universes/universes.v @@ -0,0 +1,2 @@ +Require all_stdlib. +Print Sorted Universes "universes.txt". |