chore: compatibility shims for Lake modifications

leanprover · May 14, 2024 · ee669c2 · ee669c2
1 parent daac07d
commit ee669c2
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -14,7 +14,7 @@ jobs:
           - "4.5.0"
           - "4.6.0"
           - "4.7.0"
-          - "nightly-2024-04-07"
+          - "4.8.0-rc1"
         platform:
           - os: ubuntu-latest
             installer: |

diff --git a/lakefile.lean b/lakefile.lean
@@ -26,6 +26,18 @@ lean_exe «subverso-extract» where
   root := `Extract
   supportInterpreter := true
 
+-- Compatibility shims for older Lake (where logging was manual) and
+-- newer Lake (where it isn't). Necessary from Lean 4.8.0 and up.
+section
+open Lean Elab Command
+#eval show CommandElabM Unit from do
+  let env ← getEnv
+  if !env.contains `Lake.logStep then
+    elabCommand <| ← `(def $(mkIdent `logStep) [Pure $(mkIdent `m)] (message : String) : $(mkIdent `m) Unit := pure ())
+  if !env.contains `Lake.logInfo then
+    elabCommand <| ← `(def $(mkIdent `logInfo) [Pure $(mkIdent `m)] (message : String) : $(mkIdent `m) Unit := pure ())
+end
+
 module_facet examples mod : FilePath := do
   let ws ← getWorkspace
   let some extract ← findLeanExe? `«subverso-extract»