Switched to using lakefile.lean instead of lakefile.toml

Author: bwbush

.gitignore

@@ -29,3 +29,4 @@ _build
 /simulation/docs/_minted-sim-realism/
 /data/simulation/*.trace.json
 /data/simulation/*.array.schema.json
+node_modules/

analysis/markov/lakefile.lean

@@ -0,0 +1,22 @@
+
+import Lake
+
+open Lake DSL
+
+package «linleios» where
+
+lean_lib «Linleios» where
+
+@[default_target]
+lean_exe «linleios» where
+  root := `Main
+  supportInterpreter := false
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
+
+require Parser from git
+  "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
+
+require Cli from git
+  "https://github.com/mhuisi/lean4-cli" @ "v4.20.0"