Merge pull request #5 from leanprover-community/toml

chore: migrate to lakefile.toml
leanprover-community · May 6, 2024 · 7cec593 · 7cec593
2 parents 188eb34 + 2c958bd
commit 7cec593
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 21 deletions.
diff --git a/lakefile.lean b/lakefile.lean
diff --git a/lakefile.toml b/lakefile.toml
@@ -0,0 +1,24 @@
+name = "importGraph"
+defaultTargets = ["ImportGraph", "graph"]
+
+[[require]]
+name = "Cli"
+git = "https://github.com/leanprover/lean4-cli"
+rev = "main"
+
+[[require]]
+name = "std"
+git = "https://github.com/leanprover/std4"
+rev = "main"
+
+[[lean_lib]]
+name = "ImportGraph"
+
+# `lake exe graph` constructs import graphs in `.dot` or graphical formats.
+[[lean_exe]]
+name = "graph"
+root = "Main"
+# Enables the use of the Lean interpreter by the executable (e.g., `runFrontend`) 
+# at the expense of increased binary size on Linux.
+# Remove this line if you do not need such functionality.
+supportInterpreter = true