chore: Establish initial structure

leanprover · Feb 28, 2024 · 9e6c9a7 · 9e6c9a7
1 parent 304dc71
commit 9e6c9a7
Show file tree

Hide file tree

Showing 10 changed files with 18 additions and 18 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
 /build
-/lakefile.olean
+*.olean
 /lake-packages/*
+/.lake
diff --git a/Main.lean b/Main.lean
diff --git a/Subverso.lean b/Subverso.lean
diff --git a/Subverso/Basic.lean b/Subverso/Basic.lean
diff --git a/Tests.lean b/Tests.lean
@@ -0,0 +1 @@
+def main : IO UInt32 := pure 0
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "subverso",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -4,13 +4,14 @@ open Lake DSL
 package «subverso» where
   -- add package configuration options here
 
-lean_lib «Subverso» where
-  -- add library configuration options here
+lean_lib SubversoHighlighting where
+  srcDir := "src/highlighting"
+  roots := #[`Subverso.Highlighting]
+
+lean_lib SubversoExamples where
+  srcDir := "src/examples"
+  roots := #[`Subverso.Examples]
 
 @[default_target]
-lean_exe «subverso» where
-  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
+lean_exe «subverso-tests» where
+  root := `Tests
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-stable
+leanprover/lean4:nightly-2024-02-26
diff --git a/src/examples/Subverso/Examples.lean b/src/examples/Subverso/Examples.lean
diff --git a/src/highlighting/Subverso/Highlighting.lean b/src/highlighting/Subverso/Highlighting.lean