chore: run tests, also on more versions

leanprover · Feb 28, 2024 · 50059af · 50059af
1 parent 9e6c9a7
commit 50059af
Show file tree

Hide file tree

Showing 6 changed files with 725 additions and 5 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -9,6 +9,8 @@ jobs:
     strategy:
       matrix:
         toolchain:
+          - "leanprover/lean4:4.3.0"
+          - "leanprover/lean4:4.4.0"
           - "leanprover/lean4:4.5.0"
           - "leanprover/lean4:4.6.0-rc1"
     name: Build and test
@@ -43,3 +45,7 @@ jobs:
       - name: Build the project
         run: |
           lake build
+
+      - name: Run tests
+        run: |
+          lake exe subverso-tests
diff --git a/Tests.lean b/Tests.lean
@@ -1 +1,3 @@
+import Subverso.Highlighting
+
 def main : IO UInt32 := pure 0
diff --git a/lake-manifest.json b/lake-manifest.json
diff --git a/src/highlighting/Subverso/Highlighting.lean b/src/highlighting/Subverso/Highlighting.lean
@@ -0,0 +1,2 @@
+import Subverso.Highlighting.Highlighted
+import Subverso.Highlighting.Code
Original file line number	Diff line number	Diff line change
		@@ -1 +1,3 @@
		import Subverso.Highlighting

		def main : IO UInt32 := pure 0
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		import Subverso.Highlighting.Highlighted
		import Subverso.Highlighting.Code