diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index 7c287c4c95..0000000000 --- a/lakefile.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Lake - -open Lake DSL - -package batteries where - leanOptions := #[⟨`linter.missingDocs, true⟩] - -@[default_target] -lean_lib Batteries - -@[default_target, lint_driver] -lean_exe runLinter where - srcDir := "scripts" - supportInterpreter := true - -@[test_driver] -lean_exe test where - srcDir := "scripts" diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000000..a8a658ef9f --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,19 @@ +name = "batteries" +testDriver = "test" +lintDriver = "runLinter" +defaultTargets = ["Batteries", "runLinter"] + +[leanOptions] +linter.missingDocs = true + +[[lean_lib]] +name = "Batteries" + +[[lean_exe]] +name = "runLinter" +srcDir = "scripts" +supportInterpreter = true + +[[lean_exe]] +name = "test" +srcDir = "scripts"