From 65874dc789101ee9711fe52f4f24f6faff88f195 Mon Sep 17 00:00:00 2001 From: Matej Penciak Date: Thu, 16 Jan 2025 17:38:39 -0500 Subject: [PATCH] Update CI --- .github/workflows/ci.yaml | 6 ++++++ Lampe/Lampe.lean | 33 ++++++++++++++++++++++++++++----- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 3edbe94..2fa342c 100644 --- a/.github/workflows/ci.yaml +++ b/.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: diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index b74e921..a662bc5 100644 --- a/Lampe/Lampe.lean +++ b/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