feat: move to the module system

.github/workflows/lean_action_ci.yml

@@ -17,11 +17,14 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail --iofail"
-          mk_all-check: "true"
-      - name: "lake exe shake"
+      - name: "lake exe mk_all --check --module"
         run: |
           set -e
-          lake exe shake Cslib
+          lake exe mk_all --check --module
+      #- name: "lake exe shake"
+      #  run: |
+      #    set -e
+      #    lake exe shake Cslib
       - uses: leanprover-community/lint-style-action@main
         with:
           mode: check

Cslib.lean

@@ -1,78 +1,80 @@
-import Cslib.Algorithms.Lean.MergeSort.MergeSort
-import Cslib.Algorithms.Lean.TimeM
-import Cslib.Computability.Automata.Acceptors.Acceptor
-import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
-import Cslib.Computability.Automata.DA.Basic
-import Cslib.Computability.Automata.DA.Buchi
-import Cslib.Computability.Automata.DA.Prod
-import Cslib.Computability.Automata.DA.ToNA
-import Cslib.Computability.Automata.EpsilonNA.Basic
-import Cslib.Computability.Automata.EpsilonNA.ToNA
-import Cslib.Computability.Automata.NA.Basic
-import Cslib.Computability.Automata.NA.BuchiEquiv
-import Cslib.Computability.Automata.NA.BuchiInter
-import Cslib.Computability.Automata.NA.Concat
-import Cslib.Computability.Automata.NA.Hist
-import Cslib.Computability.Automata.NA.Loop
-import Cslib.Computability.Automata.NA.Prod
-import Cslib.Computability.Automata.NA.Sum
-import Cslib.Computability.Automata.NA.ToDA
-import Cslib.Computability.Automata.NA.Total
-import Cslib.Computability.Languages.ExampleEventuallyZero
-import Cslib.Computability.Languages.Language
-import Cslib.Computability.Languages.OmegaLanguage
-import Cslib.Computability.Languages.OmegaRegularLanguage
-import Cslib.Computability.Languages.RegularLanguage
-import Cslib.Foundations.Control.Monad.Free
-import Cslib.Foundations.Control.Monad.Free.Effects
-import Cslib.Foundations.Control.Monad.Free.Fold
-import Cslib.Foundations.Data.FinFun
-import Cslib.Foundations.Data.HasFresh
-import Cslib.Foundations.Data.Nat.Segment
-import Cslib.Foundations.Data.OmegaSequence.Defs
-import Cslib.Foundations.Data.OmegaSequence.Flatten
-import Cslib.Foundations.Data.OmegaSequence.InfOcc
-import Cslib.Foundations.Data.OmegaSequence.Init
-import Cslib.Foundations.Data.OmegaSequence.Temporal
-import Cslib.Foundations.Data.Relation
-import Cslib.Foundations.Lint.Basic
-import Cslib.Foundations.Semantics.FLTS.Basic
-import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
-import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
-import Cslib.Foundations.Semantics.FLTS.Prod
-import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Semantics.LTS.Bisimulation
-import Cslib.Foundations.Semantics.LTS.Simulation
-import Cslib.Foundations.Semantics.LTS.TraceEq
-import Cslib.Foundations.Semantics.ReductionSystem.Basic
-import Cslib.Foundations.Syntax.HasAlphaEquiv
-import Cslib.Foundations.Syntax.HasSubstitution
-import Cslib.Foundations.Syntax.HasWellFormed
-import Cslib.Init
-import Cslib.Languages.CCS.Basic
-import Cslib.Languages.CCS.BehaviouralTheory
-import Cslib.Languages.CCS.Semantics
-import Cslib.Languages.CombinatoryLogic.Basic
-import Cslib.Languages.CombinatoryLogic.Confluence
-import Cslib.Languages.CombinatoryLogic.Defs
-import Cslib.Languages.CombinatoryLogic.Evaluation
-import Cslib.Languages.CombinatoryLogic.Recursion
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
-import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
-import Cslib.Logics.LinearLogic.CLL.Basic
-import Cslib.Logics.LinearLogic.CLL.CutElimination
-import Cslib.Logics.LinearLogic.CLL.EtaExpansion
-import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
+module
+
+public import Cslib.Algorithms.Lean.MergeSort.MergeSort
+public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Computability.Automata.Acceptors.Acceptor
+public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
+public import Cslib.Computability.Automata.DA.Basic
+public import Cslib.Computability.Automata.DA.Buchi
+public import Cslib.Computability.Automata.DA.Prod
+public import Cslib.Computability.Automata.DA.ToNA
+public import Cslib.Computability.Automata.EpsilonNA.Basic
+public import Cslib.Computability.Automata.EpsilonNA.ToNA
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.NA.BuchiEquiv
+public import Cslib.Computability.Automata.NA.BuchiInter
+public import Cslib.Computability.Automata.NA.Concat
+public import Cslib.Computability.Automata.NA.Hist
+public import Cslib.Computability.Automata.NA.Loop
+public import Cslib.Computability.Automata.NA.Prod
+public import Cslib.Computability.Automata.NA.Sum
+public import Cslib.Computability.Automata.NA.ToDA
+public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Languages.ExampleEventuallyZero
+public import Cslib.Computability.Languages.Language
+public import Cslib.Computability.Languages.OmegaLanguage
+public import Cslib.Computability.Languages.OmegaRegularLanguage
+public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Foundations.Control.Monad.Free
+public import Cslib.Foundations.Control.Monad.Free.Effects
+public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Data.FinFun
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Data.Nat.Segment
+public import Cslib.Foundations.Data.OmegaSequence.Defs
+public import Cslib.Foundations.Data.OmegaSequence.Flatten
+public import Cslib.Foundations.Data.OmegaSequence.InfOcc
+public import Cslib.Foundations.Data.OmegaSequence.Init
+public import Cslib.Foundations.Data.OmegaSequence.Temporal
+public import Cslib.Foundations.Data.Relation
+public import Cslib.Foundations.Lint.Basic
+public import Cslib.Foundations.Semantics.FLTS.Basic
+public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
+public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
+public import Cslib.Foundations.Semantics.FLTS.Prod
+public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Semantics.LTS.Bisimulation
+public import Cslib.Foundations.Semantics.LTS.Simulation
+public import Cslib.Foundations.Semantics.LTS.TraceEq
+public import Cslib.Foundations.Semantics.ReductionSystem.Basic
+public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Foundations.Syntax.HasWellFormed
+public import Cslib.Init
+public import Cslib.Languages.CCS.Basic
+public import Cslib.Languages.CCS.BehaviouralTheory
+public import Cslib.Languages.CCS.Semantics
+public import Cslib.Languages.CombinatoryLogic.Basic
+public import Cslib.Languages.CombinatoryLogic.Confluence
+public import Cslib.Languages.CombinatoryLogic.Defs
+public import Cslib.Languages.CombinatoryLogic.Evaluation
+public import Cslib.Languages.CombinatoryLogic.Recursion
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Logics.LinearLogic.CLL.Basic
+public import Cslib.Logics.LinearLogic.CLL.CutElimination
+public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
+public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sorrachai Yingchareonthawornhcai
 -/
 
-import Cslib.Algorithms.Lean.TimeM
-import Mathlib.Data.Nat.Cast.Order.Ring
-import Mathlib.Data.Nat.Lattice
-import Mathlib.Data.Nat.Log
+module
 
+public import Cslib.Algorithms.Lean.TimeM
+public import Mathlib.Data.Nat.Cast.Order.Ring
+public import Mathlib.Data.Nat.Lattice
+public import Mathlib.Data.Nat.Log
+
+@[expose] public section
 
 /-!
 # MergeSort on a list

Cslib/Algorithms/Lean/TimeM.lean

@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sorrachai Yingchareonthawornhcai
 -/
 
+module
+
 import Cslib.Init
 
+@[expose] public section
+
 /-!
 
 # TimeM: Time Complexity Monad

Cslib/Computability/Automata/Acceptors/Acceptor.lean

@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Init
-import Mathlib.Computability.Language
+module
+
+public import Cslib.Init
+public import Mathlib.Computability.Language
+
+@[expose] public section
 
 namespace Cslib.Automata
 

Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean

@@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.Languages.OmegaLanguage
+module
+
+public import Cslib.Computability.Languages.OmegaLanguage
+
+@[expose] public section
 
 namespace Cslib.Automata
 

Cslib/Computability/Automata/DA/Basic.lean

@@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.Acceptors.Acceptor
-import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
-import Cslib.Foundations.Data.OmegaSequence.InfOcc
-import Cslib.Foundations.Semantics.FLTS.Basic
+module
+
+public import Cslib.Computability.Automata.Acceptors.Acceptor
+public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
+public import Cslib.Foundations.Data.OmegaSequence.InfOcc
+public import Cslib.Foundations.Semantics.FLTS.Basic
+
+@[expose] public section
 
 /-! # Deterministic Automata
 

Cslib/Computability/Automata/DA/Buchi.lean

@@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.DA.Basic
+module
+
+public import Cslib.Computability.Automata.DA.Basic
+
+public section
 
 /-! # Deterministic Buchi automata.
 -/

Cslib/Computability/Automata/DA/Prod.lean

@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.DA.Basic
-import Cslib.Foundations.Semantics.FLTS.Prod
+module
+
+public import Cslib.Computability.Automata.DA.Basic
+public import Cslib.Foundations.Semantics.FLTS.Prod
+
+@[expose] public section
 
 /-! # Product of deterministic automata. -/
 

Cslib/Computability/Automata/DA/ToNA.lean

@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.Automata.DA.Basic
-import Cslib.Computability.Automata.NA.Basic
-import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
+module
+
+public import Cslib.Computability.Automata.DA.Basic
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
+
+@[expose] public section
 
 /-! # Translation of Deterministic Automata into Nonodeterministic Automata.
 

Cslib/Computability/Automata/EpsilonNA/Basic.lean

@@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA.Basic
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+
+@[expose] public section
 
 /-! # Nondeterministic automata with ε-transitions. -/
 
@@ -21,7 +25,7 @@ structure εNA (State Symbol : Type*) extends NA State (Option Symbol)
 variable {State Symbol : Type*}
 
 @[local grind =]
-private instance : HasTau (Option α) := ⟨.none⟩
+instance : HasTau (Option α) := ⟨.none⟩
 
 /-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S`
 by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance

Cslib/Computability/Automata/EpsilonNA/ToNA.lean

@@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.Automata.EpsilonNA.Basic
+module
+
+public import Cslib.Computability.Automata.EpsilonNA.Basic
+
+@[expose] public section
 
 /-! # Translation of εNA into NA -/
 
@@ -13,7 +17,7 @@ namespace Cslib
 /-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
 ε-transitions. -/
 @[local grind =]
-private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
+def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
   Tr s μ s' := lts.Tr s (some μ) s'
 
 @[local grind .]

Cslib/Computability/Automata/NA/Basic.lean

@@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou, Chris Henson.
 -/
 
-import Cslib.Computability.Automata.Acceptors.Acceptor
-import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
-import Cslib.Foundations.Data.OmegaSequence.InfOcc
-import Cslib.Foundations.Semantics.LTS.Basic
+module
+
+public import Cslib.Computability.Automata.Acceptors.Acceptor
+public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
+public import Cslib.Foundations.Data.OmegaSequence.InfOcc
+public import Cslib.Foundations.Semantics.LTS.Basic
+
+@[expose] public section
 
 /-! # Nondeterministic Automaton
 

Cslib/Computability/Automata/NA/BuchiEquiv.lean

@@ -4,7 +4,11 @@ Relexsed under Apache 2.0 license xs described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA.Basic
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+
+@[expose] public section
 
 /-! # Equivalence of nondeterministic Buchi automata (NBAs). -/
 

Cslib/Computability/Automata/NA/BuchiInter.lean

@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA.Hist
-import Cslib.Computability.Automata.NA.Prod
-import Cslib.Foundations.Data.OmegaSequence.Temporal
+module
+
+public import Cslib.Computability.Automata.NA.Hist
+public import Cslib.Computability.Automata.NA.Prod
+public import Cslib.Foundations.Data.OmegaSequence.Temporal
+
+@[expose] public section
 
 /-! # Intersection of nondeterministic Buchi automata.