Update CI

.github/workflows/ci.yaml

@@ -18,9 +18,15 @@ jobs:
                 lint: false
                 use-mathlib-cache: true
                 lake-package-directory: Lampe
+            - name: mk_all (lake)
+              working-directory: Lampe
+              run: lake exe mk_all --check --lib Lampe
             - name: Build (lake)
               working-directory: Lampe
               run: lake build
+            - name: Test (lake)
+              working-directory: Lampe
+              run: lake test
     build-cargo:
       runs-on: ubuntu-latest
       steps:

Lampe/Lampe.lean

@@ -1,9 +1,32 @@
-import Lampe.Semantics
-import Lampe.Syntax
 import Lampe.Ast
-import Lampe.Tp
-import Lampe.Lens
-import Lampe.Hoare.Total
+import Lampe.Builtin.Arith
+import Lampe.Builtin.Array
+import Lampe.Builtin.Basic
+import Lampe.Builtin.BigInt
+import Lampe.Builtin.Bit
+import Lampe.Builtin.Cast
+import Lampe.Builtin.Cmp
+import Lampe.Builtin.Field
+import Lampe.Builtin.Helpers
+import Lampe.Builtin.Lens
+import Lampe.Builtin.Memory
+import Lampe.Builtin.Slice
+import Lampe.Builtin.Str
+import Lampe.Builtin.Struct
+import Lampe.Data.Field
+import Lampe.Data.HList
+import Lampe.Data.Integers
+import Lampe.Hoare.Builtins
 import Lampe.Hoare.SepTotal
+import Lampe.Hoare.Total
+import Lampe.Lens
+import Lampe.Semantics
+import Lampe.SeparationLogic.LawfulHeap
+import Lampe.SeparationLogic.SLP
+import Lampe.SeparationLogic.State
+import Lampe.SeparationLogic.ValHeap
+import Lampe.Syntax
+import Lampe.Tactic.IntroCases
 import Lampe.Tactic.SeparationLogic
 import Lampe.Tactic.Traits
+import Lampe.Tp