diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index fc081e0b8..7cae754df 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -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 @@ -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 report: needs: build diff --git a/Iris/Iris.lean b/Iris/Iris.lean index a98250ce6..6b9e75948 100644 --- a/Iris/Iris.lean +++ b/Iris/Iris.lean @@ -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 diff --git a/Iris/Iris/Algebra/Agree.lean b/Iris/Iris/Algebra/Agree.lean index 525295d18..d21de6455 100644 --- a/Iris/Iris/Algebra/Agree.lean +++ b/Iris/Iris/Algebra/Agree.lean @@ -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 diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index 3d3e384b6..fe0a7a8af 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.View public import Iris.Algebra.LocalUpdates -meta import Iris.Std.RocqPorting /-! # Authoritative Camera diff --git a/Iris/Iris/Algebra/BigOp.lean b/Iris/Iris/Algebra/BigOp.lean index 20642200c..5eed728af 100644 --- a/Iris/Iris/Algebra/BigOp.lean +++ b/Iris/Iris/Algebra/BigOp.lean @@ -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 diff --git a/Iris/Iris/Algebra/CMRA.lean b/Iris/Iris/Algebra/CMRA.lean index cf238df17..0971a7727 100644 --- a/Iris/Iris/Algebra/CMRA.lean +++ b/Iris/Iris/Algebra/CMRA.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.OFE public import Iris.Algebra.Monoid -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean index 937c630a9..c2346d630 100644 --- a/Iris/Iris/Algebra/COFESolver.lean +++ b/Iris/Iris/Algebra/COFESolver.lean @@ -6,7 +6,6 @@ Authors: Mario Carneiro, Sebastian Graf module public import Iris.Algebra.OFE -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/Csum.lean b/Iris/Iris/Algebra/Csum.lean index eecd1b8e9..a93974231 100644 --- a/Iris/Iris/Algebra/Csum.lean +++ b/Iris/Iris/Algebra/Csum.lean @@ -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 diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean index 4be6d6623..dcd44aa0c 100644 --- a/Iris/Iris/Algebra/DFrac.lean +++ b/Iris/Iris/Algebra/DFrac.lean @@ -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 diff --git a/Iris/Iris/Algebra/Excl.lean b/Iris/Iris/Algebra/Excl.lean index 1f5999894..7b28f4aca 100644 --- a/Iris/Iris/Algebra/Excl.lean +++ b/Iris/Iris/Algebra/Excl.lean @@ -6,7 +6,6 @@ Authors: Oliver Soeser, Mario Carneiro module public import Iris.Algebra.CMRA -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 1910dc332..66aae551e 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -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 diff --git a/Iris/Iris/Algebra/Functions.lean b/Iris/Iris/Algebra/Functions.lean index cb237c378..da63a2d04 100644 --- a/Iris/Iris/Algebra/Functions.lean +++ b/Iris/Iris/Algebra/Functions.lean @@ -6,7 +6,6 @@ Authors: Zongyuan Liu module public import Iris.Algebra.Updates -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean index 685fa77ca..38d71399c 100644 --- a/Iris/Iris/Algebra/IsOp.lean +++ b/Iris/Iris/Algebra/IsOp.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.CMRA public import Iris.ProofMode.SynthInstanceAttr -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/LeibnizMultiSet.lean b/Iris/Iris/Algebra/LeibnizMultiSet.lean index d9a3834aa..92d244944 100644 --- a/Iris/Iris/Algebra/LeibnizMultiSet.lean +++ b/Iris/Iris/Algebra/LeibnizMultiSet.lean @@ -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 diff --git a/Iris/Iris/Algebra/LeibnizSet.lean b/Iris/Iris/Algebra/LeibnizSet.lean index 545db5e45..7e3fb18e6 100644 --- a/Iris/Iris/Algebra/LeibnizSet.lean +++ b/Iris/Iris/Algebra/LeibnizSet.lean @@ -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 diff --git a/Iris/Iris/Algebra/Lib/DFracAgree.lean b/Iris/Iris/Algebra/Lib/DFracAgree.lean index d6a031fe6..ba8659c73 100644 --- a/Iris/Iris/Algebra/Lib/DFracAgree.lean +++ b/Iris/Iris/Algebra/Lib/DFracAgree.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.DFrac public import Iris.Algebra.Agree -meta import Iris.Std.RocqPorting /-! # The DFrac Agree Camera diff --git a/Iris/Iris/Algebra/Lib/ExclAuth.lean b/Iris/Iris/Algebra/Lib/ExclAuth.lean index 67b4e8fc4..97846d95d 100644 --- a/Iris/Iris/Algebra/Lib/ExclAuth.lean +++ b/Iris/Iris/Algebra/Lib/ExclAuth.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.Auth public import Iris.Algebra.Excl -meta import Iris.Std.RocqPorting public section diff --git a/Iris/Iris/Algebra/Lib/FracAuth.lean b/Iris/Iris/Algebra/Lib/FracAuth.lean index e0a8d4eb0..9f1b691a4 100644 --- a/Iris/Iris/Algebra/Lib/FracAuth.lean +++ b/Iris/Iris/Algebra/Lib/FracAuth.lean @@ -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 diff --git a/Iris/Iris/Algebra/Lib/MonoZ.lean b/Iris/Iris/Algebra/Lib/MonoZ.lean index f78042809..d7952a88c 100644 --- a/Iris/Iris/Algebra/Lib/MonoZ.lean +++ b/Iris/Iris/Algebra/Lib/MonoZ.lean @@ -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 diff --git a/Iris/Iris/Algebra/Lib/UFracAuth.lean b/Iris/Iris/Algebra/Lib/UFracAuth.lean index c58b1a3a8..f23346157 100644 --- a/Iris/Iris/Algebra/Lib/UFracAuth.lean +++ b/Iris/Iris/Algebra/Lib/UFracAuth.lean @@ -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 diff --git a/Iris/Iris/Algebra/List.lean b/Iris/Iris/Algebra/List.lean index c162a93e9..273b3aa1d 100644 --- a/Iris/Iris/Algebra/List.lean +++ b/Iris/Iris/Algebra/List.lean @@ -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 diff --git a/Iris/Iris/Algebra/LocalUpdates.lean b/Iris/Iris/Algebra/LocalUpdates.lean index 1f29689ad..3f3af9bf5 100644 --- a/Iris/Iris/Algebra/LocalUpdates.lean +++ b/Iris/Iris/Algebra/LocalUpdates.lean @@ -6,7 +6,6 @@ Authors: Сухарик (@suhr), Mario Carneiro module public import Iris.Algebra.CMRA -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/Monoid.lean b/Iris/Iris/Algebra/Monoid.lean index e70bf9f38..414fc144b 100644 --- a/Iris/Iris/Algebra/Monoid.lean +++ b/Iris/Iris/Algebra/Monoid.lean @@ -6,7 +6,6 @@ Authors: Zongyuan Liu module public import Iris.Algebra.OFE -meta import Iris.Std.RocqPorting public section diff --git a/Iris/Iris/Algebra/Mra.lean b/Iris/Iris/Algebra/Mra.lean index b69ce9fd2..052a89233 100644 --- a/Iris/Iris/Algebra/Mra.lean +++ b/Iris/Iris/Algebra/Mra.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.LocalUpdates public import Iris.Std.Classes -meta import Iris.Std.RocqPorting /-! # Monotone resource algebras diff --git a/Iris/Iris/Algebra/Numbers.lean b/Iris/Iris/Algebra/Numbers.lean index 62bda5cc7..a267f0324 100644 --- a/Iris/Iris/Algebra/Numbers.lean +++ b/Iris/Iris/Algebra/Numbers.lean @@ -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: diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean index ec4fb494a..fedf0fd97 100644 --- a/Iris/Iris/Algebra/OFE.lean +++ b/Iris/Iris/Algebra/OFE.lean @@ -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 diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean index 535c883f7..0629f01e4 100644 --- a/Iris/Iris/Algebra/StepIndex.lean +++ b/Iris/Iris/Algebra/StepIndex.lean @@ -5,7 +5,6 @@ Authors: Michael Sammler, Alvin Tang -/ module -public meta import Iris.Std.RocqPorting public import Iris.Std.Classes @[expose] public section diff --git a/Iris/Iris/Algebra/UFrac.lean b/Iris/Iris/Algebra/UFrac.lean index 2bcb7369a..275079435 100644 --- a/Iris/Iris/Algebra/UFrac.lean +++ b/Iris/Iris/Algebra/UFrac.lean @@ -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 diff --git a/Iris/Iris/Algebra/Updates.lean b/Iris/Iris/Algebra/Updates.lean index 6227f57d8..abe76d669 100644 --- a/Iris/Iris/Algebra/Updates.lean +++ b/Iris/Iris/Algebra/Updates.lean @@ -6,7 +6,6 @@ Authors: Сухарик (@suhr) module public import Iris.Algebra.CMRA -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index 9cc4aac07..013fa9296 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -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 diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean index 1dbd022f9..d685fc76c 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -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 diff --git a/Iris/Iris/BI/BigOp/BigAndList.lean b/Iris/Iris/BI/BigOp/BigAndList.lean index a9de797da..4c7efdcef 100644 --- a/Iris/Iris/BI/BigOp/BigAndList.lean +++ b/Iris/Iris/BI/BigOp/BigAndList.lean @@ -7,7 +7,6 @@ module public import Iris.BI.BigOp.BigOp import Iris.BI.DerivedLawsLater -meta import Iris.Std.RocqPorting public section diff --git a/Iris/Iris/BI/BigOp/BigAndMap.lean b/Iris/Iris/BI/BigOp/BigAndMap.lean index 897393887..162608bb6 100644 --- a/Iris/Iris/BI/BigOp/BigAndMap.lean +++ b/Iris/Iris/BI/BigOp/BigAndMap.lean @@ -7,7 +7,6 @@ module public import Iris.BI.BigOp.BigOp import Iris.BI.DerivedLawsLater -meta import Iris.Std.RocqPorting public section diff --git a/Iris/Iris/BI/BigOp/BigOp.lean b/Iris/Iris/BI/BigOp/BigOp.lean index 44801d519..cd012cf45 100644 --- a/Iris/Iris/BI/BigOp/BigOp.lean +++ b/Iris/Iris/BI/BigOp/BigOp.lean @@ -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 diff --git a/Iris/Iris/BI/BigOp/BigOrList.lean b/Iris/Iris/BI/BigOp/BigOrList.lean index 44cee8f63..e45228c40 100644 --- a/Iris/Iris/BI/BigOp/BigOrList.lean +++ b/Iris/Iris/BI/BigOp/BigOrList.lean @@ -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 diff --git a/Iris/Iris/BI/BigOp/BigSepList.lean b/Iris/Iris/BI/BigOp/BigSepList.lean index 21aed5e46..66611a69c 100644 --- a/Iris/Iris/BI/BigOp/BigSepList.lean +++ b/Iris/Iris/BI/BigOp/BigSepList.lean @@ -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 diff --git a/Iris/Iris/BI/BigOp/BigSepMSet.lean b/Iris/Iris/BI/BigOp/BigSepMSet.lean index 03f7ef92d..f5f93961c 100644 --- a/Iris/Iris/BI/BigOp/BigSepMSet.lean +++ b/Iris/Iris/BI/BigOp/BigSepMSet.lean @@ -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 diff --git a/Iris/Iris/BI/BigOp/BigSepMap.lean b/Iris/Iris/BI/BigOp/BigSepMap.lean index 7b01b0a6c..fa836a873 100644 --- a/Iris/Iris/BI/BigOp/BigSepMap.lean +++ b/Iris/Iris/BI/BigOp/BigSepMap.lean @@ -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 diff --git a/Iris/Iris/BI/BigOp/BigSepSet.lean b/Iris/Iris/BI/BigOp/BigSepSet.lean index 8ca47cdcc..149c05e0b 100644 --- a/Iris/Iris/BI/BigOp/BigSepSet.lean +++ b/Iris/Iris/BI/BigOp/BigSepSet.lean @@ -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 diff --git a/Iris/Iris/BI/Cmra.lean b/Iris/Iris/BI/Cmra.lean index 35b30eee6..d3fe3e962 100644 --- a/Iris/Iris/BI/Cmra.lean +++ b/Iris/Iris/BI/Cmra.lean @@ -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 diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean index c8c02468d..ad654903f 100644 --- a/Iris/Iris/BI/DerivedLaws.lean +++ b/Iris/Iris/BI/DerivedLaws.lean @@ -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 diff --git a/Iris/Iris/BI/DerivedLawsLater.lean b/Iris/Iris/BI/DerivedLawsLater.lean index 00bc9f08e..b86fbc784 100644 --- a/Iris/Iris/BI/DerivedLawsLater.lean +++ b/Iris/Iris/BI/DerivedLawsLater.lean @@ -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 diff --git a/Iris/Iris/BI/Extensions.lean b/Iris/Iris/BI/Extensions.lean index f45bfd0b1..54247978f 100644 --- a/Iris/Iris/BI/Extensions.lean +++ b/Iris/Iris/BI/Extensions.lean @@ -5,7 +5,6 @@ Authors: Lars König -/ module -public import Iris.Std.RocqPorting public import Iris.BI.Classes public import Iris.BI.BI diff --git a/Iris/Iris/BI/Notation.lean b/Iris/Iris/BI/Notation.lean index 9fa07e3da..8f3483e89 100644 --- a/Iris/Iris/BI/Notation.lean +++ b/Iris/Iris/BI/Notation.lean @@ -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 diff --git a/Iris/Iris/BI/SIProp.lean b/Iris/Iris/BI/SIProp.lean index e303d4178..4ffa01528 100644 --- a/Iris/Iris/BI/SIProp.lean +++ b/Iris/Iris/BI/SIProp.lean @@ -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 diff --git a/Iris/Iris/BI/Sbi.lean b/Iris/Iris/BI/Sbi.lean index 879e34e31..fe313ec9d 100644 --- a/Iris/Iris/BI/Sbi.lean +++ b/Iris/Iris/BI/Sbi.lean @@ -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 diff --git a/Iris/Iris/HeapLang/Linter.lean b/Iris/Iris/HeapLang/Linter.lean index 5b8e2e740..ee302d012 100644 --- a/Iris/Iris/HeapLang/Linter.lean +++ b/Iris/Iris/HeapLang/Linter.lean @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. module public import Iris.HeapLang.Notation -public meta import Lean.Elab.Command -public meta import Lean.Linter.Util +public import Lean.Elab.Command +public import Lean.Linter.Util public meta section namespace Iris.HeapLang.Linter diff --git a/Iris/Iris/HeapLang/Notation.lean b/Iris/Iris/HeapLang/Notation.lean index 9aa141c24..10ed0e5f2 100644 --- a/Iris/Iris/HeapLang/Notation.lean +++ b/Iris/Iris/HeapLang/Notation.lean @@ -6,7 +6,7 @@ Authors: Michael Sammler module public import Iris.HeapLang.Syntax -public meta import Lean.PrettyPrinter.Parenthesizer +public import Lean.PrettyPrinter.Parenthesizer public meta section namespace Iris.HeapLang diff --git a/Iris/Iris/HeapLang/Porting.lean b/Iris/Iris/HeapLang/Porting.lean index e7e160657..a3434ddf6 100644 --- a/Iris/Iris/HeapLang/Porting.lean +++ b/Iris/Iris/HeapLang/Porting.lean @@ -5,7 +5,7 @@ Authors: Markus de Medeiros -/ module -import Iris.Std.RocqPorting +public import Iris.Init /-! # HeapLang porting bookkeeping diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean index 03229249a..58e626fc6 100644 --- a/Iris/Iris/HeapLang/ProofMode.lean +++ b/Iris/Iris/HeapLang/ProofMode.lean @@ -14,9 +14,7 @@ public import Iris.ProgramLogic.Language public import Iris.ProgramLogic.EctxLanguage public import Iris.ProgramLogic.EctxiLanguage public import Iris.ProgramLogic.Lifting -public import Lean public import Lean.Elab.Tactic.Simp -public import Qq namespace Iris.ProofMode @@ -384,7 +382,7 @@ if the step spawns a goal besides the continuation, such as an undischarged side of the reduction. -/ elab "wp_pure_step" : tactic => focus do evalTactic (← `(tactic| wp_pure)) - -- we run under `focus` so we only see the unsolved goals of `wp_pure` + -- we run under `focus` so we only see the unsolved goals of `wp_pure` let goals ← getUnsolvedGoals unless goals.length == 1 do throwError "the pure reduction step must leave exactly one goal, it left { diff --git a/Iris/Iris/HeapLang/Semantics.lean b/Iris/Iris/HeapLang/Semantics.lean index ff1c16fea..4a9f53363 100644 --- a/Iris/Iris/HeapLang/Semantics.lean +++ b/Iris/Iris/HeapLang/Semantics.lean @@ -9,7 +9,6 @@ public import Iris.HeapLang.Linter public import Std.Data.ExtTreeMap public import Std.Data.ExtTreeSet public import Iris.Std.BitOp -public import Iris.Std.RocqPorting public import Iris.Std.PartialMap public import Iris.Std.HeapInstances import Iris.Std.List diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean index bb2a8a87b..c68b97d58 100644 --- a/Iris/Iris/HeapLang/Syntax.lean +++ b/Iris/Iris/HeapLang/Syntax.lean @@ -7,7 +7,6 @@ module public import Iris.Std.Infinite public import Iris.ProgramLogic.Language -meta import Iris.Std.RocqPorting @[expose] public section namespace Iris.HeapLang diff --git a/Iris/Iris/HeapLang/Tactic.lean b/Iris/Iris/HeapLang/Tactic.lean index d4af74158..b4af74393 100644 --- a/Iris/Iris/HeapLang/Tactic.lean +++ b/Iris/Iris/HeapLang/Tactic.lean @@ -4,14 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. -/ module -public import Iris.HeapLang.Syntax -public import Iris.HeapLang.Semantics -public import Iris.ProofMode.ProofModeM -public import Lean -public import Iris.ProgramLogic.EctxiLanguage -public import Iris.ProgramLogic.EctxLanguage public import Iris.HeapLang.Instances -public import Qq namespace Iris.HeapLang diff --git a/Iris/Iris/Init.lean b/Iris/Iris/Init.lean new file mode 100644 index 000000000..e09ef946e --- /dev/null +++ b/Iris/Iris/Init.lean @@ -0,0 +1,3 @@ +module + +public meta import Iris.Std.RocqPorting diff --git a/Iris/Iris/Instances/Data/SetNotation.lean b/Iris/Iris/Instances/Data/SetNotation.lean index 0155d488a..46ddc60f2 100644 --- a/Iris/Iris/Instances/Data/SetNotation.lean +++ b/Iris/Iris/Instances/Data/SetNotation.lean @@ -5,6 +5,8 @@ Authors: Lars König -/ module +public import Iris.Init + @[expose] public section namespace Iris.Instances.Data diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 1039ca5cb..21e6f7eff 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -10,7 +10,6 @@ public import Iris.BI public import Iris.BI.BigOp public import Iris.Algebra public import Iris.Instances.UPred -public meta import Iris.Std.RocqPorting @[expose] public section namespace Iris diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean index d1cb70095..42daa1038 100644 --- a/Iris/Iris/Instances/UPred/Instance.lean +++ b/Iris/Iris/Instances/UPred/Instance.lean @@ -11,7 +11,6 @@ public import Iris.Algebra.CMRA public import Iris.Algebra.UPred public import Iris.Algebra.Updates public import Iris.BI.Lib.BUpdPlain -public meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/ProgramLogic/EctxLanguage.lean b/Iris/Iris/ProgramLogic/EctxLanguage.lean index 6964c1f6d..13852d3fc 100644 --- a/Iris/Iris/ProgramLogic/EctxLanguage.lean +++ b/Iris/Iris/ProgramLogic/EctxLanguage.lean @@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. -/ module -meta import Iris.Std.RocqPorting - public import Iris.ProgramLogic.Language namespace Iris.ProgramLogic diff --git a/Iris/Iris/ProgramLogic/EctxiLanguage.lean b/Iris/Iris/ProgramLogic/EctxiLanguage.lean index 74e23d39a..b29887c9e 100644 --- a/Iris/Iris/ProgramLogic/EctxiLanguage.lean +++ b/Iris/Iris/ProgramLogic/EctxiLanguage.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. -/ module -meta import Iris.Std.RocqPorting public import Iris.ProgramLogic.Language public import Iris.ProgramLogic.EctxLanguage diff --git a/Iris/Iris/ProgramLogic/Language.lean b/Iris/Iris/ProgramLogic/Language.lean index 695de06e2..53515985d 100644 --- a/Iris/Iris/ProgramLogic/Language.lean +++ b/Iris/Iris/ProgramLogic/Language.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. -/ module -meta import Iris.Std.RocqPorting public import Iris.ProofMode public import Iris.Std.Relation public import Iris.BI.WeakestPre diff --git a/Iris/Iris/ProofMode.lean b/Iris/Iris/ProofMode.lean index 5db7e4db9..daa583508 100644 --- a/Iris/Iris/ProofMode.lean +++ b/Iris/Iris/ProofMode.lean @@ -2,8 +2,8 @@ module public import Iris.ProofMode.Classes public import Iris.ProofMode.ClassesMake -public meta import Iris.ProofMode.Display -public meta import Iris.ProofMode.Expr +public import Iris.ProofMode.Display +public import Iris.ProofMode.Expr public import Iris.ProofMode.Instances public import Iris.ProofMode.InstancesCmra public import Iris.ProofMode.InstancesEmbedding @@ -17,9 +17,9 @@ public import Iris.ProofMode.Modalities public import Iris.ProofMode.ModalityInstances public import Iris.ProofMode.NatCancel public import Iris.ProofMode.Patterns -/- public import Iris.ProofMode.Porting -/ +public import Iris.ProofMode.Porting public import Iris.ProofMode.ProofModeM public import Iris.ProofMode.SynthInstance public import Iris.ProofMode.SynthInstanceAttr -public meta import Iris.ProofMode.Tactics +public import Iris.ProofMode.Tactics public import Iris.ProofMode.UnifHints diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index 33de6f159..95250b3df 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -6,9 +6,7 @@ Authors: Lars König, Michael Sammler, Yunsong Yang, Alvin Tang module public import Iris.BI -public meta import Iris.ProofMode.SynthInstance public import Iris.ProofMode.Modalities -public import Iris.Std.Namespaces @[expose] public section diff --git a/Iris/Iris/ProofMode/ClassesMake.lean b/Iris/Iris/ProofMode/ClassesMake.lean index 7f11e50ee..fd4ead23d 100644 --- a/Iris/Iris/ProofMode/ClassesMake.lean +++ b/Iris/Iris/ProofMode/ClassesMake.lean @@ -6,7 +6,6 @@ Authors: Michael Sammler, Yunsong Yang module public import Iris.BI -public meta import Iris.ProofMode.SynthInstance @[expose] public section diff --git a/Iris/Iris/ProofMode/Display.lean b/Iris/Iris/ProofMode/Display.lean index bdbf7cec3..ba1842ec1 100644 --- a/Iris/Iris/ProofMode/Display.lean +++ b/Iris/Iris/ProofMode/Display.lean @@ -5,9 +5,7 @@ Authors: Lars König, Mario Carneiro -/ module -public meta import Iris.BI.Notation -public meta import Iris.ProofMode.Expr -public meta import Lean.PrettyPrinter.Delaborator +public import Iris.ProofMode.Expr public meta section diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean index 5d2793e68..d7112e117 100644 --- a/Iris/Iris/ProofMode/Expr.lean +++ b/Iris/Iris/ProofMode/Expr.lean @@ -5,7 +5,6 @@ Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang -/ module -public meta import Qq public import Iris.BI public import Iris.ProofMode.Classes public import Iris.Std diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean index 89e5907e4..65f15aeda 100644 --- a/Iris/Iris/ProofMode/Instances.lean +++ b/Iris/Iris/ProofMode/Instances.lean @@ -11,7 +11,6 @@ public import Iris.ProofMode.ClassesMake public import Iris.ProofMode.ModalityInstances public import Iris.ProofMode.Expr public import Iris.Std.TC -public import Iris.Std.RocqPorting public import Iris.ProofMode.Tactics public import Iris.ProofMode.Display diff --git a/Iris/Iris/ProofMode/InstancesCmra.lean b/Iris/Iris/ProofMode/InstancesCmra.lean index 870b41917..e9bc6f32c 100644 --- a/Iris/Iris/ProofMode/InstancesCmra.lean +++ b/Iris/Iris/ProofMode/InstancesCmra.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.CMRA public import Iris.ProofMode.Classes -import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/ProofMode/InstancesFrame.lean b/Iris/Iris/ProofMode/InstancesFrame.lean index f615d6fbc..565823200 100644 --- a/Iris/Iris/ProofMode/InstancesFrame.lean +++ b/Iris/Iris/ProofMode/InstancesFrame.lean @@ -8,7 +8,8 @@ module public import Iris.BI public import Iris.ProofMode.Classes public import Iris.ProofMode.ClassesMake -public meta import Iris.ProofMode.Expr +public import Iris.ProofMode.Expr +public import Iris.ProofMode.SynthInstance public import Iris.Std.TC public meta section diff --git a/Iris/Iris/ProofMode/InstancesInternalEq.lean b/Iris/Iris/ProofMode/InstancesInternalEq.lean index bc1030070..34993af70 100644 --- a/Iris/Iris/ProofMode/InstancesInternalEq.lean +++ b/Iris/Iris/ProofMode/InstancesInternalEq.lean @@ -8,7 +8,6 @@ module public import Iris.ProofMode.Classes public import Iris.ProofMode.ModalityInstances public import Iris.ProofMode.NatCancel -import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/ProofMode/NatCancel.lean b/Iris/Iris/ProofMode/NatCancel.lean index cbf78f16d..9e7a56e16 100644 --- a/Iris/Iris/ProofMode/NatCancel.lean +++ b/Iris/Iris/ProofMode/NatCancel.lean @@ -5,7 +5,7 @@ Authors: Alvin Tang -/ module -public meta import Iris.ProofMode.SynthInstance +public import Iris.ProofMode.SynthInstance @[expose] public section diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean index 2640ec44a..6da42f434 100644 --- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean @@ -6,6 +6,7 @@ Authors: Lars König, Alvin Tang module public import Lean.Data.Name +public import Iris.Init @[expose] public section diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean index d58d52d14..fadfeadfa 100644 --- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean @@ -7,7 +7,6 @@ module public import Iris.ProofMode.Patterns.CasesPattern public import Iris.ProofMode.Patterns.SelPattern -meta import Iris.Std.RocqPorting public import Lean.Syntax diff --git a/Iris/Iris/ProofMode/Patterns/SelPattern.lean b/Iris/Iris/ProofMode/Patterns/SelPattern.lean index 1171a4240..b7ddfe45d 100644 --- a/Iris/Iris/ProofMode/Patterns/SelPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/SelPattern.lean @@ -5,7 +5,7 @@ Authors: Yunsong Yang -/ module -public meta import Iris.ProofMode.ProofModeM +public import Iris.ProofMode.ProofModeM @[expose] public section diff --git a/Iris/Iris/ProofMode/Patterns/SpecPattern.lean b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean index 55808beda..62c60429c 100644 --- a/Iris/Iris/ProofMode/Patterns/SpecPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean @@ -6,7 +6,7 @@ Authors: Oliver Soeser, Zongyuan Liu, Yunsong Yang, Michael Sammler, Alvin Tang module public import Lean.Syntax -public meta import Iris.Std.RocqPorting +public import Iris.Init @[expose] public section diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index ba365a43f..ab7db46af 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -3,7 +3,9 @@ Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ -import Iris.Std.RocqPorting +module + +import Iris.Init #rocq_ignore_file proofmode "base.v" "Rocq-specific basic functionality" #rocq_ignore_file proofmode "coq_tactics.v" "Tracked via the Tactics concept" diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean index 89b4614a9..e5aecdb79 100644 --- a/Iris/Iris/ProofMode/ProofModeM.lean +++ b/Iris/Iris/ProofMode/ProofModeM.lean @@ -6,6 +6,7 @@ Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang, Alvin Tang module public meta import Iris.ProofMode.Expr +public import Iris.ProofMode.SynthInstance public import Iris.ProofMode.Classes public meta section diff --git a/Iris/Iris/ProofMode/SynthInstance.lean b/Iris/Iris/ProofMode/SynthInstance.lean index 15e90eda0..028d47b35 100644 --- a/Iris/Iris/ProofMode/SynthInstance.lean +++ b/Iris/Iris/ProofMode/SynthInstance.lean @@ -5,7 +5,6 @@ Authors: Michael Sammler -/ module -public import Qq public import Iris.BI public import Iris.ProofMode.SynthInstanceAttr diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean index 12556fbe9..12c3cd255 100644 --- a/Iris/Iris/ProofMode/Tactics.lean +++ b/Iris/Iris/ProofMode/Tactics.lean @@ -1,32 +1,32 @@ /- A description of the tactics can be found in `tactics.md`. -/ module -public meta import Iris.ProofMode.Tactics.Accu -public meta import Iris.ProofMode.Tactics.Apply -public meta import Iris.ProofMode.Tactics.Assumption -public meta import Iris.ProofMode.Tactics.Basic -public meta import Iris.ProofMode.Tactics.Cases -public meta import Iris.ProofMode.Tactics.Clear -public meta import Iris.ProofMode.Tactics.Combine -public meta import Iris.ProofMode.Tactics.Eval -public meta import Iris.ProofMode.Tactics.Exact -public meta import Iris.ProofMode.Tactics.ExFalso -public meta import Iris.ProofMode.Tactics.Exists -public meta import Iris.ProofMode.Tactics.Frame -public meta import Iris.ProofMode.Tactics.Have -public meta import Iris.ProofMode.Tactics.HaveCore -public meta import Iris.ProofMode.Tactics.Induction -public meta import Iris.ProofMode.Tactics.Intro -public meta import Iris.ProofMode.Tactics.Inv -public meta import Iris.ProofMode.Tactics.LeftRight -public meta import Iris.ProofMode.Tactics.Loeb -public meta import Iris.ProofMode.Tactics.Mod -public meta import Iris.ProofMode.Tactics.ModIntro -public meta import Iris.ProofMode.Tactics.Pure -public meta import Iris.ProofMode.Tactics.Rename -public meta import Iris.ProofMode.Tactics.Revert -public meta import Iris.ProofMode.Tactics.RevertIntro -public meta import Iris.ProofMode.Tactics.Rewrite -public meta import Iris.ProofMode.Tactics.Specialize -public meta import Iris.ProofMode.Tactics.Split -public meta import Iris.ProofMode.Tactics.Trivial +public import Iris.ProofMode.Tactics.Accu +public import Iris.ProofMode.Tactics.Apply +public import Iris.ProofMode.Tactics.Assumption +public import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Cases +public import Iris.ProofMode.Tactics.Clear +public import Iris.ProofMode.Tactics.Combine +public import Iris.ProofMode.Tactics.Eval +public import Iris.ProofMode.Tactics.Exact +public import Iris.ProofMode.Tactics.ExFalso +public import Iris.ProofMode.Tactics.Exists +public import Iris.ProofMode.Tactics.Frame +public import Iris.ProofMode.Tactics.Have +public import Iris.ProofMode.Tactics.HaveCore +public import Iris.ProofMode.Tactics.Induction +public import Iris.ProofMode.Tactics.Intro +public import Iris.ProofMode.Tactics.Inv +public import Iris.ProofMode.Tactics.LeftRight +public import Iris.ProofMode.Tactics.Loeb +public import Iris.ProofMode.Tactics.Mod +public import Iris.ProofMode.Tactics.ModIntro +public import Iris.ProofMode.Tactics.Pure +public import Iris.ProofMode.Tactics.Rename +public import Iris.ProofMode.Tactics.Revert +public import Iris.ProofMode.Tactics.RevertIntro +public import Iris.ProofMode.Tactics.Rewrite +public import Iris.ProofMode.Tactics.Specialize +public import Iris.ProofMode.Tactics.Split +public import Iris.ProofMode.Tactics.Trivial diff --git a/Iris/Iris/ProofMode/Tactics/Accu.lean b/Iris/Iris/ProofMode/Tactics/Accu.lean index 9d0bdc930..0546ed078 100644 --- a/Iris/Iris/ProofMode/Tactics/Accu.lean +++ b/Iris/Iris/ProofMode/Tactics/Accu.lean @@ -5,7 +5,7 @@ Authors: Michael Sammler, Alvin Tang -/ module -public meta import Iris.ProofMode.ProofModeM +public import Iris.ProofMode.ProofModeM namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Apply.lean b/Iris/Iris/ProofMode/Tactics/Apply.lean index 6f317022a..cfb46afbf 100644 --- a/Iris/Iris/ProofMode/Tactics/Apply.lean +++ b/Iris/Iris/ProofMode/Tactics/Apply.lean @@ -5,11 +5,8 @@ Authors: Oliver Soeser, Michael Sammler -/ module -import Iris.BI -import Iris.ProofMode.Classes -meta import Iris.ProofMode.Patterns.SpecPattern -meta import Iris.ProofMode.Tactics.Assumption -public meta import Iris.ProofMode.Tactics.HaveCore +public import Iris.BI +public import Iris.ProofMode.Tactics.HaveCore namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Assumption.lean b/Iris/Iris/ProofMode/Tactics/Assumption.lean index 17ae33d6b..daf9d023b 100644 --- a/Iris/Iris/ProofMode/Tactics/Assumption.lean +++ b/Iris/Iris/ProofMode/Tactics/Assumption.lean @@ -6,8 +6,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler module import Iris.BI -import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode public section diff --git a/Iris/Iris/ProofMode/Tactics/Basic.lean b/Iris/Iris/ProofMode/Tactics/Basic.lean index 9c8006ddb..c8c9662c9 100644 --- a/Iris/Iris/ProofMode/Tactics/Basic.lean +++ b/Iris/Iris/ProofMode/Tactics/Basic.lean @@ -5,10 +5,10 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -import Iris.ProofMode.Classes -meta import Iris.ProofMode.Expr -meta import Iris.ProofMode.SynthInstance -public meta import Iris.ProofMode.ProofModeM +public import Iris.ProofMode.Classes +public import Iris.ProofMode.Expr +public import Iris.ProofMode.SynthInstance +public import Iris.ProofMode.ProofModeM public section diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean index df3b86fdb..2615ac55d 100644 --- a/Iris/Iris/ProofMode/Tactics/Cases.lean +++ b/Iris/Iris/ProofMode/Tactics/Cases.lean @@ -5,14 +5,12 @@ Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang, Alvin Tang -/ module -meta import Iris.ProofMode.Patterns.SpecPattern -meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.Tactics.Mod -public meta import Iris.ProofMode.Tactics.Pure -public meta import Iris.ProofMode.Tactics.Clear -public meta import Iris.ProofMode.Tactics.Basic -public meta import Iris.ProofMode.Tactics.HaveCore -public meta import Iris.ProofMode.Tactics.Frame +public import Iris.ProofMode.Tactics.Mod +public import Iris.ProofMode.Tactics.Pure +public import Iris.ProofMode.Tactics.Clear +public import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.HaveCore +public import Iris.ProofMode.Tactics.Frame namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Clear.lean b/Iris/Iris/ProofMode/Tactics/Clear.lean index e514fd48b..b7c9c9a90 100644 --- a/Iris/Iris/ProofMode/Tactics/Clear.lean +++ b/Iris/Iris/ProofMode/Tactics/Clear.lean @@ -6,9 +6,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang module import Iris.BI -import Iris.ProofMode.Classes public meta import Iris.ProofMode.Patterns.SelPattern -public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean index edc5daa08..413911b62 100644 --- a/Iris/Iris/ProofMode/Tactics/Combine.lean +++ b/Iris/Iris/ProofMode/Tactics/Combine.lean @@ -5,10 +5,8 @@ Authors: Alvin Tang, Michael Sammler -/ module -public meta import Iris.ProofMode.Tactics.Assumption -public meta import Iris.ProofMode.Tactics.Cases -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.ClassesMake +public import Iris.ProofMode.Tactics.Cases +public import Iris.ProofMode.ClassesMake namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean index 69e2366c3..c721bbfef 100644 --- a/Iris/Iris/ProofMode/Tactics/Eval.lean +++ b/Iris/Iris/ProofMode/Tactics/Eval.lean @@ -6,7 +6,6 @@ Authors: Michael Sammler, Alvin Tang module public meta import Iris.ProofMode.Patterns.SelPattern -public meta import Iris.ProofMode.ProofModeM namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/ExFalso.lean b/Iris/Iris/ProofMode/Tactics/ExFalso.lean index 18018f64e..e6b7c84f9 100644 --- a/Iris/Iris/ProofMode/Tactics/ExFalso.lean +++ b/Iris/Iris/ProofMode/Tactics/ExFalso.lean @@ -5,8 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -import Iris.BI -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Exact.lean b/Iris/Iris/ProofMode/Tactics/Exact.lean index be47e3931..bd52b8229 100644 --- a/Iris/Iris/ProofMode/Tactics/Exact.lean +++ b/Iris/Iris/ProofMode/Tactics/Exact.lean @@ -5,7 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public meta import Iris.ProofMode.Tactics.Assumption +public import Iris.ProofMode.Tactics.Assumption namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Exists.lean b/Iris/Iris/ProofMode/Tactics/Exists.lean index 1ddcd7fb7..478708dd2 100644 --- a/Iris/Iris/ProofMode/Tactics/Exists.lean +++ b/Iris/Iris/ProofMode/Tactics/Exists.lean @@ -5,9 +5,9 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -import Iris.BI -import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.BI +public import Iris.ProofMode.Classes +public import Iris.ProofMode.ProofModeM namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Frame.lean b/Iris/Iris/ProofMode/Tactics/Frame.lean index 5ac4cd59b..abb739c52 100644 --- a/Iris/Iris/ProofMode/Tactics/Frame.lean +++ b/Iris/Iris/ProofMode/Tactics/Frame.lean @@ -8,7 +8,6 @@ module import Iris.BI import Iris.ProofMode.Classes public meta import Iris.ProofMode.Patterns.SelPattern -public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Have.lean b/Iris/Iris/ProofMode/Tactics/Have.lean index 874eef80e..61f8dc03c 100644 --- a/Iris/Iris/ProofMode/Tactics/Have.lean +++ b/Iris/Iris/ProofMode/Tactics/Have.lean @@ -6,8 +6,6 @@ Authors: Michael Sammler module import Iris.BI -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.Tactics.HaveCore public meta import Iris.ProofMode.Tactics.Cases namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/HaveCore.lean b/Iris/Iris/ProofMode/Tactics/HaveCore.lean index 569eeb14b..3bf3c401f 100644 --- a/Iris/Iris/ProofMode/Tactics/HaveCore.lean +++ b/Iris/Iris/ProofMode/Tactics/HaveCore.lean @@ -8,7 +8,6 @@ module import Iris.BI import Iris.ProofMode.Classes public meta import Iris.ProofMode.Patterns.SpecPattern -public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.Specialize /- diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean index 4a1b27621..100903da1 100644 --- a/Iris/Iris/ProofMode/Tactics/Induction.lean +++ b/Iris/Iris/ProofMode/Tactics/Induction.lean @@ -5,14 +5,7 @@ Authors: Yunsong Yang, Michael Sammler, Alvin Tang -/ module -public meta import Iris.ProofMode.Tactics.Basic -public meta import Iris.ProofMode.Tactics.Assumption -public meta import Iris.ProofMode.Tactics.Cases -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.ClassesMake -public meta import Iris.ProofMode.Tactics.RevertIntro -public meta import Iris.ProofMode.Tactics.Revert -public meta import Lean.Meta.Tactic.TryThis +public import Iris.ProofMode.Tactics.RevertIntro namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean index 6a527d2dd..95704a17d 100644 --- a/Iris/Iris/ProofMode/Tactics/Intro.lean +++ b/Iris/Iris/ProofMode/Tactics/Intro.lean @@ -6,10 +6,10 @@ Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang module public meta import Iris.ProofMode.Patterns.IntroPattern -public meta import Iris.ProofMode.Tactics.Cases -public meta import Iris.ProofMode.Tactics.Pure -public meta import Iris.ProofMode.Tactics.ModIntro -public meta import Iris.ProofMode.Tactics.Trivial +public import Iris.ProofMode.Tactics.Cases +public import Iris.ProofMode.Tactics.Pure +public import Iris.ProofMode.Tactics.ModIntro +public import Iris.ProofMode.Tactics.Trivial namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Inv.lean b/Iris/Iris/ProofMode/Tactics/Inv.lean index b8bf68848..06e8f5712 100644 --- a/Iris/Iris/ProofMode/Tactics/Inv.lean +++ b/Iris/Iris/ProofMode/Tactics/Inv.lean @@ -5,13 +5,7 @@ Authors: Michael Sammler, Alvin Tang -/ module -public meta import Iris.ProofMode.Tactics.Assumption -public meta import Iris.ProofMode.Tactics.Cases -public meta import Iris.ProofMode.Tactics.Intro -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.Patterns.IntroPattern -public meta import Iris.ProofMode.Patterns.SelPattern -public meta import Iris.ProofMode.ClassesMake +public import Iris.ProofMode.Tactics.Cases namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/LeftRight.lean b/Iris/Iris/ProofMode/Tactics/LeftRight.lean index 1b4691627..15481aba2 100644 --- a/Iris/Iris/ProofMode/Tactics/LeftRight.lean +++ b/Iris/Iris/ProofMode/Tactics/LeftRight.lean @@ -7,7 +7,7 @@ module import Iris.BI import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.ProofModeM namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Mod.lean b/Iris/Iris/ProofMode/Tactics/Mod.lean index 7b2a7431a..58aff0609 100644 --- a/Iris/Iris/ProofMode/Tactics/Mod.lean +++ b/Iris/Iris/ProofMode/Tactics/Mod.lean @@ -7,7 +7,7 @@ module import Iris.BI public import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean index df1557e71..ff732097e 100644 --- a/Iris/Iris/ProofMode/Tactics/Pure.lean +++ b/Iris/Iris/ProofMode/Tactics/Pure.lean @@ -5,7 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Rename.lean b/Iris/Iris/ProofMode/Tactics/Rename.lean index c8a81ba7d..127e0769d 100644 --- a/Iris/Iris/ProofMode/Tactics/Rename.lean +++ b/Iris/Iris/ProofMode/Tactics/Rename.lean @@ -5,7 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Revert.lean b/Iris/Iris/ProofMode/Tactics/Revert.lean index 81d2121d0..bc27f0c3d 100644 --- a/Iris/Iris/ProofMode/Tactics/Revert.lean +++ b/Iris/Iris/ProofMode/Tactics/Revert.lean @@ -7,11 +7,6 @@ module public import Iris.ProofMode.ClassesMake public meta import Iris.ProofMode.Patterns.SelPattern -public meta import Iris.ProofMode.Tactics.Basic -public meta import Iris.ProofMode.Tactics.Assumption -public meta import Iris.ProofMode.Tactics.Cases -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Lean.Meta.Tactic.TryThis namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Rewrite.lean b/Iris/Iris/ProofMode/Tactics/Rewrite.lean index 9752ea5cd..9041494be 100644 --- a/Iris/Iris/ProofMode/Tactics/Rewrite.lean +++ b/Iris/Iris/ProofMode/Tactics/Rewrite.lean @@ -5,13 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. module import Iris.BI -public import Iris.BI.InternalEq -public import Iris.ProofMode.Classes -public import Iris.Std.TC -public import Iris.ProofMode.ProofModeM -public meta import Iris.ProofMode.Patterns.SpecPattern -public meta import Iris.ProofMode.Tactics.HaveCore -meta import Lean.Parser.Tactic +public import Iris.ProofMode.Tactics.HaveCore namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean index 4c130962a..95aed8fa2 100644 --- a/Iris/Iris/ProofMode/Tactics/Specialize.lean +++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean @@ -6,8 +6,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang module public meta import Iris.ProofMode.Patterns.SpecPattern -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Patterns.CasesPattern public import Iris.ProofMode.Tactics.Trivial public import Iris.ProofMode.Tactics.Frame diff --git a/Iris/Iris/ProofMode/Tactics/Split.lean b/Iris/Iris/ProofMode/Tactics/Split.lean index 12e57b9bf..913906f61 100644 --- a/Iris/Iris/ProofMode/Tactics/Split.lean +++ b/Iris/Iris/ProofMode/Tactics/Split.lean @@ -7,7 +7,7 @@ module import Iris.BI import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.ProofModeM namespace Iris.ProofMode diff --git a/Iris/Iris/ProofMode/Tactics/Trivial.lean b/Iris/Iris/ProofMode/Tactics/Trivial.lean index 5c4fc96c5..442c7496d 100644 --- a/Iris/Iris/ProofMode/Tactics/Trivial.lean +++ b/Iris/Iris/ProofMode/Tactics/Trivial.lean @@ -7,7 +7,7 @@ module import Iris.BI public import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/Iris/Iris/Std.lean b/Iris/Iris/Std.lean index 97fdad4ff..9c051af9c 100644 --- a/Iris/Iris/Std.lean +++ b/Iris/Iris/Std.lean @@ -5,7 +5,6 @@ public import Iris.Std.BitOp public import Iris.Std.Classes public import Iris.Std.CoPset public import Iris.Std.DelabRule -/- public import Iris.Std.DumpPortingData -/ public import Iris.Std.Equivalence public import Iris.Std.Expr public import Iris.Std.FromMathlib diff --git a/Iris/Iris/Std/BigOp.lean b/Iris/Iris/Std/BigOp.lean index 17eea983f..3e55daa88 100644 --- a/Iris/Iris/Std/BigOp.lean +++ b/Iris/Iris/Std/BigOp.lean @@ -5,6 +5,8 @@ Authors: Lars König, Mario Carneiro -/ module +public import Iris.Init + @[expose] public section namespace Iris.Std diff --git a/Iris/Iris/Std/BitOp.lean b/Iris/Iris/Std/BitOp.lean index 6c43a5c2a..adab1d03e 100644 --- a/Iris/Iris/Std/BitOp.lean +++ b/Iris/Iris/Std/BitOp.lean @@ -3,6 +3,7 @@ module public import Batteries.Data.Int public import Batteries.Data.Nat.Bitwise import all Init.Data.Nat.Bitwise.Basic +public import Iris.Init @[expose] public section diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean index 661575c6f..8e94c05f9 100644 --- a/Iris/Iris/Std/Classes.lean +++ b/Iris/Iris/Std/Classes.lean @@ -5,6 +5,8 @@ Authors: Lars König -/ module +public import Iris.Init + @[expose] public section namespace Iris.Std diff --git a/Iris/Iris/Std/DelabRule.lean b/Iris/Iris/Std/DelabRule.lean index f27dbe9bb..1ba209a33 100644 --- a/Iris/Iris/Std/DelabRule.lean +++ b/Iris/Iris/Std/DelabRule.lean @@ -5,8 +5,9 @@ Authors: Lars König -/ module -public meta import Lean.PrettyPrinter.Delaborator -public meta import Lean.Parser.Term +public import Lean.PrettyPrinter.Delaborator +public import Lean.Parser.Term +public import Iris.Init public meta section diff --git a/Iris/Iris/Std/Equivalence.lean b/Iris/Iris/Std/Equivalence.lean index 878b8b8ea..8bf9941c3 100644 --- a/Iris/Iris/Std/Equivalence.lean +++ b/Iris/Iris/Std/Equivalence.lean @@ -5,6 +5,8 @@ Authors: Mario Carneiro -/ module +public import Iris.Init + @[expose] public section theorem equivalence_eq : Equivalence (@Eq α) := ⟨.refl, .symm, .trans⟩ diff --git a/Iris/Iris/Std/Expr.lean b/Iris/Iris/Std/Expr.lean index 4f58a4492..219a1b5fe 100644 --- a/Iris/Iris/Std/Expr.lean +++ b/Iris/Iris/Std/Expr.lean @@ -6,6 +6,7 @@ Authors: Lars König module public import Lean.Meta +public import Iris.Init @[expose] public section diff --git a/Iris/Iris/Std/FromMathlib.lean b/Iris/Iris/Std/FromMathlib.lean index 13c65ef28..78c649de6 100644 --- a/Iris/Iris/Std/FromMathlib.lean +++ b/Iris/Iris/Std/FromMathlib.lean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. module public import Batteries.Data.List.Basic +public import Iris.Init @[expose] public section diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index 67a2a0b3e..3b34677a4 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -9,7 +9,6 @@ public import Iris.Std.Classes public import Iris.Std.Infinite import Batteries.Data.List.Perm import Iris.Std.List -import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Std/Namespaces.lean b/Iris/Iris/Std/Namespaces.lean index 4a9b1d5d0..3abf3ec66 100644 --- a/Iris/Iris/Std/Namespaces.lean +++ b/Iris/Iris/Std/Namespaces.lean @@ -8,7 +8,6 @@ module public import Iris.Std.CoPset public import Iris.Std.Positives public import Iris.Std.GenSets -meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Std/Nat.lean b/Iris/Iris/Std/Nat.lean index e2790828e..1cee3c662 100644 --- a/Iris/Iris/Std/Nat.lean +++ b/Iris/Iris/Std/Nat.lean @@ -5,6 +5,8 @@ Authors: Markus de Medeiros -/ module +public import Iris.Init + @[expose] public section namespace Nat diff --git a/Iris/Iris/Std/Option.lean b/Iris/Iris/Std/Option.lean index bd5d1681f..021171eba 100644 --- a/Iris/Iris/Std/Option.lean +++ b/Iris/Iris/Std/Option.lean @@ -6,6 +6,8 @@ Authors: Markus de Medeiros module +public import Iris.Init + @[expose] public section namespace Option diff --git a/Iris/Iris/Std/Prod.lean b/Iris/Iris/Std/Prod.lean index 7890e4d42..618c4e9f5 100644 --- a/Iris/Iris/Std/Prod.lean +++ b/Iris/Iris/Std/Prod.lean @@ -5,6 +5,8 @@ Authors: Lars König -/ module +public import Iris.Init + @[expose] public section namespace Prod diff --git a/Iris/Iris/Std/Qq.lean b/Iris/Iris/Std/Qq.lean index 54b2dc739..47e767f8e 100644 --- a/Iris/Iris/Std/Qq.lean +++ b/Iris/Iris/Std/Qq.lean @@ -6,6 +6,7 @@ Authors: Mario Carneiro module public import Qq +public import Iris.Init @[expose] public section open Qq Lean diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean index 394236610..66671cb56 100644 --- a/Iris/Iris/Std/Rewrite.lean +++ b/Iris/Iris/Std/Rewrite.lean @@ -5,7 +5,7 @@ Authors: Lars König -/ module -public meta import Iris.Std.Tactic +public import Iris.Std.Tactic public meta section diff --git a/Iris/Iris/Std/RocqPorting.lean b/Iris/Iris/Std/RocqPorting.lean index db35566f2..19033bf1d 100644 --- a/Iris/Iris/Std/RocqPorting.lean +++ b/Iris/Iris/Std/RocqPorting.lean @@ -5,8 +5,8 @@ Authors: Markus de Medeiros, Zongyuan Liu -/ module -import Lean -public meta import Lean +import Lean.Elab.DeclarationRange +public meta import Lean.Elab.Command /-! # Rocq Porting Infrastructure diff --git a/Iris/Iris/Std/Set.lean b/Iris/Iris/Std/Set.lean index c4f1818b8..33fcbfdff 100644 --- a/Iris/Iris/Std/Set.lean +++ b/Iris/Iris/Std/Set.lean @@ -5,6 +5,8 @@ Authors: Markus de Medeiros -/ module +public import Iris.Init + @[expose] public section namespace Set diff --git a/Iris/Iris/Std/TC.lean b/Iris/Iris/Std/TC.lean index 2f73daacf..28dcbf384 100644 --- a/Iris/Iris/Std/TC.lean +++ b/Iris/Iris/Std/TC.lean @@ -5,6 +5,8 @@ Authors: Lars König -/ module +public import Iris.Init + @[expose] public section namespace Iris.Std diff --git a/Iris/Iris/Std/Tactic.lean b/Iris/Iris/Std/Tactic.lean index 2d26374ee..255b1b242 100644 --- a/Iris/Iris/Std/Tactic.lean +++ b/Iris/Iris/Std/Tactic.lean @@ -5,7 +5,9 @@ Authors: Lars König -/ module -public meta import Lean.Elab.Tactic +meta import Lean.Elab.Tactic.ElabTerm +public import Lean.Elab.Tactic +public import Iris.Init public meta section diff --git a/Iris/Iris/Std/Try.lean b/Iris/Iris/Std/Try.lean index 5466baffd..bfeb15034 100644 --- a/Iris/Iris/Std/Try.lean +++ b/Iris/Iris/Std/Try.lean @@ -5,6 +5,8 @@ Authors: Mario Carneiro -/ module +public import Iris.Init + @[expose] public section namespace Iris.ProofMode diff --git a/Iris/Iris/Tests.lean b/Iris/Iris/Tests.lean deleted file mode 100644 index ee60cdaff..000000000 --- a/Iris/Iris/Tests.lean +++ /dev/null @@ -1,11 +0,0 @@ -module - -public import Iris.Tests.Display -public import Iris.Tests.HeapLang -public import Iris.Tests.Instances -public import Iris.Tests.InstancesImport -public import Iris.Tests.Language -public import Iris.Tests.Notation -public import Iris.Tests.Tactics -public import Iris.Tests.Updates -public import Iris.Tests.WeakestPre diff --git a/Iris/Iris/Tests/HeapLang.lean b/Iris/Iris/Tests/HeapLang.lean deleted file mode 100644 index 012c6f282..000000000 --- a/Iris/Iris/Tests/HeapLang.lean +++ /dev/null @@ -1,9 +0,0 @@ -module - -public import Iris.Tests.HeapLang.Linter -public import Iris.Tests.HeapLang.Notation -public import Iris.Tests.HeapLang.WeakestPre -public import Iris.Tests.HeapLang.HeapTactics -public import Iris.Tests.HeapLang.Linter -public import Iris.Tests.HeapLang.Par -public import Iris.Tests.HeapLang.Tactics diff --git a/Iris/Iris/Tests/Display.lean b/Iris/IrisTest/Display.lean similarity index 99% rename from Iris/Iris/Tests/Display.lean rename to Iris/IrisTest/Display.lean index 60a9669f2..0addb8854 100644 --- a/Iris/Iris/Tests/Display.lean +++ b/Iris/IrisTest/Display.lean @@ -9,9 +9,8 @@ module import Lean public import Iris.ProofMode -open Lean Elab Meta - -namespace Iris.Tests +namespace IrisTest +open Lean Elab Meta Iris meta section diff --git a/Iris/IrisTest/HeapLang.lean b/Iris/IrisTest/HeapLang.lean new file mode 100644 index 000000000..ce7f69b71 --- /dev/null +++ b/Iris/IrisTest/HeapLang.lean @@ -0,0 +1,9 @@ +module + +public import IrisTest.HeapLang.Linter +public import IrisTest.HeapLang.Notation +public import IrisTest.HeapLang.WeakestPre +public import IrisTest.HeapLang.HeapTactics +public import IrisTest.HeapLang.Linter +public import IrisTest.HeapLang.Par +public import IrisTest.HeapLang.Tactics diff --git a/Iris/Iris/Tests/HeapLang/HeapTactics.lean b/Iris/IrisTest/HeapLang/HeapTactics.lean similarity index 100% rename from Iris/Iris/Tests/HeapLang/HeapTactics.lean rename to Iris/IrisTest/HeapLang/HeapTactics.lean diff --git a/Iris/Iris/Tests/HeapLang/Linter.lean b/Iris/IrisTest/HeapLang/Linter.lean similarity index 97% rename from Iris/Iris/Tests/HeapLang/Linter.lean rename to Iris/IrisTest/HeapLang/Linter.lean index ba4d0fd07..27c42b22f 100644 --- a/Iris/Iris/Tests/HeapLang/Linter.lean +++ b/Iris/IrisTest/HeapLang/Linter.lean @@ -7,7 +7,7 @@ module public import Iris.HeapLang @[expose] public section -namespace Iris.Tests.HeapLang.Linter +namespace IrisTest.HeapLang.Linter open Iris.HeapLang @@ -99,4 +99,4 @@ Note: This linter can be disabled with `set_option linter.heapLang.freeVars fals #guard_msgs(drop info, check warning) in #check hl(let c := ref(#0); &(hl(c ← #1))) -end Iris.Tests.HeapLang.Linter +end IrisTest.HeapLang.Linter diff --git a/Iris/Iris/Tests/HeapLang/Notation.lean b/Iris/IrisTest/HeapLang/Notation.lean similarity index 99% rename from Iris/Iris/Tests/HeapLang/Notation.lean rename to Iris/IrisTest/HeapLang/Notation.lean index 219433cd7..0055f0e62 100644 --- a/Iris/Iris/Tests/HeapLang/Notation.lean +++ b/Iris/IrisTest/HeapLang/Notation.lean @@ -7,9 +7,9 @@ module public import Iris.HeapLang @[expose] public section -namespace Iris.Tests.HeapLang +namespace IrisTest.HeapLang -open Iris.HeapLang +open Iris HeapLang section test @@ -343,4 +343,4 @@ variable (p : ProphId) (w : Val) (e : Exp) end test -end Iris.Tests.HeapLang +end IrisTest.HeapLang diff --git a/Iris/Iris/Tests/HeapLang/Par.lean b/Iris/IrisTest/HeapLang/Par.lean similarity index 92% rename from Iris/Iris/Tests/HeapLang/Par.lean rename to Iris/IrisTest/HeapLang/Par.lean index 9f41a2ea7..c0b26b0ed 100644 --- a/Iris/Iris/Tests/HeapLang/Par.lean +++ b/Iris/IrisTest/HeapLang/Par.lean @@ -8,9 +8,9 @@ module public import Iris.HeapLang.Lib.Par @[expose] public section -namespace Iris.Tests.HeapLang.Par +namespace IrisTest.HeapLang.Par -open Iris.HeapLang BI Iris ProgramLogic Spawn Iris.HeapLang.Par +open Iris HeapLang BI Iris ProgramLogic Spawn Iris.HeapLang.Par -- Regression test for -- https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean/topic/Porting.20iris-tutorial/near/613886178 @@ -58,5 +58,5 @@ example {hlc} {GF : BundledGFunctors} [HeapLangGS hlc GF] [SpawnG GF] : iframe itrivial -end Iris.Tests.HeapLang.Par +end IrisTest.HeapLang.Par end diff --git a/Iris/Iris/Tests/HeapLang/Tactics.lean b/Iris/IrisTest/HeapLang/Tactics.lean similarity index 100% rename from Iris/Iris/Tests/HeapLang/Tactics.lean rename to Iris/IrisTest/HeapLang/Tactics.lean diff --git a/Iris/Iris/Tests/HeapLang/WeakestPre.lean b/Iris/IrisTest/HeapLang/WeakestPre.lean similarity index 100% rename from Iris/Iris/Tests/HeapLang/WeakestPre.lean rename to Iris/IrisTest/HeapLang/WeakestPre.lean diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/IrisTest/Instances.lean similarity index 80% rename from Iris/Iris/Tests/Instances.lean rename to Iris/IrisTest/Instances.lean index 22407157d..d15fc7308 100644 --- a/Iris/Iris/Tests/Instances.lean +++ b/Iris/IrisTest/Instances.lean @@ -13,8 +13,8 @@ public import Iris.ProofMode.NatCancel @[expose] public section -namespace Iris.Tests -open Lean Qq BI ProofMode +namespace IrisTest +open Lean Qq Iris BI ProofMode /- Tests the mvar handling of synth and ipm_synth -/ section mvars @@ -187,11 +187,11 @@ info: solution: TacticTest iprop(emp ∗ P) P, new goals: [] --- trace: [Meta.synthInstance] ✅️ IPM: TacticTest iprop(emp ∗ P) P [Meta.synthInstance] ✅️ IPM: new goal TacticTest iprop(emp ∗ P) ?_ => TacticTest iprop(emp ∗ P) P - [Meta.synthInstance.tactics] [Iris.Tests.tac_sep:1000, Iris.Tests.tac_emp:1000, Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to TacticTest iprop(emp ∗ P) ?_ - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances - [Meta.synthInstance] ✅️ apply tactic Iris.Tests.tac_emp to TacticTest iprop(emp ∗ P) ?_ - [Meta.synthInstance] Iris.Tests.tac_emp success: tactic_test_emp P + [Meta.synthInstance.tactics] [IrisTest.tac_sep:1000, IrisTest.tac_emp:1000, IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to TacticTest iprop(emp ∗ P) ?_ + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance] ✅️ apply tactic IrisTest.tac_emp to TacticTest iprop(emp ∗ P) ?_ + [Meta.synthInstance] IrisTest.tac_emp success: tactic_test_emp P [Meta.synthInstance] result tactic_test_emp P -/ #guard_msgs (substring := true) in @@ -209,17 +209,17 @@ info: solution: TacticTest iprop((emp ∗ P) ∗ P) iprop(P ∗ P), new goals: [ trace: [Meta.synthInstance] ✅️ IPM: TacticTest iprop((emp ∗ P) ∗ P) iprop(P ∗ P) [Meta.synthInstance] ✅️ IPM: new goal TacticTest iprop((emp ∗ P) ∗ P) ?_ => TacticTest iprop((emp ∗ P) ∗ P) iprop(P ∗ P) - [Meta.synthInstance.tactics] [Iris.Tests.tac_sep:1000, Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to TacticTest iprop((emp ∗ P) ∗ P) ?_ - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances - [Meta.synthInstance] ✅️ apply tactic Iris.Tests.tac_sep to TacticTest iprop((emp ∗ P) ∗ P) ?_ + [Meta.synthInstance.tactics] [IrisTest.tac_sep:1000, IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to TacticTest iprop((emp ∗ P) ∗ P) ?_ + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance] ✅️ apply tactic IrisTest.tac_sep to TacticTest iprop((emp ∗ P) ∗ P) ?_ [Meta.synthInstance] ✅️ IPM: new goal TacticTest iprop(emp ∗ P) ?_ => TacticTest iprop(emp ∗ P) P - [Meta.synthInstance.tactics] [Iris.Tests.tac_sep:1000, Iris.Tests.tac_emp:1000, Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to TacticTest iprop(emp ∗ P) ?_ - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances - [Meta.synthInstance] ✅️ apply tactic Iris.Tests.tac_emp to TacticTest iprop(emp ∗ P) ?_ - [Meta.synthInstance] Iris.Tests.tac_emp success: tactic_test_emp P - [Meta.synthInstance] Iris.Tests.tac_sep success: tactic_test_sep iprop(emp ∗ P) P P (tactic_test_emp P) + [Meta.synthInstance.tactics] [IrisTest.tac_sep:1000, IrisTest.tac_emp:1000, IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to TacticTest iprop(emp ∗ P) ?_ + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance] ✅️ apply tactic IrisTest.tac_emp to TacticTest iprop(emp ∗ P) ?_ + [Meta.synthInstance] IrisTest.tac_emp success: tactic_test_emp P + [Meta.synthInstance] IrisTest.tac_sep success: tactic_test_sep iprop(emp ∗ P) P P (tactic_test_emp P) [Meta.synthInstance] result tactic_test_sep iprop(emp ∗ P) P P (tactic_test_emp P) -/ #guard_msgs (substring := true) in @@ -239,9 +239,9 @@ info: solution: TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) iprop(∀ a trace: [Meta.synthInstance] ✅️ IPM: TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) iprop(∀ a, ⌜a = 5⌝ ∗ P) [Meta.synthInstance] ✅️ IPM: new goal TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) ?_ => TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) iprop(∀ a, ⌜a = 5⌝ ∗ P) - [Meta.synthInstance.tactics] [Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) ?_ - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance.tactics] [IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) ?_ + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances [Meta.synthInstance.instances] #[@tactic_test_all] [Meta.synthInstance] ✅️ apply @tactic_test_all to TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) ?_ [Meta.synthInstance.tryResolve] ✅️ TacticTest iprop(∀ a, (emp ∗ ⌜a = 5⌝) ∗ P) @@ -257,22 +257,20 @@ trace: [Meta.synthInstance] ✅️ IPM: TacticTest iprop(∀ a, (emp ∗ ⌜a = [Meta.synthInstance] ✅️ IPM: new goal ∀ (a : Nat), TacticTest iprop((emp ∗ ⌜a = 5⌝) ∗ P) (?_ a) => ∀ (a : Nat), TacticTest iprop((emp ∗ ⌜a = 5⌝) ∗ P) iprop(⌜a = 5⌝ ∗ P) - [Meta.synthInstance.tactics] [Iris.Tests.tac_sep:1000, Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to ∀ (a : Nat), + [Meta.synthInstance.tactics] [IrisTest.tac_sep:1000, IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to ∀ (a : Nat), TacticTest iprop((emp ∗ ⌜a = 5⌝) ∗ P) (?_ a) - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances - [Meta.synthInstance] ✅️ apply tactic Iris.Tests.tac_sep to ∀ (a : Nat), + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance] ✅️ apply tactic IrisTest.tac_sep to ∀ (a : Nat), TacticTest iprop((emp ∗ ⌜a = 5⌝) ∗ P) (?_ a) [Meta.synthInstance] ✅️ IPM: new goal TacticTest iprop(emp ∗ ⌜a = 5⌝) ?_ => TacticTest iprop(emp ∗ ⌜a = 5⌝) iprop(⌜a = 5⌝) - [Meta.synthInstance.tactics] [Iris.Tests.tac_sep:1000, - Iris.Tests.tac_emp:1000, - Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to TacticTest iprop(emp ∗ ⌜a = 5⌝) ?_ - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances - [Meta.synthInstance] ✅️ apply tactic Iris.Tests.tac_emp to TacticTest iprop(emp ∗ ⌜a = 5⌝) ?_ - [Meta.synthInstance] Iris.Tests.tac_emp success: tactic_test_emp iprop(⌜a = 5⌝) - [Meta.synthInstance] Iris.Tests.tac_sep success: tactic_test_sep iprop(emp ∗ ⌜a = 5⌝) iprop(⌜a = 5⌝) P + [Meta.synthInstance.tactics] [IrisTest.tac_sep:1000, IrisTest.tac_emp:1000, IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to TacticTest iprop(emp ∗ ⌜a = 5⌝) ?_ + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance] ✅️ apply tactic IrisTest.tac_emp to TacticTest iprop(emp ∗ ⌜a = 5⌝) ?_ + [Meta.synthInstance] IrisTest.tac_emp success: tactic_test_emp iprop(⌜a = 5⌝) + [Meta.synthInstance] IrisTest.tac_sep success: tactic_test_sep iprop(emp ∗ ⌜a = 5⌝) iprop(⌜a = 5⌝) P (tactic_test_emp iprop(⌜a = 5⌝)) [Meta.synthInstance] result tactic_test_all (fun a => iprop((emp ∗ ⌜a = 5⌝) ∗ P)) fun a => iprop(⌜a = 5⌝ ∗ P) -/ @@ -288,11 +286,11 @@ info: None --- trace: [Meta.synthInstance] ❌️ IPM: TacticTest iprop(True) ?_ [Meta.synthInstance] ❌️ IPM: new goal TacticTest iprop(True) ?_ => TacticTest iprop(True) ?_ - [Meta.synthInstance.tactics] [Iris.Tests.tac_fail:100, Iris.Tests.tac_continue:10000] - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_continue to TacticTest iprop(True) ?_ - [Meta.synthInstance] Iris.Tests.tac_continue did not find an instance, continue to other instances - [Meta.synthInstance] ❌️ apply tactic Iris.Tests.tac_fail to TacticTest iprop(True) ?_ - [Meta.synthInstance] Iris.Tests.tac_fail failed, no backtracking to other instances + [Meta.synthInstance.tactics] [IrisTest.tac_fail:100, IrisTest.tac_continue:10000] + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_continue to TacticTest iprop(True) ?_ + [Meta.synthInstance] IrisTest.tac_continue did not find an instance, continue to other instances + [Meta.synthInstance] ❌️ apply tactic IrisTest.tac_fail to TacticTest iprop(True) ?_ + [Meta.synthInstance] IrisTest.tac_fail failed, no backtracking to other instances [Meta.synthInstance] result -/ #guard_msgs (substring := true) in diff --git a/Iris/Iris/Tests/InstancesImport.lean b/Iris/IrisTest/InstancesImport.lean similarity index 91% rename from Iris/Iris/Tests/InstancesImport.lean rename to Iris/IrisTest/InstancesImport.lean index 61db2f808..7881654c5 100644 --- a/Iris/Iris/Tests/InstancesImport.lean +++ b/Iris/IrisTest/InstancesImport.lean @@ -5,14 +5,14 @@ Authors: Michael Sammler -/ module -import Iris.Tests.Instances +import IrisTest.Instances /- This file tests that IPM tactic instances declared in other files are imported and applied correctly. -/ @[expose] public section -namespace Iris.Tests -open Lean Qq BI ProofMode +namespace IrisTest +open Lean Iris Qq BI ProofMode variable {PROP} [BI PROP] (P : PROP) diff --git a/Iris/Iris/Tests/Language.lean b/Iris/IrisTest/Language.lean similarity index 98% rename from Iris/Iris/Tests/Language.lean rename to Iris/IrisTest/Language.lean index 28afb5ec5..f567ac7f2 100644 --- a/Iris/Iris/Tests/Language.lean +++ b/Iris/IrisTest/Language.lean @@ -8,7 +8,7 @@ public import Iris.ProgramLogic.Language @[expose] public section -namespace Iris.Tests +namespace IrisTest open Iris ProgramLogic Language Notation /-! This section provides tests for notation used for the Language interface. -/ diff --git a/Iris/Iris/Tests/Notation.lean b/Iris/IrisTest/Notation.lean similarity index 99% rename from Iris/Iris/Tests/Notation.lean rename to Iris/IrisTest/Notation.lean index 8fe4bb166..f1c2a7d04 100644 --- a/Iris/Iris/Tests/Notation.lean +++ b/Iris/IrisTest/Notation.lean @@ -10,8 +10,8 @@ public import Iris.BI.Updates @[expose] public section -namespace Iris.Tests -open Iris.BI +namespace IrisTest +open Iris BI /-! This file contains tests for the predefined separation logic notations. -/ @@ -243,4 +243,4 @@ def f (g : A R → (R → PROP) → PROP) : end MWE -end Iris.Tests +end IrisTest diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/IrisTest/Tactics.lean similarity index 99% rename from Iris/Iris/Tests/Tactics.lean rename to Iris/IrisTest/Tactics.lean index 4b4adebc9..61f23f8b1 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/IrisTest/Tactics.lean @@ -21,8 +21,8 @@ public import Iris.ProgramLogic.WeakestPre @[expose] public section -namespace Iris.Tests -open BI CMRA DFrac CancelableInvariant NonAtomicInvariant ProgramLogic +namespace IrisTest +open Iris BI CMRA DFrac CancelableInvariant NonAtomicInvariant ProgramLogic /- This file contains tests with various scenarios for all available tactics. -/ diff --git a/Iris/Iris/Tests/Updates.lean b/Iris/IrisTest/Updates.lean similarity index 100% rename from Iris/Iris/Tests/Updates.lean rename to Iris/IrisTest/Updates.lean diff --git a/Iris/Iris/Tests/WeakestPre.lean b/Iris/IrisTest/WeakestPre.lean similarity index 99% rename from Iris/Iris/Tests/WeakestPre.lean rename to Iris/IrisTest/WeakestPre.lean index f4c06e08d..4f4aeca18 100644 --- a/Iris/Iris/Tests/WeakestPre.lean +++ b/Iris/IrisTest/WeakestPre.lean @@ -9,7 +9,7 @@ public import Iris.HeapLang @[expose] public section -namespace Iris.Tests +namespace IrisTest open Iris /- This section checks whether the syntax is recognized correctly for all combinations -/ @@ -287,4 +287,3 @@ info: iprop(□ ∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl(if (#1 < #2) #guard_msgs in #check iprop({{ P }} hl(#1) {{ v, RET v; ⌜v = hl_val(#1)⌝ }} : PROP) end HeapLangTestTexanTriple - diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml index a15eb9aa5..b3d4614f7 100644 --- a/Iris/lakefile.toml +++ b/Iris/lakefile.toml @@ -1,5 +1,6 @@ name = "iris" -defaultTargets = ["Iris", "IrisTest"] +defaultTargets = ["Iris"] +testDriver = "IrisTest" [[require]] name = "Qq" @@ -16,11 +17,11 @@ name = "Iris" [[lean_lib]] name = "IrisTest" -globs = ["Iris.*"] +globs = ["IrisTest.+"] [[lean_exe]] name = "dumpPortingData" -srcDir = "Iris/Std" +srcDir = "../scripts" root = "DumpPortingData" supportInterpreter = true diff --git a/IrisMath/IrisMath.lean b/IrisMath/IrisMath.lean index 859caa33f..0c04fcdd8 100644 --- a/IrisMath/IrisMath.lean +++ b/IrisMath/IrisMath.lean @@ -3,4 +3,3 @@ module public import IrisMath.MeasureTheory public import IrisMath.Numbers public import IrisMath.StepIndex -public import IrisMath.Tests diff --git a/IrisMath/IrisMath/Tests.lean b/IrisMath/IrisMath/Tests.lean deleted file mode 100644 index de41660ba..000000000 --- a/IrisMath/IrisMath/Tests.lean +++ /dev/null @@ -1,3 +0,0 @@ -module - -public import IrisMath.Tests.Numbers diff --git a/IrisMath/IrisMath/Tests/Numbers.lean b/IrisMath/IrisMathTest/Numbers.lean similarity index 100% rename from IrisMath/IrisMath/Tests/Numbers.lean rename to IrisMath/IrisMathTest/Numbers.lean diff --git a/IrisMath/lakefile.toml b/IrisMath/lakefile.toml index 5916a8609..991bdedbd 100644 --- a/IrisMath/lakefile.toml +++ b/IrisMath/lakefile.toml @@ -2,6 +2,7 @@ name = "irismath" version = "0.1.0" keywords = ["math"] defaultTargets = ["IrisMath"] +testDriver = "IrisMathTest" [leanOptions] pp.unicode.fun = true @@ -22,6 +23,10 @@ path = "../Iris/" [[lean_lib]] name = "IrisMath" +[[lean_lib]] +name = "IrisMathTest" +globs = ["IrisMathTest.+"] + [[lean_exe]] name = "check-imports" srcDir = "../scripts" diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index bbb89df3b..285702092 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -9,9 +9,13 @@ import Lean.Elab.ParseImportsFast import Std.Data.HashMap import Std.Data.HashSet -/- -This script checks that the modules of a library (e.g. `Iris`, `IrisMath`) are -imported by the entry-point files of the directories containing them. +/-! +This script has two functions. + +### Recursive check for missing imports + +The first functionality is to check that the modules of a library (e.g. `Iris`, `IrisMath`) +are imported by the entry-point files of the directories containing them. The project is assumed to be organised so that every directory `Foo` is accompanied by a module `Foo.lean` acting as its entry point: `Iris/BI/` by `Iris/BI.lean`, @@ -19,70 +23,64 @@ a module `Foo.lean` acting as its entry point: `Iris/BI/` by `Iris/BI.lean`, for every directory, its entry point must transitively import every module below it. Directories listed in `detachedDirs` are the only exception, see below. +### Check that all modules imports `Init.lean` + +The second functionality is to check that every module of a library +(e.g. `Iris`, `IrisMath`) directly or transitively imports the initialisation +module of that library, e.g. `Iris.Init`. + +`Init.lean` collects the imports that set up the environment of the library (options, +attributes, notation, linters, ...), so it has to be reached from every module of the +library. The only modules exempt from this are the ones `Init.lean` itself depends on: +these are reachable *from* `Init` and could not import it without creating a cycle. + +### Usage + Run the script using `lake exe check-imports `. For example, `lake exe check-imports Iris` checks `Iris.lean` against all of `Iris/`, then -`Iris/Algebra.lean` against `Iris/Algebra/`, and so on down the tree. +`Iris/Algebra.lean` against `Iris/Algebra/`, and so on down the tree. It then +checks that all modules under `Iris/` imports `Iris/Init.lean`. +- Use the flag `--entry-points-only` for the first check only. +- Use the flag `--init-only` for the second check only. -Returns `0` if all modules are imported, `1` if that list is non-empty, or +Returns `0` if all checks pass, `1` if any of the checks fails, or `2` if the check fails for another reason (e.g. module not found). -/ open System (FilePath) open Lean SearchPath -/-- Root of the package sources: the module `A.B` lives in `/A/B.lean`. -/ -private def srcDir : FilePath := ⟨"."⟩ - -/-- Search path used to resolve a module to a source file *of this package*. Imports of -`Init`, `Std`, `Batteries` or `Qq` resolve to `none` here and are hence not followed. -/ +/-- +Search path used to resolve a module to a source file of this package. +Imports of `Init`, `Std`, `Batteries` or `Qq` resolve to `none` here and are +hence not followed. +-/ private def srcPath : SearchPath := [⟨"."⟩] /-- The source file of a module, e.g. `Iris.BI` to `./Iris/BI.lean`. -/ private def moduleFile (mod : Name) : FilePath := - modToFilePath srcDir mod "lean" + modToFilePath ⟨"."⟩ mod "lean" /-- The directory holding the submodules of a module, e.g. `Iris.BI` to `./Iris/BI`. -/ private def moduleDir (mod : Name) : FilePath := (moduleFile mod).withExtension "" -/-- These are not modules and should be excluded from the check everywhere. -/ -private def excludedModules : Array Name := - #[`Iris.ProofMode.Porting, `Iris.Std.DumpPortingData] - -/-- -Directories whose entry point is deliberately *not* imported by the entry point of -their parent directory, e.g. `Iris/Algebra.lean` does not import `Iris/Algebra/Lib.lean`. - -Such a directory is exempt from the check of its immediate parent only: every further -ancestor still has to reach it (`Iris.lean` imports `Iris/Algebra/Lib.lean` directly), -and its own entry point still has to cover everything below it. --/ +/-- Directories whose entry point is deliberately *not* imported by the entry point of +their parent directory, e.g. `Iris/Algebra.lean` does not import `Iris/Algebra/Lib.lean`. -/ private def detachedDirs : Array Name := #[`Iris.Algebra.Lib, `Iris.BI.Lib, `Iris.HeapLang.Lib, `Iris.Instances.Lib] -/-- Checks whether the module is excluded from the check. -/ -private def isExcluded (mod : Name) : Bool := - excludedModules.any (·.isPrefixOf mod) - -/-- Checks whether `mod` is exempt from the check performed for the entry point `entry`. -/ -private def isSkipped (entry mod : Name) : Bool := - isExcluded mod || detachedDirs.any fun dir => dir.getPrefix == entry && dir.isPrefixOf mod - -/-- -All modules whose source file lies in the directory of `root`, sorted by name. -For `root = Iris`, the file `Iris/BI/Lemmas.lean` yields the module `Iris.BI.Lemmas`. --/ -private def modulesUnder (root : Name) : IO (Array Name) := do +/-- All modules of the library, i.e. `root` and everything in its directory, sorted. -/ +private def libraryModules (root : Name) : IO (Array Name) := do let collect : StateT (Array Name) IO PUnit := forEachModuleInDir (moduleDir root) fun mod => modify (·.push (root ++ mod)) - let (_, mods) ← collect.run #[] - return mods.qsort (·.toString < ·.toString) + let ⟨_, mods⟩ ← collect.run #[] + return (mods.push root).qsort (·.toString < ·.toString) /-- The import graph of the given modules. -/ private def importGraph (modules : Array Name) : IO (Std.HashMap Name (Array Name)) := do let mut graph := ∅ for m in modules do - -- Find the direct imports of `module` let some file ← findModuleWithExt srcPath "lean" m | continue let header ← parseImports' (← IO.FS.readFile file) file.toString graph := graph.insert m (header.imports.map (·.module)) @@ -102,58 +100,107 @@ private def reachableFrom (graph : Std.HashMap Name (Array Name)) (entry : Name) frontier := frontier ++ graph.getD mod #[] return visited -/-- Every namespace with at least one module strictly below it, i.e. every directory of -the library, including `root` itself. Sorted, so that a directory precedes its children. -/ -private def directoriesUnder (root : Name) (all : Array Name) : Array Name := Id.run do +/-- Reports the modules of `missing` under the given heading. -/ +private def report (heading : String) (missing : Array Name) : IO PUnit := do + IO.eprintln heading + for mod in missing do + IO.eprintln s!" {mod}" + +/-- Every entry point must transitively import the modules of its own directory. -/ +private def checkEntryPoints (root : Name) (all : Array Name) + (graph : Std.HashMap Name (Array Name)) : IO Bool := do + -- Every namespace with at least one module strictly below it, i.e. every directory let mut dirs := #[root] let mut seen : Std.HashSet Name := (∅ : Std.HashSet Name).insert root for mod in all do - -- Add the chain of directories from the one containing `mod` up to `root` let mut dir := mod.getPrefix while root.isPrefixOf dir && !seen.contains dir do seen := seen.insert dir dirs := dirs.push dir dir := dir.getPrefix - return dirs.qsort (·.toString < ·.toString) + let mut ok := true + let mut checked := 0 + for dir in dirs.qsort (·.toString < ·.toString) do + unless (← (moduleFile dir).pathExists) do + IO.eprintln s!"check-imports: no entry-point file {moduleFile dir} \ + for directory {moduleDir dir}." + ok := false + continue + checked := checked + 1 + let reachable := reachableFrom graph dir + -- The modules that the entry point of the directory `dir` must import + let expected := all.filter fun mod => mod != dir && dir.isPrefixOf mod && + !(detachedDirs.any fun d => d.getPrefix == dir && d.isPrefixOf mod) + let missing := expected.filter (!reachable.contains ·) + unless missing.isEmpty do + report s!"check-imports: {missing.size} file(s) under {dir} are never imported \ + (directly or transitively) from {moduleFile dir}:" missing + ok := false + if ok then + IO.println s!"check-imports: all {all.size} modules of {root} are imported from the \ + entry point of their directory ({checked} entry points checked)." + return ok + +/-- + Every module must transitively import `Init`, unless `Init` depends on it. + When `minimalOnly` is `true`, only print the minimal set of modules that should import `Init`. +-/ +private def checkInit (root : Name) (all : Array Name) + (graph : Std.HashMap Name (Array Name)) (minimalOnly : Bool) : IO Bool := do + let init := root ++ `Init + -- The reversed import graph: reachability from `init` in it is the set of importers + let mut rev := ∅ + for ⟨module, imports⟩ in graph do + for i in imports do + rev := rev.insert i ((rev.getD i #[]).push module) + let importers := reachableFrom rev init + -- The modules that `init` itself depends on; these cannot import it back + let dependencies := reachableFrom graph init + let expected := all.filter (!dependencies.contains ·) + if minimalOnly then + -- The modules with no non-exempt import: importing `init` from these suffices + let minimal := expected.filter fun mod => + (graph.getD mod #[]).all fun i => dependencies.contains i || !graph.contains i + report s!"check-imports: it suffices to import `{init}` in {minimal.size} module(s):" minimal + return true + let missing := expected.filter (!importers.contains ·) + unless missing.isEmpty do + report s!"check-imports: {missing.size} module(s) of {root} never import (directly \ + or transitively) {moduleFile init}:" missing + -- Importing `init` from the modules with no non-exempt import suffices to fix this + report s!"check-imports: it suffices to add `import {init}` to:" <| + expected.filter fun mod => + (graph.getD mod #[]).all fun i => dependencies.contains i || !graph.contains i + return false + IO.println s!"check-imports: all {expected.size} modules of {root} import {init} \ + ({all.size - expected.size - 1} module(s) exempt as imports of {init})." + return true def main (args : List String) : IO UInt32 := do - match args with - | [libName] => - let root := libName.toName - -- Check the validity of the argument (top-level entry point module) - unless (← (moduleFile root).pathExists) && (← (moduleDir root).isDir) do - IO.eprintln s!"check-imports: expected an entry-point file {moduleFile root} \ - next to a directory {moduleDir root}." + let ⟨entryPoints, initModule, minimalOnly, libName?⟩ := match args with + | ["--entry-points-only", lib] => (true, false, false, some lib) + | ["--init-only", lib] => (false, true, false, some lib) + | ["--minimal-init", lib] => (false, true, true, some lib) + | [lib] => (true, true, false, some lib) + | _ => (false, false, false, none) + let some libName := libName? + | do IO.eprintln "usage: check-imports [--entry-points-only | --init-only | \ + --minimal-init] (e.g. `lake exe check-imports Iris`)" return 2 - -- Find all modules under the top-level directory - let all ← modulesUnder root - let graph ← importGraph (all.push root) - let mut ok := true - let mut checked := 0 - for dir in directoriesUnder root all do - if isExcluded dir then continue - unless (← (moduleFile dir).pathExists) do - IO.eprintln s!"check-imports: no entry-point file {moduleFile dir} \ - for directory {moduleDir dir}." - ok := false - continue - checked := checked + 1 - let reachable := reachableFrom graph dir - -- The modules of `all` that the entry point of the directory `dir` must import - let expectedUnder := all.filter - fun mod => mod != dir && dir.isPrefixOf mod && !isSkipped dir mod - let missing := expectedUnder.filter (!reachable.contains ·) - unless missing.isEmpty do - IO.eprintln s!"check-imports: {missing.size} file(s) under {dir} are never \ - imported (directly or transitively) from {moduleFile dir}:" - for mod in missing do - IO.eprintln s!" {mod}" - ok := false - if ok then - IO.println s!"check-imports: all {all.size} modules under {root} are imported \ - from the entry point of their directory ({checked} entry points checked)." - return if ok then 0 else 1 - -- Return error for invalid arguments - | _ => - IO.eprintln "usage: check-imports (e.g. `lake exe check-imports Iris`)" + let root := libName.toName + unless (← (moduleFile root).pathExists) && (← (moduleDir root).isDir) do + IO.eprintln s!"check-imports: expected an entry-point file {moduleFile root} \ + next to a directory {moduleDir root}." + return 2 + if initModule && !(← (moduleFile (root ++ `Init)).pathExists) then + IO.eprintln s!"check-imports: no initialisation file \ + {moduleFile (root ++ `Init)} for {root}." return 2 + let all ← libraryModules root + let graph ← importGraph all + let mut ok := true + if entryPoints then + ok := (← checkEntryPoints root all graph) && ok + if initModule then + ok := (← checkInit root all graph minimalOnly) && ok + return if ok then 0 else 1 diff --git a/Iris/Iris/Std/DumpPortingData.lean b/scripts/DumpPortingData.lean similarity index 99% rename from Iris/Iris/Std/DumpPortingData.lean rename to scripts/DumpPortingData.lean index 7f6749061..a54a7aee4 100644 --- a/Iris/Iris/Std/DumpPortingData.lean +++ b/scripts/DumpPortingData.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ -import Lean -import Iris.Std.RocqPorting +import Iris.Init /-! # Dump Porting Data