From a66332fae74d615e80f50ed685ff159afa856897 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 2 Oct 2023 15:12:51 +0200
Subject: [PATCH] split tests/tactics

---
 tests/tactics.ref      |  2 ++
 tests/tactics.v        | 25 +++++++------------------
 tests/tactics_more.ref |  0
 tests/tactics_more.v   | 10 ++++++++++
 4 files changed, 19 insertions(+), 18 deletions(-)
 create mode 100644 tests/tactics_more.ref
 create mode 100644 tests/tactics_more.v

diff --git a/tests/tactics.ref b/tests/tactics.ref
index 119886a9..908ccb71 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -4,6 +4,8 @@ The command has indeed failed with message:
 Failed to progress.
 The command has indeed failed with message:
 Failed to progress.
+"otest"
+     : string
 The command has indeed failed with message:
 Cannot infer this placeholder of type "nat" in
 environment:
diff --git a/tests/tactics.v b/tests/tactics.v
index 5aa85fce..ff939a6d 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -1,6 +1,10 @@
+(** Basic tests for atctics that don't import anything else
+(and hence can be run even when nothing else even builds. *)
+From Coq Require Import String.
 From stdpp Require Import tactics.
 
 Local Unset Mangle Names. (* for stable goal printing *)
+Local Open Scope string_scope.
 
 Goal ∀ P1 P2 P3 P4 (P: Prop),
   P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
@@ -106,7 +110,7 @@ Proof.
 Abort.
 
 (** o-tactic tests *)
-(* Check "otest". *)
+Check "otest".
 Lemma otest (P Q R : nat → Prop)
   (HPQR1 : ∀ m n, P n → Q m → R (n + m))
   (HPQR2 : ∀ m n, P n → Q m → R (n + m) ∧ R 2)
@@ -164,23 +168,8 @@ Restart.
   opose proof* HR as HR'; [exact HP|exact HQ|exact HR'].
 Qed.
 
-(** Now that we have seen that the basic tactics are working,
-we are okay importing some other files. We don't want to do this
-above since it can make debugging hard: if a tactic breaks,
-[option] breaks, and then we cannot even use the tests here to figure out
-what is going on! *)
-From stdpp Require Import option.
-
-(** Make sure that [done] is not called recursively when solving [is_Some],
-which might leave an unresolved evar before performing ex falso. *)
-Goal False → is_Some (@None nat).
-Proof. done. Qed.
-Goal ∀ mx, mx = Some 10 → is_Some mx.
-Proof. done. Qed.
-Goal ∀ mx, Some 10 = mx → is_Some mx.
-Proof. done. Qed.
-
-(** Regression tests for [naive_solver]. *)
+(** Regression tests for [naive_solver].
+Requires a bunch of other tactics to work so it comes last in this file. *)
 Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
   (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
 Proof. naive_solver. Qed.
diff --git a/tests/tactics_more.ref b/tests/tactics_more.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/tactics_more.v b/tests/tactics_more.v
new file mode 100644
index 00000000..6163a4f5
--- /dev/null
+++ b/tests/tactics_more.v
@@ -0,0 +1,10 @@
+From stdpp Require Import tactics option.
+
+(** Make sure that [done] is not called recursively when solving [is_Some],
+which might leave an unresolved evar before performing ex falso. *)
+Goal False → is_Some (@None nat).
+Proof. done. Qed.
+Goal ∀ mx, mx = Some 10 → is_Some mx.
+Proof. done. Qed.
+Goal ∀ mx, Some 10 = mx → is_Some mx.
+Proof. done. Qed.
-- 
GitLab