Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: compatibility with lakefile.toml in subprojects #23

Merged
merged 1 commit into from
May 15, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 13 additions & 5 deletions Tests.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"
Expand Down
1 change: 1 addition & 0 deletions demo-toml/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
/.lake
30 changes: 30 additions & 0 deletions demo-toml/Demo.lean
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions demo-toml/Demo/Basic.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
def hello := "world"
4 changes: 4 additions & 0 deletions demo-toml/Main.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
import «Demo»

def main : IO Unit :=
IO.println s!"Hello, {hello}!"
13 changes: 13 additions & 0 deletions demo-toml/lakefile.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
name = "demo"
defaultTargets = ["demo"]

[[require]]
name = "subverso"
git = ".."

[[lean_lib]]
name = "Demo"

[[lean_exe]]
name = "demo"
root = "Main"
1 change: 1 addition & 0 deletions demo-toml/lean-toolchain
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
leanprover/lean4:v4.8.0-rc1
11 changes: 6 additions & 5 deletions src/examples/SubVerso/Examples.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
Loading