Bml: Syntax, run separate CI action

.github/workflows/build.yml

@@ -11,7 +11,7 @@ jobs:
     name: Build
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
@@ -25,11 +25,29 @@ jobs:
       - name: make
         run: make
 
+  bml:
+    name: Build Bml
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: make bml
+        run: make bml
+
   stats:
     name: Stats
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: install ripgrep
         run: sudo apt install -y ripgrep
@@ -41,3 +59,11 @@ jobs:
       - name: count sorries
         run: |
           rg --count-matches sorry Pdl | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}'
+
+      - name: Bml count lines in src
+        run: |
+          shopt -s globstar
+          wc -l Bml/**/*.lean
+      - name: Bml count sorries
+        run: |
+          rg --count-matches sorry Bml | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}'

Bml.lean

@@ -0,0 +1,14 @@
+-- This module serves as the root of the `Pdl` library.
+-- Import modules here that should be built as part of the library.
+import «Bml».Syntax
+-- TODO import «Bml».Semantics
+-- TODO import «Bml».Setsimp
+-- TODO import «Bml».Modelgraphs
+-- TODO import «Bml».Tableau
+-- TODO import «Bml».Examples
+-- TODO import «Bml».Vocabulary
+-- TODO import «Bml».Soundness
+-- TODO import «Bml».Tableauexamples
+-- TODO import «Bml».Completeness
+-- TODO import «Bml».Partitions
+-- TODO import «Bml».Interpolation

Bml/Syntax.lean

@@ -1,10 +1,8 @@
 -- SYNTAX
-import Data.Set.Finite
-import Algebra.BigOperators.Basic
+import Mathlib.Data.Finset.Basic
 
-#align_import syntax
+import Mathlib.Algebra.BigOperators.Basic
 
--- Definition 1, page 4
 -- Definition 1, page 4
 inductive Formula : Type
   | bottom : Formula
@@ -13,20 +11,11 @@ inductive Formula : Type
   | And : Formula → Formula → Formula
   | box : Formula → Formula
   deriving DecidableEq
-#align formula Formula
 
 -- Predefined atomic propositions for convenience
-def p :=
-  Formula.atom_prop 'p'
-#align p p
-
-def q :=
-  Formula.atom_prop 'q'
-#align q q
-
-def r :=
-  Formula.atom_prop 'r'
-#align r r
+def p := Formula.atom_prop 'p'
+def q := Formula.atom_prop 'q'
+def r := Formula.atom_prop 'r'
 
 notation "·" -- Notation and abbreviations
 c => Formula.atom_prop c
@@ -35,11 +24,10 @@ prefix:88 "~" => Formula.neg
 
 prefix:77 "□" => Formula.box
 
-infixr:66 "⋏" => Formula.and
+infixr:66 "⋏" => Formula.And
 
 @[simp]
-def impl (φ ψ : Formula) :=
-  ~(φ⋏~ψ)
+def impl (φ ψ : Formula) := ~(φ ⋏ ~ψ)
 #align impl impl
 
 infixr:55 "↣" => impl
@@ -56,71 +44,57 @@ instance : Top Formula :=
 -- showing formulas as strings that are valid Lean code
 def formToString : Formula → String
   | ⊥ => "⊥"
-  | ·c => repr c
+  | ·c => sorry -- repr c
   | ~ϕ => "~" ++ formToString ϕ
   | ϕ⋏ψ => "(" ++ formToString ϕ ++ " ⋏ " ++ formToString ψ ++ ")"
   | □ϕ => "(□ " ++ formToString ϕ ++ ")"
-#align formToString formToString
 
-instance : Repr Formula :=
-  ⟨formToString⟩
+-- instance : Repr Formula :=
+--   ⟨formToString⟩
 
 -- COMPLEXITY
 -- this should later be the measure from Lemma 2, page 20
 @[simp]
 def lengthOfFormula : Formula → ℕ
   | ⊥ => 1
-  |-- FIXME: has bad width
-    ·c =>
-    1
+  | ·_ => 1
   | ~φ => 1 + lengthOfFormula φ
   | φ⋏ψ => 1 + lengthOfFormula φ + lengthOfFormula ψ
   | □φ => 1 + lengthOfFormula φ
-#align lengthOfFormula lengthOfFormula
 
 @[simp]
 def lengthOfSet : Finset Formula → ℕ
-  | X => X.Sum lengthOfFormula
-#align lengthOfSet lengthOfSet
+  | X => X.sum lengthOfFormula
 
 class HasLength (α : Type) where
   lengthOf : α → ℕ
-#align hasLength HasLength
 
 open HasLength
 
 instance formulaHasLength : HasLength Formula :=
   HasLength.mk lengthOfFormula
-#align formula_hasLength formulaHasLength
 
 instance setFormulaHasLength : HasLength (Finset Formula) :=
   HasLength.mk lengthOfSet
-#align setFormula_hasLength setFormulaHasLength
 
 @[simp]
 def complexityOfFormula : Formula → ℕ
   | ⊥ => 1
-  | ·c => 1
+  | ·_ => 1
   | ~φ => 1 + complexityOfFormula φ
   | φ⋏ψ => 1 + max (complexityOfFormula φ) (complexityOfFormula ψ)
   | □φ => 1 + complexityOfFormula φ
-#align complexityOfFormula complexityOfFormula
 
 def complexityOfSet : Finset Formula → ℕ
-  | X => X.Sum complexityOfFormula
-#align complexityOfSet complexityOfSet
+  | X => X.sum complexityOfFormula
 
 class HasComplexity (α : Type) where
   complexityOf : α → ℕ
-#align hasComplexity HasComplexity
 
 open HasComplexity
 
 instance formulaHasComplexity : HasComplexity Formula :=
   HasComplexity.mk complexityOfFormula
-#align formula_hasComplexity formulaHasComplexity
 
 instance setFormulaHasComplexity : HasComplexity (Finset Formula) :=
   HasComplexity.mk complexityOfSet
-#align setFormula_hasComplexity setFormulaHasComplexity
-

Makefile

@@ -2,6 +2,9 @@
 default: .first-run-done
 	lake build
 
+bml: .first-run-done
+	lake build Bml
+
 # https://leanprover-community.github.io/install/project.html#creating-a-lean-project
 .first-run-done:
 	lake exe cache get

lakefile.lean

@@ -10,3 +10,6 @@ require mathlib from git
 @[default_target]
 lean_lib «Pdl» where
   -- add any library configuration options here
+
+lean_lib «Bml» where
+  -- add any library configuration options here