From 41cfd960ba1cd2b22af41cf536988d0f33fe8f5c Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 15 May 2024 11:12:06 +0200 Subject: [PATCH] chore: compatibility with lakefile.toml in subprojects --- Tests.lean | 18 ++++++++++++----- demo-toml/.gitignore | 1 + demo-toml/Demo.lean | 30 +++++++++++++++++++++++++++++ demo-toml/Demo/Basic.lean | 1 + demo-toml/Main.lean | 4 ++++ demo-toml/lakefile.toml | 13 +++++++++++++ demo-toml/lean-toolchain | 1 + src/examples/SubVerso/Examples.lean | 11 ++++++----- 8 files changed, 69 insertions(+), 10 deletions(-) create mode 100644 demo-toml/.gitignore create mode 100644 demo-toml/Demo.lean create mode 100644 demo-toml/Demo/Basic.lean create mode 100644 demo-toml/Main.lean create mode 100644 demo-toml/lakefile.toml create mode 100644 demo-toml/lean-toolchain diff --git a/Tests.lean b/Tests.lean index 6179f38..3c7c4e1 100644 --- a/Tests.lean +++ b/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" diff --git a/demo-toml/.gitignore b/demo-toml/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/demo-toml/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/demo-toml/Demo.lean b/demo-toml/Demo.lean new file mode 100644 index 0000000..2e70ebc --- /dev/null +++ b/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 diff --git a/demo-toml/Demo/Basic.lean b/demo-toml/Demo/Basic.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/demo-toml/Demo/Basic.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/demo-toml/Main.lean b/demo-toml/Main.lean new file mode 100644 index 0000000..4a6d743 --- /dev/null +++ b/demo-toml/Main.lean @@ -0,0 +1,4 @@ +import «Demo» + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/demo-toml/lakefile.toml b/demo-toml/lakefile.toml new file mode 100644 index 0000000..2ca2305 --- /dev/null +++ b/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" diff --git a/demo-toml/lean-toolchain b/demo-toml/lean-toolchain new file mode 100644 index 0000000..d8a6d7e --- /dev/null +++ b/demo-toml/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.8.0-rc1 diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index 3dac222..0fc7cff 100644 --- a/src/examples/SubVerso/Examples.lean +++ b/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,7 +211,7 @@ 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) @@ -218,10 +219,10 @@ where | .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