feat: run tests in CI

Author: Vtec234

.github/workflows/build.yml

@@ -56,6 +56,9 @@ jobs:
       - name: Build demos
         run: lake build ProofWidgets.Demos
 
+      - name: Run tests
+        run: lake test
+
       - name: Create GitHub release for tag (Ubuntu)
         if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest'
         uses: softprops/action-gh-release@v2

lakefile.lean

@@ -101,3 +101,7 @@ lean_lib ProofWidgets where
 lean_lib ProofWidgets.Demos where
   needs := #[widgetJsAll]
   globs := #[.submodules `ProofWidgets.Demos]
+
+@[test_driver]
+lean_lib test where
+  globs := #[.submodules `test]

test/checkh.lean

@@ -3,6 +3,7 @@ import ProofWidgets.Extra.CheckHighlight
 /-- info: Decidable.em (p : Prop) : p ∨ ¬p -/
 #guard_msgs in
 #checkh Decidable.em
+
 /-- info: Decidable.em (p : Prop) [Decidable p] : p ∨ ¬p -/
 #guard_msgs in
 #checkh' Decidable.em