Skip to content

chore: Init.lean and some related refactoring #625

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
markusdemedeiros merged 19 commits into from
Aug 13, 2026
Merged

chore: Init.lean and some related refactoring #625

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
73fd66d
Add `Iris/Init.lean` and script checking that all modules import it
alvinylt Aug 12, 2026
e5626e5
Import `Init.lean` in all the source nodes
alvinylt Aug 12, 2026
3e99009
Remove `Iris.Std.RocqPorting` imports
alvinylt Aug 12, 2026
0bae996
`Iris.Std.DumpPortingData` and `Iris.ProofMode.Porting` as modules
alvinylt Aug 12, 2026
bbf29ce
Simplify scripts
alvinylt Aug 12, 2026
2bae2c0
Remove unnecessary imports and `meta` modifiers
alvinylt Aug 12, 2026
cb9a0e2
Move `Iris/Tests` to `IrisTest`, `IrisMath/Tests` to `IrisMathTest`
alvinylt Aug 12, 2026
04d42bd
Combine two scripts into one
alvinylt Aug 12, 2026
6c7771e
Update the CI scripts and `lakefile.toml` for the refactoring
alvinylt Aug 12, 2026
055a536
Extend `CheckImports.lean` for finding the minimal set of modules for…
alvinylt Aug 12, 2026
4090f72
Replace `import Lean` with smaller imports
alvinylt Aug 12, 2026
472d38c
Merge remote-tracking branch 'upstream/master' into InitLean
alvinylt Aug 12, 2026
04d7a5c
Update CI task description
alvinylt Aug 12, 2026
5efc510
Revert `module` for `Iris.ProofMode.Porting` and `Iris.Std.DumpPortin…
alvinylt Aug 12, 2026
796f38f
Remove outdated imports
alvinylt Aug 12, 2026
766f579
Retry CI
alvinylt Aug 12, 2026
05e20f1
Minor fixes
alvinylt Aug 12, 2026
8deb226
Move `Std/DumpPortingData.lean` to `scripts/`
alvinylt Aug 12, 2026
846b347
Merge branch 'master' into InitLean
markusdemedeiros Aug 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ jobs:
with:
lake-package-directory: Iris
build-args: "--wfail"
- name: Check that all modules are imported by Iris.lean and other entry-point modules
test: true
- name: Check Iris.lean, Init.lean and other entry-point module imports
working-directory: Iris
run: lake exe check-imports Iris
- name: Dump porting data
Expand All @@ -44,9 +45,10 @@ jobs:
lake-package-directory: IrisMath
use-mathlib-cache: true
build-args: "--wfail"
test: true
- name: Check that all modules are imported by IrisMath.lean
working-directory: IrisMath
run: lake exe check-imports IrisMath
run: lake exe check-imports --entry-points-only IrisMath
Comment thread
alvinylt marked this conversation as resolved.

report:
needs: build
Expand Down
2 changes: 1 addition & 1 deletion Iris/Iris.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,9 @@ public import Iris.BI.Lib
public import Iris.Examples
public import Iris.HeapLang
public import Iris.HeapLang.Lib
public import Iris.Init
public import Iris.Instances
public import Iris.Instances.Lib
public import Iris.ProgramLogic
public import Iris.ProofMode
public import Iris.Std
public import Iris.Tests
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Agree.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.Algebra.CMRA
public import Iris.Algebra.OFE
public import Iris.Algebra.IsOp
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Auth.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.Algebra.View
public import Iris.Algebra.LocalUpdates
meta import Iris.Std.RocqPorting

/-!
# Authoritative Camera
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/BigOp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ public import Iris.Std.GenSets
public import Iris.Std.GenMultiSets
public import Iris.Std.Positives
public import Iris.Std.Equivalence
meta import Iris.Std.RocqPorting

namespace Iris.Algebra

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/CMRA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.Algebra.OFE
public import Iris.Algebra.Monoid
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/COFESolver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Mario Carneiro, Sebastian Graf
module

public import Iris.Algebra.OFE
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Csum.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.Algebra.CMRA
public import Iris.Algebra.Updates
public import Iris.Algebra.LocalUpdates
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/DFrac.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ public import Iris.Algebra.Frac
public import Iris.Algebra.Updates
public import Iris.Algebra.LocalUpdates
public import Iris.Algebra.IsOp
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Excl.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Oliver Soeser, Mario Carneiro
module

public import Iris.Algebra.CMRA
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Frac.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.Algebra.CMRA
public import Iris.Algebra.OFE
public import Iris.Algebra.IsOp
meta import Iris.Std.RocqPorting

/-!
# The Frac CMRA
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Functions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Zongyuan Liu
module

public import Iris.Algebra.Updates
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/IsOp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.Algebra.CMRA
public import Iris.ProofMode.SynthInstanceAttr
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/LeibnizMultiSet.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ public import Iris.Algebra.CMRA
public import Iris.Algebra.LocalUpdates
public import Iris.Algebra.Updates
public import Iris.Std.GenMultiSets
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/LeibnizSet.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ public import Iris.Algebra.Updates
public import Iris.Std.GenSets
public import Iris.Std.Infinite
public import Iris.Std.CoPset
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Lib/DFracAgree.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.Algebra.DFrac
public import Iris.Algebra.Agree
meta import Iris.Std.RocqPorting

/-!
# The DFrac Agree Camera
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Lib/ExclAuth.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.Algebra.Auth
public import Iris.Algebra.Excl
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Lib/FracAuth.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.Algebra.Auth
public import Iris.Algebra.IsOp
import Iris.Algebra.LocalUpdates
meta import Iris.Std.RocqPorting

/-!
# Fractional Authoritative Camera
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Lib/MonoZ.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.Algebra.Auth
public import Iris.Algebra.LocalUpdates
public import Iris.Algebra.Numbers
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Lib/UFracAuth.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ public import Iris.Algebra.Auth
public import Iris.Algebra.IsOp
public import Iris.Algebra.UFrac
import Iris.Algebra.LocalUpdates
meta import Iris.Std.RocqPorting

/-!
# Unbounded Fractional Authoritative Camera
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/List.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.Algebra.OFE
public import Iris.Algebra.BigOp
public import Iris.Std.List
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/LocalUpdates.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Сухарик (@suhr), Mario Carneiro
module

public import Iris.Algebra.CMRA
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Monoid.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Zongyuan Liu
module

public import Iris.Algebra.OFE
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Mra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.Algebra.LocalUpdates
public import Iris.Std.Classes
meta import Iris.Std.RocqPorting

/-!
# Monotone resource algebras
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Numbers.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ public import Iris.Algebra.CMRA
public import Iris.Algebra.OFE
public import Iris.Algebra.IsOp
public import Iris.Algebra.LocalUpdates
meta import Iris.Std.RocqPorting

/-! ## Numbers CMRAs
For simple numerical types which form commutative monoids, there are three classes of CMRA:
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/OFE.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Mario Carneiro, Sebastian Graf, Sergei Stepanenko
module

public import Iris.Std.Option
public meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/StepIndex.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ Authors: Michael Sammler, Alvin Tang
-/
module

public meta import Iris.Std.RocqPorting
public import Iris.Std.Classes

@[expose] public section
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/UFrac.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ public import Iris.Algebra.CMRA
public import Iris.Algebra.OFE
public import Iris.Algebra.Frac
public import Iris.Algebra.IsOp
meta import Iris.Std.RocqPorting

/-!
# The UFrac CMRA
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/Updates.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Сухарик (@suhr)
module

public import Iris.Algebra.CMRA
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/Algebra/View.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ public import Iris.Algebra.Agree
public import Iris.Algebra.BigOp
public import Iris.Algebra.Updates
public import Iris.Algebra.LocalUpdates
meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
7 changes: 3 additions & 4 deletions Iris/Iris/BI/BIBase.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,11 @@ Authors: Lars König, Mario Carneiro
-/
module

public meta import Iris.BI.Notation
public import Iris.BI.Notation
public import Iris.Std.Classes
public meta import Iris.Std.DelabRule
public meta import Iris.Std.Rewrite
public import Iris.Std.DelabRule
public import Iris.Std.Rewrite
public import Iris.Std.BigOp
public meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigAndList.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.BI.BigOp.BigOp
import Iris.BI.DerivedLawsLater
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigAndMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.BI.BigOp.BigOp
import Iris.BI.DerivedLawsLater
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigOp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ public import Iris.Algebra.Monoid
public import Iris.Algebra.BigOp
public import Iris.BI.DerivedLaws
public import Iris.BI.Notation
import Lean

namespace Iris.BI

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigOrList.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

public import Iris.BI.BigOp.BigOp
import Iris.BI.DerivedLawsLater
meta import Iris.Std.RocqPorting

public section
namespace Iris.BI
Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigSepList.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ public import Iris.BI.BigOp.BigOp
import Iris.BI.DerivedLawsLater
import Iris.BI.Instances
import Iris.Std.TC
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigSepMSet.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ import Iris.BI.BigOp.BigSepSet
import Iris.BI.DerivedLawsLater
import Iris.BI.Instances
import Iris.Std.TC
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigSepMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ import Iris.BI.Instances
import Iris.BI.BigOp.BigSepSet
import Iris.Std.TC
import Batteries.Data.List.Perm
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/BigOp/BigSepSet.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ import Iris.BI.BigOp.BigSepList
import Iris.BI.DerivedLawsLater
import Iris.BI.Instances
import Iris.Std.TC
meta import Iris.Std.RocqPorting

public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/Cmra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module
public import Iris.BI.Sbi
public import Iris.BI.Plainly
public import Iris.BI.InternalEq
public import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/DerivedLaws.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ public import Iris.Std.Nat
public import Iris.Std.Classes
public import Iris.Std.Rewrite
public import Iris.Std.TC
import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/DerivedLawsLater.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ public import Iris.BI.BigOp.BigOp
public import Iris.Std.Classes
public import Iris.Std.Rewrite
public import Iris.Std.TC
public import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/Extensions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ Authors: Lars König
-/
module

public import Iris.Std.RocqPorting
public import Iris.BI.Classes
public import Iris.BI.BI

Expand Down
3 changes: 2 additions & 1 deletion Iris/Iris/BI/Notation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@ Authors: Lars König, Alex Keizer
-/
module

meta import Lean.Parser.Term
import Lean.Parser.Term
public import Iris.Init

public meta section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/SIProp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ public import Iris.BI.Extensions
public import Iris.BI.Classes
public import Iris.BI.DerivedLaws
public import Iris.Algebra.CMRA
public meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
1 change: 0 additions & 1 deletion Iris/Iris/BI/Sbi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ public import Iris.BI.DerivedLaws
public import Iris.BI.DerivedLawsLater
public import Iris.BI.Extensions
public import Iris.BI.SIProp
public meta import Iris.Std.RocqPorting

@[expose] public section

Expand Down
Loading