From 0129a1eae41777fd695710f194b91421fe19d709 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 25 Jul 2025 14:44:51 +0200 Subject: [PATCH 1/2] Activate mathlib linters and fix some warnings. --- Cslib/Semantics/LTS/Basic.lean | 56 +++++++++++++++++++++++++--------- lakefile.toml | 3 ++ 2 files changed, 45 insertions(+), 14 deletions(-) diff --git a/Cslib/Semantics/LTS/Basic.lean b/Cslib/Semantics/LTS/Basic.lean index c91227ed..f4226175 100644 --- a/Cslib/Semantics/LTS/Basic.lean +++ b/Cslib/Semantics/LTS/Basic.lean @@ -396,13 +396,20 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) : lts.Tr s μ s' intro h apply LTS.STr.tr LTS.STr.refl h LTS.STr.refl -/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction metric. -/ -inductive LTS.strN [HasTau Label] (lts : LTS State Label) : ℕ → State → Label → State → Prop where -| refl : lts.strN 0 s HasTau.τ s -| tr : lts.strN n s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.strN m s3 HasTau.τ s4 → lts.strN (n + m + 1) s1 μ s4 +/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction +metric. -/ +inductive LTS.strN [HasTau Label] (lts : LTS State Label) : + ℕ → State → Label → State → Prop where + | refl : lts.strN 0 s HasTau.τ s + | tr : + lts.strN n s1 HasTau.τ s2 → + lts.Tr s2 μ s3 → + lts.strN m s3 HasTau.τ s4 → + lts.strN (n + m + 1) s1 μ s4 /-- `LTS.str` and `LTS.strN` are equivalent. -/ -theorem LTS.str_strN [HasTau Label] (lts : LTS State Label) : lts.STr s1 μ s2 ↔ ∃ n, lts.strN n s1 μ s2 := by +theorem LTS.str_strN [HasTau Label] (lts : LTS State Label) : + lts.STr s1 μ s2 ↔ ∃ n, lts.strN n s1 μ s2 := by apply Iff.intro <;> intro h case mp => induction h @@ -512,7 +519,10 @@ def LTS.Divergent [HasTau Label] (lts : LTS State Label) (s : State) : Prop := ∃ stream : Stream' State, stream 0 = s ∧ lts.DivergentExecution stream /-- If a stream is a divergent execution, then any 'suffix' is also a divergent execution. -/ -theorem LTS.divergent_drop [HasTau Label] (lts : LTS State Label) (stream : Stream' State) (h : lts.DivergentExecution stream) (n : ℕ) : lts.DivergentExecution (stream.drop n) := by +theorem LTS.divergent_drop + [HasTau Label] (lts : LTS State Label) (stream : Stream' State) + (h : lts.DivergentExecution stream) (n : ℕ) : + lts.DivergentExecution (stream.drop n) := by simp only [LTS.DivergentExecution] intro m simp only [Stream'.drop, Stream'.get] @@ -535,7 +545,8 @@ section Relation def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop := fun s1 s2 => lts.Tr s1 μ s2 -/-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition labels `μs`. -/ +/-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition +labels `μs`. -/ def LTS.MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop := fun s1 s2 => lts.MTr s1 μs s2 @@ -551,7 +562,11 @@ section Trans /-! ## Support for the calc tactic -/ /-- Transitions can be chained. -/ -instance (lts : LTS State Label) : Trans (LTS.Tr.toRelation lts μ1) (LTS.Tr.toRelation lts μ2) (LTS.MTr.toRelation lts [μ1, μ2]) where +instance (lts : LTS State Label) : + Trans + (LTS.Tr.toRelation lts μ1) + (LTS.Tr.toRelation lts μ2) + (LTS.MTr.toRelation lts [μ1, μ2]) where trans := by intro s1 s2 s3 htr1 htr2 apply LTS.MTr.single at htr1 @@ -559,21 +574,33 @@ instance (lts : LTS State Label) : Trans (LTS.Tr.toRelation lts μ1) (LTS.Tr.toR apply LTS.MTr.comp lts htr1 htr2 /-- Transitions can be chained with multi-step transitions. -/ -instance (lts : LTS State Label) : Trans (LTS.Tr.toRelation lts μ) (LTS.MTr.toRelation lts μs) (LTS.MTr.toRelation lts (μ :: μs)) where +instance (lts : LTS State Label) : + Trans + (LTS.Tr.toRelation lts μ) + (LTS.MTr.toRelation lts μs) + (LTS.MTr.toRelation lts (μ :: μs)) where trans := by intro s1 s2 s3 htr1 hmtr2 apply LTS.MTr.single at htr1 apply LTS.MTr.comp lts htr1 hmtr2 /-- Multi-step transitions can be chained with transitions. -/ -instance (lts : LTS State Label) : Trans (LTS.MTr.toRelation lts μs) (LTS.Tr.toRelation lts μ) (LTS.MTr.toRelation lts (μs ++ [μ])) where +instance (lts : LTS State Label) : + Trans + (LTS.MTr.toRelation lts μs) + (LTS.Tr.toRelation lts μ) + (LTS.MTr.toRelation lts (μs ++ [μ])) where trans := by intro s1 s2 s3 hmtr1 htr2 apply LTS.MTr.single at htr2 apply LTS.MTr.comp lts hmtr1 htr2 /-- Multi-step transitions can be chained. -/ -instance (lts : LTS State Label) : Trans (LTS.MTr.toRelation lts μs1) (LTS.MTr.toRelation lts μs2) (LTS.MTr.toRelation lts (μs1 ++ μs2)) where +instance (lts : LTS State Label) : + Trans + (LTS.MTr.toRelation lts μs1) + (LTS.MTr.toRelation lts μs2) + (LTS.MTr.toRelation lts (μs1 ++ μs2)) where trans := by intro s1 s2 s3 hmtr1 hmtr2 apply LTS.MTr.comp lts hmtr1 hmtr2 @@ -582,7 +609,8 @@ end Trans open Lean Elab Meta Command Term -/-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of `variable `-/ +/-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of +`variable `-/ elab "create_lts" lt:ident name:ident : command => do liftTermElabM do let lt ← realizeGlobalConstNoOverloadWithInfo lt @@ -612,8 +640,8 @@ elab "create_lts" lt:ident name:ident : command => do addDeclarationRangesFromSyntax name.getId name /-- - This command adds transition notations for an `LTS`. This should not usually be called directly, but from - the `lts` attribute. + This command adds transition notations for an `LTS`. This should not usually be called directly, + but from the `lts` attribute. As an example `lts_transition_notation foo "β"` will add the notations "[⬝]⭢β" and "[⬝]↠β" diff --git a/lakefile.toml b/lakefile.toml index 79fb9b28..8b170180 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -3,6 +3,9 @@ version = "0.1.0" defaultTargets = ["Cslib"] testDriver = "CslibTests" +[leanOptions] +weak.linter.mathlibStandardSet = true + [[require]] name = "mathlib" scope = "leanprover-community" From a4ab51b9796f983cf87ff2dc971f9daa2a44db52 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 25 Jul 2025 15:38:46 +0200 Subject: [PATCH 2/2] Add lint & suggest action --- .github/workflows/lean_lint_suggest.yml | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 .github/workflows/lean_lint_suggest.yml diff --git a/.github/workflows/lean_lint_suggest.yml b/.github/workflows/lean_lint_suggest.yml new file mode 100644 index 00000000..6f83ca22 --- /dev/null +++ b/.github/workflows/lean_lint_suggest.yml @@ -0,0 +1,13 @@ +on: + pull_request + +name: Lint and suggest + +jobs: + lint: + if: github.repository == 'cs-lean/cslib' && github.event.pull_request.draft == false + runs-on: ubuntu-latest + steps: + - uses: leanprover-community/lint-style-action + with: + mode: suggest \ No newline at end of file