aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_12196.v46
-rw-r--r--test-suite/bugs/closed/bug_12257.v3
-rw-r--r--test-suite/bugs/closed/bug_6378.v9
-rw-r--r--test-suite/complexity/ConstructiveCauchyRealsPerformance.v2
-rw-r--r--test-suite/micromega/bug_12210.v19
-rw-r--r--test-suite/output/Extraction_Haskell_String_12258.out73
-rw-r--r--test-suite/output/Extraction_Haskell_String_12258.v52
-rw-r--r--test-suite/output/Fixpoint.out24
-rw-r--r--test-suite/output/Fixpoint.v38
-rw-r--r--test-suite/ssr/simpl_done.v28
-rw-r--r--test-suite/ssr/try_case.v11
-rw-r--r--test-suite/success/ltacprof.v17
12 files changed, 318 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/bug_12196.v b/test-suite/bugs/closed/bug_12196.v
new file mode 100644
index 0000000000..c0851b3204
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12196.v
@@ -0,0 +1,46 @@
+(** TODO: Figure out how to test "sanity" for the ltac profiler output *)
+Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end.
+Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end.
+Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
+Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
+Ltac multi := idtac + slow + slow2.
+Set Ltac Profiling.
+Goal True.
+ Time try (multi; fail).
+ (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success
+ tactics; profiling results may be wildly inaccurate.
+ [profile-backtracking,ltac] *)
+ Show Ltac Profile.
+ (* Used to be:
+total time: 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 47.1% 47.1% 1 0.000s
+─slow ---------------------------------- 35.3% 35.3% 1 0.000s
+─slow2 --------------------------------- 17.6% 17.6% 1 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 47.1% 47.1% 1 0.000s
+─slow ---------------------------------- 35.3% 35.3% 1 0.000s
+─slow2 --------------------------------- 17.6% 17.6% 1 0.000s
+
+ *)
+ (* Now:
+total time: 2.074s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 0.0% 100.0% 6 1.119s
+─slow ---------------------------------- 54.0% 54.0% 3 1.119s
+─slow2 --------------------------------- 46.0% 46.0% 3 0.955s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 0.0% 100.0% 6 1.119s
+ ├─slow -------------------------------- 54.0% 54.0% 3 1.119s
+ └─slow2 ------------------------------- 46.0% 46.0% 3 0.955s
+
+*)
+Abort.
diff --git a/test-suite/bugs/closed/bug_12257.v b/test-suite/bugs/closed/bug_12257.v
new file mode 100644
index 0000000000..4962048a42
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12257.v
@@ -0,0 +1,3 @@
+(* Test that ExtrHaskellString transitively requires ExtrHaskellBasic *)
+Require Coq.extraction.ExtrHaskellString.
+Import Coq.extraction.ExtrHaskellBasic.
diff --git a/test-suite/bugs/closed/bug_6378.v b/test-suite/bugs/closed/bug_6378.v
index 68ae7961dd..453924d587 100644
--- a/test-suite/bugs/closed/bug_6378.v
+++ b/test-suite/bugs/closed/bug_6378.v
@@ -7,11 +7,20 @@ Ltac profile_constr tac :=
Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).
+Ltac manipulate_ltac_prof :=
+ start ltac profiling;
+ reset ltac profile;
+ try ((idtac + reset ltac profile + idtac); fail);
+ try ((idtac + start ltac profiling + idtac); fail);
+ try ((idtac + stop ltac profiling + idtac); fail).
+
Goal True.
start ltac profiling.
reset ltac profile.
+ manipulate_ltac_prof.
reset ltac profile.
stop ltac profiling.
+ Set Warnings Append "+profile-invalid-stack-no-self".
time profile_constr slow.
show ltac profile cutoff 0.
show ltac profile "slow".
diff --git a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v
index c901334da9..f3bc1767da 100644
--- a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v
+++ b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v
@@ -105,7 +105,7 @@ Proof.
Qed.
Lemma approx_sqrt_Q_cauchy :
- forall q:Q, QCauchySeq (approx_sqrt_Q q) id.
+ forall q:Q, QCauchySeq (approx_sqrt_Q q).
Proof.
intro q. destruct q as [k j]. destruct k.
- intros n a b H H0. reflexivity.
diff --git a/test-suite/micromega/bug_12210.v b/test-suite/micromega/bug_12210.v
new file mode 100644
index 0000000000..ca011def09
--- /dev/null
+++ b/test-suite/micromega/bug_12210.v
@@ -0,0 +1,19 @@
+Require Import PeanoNat Lia.
+
+Goal forall x, Nat.le x x.
+Proof.
+intros.
+lia.
+Qed.
+
+Goal forall x, Nat.lt x x -> False.
+Proof.
+intros.
+lia.
+Qed.
+
+Goal forall x, Nat.eq x x.
+Proof.
+intros.
+lia.
+Qed.
diff --git a/test-suite/output/Extraction_Haskell_String_12258.out b/test-suite/output/Extraction_Haskell_String_12258.out
new file mode 100644
index 0000000000..615abaa3e8
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.out
@@ -0,0 +1,73 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+{- IMPORTANT: If you change this file, make sure that running [cp
+ Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs &&
+ ghc -o test Extraction_Haskell_String_12258.hs] succeeds -}
+
+module Main where
+
+import qualified Prelude
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+#else
+-- HUGS
+import qualified IOExts
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Base.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+data Output_type_code =
+ Ascii_dec
+ | Ascii_eqb
+ | String_dec
+ | String_eqb
+ | Byte_eqb
+ | Byte_eq_dec
+
+type Output_type = Any
+
+output :: Output_type_code -> Output_type
+output c =
+ case c of {
+ Ascii_dec ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+ Ascii_eqb ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+ String_dec ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+ String_eqb ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+ Byte_eqb ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+ Byte_eq_dec ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)}
+
+type Coq__IO a = GHC.Base.IO a
+
+main :: GHC.Base.IO ()
+main =
+ ((Prelude.>>=) (GHC.Base.return output) (\_ -> GHC.Base.return ()))
+
+
diff --git a/test-suite/output/Extraction_Haskell_String_12258.v b/test-suite/output/Extraction_Haskell_String_12258.v
new file mode 100644
index 0000000000..063ff64337
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.v
@@ -0,0 +1,52 @@
+Require Import Coq.extraction.Extraction.
+Require Import Coq.extraction.ExtrHaskellString.
+Extraction Language Haskell.
+Set Extraction File Comment "IMPORTANT: If you change this file, make sure that running [cp Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs && ghc -o test Extraction_Haskell_String_12258.hs] succeeds".
+Inductive output_type_code :=
+| ascii_dec
+| ascii_eqb
+| string_dec
+| string_eqb
+| byte_eqb
+| byte_eq_dec
+.
+
+Definition output_type_sig (c : output_type_code) : { T : Type & T }
+ := existT (fun T => T)
+ _
+ match c return match c with ascii_dec => _ | _ => _ end with
+ | ascii_dec => Ascii.ascii_dec
+ | ascii_eqb => Ascii.eqb
+ | string_dec => String.string_dec
+ | string_eqb => String.eqb
+ | byte_eqb => Byte.eqb
+ | byte_eq_dec => Byte.byte_eq_dec
+ end.
+
+Definition output_type (c : output_type_code)
+ := Eval cbv [output_type_sig projT1 projT2] in
+ projT1 (output_type_sig c).
+Definition output (c : output_type_code) : output_type c
+ := Eval cbv [output_type_sig projT1 projT2] in
+ match c return output_type c with
+ | ascii_dec as c
+ | _ as c
+ => projT2 (output_type_sig c)
+ end.
+
+Axiom IO_unit : Set.
+Axiom _IO : Set -> Set.
+Axiom _IO_bind : forall {A B}, _IO A -> (A -> _IO B) -> _IO B.
+Axiom _IO_return : forall {A : Set}, A -> _IO A.
+Axiom cast_io : _IO unit -> IO_unit.
+Extract Constant _IO "a" => "GHC.Base.IO a".
+Extract Inlined Constant _IO_bind => "(Prelude.>>=)".
+Extract Inlined Constant _IO_return => "GHC.Base.return".
+Extract Inlined Constant IO_unit => "GHC.Base.IO ()".
+Extract Inlined Constant cast_io => "".
+
+Definition main : IO_unit
+ := cast_io (_IO_bind (_IO_return output)
+ (fun _ => _IO_return tt)).
+
+Recursive Extraction main.
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 60bc9cbf55..ff7918b4e6 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -12,3 +12,27 @@ let fix f (m : nat) : nat := match m with
Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
= cofix inf : Inf := {| projS := inf |}
: Inf
+File "stdin", line 57, characters 0-51:
+Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
+File "stdin", line 60, characters 0-103:
+Warning: Not a fully mutually defined fixpoint
+(k1 depends on k2 but not conversely).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 62, characters 0-106:
+Warning: Not a fully mutually defined fixpoint
+(l2 and l1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 64, characters 0-103:
+Warning: Not a fully mutually defined fixpoint
+(m2 and m1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 72, characters 0-25:
+Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
+File "stdin", line 75, characters 0-48:
+Warning: Not a fully mutually defined fixpoint
+(a2 and a1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 398528de72..26c276b68b 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,39 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
lia.
Qed.
-CoInductive Inf := S { projS : Inf }.
-Definition expand_Inf (x : Inf) := S (projS x).
-CoFixpoint inf := S inf.
+CoInductive Inf := IS { projS : Inf }.
+Definition expand_Inf (x : Inf) := IS (projS x).
+CoFixpoint inf := IS inf.
Eval compute in inf.
+
+Module Recursivity.
+
+Open Scope nat_scope.
+
+Fixpoint f n := match n with 0 => 0 | S n => f n end.
+Fixpoint g n := match n with 0 => 0 | S n => n end.
+Fixpoint h1 n := match n with 0 => 0 | S n => h2 n end
+with h2 n := match n with 0 => 0 | S n => h1 n end.
+Fixpoint k1 n := match n with 0 => 0 | S n => k2 n end
+with k2 n := match n with 0 => 0 | S n => n end.
+Fixpoint l1 n := match n with 0 => 0 | S n => l1 n end
+with l2 n := match n with 0 => 0 | S n => l2 n end.
+Fixpoint m1 n := match n with 0 => 0 | S n => m1 n end
+with m2 n := match n with 0 => 0 | S n => n end.
+(* Why not to allow this definition ?
+Fixpoint h1' n := match n with 0 => 0 | S n => h2' n end
+with h2' n := h1' n.
+*)
+CoInductive S := cons : nat -> S -> S.
+CoFixpoint c := cons 0 c.
+CoFixpoint d := cons 0 c.
+CoFixpoint e1 := cons 0 e2
+with e2 := cons 1 e1.
+CoFixpoint a1 := cons 0 a1
+with a2 := cons 1 a2.
+(* Why not to allow this definition ?
+CoFixpoint b1 := cons 0 b2
+with b2 := b1.
+*)
+
+End Recursivity.
diff --git a/test-suite/ssr/simpl_done.v b/test-suite/ssr/simpl_done.v
new file mode 100644
index 0000000000..f5c766209a
--- /dev/null
+++ b/test-suite/ssr/simpl_done.v
@@ -0,0 +1,28 @@
+Require Import ssreflect.
+
+Inductive lit : Set :=
+| LitP : lit
+| LitL : lit
+.
+
+Inductive val : Set :=
+| Val : lit -> val.
+
+Definition tyref :=
+fun (vl : list val) =>
+match vl with
+| cons (Val LitL) (cons (Val LitP) _) => False
+| _ => False
+end.
+
+(** Check that simplification and resolution are performed in the right order
+ by "//=" when several goals are under focus. *)
+Goal exists vl1 : list val,
+ cons (Val LitL) (cons (Val LitL) nil) = vl1 /\
+ (tyref vl1)
+.
+Proof.
+eexists (cons _ (cons _ _)).
+split =>//=.
+Fail progress simpl.
+Abort.
diff --git a/test-suite/ssr/try_case.v b/test-suite/ssr/try_case.v
new file mode 100644
index 0000000000..114bf2cecf
--- /dev/null
+++ b/test-suite/ssr/try_case.v
@@ -0,0 +1,11 @@
+From Coq Require Import ssreflect.
+
+Axiom T : Type.
+Axiom R : T -> T -> Type.
+
+(** Check that internal exceptions are correctly caught in the monad *)
+Goal forall (a b : T) (Hab : R a b), True.
+Proof.
+intros.
+try (case: Hab).
+Abort.
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
index d5552695c4..f40f40c2bb 100644
--- a/test-suite/success/ltacprof.v
+++ b/test-suite/success/ltacprof.v
@@ -6,3 +6,20 @@ Goal True.
try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
Admitted.
Show Ltac Profile.
+
+(* backtracking across profiler manipulation *)
+Unset Ltac Profiling.
+Reset Ltac Profile.
+
+Fixpoint slow (n : nat) : unit
+ := match n with
+ | 0 => tt
+ | S n => fst (slow n, slow n)
+ end.
+
+Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac.
+Ltac multi2 :=
+ try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile.
+Goal True.
+ multi2.
+Admitted.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 12:19:58 +0000