chore: update to work with latest nightly

.github/workflows/ci.yml

@@ -23,11 +23,15 @@ jobs:
           - "4.9.0"
           - "4.10.0"
           - "4.11.0"
-          - "4.12.0-rc1"
+          - "4.12.0"
+          - "4.13.0-rc4"
           - "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: |

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)))
 
 
 

lakefile.lean

@@ -1,5 +1,6 @@
 import Lake
 open Lake DSL
+open System (FilePath)
 
 package «subverso» where
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.6.0
+leanprover/lean4:nightly-2024-10-30