From 26bdce6a267528b8ce67a96cebd3adf4ebcf4cd8 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 30 Aug 2024 22:34:30 +0200
Subject: [PATCH] chore: compatibility shims for 2024-08-29

---
 .github/workflows/ci.yml                  |  3 +-
 src/compat/SubVerso/Compat.lean           | 34 ++++++++++++++++++++++-
 src/examples/SubVerso/Examples/Slice.lean |  6 ++--
 3 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index eda612f..ef297bb 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -20,8 +20,9 @@ jobs:
           - "4.8.0"
           - "4.9.0"
           - "4.10.0"
-          - "4.11.0-rc1"
+          - "4.11.0-rc3"
           - "nightly-2024-08-09"
+          - "nightly-2024-08-29"
         platform:
           - os: ubuntu-latest
             installer: |
diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
index 14aa90c..a522d75 100644
--- a/src/compat/SubVerso/Compat.lean
+++ b/src/compat/SubVerso/Compat.lean
@@ -45,6 +45,28 @@ elab "%first_succeeding" "[" es:term,* "]" : term <= ty => do
   throwError m!"No alternative succeeded. Attempts were: " ++
     indentD (MessageData.joinSep msgErrs Format.line)
 
+scoped syntax "export_from_namespaces " "(" ident+ ") " "(" ident+ ")" : command
+
+elab_rules : command
+  | `(export_from_namespaces ($nss*) ($xs*)) => do
+    let env ← getEnv
+    let mut toAlias := #[]
+    for x in xs do
+      let x' := x.getId
+      let mut found := none
+      for ns in nss do
+        let ns' := ns.getId
+        let y := ns' ++ x'
+        if env.contains y then
+          found := some (ns, x)
+          break
+      if let some ok := found then
+        toAlias := toAlias.push ok
+      else
+        throwErrorAt x "'{x}' not found in namespaces {indentD <| toMessageData nss}"
+    for (ns, x) in toAlias do
+      Command.elabCommand <| ← `(export $ns ($x))
+
 open Command in
 elab "%if_bound" x:ident cmd:command : command => do
   if (← getEnv).contains x.getId then elabCommand cmd
@@ -71,7 +93,17 @@ def refIdentCase (ri : Lsp.RefIdent)
   ]
 
 abbrev Parsec (α : Type) : Type :=
-  %first_succeeding [(Lean.Parsec α : Type), (Lean.Parsec String.Iterator α : Type)]
+  %first_succeeding [
+    (Lean.Parsec α : Type),
+    (Lean.Parsec String.Iterator α : Type),
+    (Std.Internal.Parsec String.Iterator α : Type)
+  ]
+
+namespace Parsec
+export_from_namespaces
+  (Lean.Parsec.String Lean.Parsec Std.Internal.Parsec.String Std.Internal.Parsec)
+  (ws skipString skipChar many1Chars satisfy)
+end Parsec
 
 def HashMap := %first_succeeding [Std.HashMap, Lean.HashMap]
 def HashSet := %first_succeeding [Std.HashSet, Lean.HashSet]
diff --git a/src/examples/SubVerso/Examples/Slice.lean b/src/examples/SubVerso/Examples/Slice.lean
index 4cbd96d..963d790 100644
--- a/src/examples/SubVerso/Examples/Slice.lean
+++ b/src/examples/SubVerso/Examples/Slice.lean
@@ -3,15 +3,15 @@ Copyright (c) 2024 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
-import Lean.Data.Parsec
+import Lean.Data.Json
 import Lean.Data.Position
 import Lean.Syntax
 import Lean.Elab.Command
 import SubVerso.Compat
 import SubVerso.Examples.Slice.Attribute
 
+open Lean (SourceInfo Syntax Environment FileMap MonadEnv MonadError MonadFileMap getFileMap getEnv nullKind)
 
-open Lean hiding Parsec HashMap
 open SubVerso.Compat (Parsec HashMap)
 
 namespace SubVerso.Examples.Slice
@@ -71,7 +71,7 @@ deriving Repr
 private def SliceCommand.beginRange := SliceCommand.mk true
 private def SliceCommand.endRange := SliceCommand.mk false
 
-open Lean.Parsec String in
+open SubVerso.Compat.Parsec String in
 private def sliceCommand (range : String.Range) : Parsec SliceCommand := do
   ws
   skipString "!!"