chore: bump toolchain to v4.3.0 (#87)

.gitignore

@@ -1,4 +1,11 @@
-/build/
 /tests/*.produced
-/lake-packages
+
+# macOS leaves these files everywhere:
+.DS_Store
+# Prior to v4.3.0-rc2 lake stored files in these locations.
+# We'll leave them in the `.gitignore` for a while for users switching between toolchains.
+/build/
+/lake-packages/
 /lakefile.olean
+# After v4.3.0-rc2 lake stores its files here:
+/.lake/

AesopTest/Ext.lean

@@ -10,7 +10,5 @@ import Std.Tactic.Ext
 example (f g : α → β) (h : ∀ a, f a = g a) : f = g := by
   aesop
 
-attribute [local ext] Prod
-
 example (x y : α × β) (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) : x = y := by
   aesop

AesopTest/HeartbeatLimit.lean

@@ -5,17 +5,27 @@ Authors: Jannis Limperg
 -/
 
 import Aesop
+import Std.Tactic.GuardMsgs
 
 set_option aesop.check.all true
+-- There is incorrectly a `linter.unreachableTactic` warning on
+-- `aesop (options := { maxRuleHeartbeats := 1, terminal := true })`
+-- below. This is perhaps because of a bad interaction with `#guard_msgs`?
+set_option linter.unreachableTactic false
 
 @[aesop safe constructors]
 inductive Even : Nat → Prop
   | zero : Even 0
   | plusTwo : Even n → Even (n + 2)
 
+/--
+error: (deterministic) timeout at 'whnf', maximum number of heartbeats (1) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
+-/
+#guard_msgs in
+example : Even 10 := by
+  aesop (options := { maxRuleHeartbeats := 1, terminal := true })
+
 example : Even 10 := by
-  fail_if_success
-    aesop (options := { maxRuleHeartbeats := 1, terminal := true })
   aesop
 
 example (n m k : Nat) : n + m + k = (n + m) + k := by

AesopTest/SeqCalcProver.lean

@@ -273,14 +273,14 @@ abbrev Prove (φ : Form Φ) : Prop := Cal [] [] [] [φ]
 example : Prove (⊥ ⇒ ♩0) := by simp
 example : Prove (♩0 ⇒ ♩0) := by simp
 example : Prove (♩0 ⇒ ♩1 ⇒ ♩0) := by simp
-example : ¬ Prove (♩0 ⇒ ♩1) := by simp
+example : ¬ Prove (♩0 ⇒ ♩1) := by simp (config := {decide := true})
 
 
 --- Soundness and Completeness
 
 @[simp]
 def SC' (i : Φ → Prop) (l r : List Φ) (Γ Δ : List (Form Φ)) : Prop :=
-  SC i (Γ ++ l.map (♩·)) (Δ ++ r.map (♩·)) 
+  SC i (Γ ++ l.map (♩·)) (Δ ++ r.map (♩·))
 
 theorem Cal_sound_complete [DecidableEq Φ]
   (l r : List Φ) (Γ Δ : List (Form Φ))
@@ -439,7 +439,7 @@ end Proof
 
 @[simp]
 def Proof' (l r : List Φ) (Γ Δ : List (Form Φ)) : Prop :=
-  Proof (Γ ++ l.map (♩·)) (Δ ++ r.map (♩·)) 
+  Proof (Γ ++ l.map (♩·)) (Δ ++ r.map (♩·))
 
 theorem Cal_Proof [DecidableEq Φ]
   (l r : List Φ) (Γ Δ : List (Form Φ)) (h : Cal l r Γ Δ)

lake-manifest.json

@@ -1,12 +1,14 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": false}}],
- "name": "aesop"}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "aesop",
+ "lakeDir": ".lake"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.3.0

tests/TraceProof.lean.expected

@@ -4,4 +4,4 @@ tests/TraceProof.lean:14:2: error: tactic 'aesop' failed, made no progress
 tests/TraceProof.lean:20:2: warning: aesop: failed to prove the goal after exhaustive search.
 tests/TraceProof.lean:19:15: error: unsolved goals
 ⊢ False
-[aesop.proof] id ?m.38
+[aesop.proof] id ?m.36