fix: compatibility with Lake and Lean changes (#65)

Closes #64

.github/workflows/ci.yml

@@ -26,8 +26,9 @@ jobs:
           - "4.12.0"
           - "4.13.0"
           - "4.14.0"
-          - "4.15.0-rc1"
-          - "nightly-2024-11-04"
+          - "4.15.0"
+          - "4.16.0-rc1"
+          - "nightly-2025-01-05"
         platform:
           - os: ubuntu-latest
             installer: |

README.md

@@ -9,7 +9,7 @@ library will maintain broader compatibility with various Lean versions.
 ## Versions and Compatibility
 
 SubVerso's CI currently validates it on every Lean release since
-4.3.0, along with whatever version or snapshot is currently targeted
+4.0.0, along with whatever version or snapshot is currently targeted
 by Verso itself.
 
 There should be no expectations of compatibility between different
@@ -64,4 +64,3 @@ def f (n : Nat) : Nat := %ex{plus23}{$ex{N}{n} + 23}
 then three pieces of highlighted code are saved, named `F` (the whole
 block), `plus23` (which contains `n + 23`), and `N` (which contains
 `n`).
-

Tests.lean

@@ -160,7 +160,7 @@ def main : IO UInt32 := do
     return 1
   else IO.println s!"Found {proofCount examplesToml} proofs"
 
-  IO.println "Checking that the test project generates at least some deserializable JSON"
+  IO.println "Checking that the test project generates at least some deserializable JSON with 4.3.0"
   cleanupDemo
   let examples ← loadExamples "demo"
   if examples.isEmpty then
@@ -174,23 +174,23 @@ def main : IO UInt32 := do
 
   IO.println "Checking that the test project generates at least some deserializable JSON with 4.8.0"
   cleanupDemo
-  let examples' ← loadExamples "demo" (overrideToolchain := some "leanprover/lean4:nightly-2024-04-25")
+  let examples' ← loadExamples "demo" (overrideToolchain := some "leanprover/lean4:v4.8.0")
   if examples'.isEmpty then
     IO.eprintln "No examples found with later toolchain"
     return 1
-  checkVersion "4.8.0-nightly-2024-04-25" examples'
+  checkVersion "4.8.0" examples'
   checkHasSorry examples'
   checkIsLinted examples'
   let proofCount2 := proofCount examples'
   IO.println s!"Found {proofCount2} proofs "
 
-  IO.println "Checking that the test project generates at least some deserializable JSON with 4.10.0-rc1"
+  IO.println "Checking that the test project generates at least some deserializable JSON with 4.10.0"
   cleanupDemo
-  let examples'' ← loadExamples "demo" (overrideToolchain := some "leanprover/lean4:4.10.0-rc1")
+  let examples'' ← loadExamples "demo" (overrideToolchain := some "leanprover/lean4:4.10.0")
   if examples''.isEmpty then
     IO.eprintln "No examples found with later toolchain"
     return 1
-  checkVersion "4.10.0-rc1" examples''
+  checkVersion "4.10.0" examples''
   checkHasSorry examples''
   checkIsLinted examples''
   let proofCount3 := proofCount examples''

lakefile.lean

@@ -2,6 +2,33 @@ import Lake
 open Lake DSL
 open System (FilePath)
 
+-- Minimal compatibility infrastructure to make this file cross-compatible with more Lean/Lake versions
+namespace Compat
+
+open Lean Elab Command in
+#eval show CommandElabM Unit from do
+  let env ← getEnv
+  let useOldBind := mkIdent `useOldBind
+  elabCommand <| ← `(def $useOldBind := !$(quote <| env.contains `Lake.buildFileUnlessUpToDate'))
+
+-- Compatibility shims for older Lake (where logging was manual) and
+-- newer Lake (where it isn't). Necessary from Lean 4.8.0 and up.
+open Lean Elab Command in
+#eval show CommandElabM Unit from do
+  let env ← getEnv
+  let m := mkIdent `m
+  if !env.contains `Lake.logStep || Linter.isDeprecated env `Lake.logStep then
+    elabCommand <| ← `(def $(mkIdent `logStep) [Pure $m] (message : String) : $m Unit := pure ())
+  else
+    elabCommand <| ← `(def $(mkIdent `logStep) := @Lake.logStep)
+  if !env.contains `Lake.logInfo || Linter.isDeprecated env `Lake.logStep then
+    elabCommand <| ← `(def $(mkIdent `logInfo) [Pure $m] (message : String) : $m Unit := pure ())
+  else
+    elabCommand <| ← `(def $(mkIdent `logInfo) := @Lake.logInfo)
+
+end Compat
+-- End compatibility infrastructure
+
 package «subverso» where
   precompileModules := true
   -- add package configuration options here
@@ -38,64 +65,97 @@ lean_exe «subverso-extract-mod» where
   root := `ExtractModule
   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 highlighted mod : FilePath := do
-  let ws ← getWorkspace
-  let some extract ← findLeanExe? `«subverso-extract-mod»
-    | error "The subverso-extract-mod executable was not found"
-
-  let exeJob ← extract.exe.fetch
-  let modJob ← mod.olean.fetch
-
-  let buildDir := ws.root.buildDir
-  let hlFile := mod.filePath (buildDir / "highlighted") "json"
-
-  exeJob.bindAsync fun exeFile exeTrace =>
-    modJob.bindSync fun _oleanPath modTrace => do
-      let depTrace := mixTrace exeTrace modTrace
-      let trace ← buildFileUnlessUpToDate hlFile depTrace do
-        logStep s!"Exporting highlighted source file JSON for '{mod.name}'"
-        proc {
-          cmd := exeFile.toString
-          args := #[mod.name.toString, hlFile.toString]
-          env := ← getAugmentedEnv
-        }
-      pure (hlFile, trace)
-
-module_facet examples mod : FilePath := do
-  let ws ← getWorkspace
-  let some extract ← findLeanExe? `«subverso-extract»
-    | error "The subverso-extract executable was not found"
-
-  let exeJob ← extract.exe.fetch
-  let modJob ← mod.olean.fetch
-
-  let buildDir := ws.root.buildDir
-  let hlFile := mod.filePath (buildDir / "examples") "json"
-
-  exeJob.bindAsync fun exeFile exeTrace =>
-    modJob.bindSync fun _oleanPath modTrace => do
-      let depTrace := mixTrace exeTrace modTrace
-      let trace ← buildFileUnlessUpToDate hlFile depTrace do
-        logStep s!"Exporting highlighted example JSON for '{mod.name}'"
-        proc {
-          cmd := exeFile.toString
-          args := #[mod.name.toString, hlFile.toString]
-          env := ← getAugmentedEnv
-        }
-      pure (hlFile, trace)
+meta if Compat.useOldBind then
+  module_facet highlighted mod : FilePath := do
+    let ws ← getWorkspace
+    let some extract ← findLeanExe? `«subverso-extract-mod»
+      | error "The subverso-extract-mod executable was not found"
+
+    let exeJob ← extract.exe.fetch
+    let modJob ← mod.olean.fetch
+
+    let buildDir := ws.root.buildDir
+    let hlFile := mod.filePath (buildDir / "highlighted") "json"
+
+    exeJob.bindAsync fun exeFile exeTrace =>
+      modJob.bindSync fun _oleanPath modTrace => do
+        let depTrace := mixTrace exeTrace modTrace
+        let trace ← buildFileUnlessUpToDate hlFile depTrace do
+          Compat.logStep s!"Exporting highlighted source file JSON for '{mod.name}'"
+          proc {
+            cmd := exeFile.toString
+            args := #[mod.name.toString, hlFile.toString]
+            env := ← getAugmentedEnv
+          }
+        pure (hlFile, trace)
+
+else
+  module_facet highlighted mod : FilePath := do
+    let ws ← getWorkspace
+    let some extract ← findLeanExe? `«subverso-extract-mod»
+      | error "The subverso-extract-mod executable was not found"
+
+    let exeJob ← extract.exe.fetch
+    let modJob ← mod.olean.fetch
+
+    let buildDir := ws.root.buildDir
+    let hlFile := mod.filePath (buildDir / "highlighted") "json"
+
+    exeJob.bindM fun exeFile =>
+      modJob.mapM fun _oleanPath => do
+        buildFileUnlessUpToDate' (text := true) hlFile <|
+          proc {
+            cmd := exeFile.toString
+            args :=  #[mod.name.toString, hlFile.toString]
+            env := ← getAugmentedEnv
+          }
+        pure hlFile
+
+meta if Compat.useOldBind then
+  module_facet examples mod : FilePath := do
+    let ws ← getWorkspace
+    let some extract ← findLeanExe? `«subverso-extract»
+      | error "The subverso-extract executable was not found"
+
+    let exeJob ← extract.exe.fetch
+    let modJob ← mod.olean.fetch
+
+    let buildDir := ws.root.buildDir
+    let hlFile := mod.filePath (buildDir / "examples") "json"
+
+    exeJob.bindAsync fun exeFile exeTrace =>
+      modJob.bindSync fun _oleanPath modTrace => do
+        let depTrace := mixTrace exeTrace modTrace
+        let trace ← buildFileUnlessUpToDate hlFile depTrace do
+          Compat.logStep s!"Exporting highlighted example JSON for '{mod.name}'"
+          proc {
+            cmd := exeFile.toString
+            args := #[mod.name.toString, hlFile.toString]
+            env := ← getAugmentedEnv
+          }
+        pure (hlFile, trace)
+
+else
+  module_facet examples mod : FilePath := do
+    let ws ← getWorkspace
+    let some extract ← findLeanExe? `«subverso-extract»
+      | error "The subverso-extract executable was not found"
+
+    let exeJob ← extract.exe.fetch
+    let modJob ← mod.olean.fetch
+
+    let buildDir := ws.root.buildDir
+    let hlFile := mod.filePath (buildDir / "examples") "json"
+
+    exeJob.bindM fun exeFile =>
+      modJob.mapM fun _oleanPath => do
+        buildFileUnlessUpToDate' (text := true) hlFile do
+          proc {
+            cmd := exeFile.toString
+            args := #[mod.name.toString, hlFile.toString]
+            env := ← getAugmentedEnv
+          }
+        pure hlFile
 
 library_facet highlighted lib : FilePath := do
   let ws ← getWorkspace
@@ -125,7 +185,7 @@ package_facet highlighted pkg : FilePath := do
   let buildDir := ws.root.buildDir
   let hlDir := buildDir / "highlighted"
   libJobs.bindSync fun () trace => do
-    logInfo s!"Highlighted code written to '{hlDir}'"
+    Compat.logInfo s!"Highlighted code written to '{hlDir}'"
     pure (hlDir, trace)
 
 package_facet examples pkg : FilePath := do
@@ -135,5 +195,5 @@ package_facet examples pkg : FilePath := do
   let buildDir := ws.root.buildDir
   let hlDir := buildDir / "examples"
   libJobs.bindSync fun () trace => do
-    logInfo s!"Highlighted code written to '{hlDir}'"
+    Compat.logInfo s!"Highlighted code written to '{hlDir}'"
     pure (hlDir, trace)

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.15.0

src/compat/SubVerso/Compat.lean

@@ -31,7 +31,9 @@ def realizeNameNoOverloads
 
 elab "%first_succeeding" "[" es:term,* "]" : term <= ty => do
   let mut errs := #[]
+  let msgs ← Core.getMessageLog
   for e in es.getElems do
+    Core.setMessageLog msgs
     try
       let expr ←
         withReader ({· with errToSorry := false}) <|