From 2244e639c51917dd721d8ed2fd1d702c1ae47548 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 30 Oct 2024 18:14:21 +0100
Subject: [PATCH] chore: update to work with latest nightly

---
 .github/workflows/ci.yml |  4 ++++
 InternalTests.lean       | 23 +++++++++++++++++++++--
 lakefile.lean            |  1 +
 lean-toolchain           |  2 +-
 4 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 49f184e..8454646 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -25,9 +25,13 @@ jobs:
           - "4.11.0"
           - "4.12.0"
           - "4.13.0-rc1"
+          - "nightly-2024-08-09"
+          - "nightly-2024-08-29"
           - "nightly-2024-09-03"
           - "nightly-2024-09-17"
           - "nightly-2024-10-10"
+          - "nightly-2024-10-18"
+          - "nightly-2024-10-30"
         platform:
           - os: ubuntu-latest
             installer: |
diff --git a/InternalTests.lean b/InternalTests.lean
index 9d7a46f..724650a 100644
--- a/InternalTests.lean
+++ b/InternalTests.lean
@@ -72,11 +72,30 @@ elab "#evalString" s:str e:term : command => do
   finally
     modify ({· with messages := msgs})
 
+open Lean Elab Command in
+elab "#evalStrings " "[" ss:str,* "] " e:term : command => do
+  let msgs := (← get).messages
+  try
+    modify ({· with messages := {}})
+    elabCommand <| ← `(#eval $e)
+    let msgs' := (← get).messages
+    let [msg] := msgs'.toList
+      | throwError "Too many messages"
+    let ok := ss.getElems.toList.map (·.getString)
+    if (← msg.toString) ∉ ok then
+      throwErrorAt e "Expected one of {ok.map String.quote}, got {String.quote (← msg.toString)}"
+  finally
+    modify ({· with messages := msgs})
+
 #evalString "[[\"n * 1 = n\"]]\n"
   (proofEx.highlighted[0].proofStates.toList.filter (·.fst == "by") |>.map (·.snd.toList.map (·.conclusion)))
 
-#evalString "[[some `zero], [some `succ], [none], [some `succ.succ], [none]]\n"
-  (proofEx.highlighted[0].proofStates.toList.filter (·.fst == "=>") |>.map (·.snd.toList.map (·.name)))
+#evalStrings [ -- NB #5677 changed goal displays, so the second
+               -- version here became the expected output after
+               -- nightly-2024-10-18.
+    "[[some `zero], [some `succ], [none], [some `succ.succ], [none]]\n",
+    "[[none], [some `succ.succ], [none]]\n"]
+ (proofEx.highlighted[0].proofStates.toList.filter (·.fst == "=>") |>.map (·.snd.toList.map (·.name)))
 
 
 
diff --git a/lakefile.lean b/lakefile.lean
index ca15da3..2583e19 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,5 +1,6 @@
 import Lake
 open Lake DSL
+open System (FilePath)
 
 package «subverso» where
   precompileModules := true
diff --git a/lean-toolchain b/lean-toolchain
index 63510c1..fcce113 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.6.0
+leanprover/lean4:nightly-2024-10-30