chore: compatibility with lakefile.toml in subprojects

Tests.lean

@@ -90,11 +90,11 @@ def Example.countProofStates (e : Example) : Nat :=
 end Examples
 end SubVerso
 
-def cleanupDemo : IO Unit := do
-  if ← System.FilePath.pathExists "demo/lake-manifest.json" then
-    IO.FS.removeFile "demo/lake-manifest.json"
-  if ← System.FilePath.isDir "demo/.lake" then
-    IO.FS.removeDirAll "demo/.lake"
+def cleanupDemo (demo : System.FilePath := "demo") : IO Unit := do
+  if ← System.FilePath.pathExists (demo / "lake-manifest.json") then
+    IO.FS.removeFile (demo / "lake-manifest.json")
+  if ← System.FilePath.isDir (demo / ".lake") then
+    IO.FS.removeDirAll (demo / ".lake")
 
 open Lean in
 def proofCount (examples : NameMap (NameMap Example)) : Nat := Id.run do
@@ -120,6 +120,14 @@ def main : IO UInt32 := do
     IO.println "and actual:"
     IO.println expectedLog
 
+  IO.println "Checking that the TOML project will load"
+  cleanupDemo (demo := "demo-toml")
+  let examplesToml ← loadExamples "demo-toml"
+  if examplesToml.isEmpty then
+    IO.eprintln "No examples found"
+    return 1
+  else IO.println s!"Found {proofCount examplesToml} proofs"
+
   IO.println "Checking that the test project generates at least some deserializable JSON"
   cleanupDemo
   let examples ← loadExamples "demo"

demo-toml/.gitignore

@@ -0,0 +1 @@
+/.lake

demo-toml/Demo.lean

@@ -0,0 +1,30 @@
+-- This module serves as the root of the `Demo` library.
+-- Import modules here that should be built as part of the library.
+import «Demo».Basic
+
+import SubVerso.Examples
+
+open SubVerso.Examples
+
+%example version
+#eval Lean.versionString
+%end
+
+%example xdef
+def f (x : Nat) := %ex{add}{33 + %ex{X}{x}}
+%end
+
+%example proof
+theorem test (n : Nat) : n * 1 = n := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [← ih]
+    simp
+%end
+
+%example proofWithInstance
+-- Test that proof states containing daggered names can round-trip
+def test2 [ToString α] (x : α) : Decidable (toString x = "") := by
+  constructor; sorry
+%end

demo-toml/Demo/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

demo-toml/Main.lean

@@ -0,0 +1,4 @@
+import «Demo»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

demo-toml/lakefile.toml

@@ -0,0 +1,13 @@
+name = "demo"
+defaultTargets = ["demo"]
+
+[[require]]
+name = "subverso"
+git = ".."
+
+[[lean_lib]]
+name = "Demo"
+
+[[lean_exe]]
+name = "demo"
+root = "Main"

demo-toml/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.8.0-rc1

src/examples/SubVerso/Examples.lean

@@ -155,8 +155,9 @@ partial def loadExamples
   let projectDir := ((← IO.currentDir) / leanProject).normalize
   -- Validate that the path is really a Lean project
   let lakefile := projectDir / "lakefile.lean"
-  if !(← lakefile.pathExists) then
-    throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project"
+  let lakefile' := projectDir / "lakefile.toml"
+  if !(← lakefile.pathExists) && !(← lakefile'.pathExists) then
+    throw <| .userError s!"Neither {lakefile} nor {lakefile'} exist, couldn't load project"
   let toolchain ← match overrideToolchain with
     | none =>
       let toolchainfile := projectDir / "lean-toolchain"
@@ -210,18 +211,18 @@ where
         let sub ← collectExamples (.str modName f.fileName) f.path
         out := out.mergeBy (fun _ j1 j2 => j1.mergeBy (fun _ _ x => x) j2) sub
       | .file =>
-        if f.path.extension == some "json" then
+        if f.path.extension == some "json" && f.path.fileStem.map (·.takeRight 4) != some ".log" then
           if let some mod := f.path.fileStem then
             let name' : Name := .str modName mod
             let contents := Json.parse (← IO.FS.readFile f.path)
             match contents with
             | .error err => throw <| .userError s!"Couldn't parse {f.path} as JSON: {err}"
             | .ok val =>
               let .ok o := val.getObj?
-                | throw <| IO.userError "Expected JSON object in '{f.path}'"
+                | throw <| IO.userError s!"Expected JSON object in '{f.path}', got {val}"
               for ⟨exName, exJson⟩ in o.toArray do
                 match FromJson.fromJson? (α := Example) exJson with
-                | .error err => throw <| IO.userError s!"Couldn't deserialized example: {err}"
+                | .error err => throw <| IO.userError s!"Couldn't deserialize example '{exName}': {err}"
                 | .ok ex => out := out.insert name' (out.find? name' |>.getD {} |>.insert exName.toName ex)
       | _ => pure ()
     return out