chore: bump to v4.14.0-rc1 (#58)

Co-authored-by: David Thrane Christiansen <[email protected]>

.github/workflows/ci.yml

@@ -24,7 +24,8 @@ jobs:
           - "4.10.0"
           - "4.11.0"
           - "4.12.0"
-          - "4.13.0-rc1"
+          - "4.13.0"
+          - "4.14.0-rc1"
           - "nightly-2024-08-09"
           - "nightly-2024-08-29"
           - "nightly-2024-09-03"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-30
+leanprover/lean4:v4.14.0-rc1

src/compat/SubVerso/Compat.lean

@@ -96,6 +96,35 @@ def refIdentCase (ri : Lsp.RefIdent)
     | .const x => onConst x
   ]
 
+/--
+If the provided syntax is the syntax of the `rw` or `rewrite` tactics, returns the syntax of the
+closing bracket of the rewrite rules. Otherwise returns `none`.
+
+This is needed because the syntax of `rw` changed in 4.14, so it's no longer possible to have a
+quasiquote that matches both versions.
+-/
+def rwTacticRightBracket? (stx : Syntax) : Option Syntax := Id.run do
+  if let .node _ k children := stx then
+    if k ∈ [``Lean.Parser.Tactic.rwSeq, ``Lean.Parser.Tactic.rewriteSeq] then
+      for child in children do
+        match child with
+        | `(Lean.Parser.Tactic.rwRuleSeq|[$_rs,*]%$brak) => return some brak
+        | _ => continue
+  return none
+
+
+namespace List
+-- bind was renamed to flatMap in 4.14
+def flatMap (xs : List α) (f : α → List β) : List β :=
+  %first_succeeding [_root_.List.flatMap xs f, _root_.List.bind xs f]
+end List
+
+namespace Array
+-- back was renamed to back! in 4.14
+def back! [Inhabited α] (xs : Array α) : α :=
+  %first_succeeding [_root_.Array.back! xs, _root_.Array.back xs]
+end Array
+
 abbrev Parsec (α : Type) : Type :=
   %first_succeeding [
     (Lean.Parsec α : Type),

src/examples/SubVerso/Examples.lean

@@ -127,8 +127,8 @@ elab_rules : command
     let freshMsgs ← allNewMessages.toList.mapM fun m => do pure (m.severity, ← contents m)
     let .original leading startPos _ _ := allCommands[0]!.getHeadInfo
       | throwErrorAt allCommands[0]! "Failed to get source position"
-    let .original _ _ trailing stopPos := allCommands.back.getTailInfo
-      | throwErrorAt allCommands.back "Failed to get source position"
+    let .original _ _ trailing stopPos := Compat.Array.back! allCommands |>.getTailInfo
+      | throwErrorAt (Compat.Array.back! allCommands) "Failed to get source position"
     let text ← getFileMap
     let str := text.source.extract leading.startPos trailing.stopPos
     let mod ← getMainModule

src/examples/SubVerso/Examples/Slice.lean

@@ -235,9 +235,10 @@ def sliceSyntax [Monad m] [MonadEnv m] [MonadError m] [MonadFileMap m] (stx : Sy
   let env ← getEnv
   let mut sliced : HashMap String Syntax := {}
   for (s, _) in ss.toArray do
-    let rem := ss.erase s |>.toList |>.bind (·.snd.toList) |>.toArray
+    let rem := ss.erase s |>.toList |> (Compat.List.flatMap · (·.snd.toList)) |>.toArray
     sliced := sliced.insert s (removeRanges env rem stx')
-  let residual := removeRanges env (ss.toList.bind (·.snd.toList) |>.toArray) stx'
+  let residual :=
+    removeRanges env (ss.toList |> (Compat.List.flatMap · (·.snd.toList)) |>.toArray) stx'
 
   return {original := stx, residual, sliced}
 

src/highlighting/SubVerso/Highlighting/Code.lean

@@ -701,7 +701,7 @@ partial def findTactics
 
   -- Override states - some tactics show many intermediate states, which is overwhelming in rendered
   -- output. Get the right one to show for the whole thing, then adjust its positioning.
-  if let `(tactic|rw $[$_c:config]? [$_rs,*]%$brak $[$_l:location]?) := stx then
+  if let some brak := Compat.rwTacticRightBracket? stx then
     if let some (goals, _startPos, _endPos, _endPosition) ← findTactics ids trees brak then
       return some (goals, startPos.byteIdx, endPos.byteIdx, endPosition)