chore: update CI matrix and compatibility (#38)

Supports generalized `Lean.Parsec`
leanprover · Aug 8, 2024 · 812038c · 812038c
1 parent cd093ca
commit 812038c
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 3 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -17,7 +17,8 @@ jobs:
           - "4.8.0"
           - "4.9.0"
           - "4.10.0"
-          - "nightly-2024-08-03"
+          - "4.11.0-rc1"
+          - "nightly-2024-08-08"
         platform:
           - os: ubuntu-latest
             installer: |

diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
@@ -57,3 +57,6 @@ def refIdentCase (ri : Lsp.RefIdent)
     | .fvar id => onFVar id
     | .const x => onConst x
   ]
+
+abbrev Parsec (α : Type) : Type :=
+  %first_succeeding [(Lean.Parsec α : Type), (Lean.Parsec String.Iterator α : Type)]
diff --git a/src/examples/SubVerso/Examples/Slice.lean b/src/examples/SubVerso/Examples/Slice.lean
@@ -7,9 +7,12 @@ import Lean.Data.Parsec
 import Lean.Data.Position
 import Lean.Syntax
 import Lean.Elab.Command
+import SubVerso.Compat
 import SubVerso.Examples.Slice.Attribute
 
-open Lean
+
+open Lean hiding Parsec
+open SubVerso.Compat (Parsec)
 
 namespace SubVerso.Examples.Slice
 
@@ -68,7 +71,7 @@ deriving Repr
 private def SliceCommand.beginRange := SliceCommand.mk true
 private def SliceCommand.endRange := SliceCommand.mk false
 
-open Parsec in
+open Lean.Parsec String in
 private def sliceCommand (range : String.Range) : Parsec SliceCommand := do
   ws
   skipString "!!"