From 73fd66db57b46c8dce769e3094331310f31b2cb0 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 14:46:55 +0200 Subject: [PATCH 01/17] Add `Iris/Init.lean` and script checking that all modules import it --- Iris/Iris.lean | 1 + Iris/Iris/Init.lean | 3 + Iris/lakefile.toml | 5 ++ scripts/CheckInit.lean | 140 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 149 insertions(+) create mode 100644 Iris/Iris/Init.lean create mode 100644 scripts/CheckInit.lean diff --git a/Iris/Iris.lean b/Iris/Iris.lean index a98250ce6..224f4d127 100644 --- a/Iris/Iris.lean +++ b/Iris/Iris.lean @@ -7,6 +7,7 @@ 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 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/lakefile.toml b/Iris/lakefile.toml index a15eb9aa5..aa874d50c 100644 --- a/Iris/lakefile.toml +++ b/Iris/lakefile.toml @@ -28,3 +28,8 @@ supportInterpreter = true name = "check-imports" srcDir = "../scripts" root = "CheckImports" + +[[lean_exe]] +name = "check-init" +srcDir = "../scripts" +root = "CheckInit" diff --git a/scripts/CheckInit.lean b/scripts/CheckInit.lean new file mode 100644 index 000000000..c66803ff6 --- /dev/null +++ b/scripts/CheckInit.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2026 Alvin Tang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alvin Tang +-/ +import Lean.Data.Name +import Lean.Util.Path +import Lean.Elab.ParseImportsFast +import Std.Data.HashMap +import Std.Data.HashSet + +/- +This script checks 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. + +Run the script using `lake exe check-init `. For example, +`lake exe check-init Iris` checks every module under `Iris/` (and `Iris.lean` itself) +against `Iris/Init.lean`. + +Returns `0` if all modules import the initialisation module, `1` if that list is +non-empty, 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. -/ +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" + +/-- 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] + +/-- Checks whether the module is excluded from the check. -/ +private def isExcluded (mod : Name) : Bool := + excludedModules.any (·.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 + 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) + +/-- 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)) + return graph + +/-- Transitive closure of the import graph starting from `entry`. -/ +private def reachableFrom (graph : Std.HashMap Name (Array Name)) (entry : Name) : + Std.HashSet Name := Id.run do + let mut visited : Std.HashSet Name := ∅ + let mut frontier := #[entry] + while !frontier.isEmpty do + let current := frontier + frontier := #[] + for mod in current do + unless visited.contains mod do + visited := visited.insert mod + frontier := frontier ++ graph.getD mod #[] + return visited + +/-- +The reversed import graph: `m` is an edge target of each of its imports. Reachability in +this graph from a module `i` is exactly the set of modules that (transitively) import `i`. +-/ +private def reverseGraph (graph : Std.HashMap Name (Array Name)) : + Std.HashMap Name (Array Name) := Id.run do + let mut rev := ∅ + for (mod, imports) in graph do + for i in imports do + rev := rev.insert i ((rev.getD i #[]).push mod) + return rev + +def main (args : List String) : IO UInt32 := do + match args with + | [libName] => + let root := libName.toName + let init := root ++ `Init + -- Check the validity of the argument (top-level entry point module) + unless (← (moduleFile root).pathExists) && (← (moduleDir root).isDir) do + IO.eprintln s!"check-init: expected an entry-point file {moduleFile root} \ + next to a directory {moduleDir root}." + return 2 + -- Check that the initialisation module exists + unless (← (moduleFile init).pathExists) do + IO.eprintln s!"check-init: no initialisation file {moduleFile init} for {root}." + return 2 + -- Find all modules under the top-level directory, plus the top-level entry point + let all := (← modulesUnder root).push root + let graph ← importGraph all + -- The modules that reach `init` by importing it, directly or transitively + let importers := reachableFrom (reverseGraph graph) init + -- The modules that `init` itself depends on; these cannot import it back + let dependencies := reachableFrom graph init + -- The modules of the library that are subject to the check, and the ones that fail it + let expected := all.filter fun mod => + !isExcluded mod && !dependencies.contains mod + let exempt := all.filter fun mod => + !isExcluded mod && mod != init && dependencies.contains mod + let missing := expected.filter (!importers.contains ·) + unless missing.isEmpty do + IO.eprintln s!"check-init: {missing.size} module(s) of {root} never import \ + (directly or transitively) {moduleFile init}:" + for mod in missing do + IO.eprintln s!" {mod}" + return 1 + IO.println s!"check-init: all {expected.size} modules of {root} import {init} \ + ({exempt.size} module(s) exempt as imports of {init})." + return 0 + -- Return error for invalid arguments + | _ => + IO.eprintln "usage: check-init (e.g. `lake exe check-init Iris`)" + return 2 From e5626e544346af125ece94453bb7646300e51b52 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 14:56:07 +0200 Subject: [PATCH 02/17] Import `Init.lean` in all the source nodes --- Iris/Iris/BI/Notation.lean | 1 + Iris/Iris/HeapLang/Porting.lean | 2 +- Iris/Iris/Instances/Data/SetNotation.lean | 2 ++ Iris/Iris/ProofMode/Patterns/CasesPattern.lean | 1 + Iris/Iris/ProofMode/Patterns/SpecPattern.lean | 1 + Iris/Iris/Std/BigOp.lean | 2 ++ Iris/Iris/Std/BitOp.lean | 1 + Iris/Iris/Std/Classes.lean | 2 ++ Iris/Iris/Std/DelabRule.lean | 1 + Iris/Iris/Std/Equivalence.lean | 2 ++ Iris/Iris/Std/Expr.lean | 1 + Iris/Iris/Std/FromMathlib.lean | 1 + Iris/Iris/Std/Nat.lean | 2 ++ Iris/Iris/Std/Option.lean | 2 ++ Iris/Iris/Std/Prod.lean | 2 ++ Iris/Iris/Std/Qq.lean | 1 + Iris/Iris/Std/Set.lean | 2 ++ Iris/Iris/Std/TC.lean | 2 ++ Iris/Iris/Std/Tactic.lean | 1 + Iris/Iris/Std/Try.lean | 2 ++ scripts/CheckInit.lean | 7 +++++++ 21 files changed, 37 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/BI/Notation.lean b/Iris/Iris/BI/Notation.lean index 9fa07e3da..029be4f7e 100644 --- a/Iris/Iris/BI/Notation.lean +++ b/Iris/Iris/BI/Notation.lean @@ -6,6 +6,7 @@ Authors: Lars König, Alex Keizer module meta import Lean.Parser.Term +public import Iris.Init public meta section 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/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/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/SpecPattern.lean b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean index 55808beda..f82d899de 100644 --- a/Iris/Iris/ProofMode/Patterns/SpecPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean @@ -7,6 +7,7 @@ module public import Lean.Syntax public meta import Iris.Std.RocqPorting +public import Iris.Init @[expose] public section 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..67bfa7fd8 100644 --- a/Iris/Iris/Std/DelabRule.lean +++ b/Iris/Iris/Std/DelabRule.lean @@ -7,6 +7,7 @@ module public meta import Lean.PrettyPrinter.Delaborator public meta 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/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/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..8ebee4267 100644 --- a/Iris/Iris/Std/Tactic.lean +++ b/Iris/Iris/Std/Tactic.lean @@ -6,6 +6,7 @@ Authors: Lars König module public meta 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/scripts/CheckInit.lean b/scripts/CheckInit.lean index c66803ff6..215f46c4d 100644 --- a/scripts/CheckInit.lean +++ b/scripts/CheckInit.lean @@ -122,6 +122,13 @@ def main (args : List String) : IO UInt32 := do -- The modules of the library that are subject to the check, and the ones that fail it let expected := all.filter fun mod => !isExcluded mod && !dependencies.contains mod + + let minimal := expected.filter fun mod => + (graph.getD mod #[]).all fun i => dependencies.contains i || !graph.contains i + IO.eprintln s!"check-init: minimal set of modules to import {moduleFile init}:" + for m in minimal do + IO.eprintln s!" {m}" + let exempt := all.filter fun mod => !isExcluded mod && mod != init && dependencies.contains mod let missing := expected.filter (!importers.contains ·) From 3e99009b1e403f0bf0b1846afa8828ed265274d3 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 15:13:08 +0200 Subject: [PATCH 03/17] Remove `Iris.Std.RocqPorting` imports --- Iris/Iris/Algebra/Agree.lean | 1 - Iris/Iris/Algebra/Auth.lean | 1 - Iris/Iris/Algebra/BigOp.lean | 1 - Iris/Iris/Algebra/CMRA.lean | 1 - Iris/Iris/Algebra/COFESolver.lean | 1 - Iris/Iris/Algebra/Csum.lean | 1 - Iris/Iris/Algebra/DFrac.lean | 1 - Iris/Iris/Algebra/Excl.lean | 1 - Iris/Iris/Algebra/Frac.lean | 1 - Iris/Iris/Algebra/Functions.lean | 1 - Iris/Iris/Algebra/IsOp.lean | 1 - Iris/Iris/Algebra/LeibnizMultiSet.lean | 1 - Iris/Iris/Algebra/LeibnizSet.lean | 1 - Iris/Iris/Algebra/Lib/DFracAgree.lean | 1 - Iris/Iris/Algebra/Lib/ExclAuth.lean | 1 - Iris/Iris/Algebra/Lib/FracAuth.lean | 1 - Iris/Iris/Algebra/Lib/MonoZ.lean | 1 - Iris/Iris/Algebra/Lib/UFracAuth.lean | 1 - Iris/Iris/Algebra/List.lean | 1 - Iris/Iris/Algebra/LocalUpdates.lean | 1 - Iris/Iris/Algebra/Monoid.lean | 1 - Iris/Iris/Algebra/Mra.lean | 1 - Iris/Iris/Algebra/Numbers.lean | 1 - Iris/Iris/Algebra/OFE.lean | 1 - Iris/Iris/Algebra/StepIndex.lean | 1 - Iris/Iris/Algebra/UFrac.lean | 1 - Iris/Iris/Algebra/Updates.lean | 1 - Iris/Iris/Algebra/View.lean | 1 - Iris/Iris/BI/BIBase.lean | 1 - Iris/Iris/BI/BigOp/BigAndList.lean | 1 - Iris/Iris/BI/BigOp/BigAndMap.lean | 1 - Iris/Iris/BI/BigOp/BigOrList.lean | 1 - Iris/Iris/BI/BigOp/BigSepList.lean | 1 - Iris/Iris/BI/BigOp/BigSepMSet.lean | 1 - Iris/Iris/BI/BigOp/BigSepMap.lean | 1 - Iris/Iris/BI/BigOp/BigSepSet.lean | 1 - Iris/Iris/BI/Cmra.lean | 1 - Iris/Iris/BI/DerivedLaws.lean | 1 - Iris/Iris/BI/DerivedLawsLater.lean | 1 - Iris/Iris/BI/Extensions.lean | 1 - Iris/Iris/BI/SIProp.lean | 1 - Iris/Iris/BI/Sbi.lean | 1 - Iris/Iris/HeapLang/Semantics.lean | 1 - Iris/Iris/HeapLang/Syntax.lean | 1 - Iris/Iris/Instances/IProp/Instance.lean | 1 - Iris/Iris/Instances/UPred/Instance.lean | 1 - Iris/Iris/ProgramLogic/EctxLanguage.lean | 2 -- Iris/Iris/ProgramLogic/EctxiLanguage.lean | 1 - Iris/Iris/ProgramLogic/Language.lean | 1 - Iris/Iris/ProofMode/Instances.lean | 1 - Iris/Iris/ProofMode/InstancesCmra.lean | 1 - Iris/Iris/ProofMode/InstancesInternalEq.lean | 1 - Iris/Iris/ProofMode/Patterns/IntroPattern.lean | 1 - Iris/Iris/ProofMode/Patterns/SpecPattern.lean | 1 - Iris/Iris/ProofMode/Porting.lean | 3 ++- Iris/Iris/Std/DumpPortingData.lean | 2 +- Iris/Iris/Std/GenSets.lean | 1 - Iris/Iris/Std/Namespaces.lean | 1 - 58 files changed, 3 insertions(+), 59 deletions(-) diff --git a/Iris/Iris/Algebra/Agree.lean b/Iris/Iris/Algebra/Agree.lean index 4411f82c4..aa3f85df7 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..5f825b128 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -10,7 +10,6 @@ public import Iris.Std.Classes public meta import Iris.Std.DelabRule public meta 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/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/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/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/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/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/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/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/SpecPattern.lean b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean index f82d899de..62c60429c 100644 --- a/Iris/Iris/ProofMode/Patterns/SpecPattern.lean +++ b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean @@ -6,7 +6,6 @@ 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..35cc79058 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -3,7 +3,8 @@ 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 + +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/Std/DumpPortingData.lean b/Iris/Iris/Std/DumpPortingData.lean index 7f6749061..b37c0ad63 100644 --- a/Iris/Iris/Std/DumpPortingData.lean +++ b/Iris/Iris/Std/DumpPortingData.lean @@ -5,7 +5,7 @@ Authors: Zongyuan Liu -/ import Lean -import Iris.Std.RocqPorting +import Iris.Init /-! # Dump Porting Data 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 fa9ddbb8e..6c8af6df4 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 From 0bae99608d775098f3e19107440cd8e72271a8ff Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 15:23:36 +0200 Subject: [PATCH 04/17] `Iris.Std.DumpPortingData` and `Iris.ProofMode.Porting` as modules This avoids having to make exceptions regarding how code is organised --- Iris/Iris/ProofMode.lean | 2 +- Iris/Iris/ProofMode/Porting.lean | 1 + Iris/Iris/Std.lean | 2 +- Iris/Iris/Std/DumpPortingData.lean | 3 ++- 4 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/ProofMode.lean b/Iris/Iris/ProofMode.lean index 5db7e4db9..2d3e5141f 100644 --- a/Iris/Iris/ProofMode.lean +++ b/Iris/Iris/ProofMode.lean @@ -17,7 +17,7 @@ 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 diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index 35cc79058..ab7db46af 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -3,6 +3,7 @@ Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ +module import Iris.Init diff --git a/Iris/Iris/Std.lean b/Iris/Iris/Std.lean index 97fdad4ff..1cca234d1 100644 --- a/Iris/Iris/Std.lean +++ b/Iris/Iris/Std.lean @@ -5,7 +5,7 @@ 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.DumpPortingData public import Iris.Std.Equivalence public import Iris.Std.Expr public import Iris.Std.FromMathlib diff --git a/Iris/Iris/Std/DumpPortingData.lean b/Iris/Iris/Std/DumpPortingData.lean index b37c0ad63..4e716f037 100644 --- a/Iris/Iris/Std/DumpPortingData.lean +++ b/Iris/Iris/Std/DumpPortingData.lean @@ -3,9 +3,10 @@ Copyright (c) 2025. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ +module import Lean -import Iris.Init +public import Iris.Init /-! # Dump Porting Data From bbf29ce50fcda45a7c4ab488068b83ea1fa301e9 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 15:29:13 +0200 Subject: [PATCH 05/17] Simplify scripts --- scripts/CheckImports.lean | 14 +++----------- scripts/CheckInit.lean | 14 ++------------ 2 files changed, 5 insertions(+), 23 deletions(-) diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index bbb89df3b..48120081b 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -45,10 +45,6 @@ private def moduleFile (mod : Name) : FilePath := 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`. @@ -60,13 +56,9 @@ and its own entry point still has to cover everything below it. 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 + detachedDirs.any fun dir => dir.getPrefix == entry && dir.isPrefixOf mod /-- All modules whose source file lies in the directory of `root`, sorted by name. @@ -131,7 +123,6 @@ def main (args : List String) : IO UInt32 := do 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}." @@ -141,7 +132,8 @@ def main (args : List String) : IO UInt32 := do 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 + fun mod => mod != dir && dir.isPrefixOf mod && + !(detachedDirs.any fun d => d.getPrefix == dir && d.isPrefixOf mod) let missing := expectedUnder.filter (!reachable.contains ·) unless missing.isEmpty do IO.eprintln s!"check-imports: {missing.size} file(s) under {dir} are never \ diff --git a/scripts/CheckInit.lean b/scripts/CheckInit.lean index 215f46c4d..375877742 100644 --- a/scripts/CheckInit.lean +++ b/scripts/CheckInit.lean @@ -44,14 +44,6 @@ private def moduleFile (mod : Name) : FilePath := 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] - -/-- Checks whether the module is excluded from the check. -/ -private def isExcluded (mod : Name) : Bool := - excludedModules.any (·.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`. @@ -120,8 +112,7 @@ def main (args : List String) : IO UInt32 := do -- The modules that `init` itself depends on; these cannot import it back let dependencies := reachableFrom graph init -- The modules of the library that are subject to the check, and the ones that fail it - let expected := all.filter fun mod => - !isExcluded mod && !dependencies.contains mod + let expected := all.filter (!dependencies.contains ·) let minimal := expected.filter fun mod => (graph.getD mod #[]).all fun i => dependencies.contains i || !graph.contains i @@ -129,8 +120,7 @@ def main (args : List String) : IO UInt32 := do for m in minimal do IO.eprintln s!" {m}" - let exempt := all.filter fun mod => - !isExcluded mod && mod != init && dependencies.contains mod + let exempt := all.filter fun mod => mod != init && dependencies.contains mod let missing := expected.filter (!importers.contains ·) unless missing.isEmpty do IO.eprintln s!"check-init: {missing.size} module(s) of {root} never import \ From 2bae2c003e6d940efc9cf4ffa537d04f9899f948 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 16:08:38 +0200 Subject: [PATCH 06/17] Remove unnecessary imports and `meta` modifiers --- Iris/Iris/BI/BIBase.lean | 6 +- Iris/Iris/BI/Notation.lean | 2 +- Iris/Iris/HeapLang/Linter.lean | 4 +- Iris/Iris/HeapLang/Notation.lean | 2 +- Iris/Iris/ProofMode.lean | 6 +- Iris/Iris/ProofMode/Classes.lean | 2 - Iris/Iris/ProofMode/ClassesMake.lean | 1 - Iris/Iris/ProofMode/Display.lean | 4 +- Iris/Iris/ProofMode/Expr.lean | 1 - Iris/Iris/ProofMode/InstancesFrame.lean | 3 +- Iris/Iris/ProofMode/NatCancel.lean | 2 +- Iris/Iris/ProofMode/Patterns/SelPattern.lean | 2 +- Iris/Iris/ProofMode/ProofModeM.lean | 1 + Iris/Iris/ProofMode/Tactics.lean | 58 ++++++++++---------- Iris/Iris/ProofMode/Tactics/Accu.lean | 2 +- Iris/Iris/ProofMode/Tactics/Apply.lean | 7 +-- Iris/Iris/ProofMode/Tactics/Assumption.lean | 3 +- Iris/Iris/ProofMode/Tactics/Basic.lean | 8 +-- Iris/Iris/ProofMode/Tactics/Cases.lean | 14 ++--- Iris/Iris/ProofMode/Tactics/Clear.lean | 2 - Iris/Iris/ProofMode/Tactics/Combine.lean | 6 +- Iris/Iris/ProofMode/Tactics/Eval.lean | 1 - Iris/Iris/ProofMode/Tactics/ExFalso.lean | 3 +- Iris/Iris/ProofMode/Tactics/Exact.lean | 2 +- Iris/Iris/ProofMode/Tactics/Exists.lean | 6 +- Iris/Iris/ProofMode/Tactics/Frame.lean | 1 - Iris/Iris/ProofMode/Tactics/Have.lean | 2 - Iris/Iris/ProofMode/Tactics/HaveCore.lean | 1 - Iris/Iris/ProofMode/Tactics/Induction.lean | 9 +-- Iris/Iris/ProofMode/Tactics/Intro.lean | 8 +-- Iris/Iris/ProofMode/Tactics/Inv.lean | 8 +-- Iris/Iris/ProofMode/Tactics/LeftRight.lean | 2 +- Iris/Iris/ProofMode/Tactics/Mod.lean | 2 +- Iris/Iris/ProofMode/Tactics/Pure.lean | 2 +- Iris/Iris/ProofMode/Tactics/Rename.lean | 2 +- Iris/Iris/ProofMode/Tactics/Revert.lean | 5 -- Iris/Iris/ProofMode/Tactics/Rewrite.lean | 8 +-- Iris/Iris/ProofMode/Tactics/Specialize.lean | 3 +- Iris/Iris/ProofMode/Tactics/Split.lean | 2 +- Iris/Iris/ProofMode/Tactics/Trivial.lean | 2 +- Iris/Iris/Std/DelabRule.lean | 4 +- Iris/Iris/Std/Rewrite.lean | 2 +- Iris/Iris/Std/Tactic.lean | 2 +- 43 files changed, 84 insertions(+), 129 deletions(-) diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean index 5f825b128..d685fc76c 100644 --- a/Iris/Iris/BI/BIBase.lean +++ b/Iris/Iris/BI/BIBase.lean @@ -5,10 +5,10 @@ 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 @[expose] public section diff --git a/Iris/Iris/BI/Notation.lean b/Iris/Iris/BI/Notation.lean index 029be4f7e..8f3483e89 100644 --- a/Iris/Iris/BI/Notation.lean +++ b/Iris/Iris/BI/Notation.lean @@ -5,7 +5,7 @@ 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/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/ProofMode.lean b/Iris/Iris/ProofMode.lean index 2d3e5141f..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 @@ -21,5 +21,5 @@ 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/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/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/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/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/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 7a946a437..0e73e3c40 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/DelabRule.lean b/Iris/Iris/Std/DelabRule.lean index 67bfa7fd8..1ba209a33 100644 --- a/Iris/Iris/Std/DelabRule.lean +++ b/Iris/Iris/Std/DelabRule.lean @@ -5,8 +5,8 @@ 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/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/Tactic.lean b/Iris/Iris/Std/Tactic.lean index 8ebee4267..4a07b8fcc 100644 --- a/Iris/Iris/Std/Tactic.lean +++ b/Iris/Iris/Std/Tactic.lean @@ -5,7 +5,7 @@ Authors: Lars König -/ module -public meta import Lean.Elab.Tactic +public import Lean.Elab.Tactic public import Iris.Init public meta section From cb9a0e2b7b94c1f4f2bb569a750378e24c6dd344 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 16:34:07 +0200 Subject: [PATCH 07/17] Move `Iris/Tests` to `IrisTest`, `IrisMath/Tests` to `IrisMathTest` --- Iris/Iris.lean | 1 - Iris/Iris/Tests.lean | 11 --- Iris/Iris/Tests/HeapLang.lean | 9 --- Iris/IrisTest.lean | 12 ++++ Iris/{Iris/Tests => IrisTest}/Display.lean | 5 +- Iris/IrisTest/HeapLang.lean | 9 +++ .../HeapLang/HeapTactics.lean | 0 .../Tests => IrisTest}/HeapLang/Linter.lean | 4 +- .../Tests => IrisTest}/HeapLang/Notation.lean | 6 +- .../Tests => IrisTest}/HeapLang/Par.lean | 6 +- .../Tests => IrisTest}/HeapLang/Tactics.lean | 0 .../HeapLang/WeakestPre.lean | 0 Iris/{Iris/Tests => IrisTest}/Instances.lean | 72 +++++++++---------- .../Tests => IrisTest}/InstancesImport.lean | 6 +- Iris/{Iris/Tests => IrisTest}/Language.lean | 2 +- Iris/{Iris/Tests => IrisTest}/Notation.lean | 6 +- Iris/{Iris/Tests => IrisTest}/Tactics.lean | 4 +- Iris/{Iris/Tests => IrisTest}/Updates.lean | 0 Iris/{Iris/Tests => IrisTest}/WeakestPre.lean | 3 +- Iris/lakefile.toml | 1 - IrisMath/IrisMath.lean | 1 - IrisMath/IrisMath/Tests.lean | 3 - IrisMath/IrisMathTest.lean | 4 ++ .../Tests => IrisMathTest}/Numbers.lean | 0 IrisMath/lakefile.toml | 5 +- 25 files changed, 84 insertions(+), 86 deletions(-) delete mode 100644 Iris/Iris/Tests.lean delete mode 100644 Iris/Iris/Tests/HeapLang.lean create mode 100644 Iris/IrisTest.lean rename Iris/{Iris/Tests => IrisTest}/Display.lean (99%) create mode 100644 Iris/IrisTest/HeapLang.lean rename Iris/{Iris/Tests => IrisTest}/HeapLang/HeapTactics.lean (100%) rename Iris/{Iris/Tests => IrisTest}/HeapLang/Linter.lean (97%) rename Iris/{Iris/Tests => IrisTest}/HeapLang/Notation.lean (99%) rename Iris/{Iris/Tests => IrisTest}/HeapLang/Par.lean (92%) rename Iris/{Iris/Tests => IrisTest}/HeapLang/Tactics.lean (100%) rename Iris/{Iris/Tests => IrisTest}/HeapLang/WeakestPre.lean (100%) rename Iris/{Iris/Tests => IrisTest}/Instances.lean (80%) rename Iris/{Iris/Tests => IrisTest}/InstancesImport.lean (91%) rename Iris/{Iris/Tests => IrisTest}/Language.lean (98%) rename Iris/{Iris/Tests => IrisTest}/Notation.lean (99%) rename Iris/{Iris/Tests => IrisTest}/Tactics.lean (99%) rename Iris/{Iris/Tests => IrisTest}/Updates.lean (100%) rename Iris/{Iris/Tests => IrisTest}/WeakestPre.lean (99%) delete mode 100644 IrisMath/IrisMath/Tests.lean create mode 100644 IrisMath/IrisMathTest.lean rename IrisMath/{IrisMath/Tests => IrisMathTest}/Numbers.lean (100%) diff --git a/Iris/Iris.lean b/Iris/Iris.lean index 224f4d127..6b9e75948 100644 --- a/Iris/Iris.lean +++ b/Iris/Iris.lean @@ -13,4 +13,3 @@ 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/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/IrisTest.lean b/Iris/IrisTest.lean new file mode 100644 index 000000000..53efce6a5 --- /dev/null +++ b/Iris/IrisTest.lean @@ -0,0 +1,12 @@ +module + +public import Iris +public import IrisTest.Display +public import IrisTest.HeapLang +public import IrisTest.Instances +public import IrisTest.InstancesImport +public import IrisTest.Language +public import IrisTest.Notation +public import IrisTest.Tactics +public import IrisTest.Updates +public import IrisTest.WeakestPre 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 b234f7ab8..9652fb369 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 aa874d50c..a4375c545 100644 --- a/Iris/lakefile.toml +++ b/Iris/lakefile.toml @@ -16,7 +16,6 @@ name = "Iris" [[lean_lib]] name = "IrisTest" -globs = ["Iris.*"] [[lean_exe]] name = "dumpPortingData" 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/IrisMathTest.lean b/IrisMath/IrisMathTest.lean new file mode 100644 index 000000000..2c232124c --- /dev/null +++ b/IrisMath/IrisMathTest.lean @@ -0,0 +1,4 @@ +module + +public import IrisMath +public import IrisMathTest.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..a131f6bb4 100644 --- a/IrisMath/lakefile.toml +++ b/IrisMath/lakefile.toml @@ -1,7 +1,7 @@ name = "irismath" version = "0.1.0" keywords = ["math"] -defaultTargets = ["IrisMath"] +defaultTargets = ["IrisMath", "IrisMathTest"] [leanOptions] pp.unicode.fun = true @@ -22,6 +22,9 @@ path = "../Iris/" [[lean_lib]] name = "IrisMath" +[[lean_lib]] +name = "IrisMathTest" + [[lean_exe]] name = "check-imports" srcDir = "../scripts" From 04d42bd30e27a40b2f26e3532dd663306828be4d Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 17:36:30 +0200 Subject: [PATCH 08/17] Combine two scripts into one --- scripts/CheckImports.lean | 180 ++++++++++++++++++++++++-------------- scripts/CheckInit.lean | 137 ----------------------------- 2 files changed, 113 insertions(+), 204 deletions(-) delete mode 100644 scripts/CheckInit.lean diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index 48120081b..ed89c9618 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,11 +23,27 @@ 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). -/ @@ -45,36 +65,22 @@ private def moduleFile (mod : Name) : FilePath := private def moduleDir (mod : Name) : FilePath := (moduleFile mod).withExtension "" -/-- -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 `mod` is exempt from the check performed for the entry point `entry`. -/ -private def isSkipped (entry mod : Name) : Bool := - 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) + 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)) @@ -94,58 +100,98 @@ 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. -/ +private def checkInit (root : Name) (all : Array Name) + (graph : Std.HashMap Name (Array Name)) : 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 ·) + 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, libName?) := match args with + | ["--entry-points-only", lib] => (true, false, some lib) + | ["--init-only", lib] => (false, true, some lib) + | [lib] => (true, true, some lib) + | _ => (false, false, none) + let some libName := libName? + | do + IO.eprintln "usage: check-imports [--entry-points-only | --init-only] \ + (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 - 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 && - !(detachedDirs.any fun d => d.getPrefix == dir && d.isPrefixOf 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) && ok + return if ok then 0 else 1 diff --git a/scripts/CheckInit.lean b/scripts/CheckInit.lean deleted file mode 100644 index 375877742..000000000 --- a/scripts/CheckInit.lean +++ /dev/null @@ -1,137 +0,0 @@ -/- -Copyright (c) 2026 Alvin Tang. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alvin Tang --/ -import Lean.Data.Name -import Lean.Util.Path -import Lean.Elab.ParseImportsFast -import Std.Data.HashMap -import Std.Data.HashSet - -/- -This script checks 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. - -Run the script using `lake exe check-init `. For example, -`lake exe check-init Iris` checks every module under `Iris/` (and `Iris.lean` itself) -against `Iris/Init.lean`. - -Returns `0` if all modules import the initialisation module, `1` if that list is -non-empty, 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. -/ -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" - -/-- The directory holding the submodules of a module, e.g. `Iris.BI` to `./Iris/BI`. -/ -private def moduleDir (mod : Name) : FilePath := - (moduleFile mod).withExtension "" - -/-- -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 - 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) - -/-- 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)) - return graph - -/-- Transitive closure of the import graph starting from `entry`. -/ -private def reachableFrom (graph : Std.HashMap Name (Array Name)) (entry : Name) : - Std.HashSet Name := Id.run do - let mut visited : Std.HashSet Name := ∅ - let mut frontier := #[entry] - while !frontier.isEmpty do - let current := frontier - frontier := #[] - for mod in current do - unless visited.contains mod do - visited := visited.insert mod - frontier := frontier ++ graph.getD mod #[] - return visited - -/-- -The reversed import graph: `m` is an edge target of each of its imports. Reachability in -this graph from a module `i` is exactly the set of modules that (transitively) import `i`. --/ -private def reverseGraph (graph : Std.HashMap Name (Array Name)) : - Std.HashMap Name (Array Name) := Id.run do - let mut rev := ∅ - for (mod, imports) in graph do - for i in imports do - rev := rev.insert i ((rev.getD i #[]).push mod) - return rev - -def main (args : List String) : IO UInt32 := do - match args with - | [libName] => - let root := libName.toName - let init := root ++ `Init - -- Check the validity of the argument (top-level entry point module) - unless (← (moduleFile root).pathExists) && (← (moduleDir root).isDir) do - IO.eprintln s!"check-init: expected an entry-point file {moduleFile root} \ - next to a directory {moduleDir root}." - return 2 - -- Check that the initialisation module exists - unless (← (moduleFile init).pathExists) do - IO.eprintln s!"check-init: no initialisation file {moduleFile init} for {root}." - return 2 - -- Find all modules under the top-level directory, plus the top-level entry point - let all := (← modulesUnder root).push root - let graph ← importGraph all - -- The modules that reach `init` by importing it, directly or transitively - let importers := reachableFrom (reverseGraph graph) init - -- The modules that `init` itself depends on; these cannot import it back - let dependencies := reachableFrom graph init - -- The modules of the library that are subject to the check, and the ones that fail it - let expected := all.filter (!dependencies.contains ·) - - let minimal := expected.filter fun mod => - (graph.getD mod #[]).all fun i => dependencies.contains i || !graph.contains i - IO.eprintln s!"check-init: minimal set of modules to import {moduleFile init}:" - for m in minimal do - IO.eprintln s!" {m}" - - let exempt := all.filter fun mod => mod != init && dependencies.contains mod - let missing := expected.filter (!importers.contains ·) - unless missing.isEmpty do - IO.eprintln s!"check-init: {missing.size} module(s) of {root} never import \ - (directly or transitively) {moduleFile init}:" - for mod in missing do - IO.eprintln s!" {mod}" - return 1 - IO.println s!"check-init: all {expected.size} modules of {root} import {init} \ - ({exempt.size} module(s) exempt as imports of {init})." - return 0 - -- Return error for invalid arguments - | _ => - IO.eprintln "usage: check-init (e.g. `lake exe check-init Iris`)" - return 2 From 6c7771e944e9af3c52aa16c80ca232716fdb0712 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 17:37:30 +0200 Subject: [PATCH 09/17] Update the CI scripts and `lakefile.toml` for the refactoring --- .github/workflows/build.yml | 4 +++- Iris/IrisTest.lean | 12 ------------ Iris/lakefile.toml | 9 +++------ IrisMath/IrisMathTest.lean | 4 ---- IrisMath/lakefile.toml | 4 +++- 5 files changed, 9 insertions(+), 24 deletions(-) delete mode 100644 Iris/IrisTest.lean delete mode 100644 IrisMath/IrisMathTest.lean diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index fc081e0b8..c2c633b2b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -22,6 +22,7 @@ jobs: with: lake-package-directory: Iris build-args: "--wfail" + test: true - name: Check that all modules are imported by Iris.lean and other entry-point modules working-directory: Iris run: lake exe check-imports Iris @@ -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/IrisTest.lean b/Iris/IrisTest.lean deleted file mode 100644 index 53efce6a5..000000000 --- a/Iris/IrisTest.lean +++ /dev/null @@ -1,12 +0,0 @@ -module - -public import Iris -public import IrisTest.Display -public import IrisTest.HeapLang -public import IrisTest.Instances -public import IrisTest.InstancesImport -public import IrisTest.Language -public import IrisTest.Notation -public import IrisTest.Tactics -public import IrisTest.Updates -public import IrisTest.WeakestPre diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml index a4375c545..ed301d259 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,6 +17,7 @@ name = "Iris" [[lean_lib]] name = "IrisTest" +globs = ["IrisTest.+"] [[lean_exe]] name = "dumpPortingData" @@ -27,8 +29,3 @@ supportInterpreter = true name = "check-imports" srcDir = "../scripts" root = "CheckImports" - -[[lean_exe]] -name = "check-init" -srcDir = "../scripts" -root = "CheckInit" diff --git a/IrisMath/IrisMathTest.lean b/IrisMath/IrisMathTest.lean deleted file mode 100644 index 2c232124c..000000000 --- a/IrisMath/IrisMathTest.lean +++ /dev/null @@ -1,4 +0,0 @@ -module - -public import IrisMath -public import IrisMathTest.Numbers diff --git a/IrisMath/lakefile.toml b/IrisMath/lakefile.toml index a131f6bb4..991bdedbd 100644 --- a/IrisMath/lakefile.toml +++ b/IrisMath/lakefile.toml @@ -1,7 +1,8 @@ name = "irismath" version = "0.1.0" keywords = ["math"] -defaultTargets = ["IrisMath", "IrisMathTest"] +defaultTargets = ["IrisMath"] +testDriver = "IrisMathTest" [leanOptions] pp.unicode.fun = true @@ -24,6 +25,7 @@ name = "IrisMath" [[lean_lib]] name = "IrisMathTest" +globs = ["IrisMathTest.+"] [[lean_exe]] name = "check-imports" From 055a536bc06fb1ae5b3faa232a5809679ef26984 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 17:45:23 +0200 Subject: [PATCH 10/17] Extend `CheckImports.lean` for finding the minimal set of modules for importing `Init.lean` --- scripts/CheckImports.lean | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index ed89c9618..5965ce3ba 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -141,9 +141,12 @@ private def checkEntryPoints (root : Name) (all : Array Name) entry point of their directory ({checked} entry points checked)." return ok -/-- Every module must transitively import `Init`, unless `Init` depends on it. -/ +/-- + 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)) : IO Bool := do + (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 := ∅ @@ -154,6 +157,12 @@ private def checkInit (root : Name) (all : Array Name) -- 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 \ @@ -168,15 +177,16 @@ private def checkInit (root : Name) (all : Array Name) return true def main (args : List String) : IO UInt32 := do - let (entryPoints, initModule, libName?) := match args with - | ["--entry-points-only", lib] => (true, false, some lib) - | ["--init-only", lib] => (false, true, some lib) - | [lib] => (true, true, some lib) - | _ => (false, false, none) + 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] \ - (e.g. `lake exe check-imports Iris`)" + IO.eprintln "usage: check-imports [--entry-points-only | --init-only | \ + --minimal-init] (e.g. `lake exe check-imports Iris`)" return 2 let root := libName.toName unless (← (moduleFile root).pathExists) && (← (moduleDir root).isDir) do @@ -193,5 +203,5 @@ def main (args : List String) : IO UInt32 := do if entryPoints then ok := (← checkEntryPoints root all graph) && ok if initModule then - ok := (← checkInit root all graph) && ok + ok := (← checkInit root all graph minimalOnly) && ok return if ok then 0 else 1 From 4090f72636914ad37c2cc5cffed5d4cc08dcafe6 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 18:14:17 +0200 Subject: [PATCH 11/17] Replace `import Lean` with smaller imports --- Iris/Iris/BI/BigOp/BigOp.lean | 1 - Iris/Iris/HeapLang/ProofMode.lean | 4 +--- Iris/Iris/HeapLang/Tactic.lean | 7 ------- Iris/Iris/ProofMode/SynthInstance.lean | 1 - Iris/Iris/Std/DumpPortingData.lean | 1 - Iris/Iris/Std/RocqPorting.lean | 4 ++-- Iris/Iris/Std/Tactic.lean | 1 + 7 files changed, 4 insertions(+), 15 deletions(-) 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/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/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/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/Std/DumpPortingData.lean b/Iris/Iris/Std/DumpPortingData.lean index 4e716f037..9fd59af46 100644 --- a/Iris/Iris/Std/DumpPortingData.lean +++ b/Iris/Iris/Std/DumpPortingData.lean @@ -5,7 +5,6 @@ Authors: Zongyuan Liu -/ module -import Lean public import Iris.Init /-! 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/Tactic.lean b/Iris/Iris/Std/Tactic.lean index 4a07b8fcc..255b1b242 100644 --- a/Iris/Iris/Std/Tactic.lean +++ b/Iris/Iris/Std/Tactic.lean @@ -5,6 +5,7 @@ Authors: Lars König -/ module +meta import Lean.Elab.Tactic.ElabTerm public import Lean.Elab.Tactic public import Iris.Init From 04d7a5ccb0a5e39e91927d8104cf2803bbdfed7e Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 19:52:37 +0200 Subject: [PATCH 12/17] Update CI task description --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index c2c633b2b..7cae754df 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -23,7 +23,7 @@ jobs: lake-package-directory: Iris build-args: "--wfail" test: true - - name: Check that all modules are imported by Iris.lean and other entry-point modules + - 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 From 5efc510808f472ea34737c5254db76acf91449bd Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 19:58:29 +0200 Subject: [PATCH 13/17] Revert `module` for `Iris.ProofMode.Porting` and `Iris.Std.DumpPortingData.lean` CI fails with them as modules --- Iris/Iris/ProofMode/Porting.lean | 1 - Iris/Iris/Std/DumpPortingData.lean | 3 +-- scripts/CheckImports.lean | 9 ++++++++- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index ab7db46af..35cc79058 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -3,7 +3,6 @@ Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ -module import Iris.Init diff --git a/Iris/Iris/Std/DumpPortingData.lean b/Iris/Iris/Std/DumpPortingData.lean index 9fd59af46..a54a7aee4 100644 --- a/Iris/Iris/Std/DumpPortingData.lean +++ b/Iris/Iris/Std/DumpPortingData.lean @@ -3,9 +3,8 @@ Copyright (c) 2025. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ -module -public import Iris.Init +import Iris.Init /-! # Dump Porting Data diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index 5965ce3ba..f1b3f157f 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -70,6 +70,12 @@ their parent directory, e.g. `Iris/Algebra.lean` does not import `Iris/Algebra/L private def detachedDirs : Array Name := #[`Iris.Algebra.Lib, `Iris.BI.Lib, `Iris.HeapLang.Lib, `Iris.Instances.Lib] +/-- Modules that are deliberately not imported by the entry point of their directory, +e.g. `Iris/Std/DumpPortingData.lean` is the root of an executable rather than a part of +the library proper. -/ +private def detachedModules : Array Name := + #[`Iris.Std.DumpPortingData, `Iris.Foo.Bar] + /-- 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 := @@ -130,7 +136,8 @@ private def checkEntryPoints (root : Name) (all : Array Name) 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) + !(detachedDirs.any fun d => d.getPrefix == dir && d.isPrefixOf mod) && + !detachedModules.contains mod let missing := expected.filter (!reachable.contains ·) unless missing.isEmpty do report s!"check-imports: {missing.size} file(s) under {dir} are never imported \ From 796f38f7dc99bd10acb8ad5807c15c895d85aa40 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 20:03:16 +0200 Subject: [PATCH 14/17] Remove outdated imports --- Iris/Iris/ProofMode.lean | 1 - Iris/Iris/Std.lean | 1 - 2 files changed, 2 deletions(-) diff --git a/Iris/Iris/ProofMode.lean b/Iris/Iris/ProofMode.lean index daa583508..254800062 100644 --- a/Iris/Iris/ProofMode.lean +++ b/Iris/Iris/ProofMode.lean @@ -17,7 +17,6 @@ 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.ProofModeM public import Iris.ProofMode.SynthInstance public import Iris.ProofMode.SynthInstanceAttr diff --git a/Iris/Iris/Std.lean b/Iris/Iris/Std.lean index 1cca234d1..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 From 766f5790a5f2435e8bae87e306b4e79f7bd0c564 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 20:04:49 +0200 Subject: [PATCH 15/17] Retry CI --- scripts/CheckImports.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index f1b3f157f..2d48aecc5 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -70,9 +70,11 @@ their parent directory, e.g. `Iris/Algebra.lean` does not import `Iris/Algebra/L private def detachedDirs : Array Name := #[`Iris.Algebra.Lib, `Iris.BI.Lib, `Iris.HeapLang.Lib, `Iris.Instances.Lib] -/-- Modules that are deliberately not imported by the entry point of their directory, +/-- +Modules that are deliberately not imported by the entry point of their directory, e.g. `Iris/Std/DumpPortingData.lean` is the root of an executable rather than a part of -the library proper. -/ +the library proper. +-/ private def detachedModules : Array Name := #[`Iris.Std.DumpPortingData, `Iris.Foo.Bar] From 05e20f1df61951087ce22c17fae200e2e55d5516 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 20:42:27 +0200 Subject: [PATCH 16/17] Minor fixes --- scripts/CheckImports.lean | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index 2d48aecc5..21a5c4e80 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -50,16 +50,16 @@ Returns `0` if all checks pass, `1` if any of the checks fails, or 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 := @@ -76,13 +76,13 @@ e.g. `Iris/Std/DumpPortingData.lean` is the root of an executable rather than a the library proper. -/ private def detachedModules : Array Name := - #[`Iris.Std.DumpPortingData, `Iris.Foo.Bar] + #[`Iris.Std.DumpPortingData, `Iris.ProofMode.Porting] /-- 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 #[] + let ⟨_, mods⟩ ← collect.run #[] return (mods.push root).qsort (·.toString < ·.toString) /-- The import graph of the given modules. -/ @@ -186,15 +186,14 @@ private def checkInit (root : Name) (all : Array Name) return true def main (args : List String) : IO UInt32 := do - let (entryPoints, initModule, minimalOnly, libName?) := match args with + 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 | \ + | do IO.eprintln "usage: check-imports [--entry-points-only | --init-only | \ --minimal-init] (e.g. `lake exe check-imports Iris`)" return 2 let root := libName.toName From 8deb226c1402a929f0f6e419972872caa2a7611e Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Wed, 12 Aug 2026 22:39:47 +0200 Subject: [PATCH 17/17] Move `Std/DumpPortingData.lean` to `scripts/` No exception for `Iris/ProofMode/Porting.lean` --- Iris/Iris/ProofMode.lean | 1 + Iris/Iris/ProofMode/Porting.lean | 1 + Iris/lakefile.toml | 2 +- scripts/CheckImports.lean | 11 +---------- {Iris/Iris/Std => scripts}/DumpPortingData.lean | 0 5 files changed, 4 insertions(+), 11 deletions(-) rename {Iris/Iris/Std => scripts}/DumpPortingData.lean (100%) diff --git a/Iris/Iris/ProofMode.lean b/Iris/Iris/ProofMode.lean index 254800062..daa583508 100644 --- a/Iris/Iris/ProofMode.lean +++ b/Iris/Iris/ProofMode.lean @@ -17,6 +17,7 @@ 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.ProofModeM public import Iris.ProofMode.SynthInstance public import Iris.ProofMode.SynthInstanceAttr diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index 35cc79058..ab7db46af 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -3,6 +3,7 @@ Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu -/ +module import Iris.Init diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml index ed301d259..b3d4614f7 100644 --- a/Iris/lakefile.toml +++ b/Iris/lakefile.toml @@ -21,7 +21,7 @@ globs = ["IrisTest.+"] [[lean_exe]] name = "dumpPortingData" -srcDir = "Iris/Std" +srcDir = "../scripts" root = "DumpPortingData" supportInterpreter = true diff --git a/scripts/CheckImports.lean b/scripts/CheckImports.lean index 21a5c4e80..285702092 100644 --- a/scripts/CheckImports.lean +++ b/scripts/CheckImports.lean @@ -70,14 +70,6 @@ their parent directory, e.g. `Iris/Algebra.lean` does not import `Iris/Algebra/L private def detachedDirs : Array Name := #[`Iris.Algebra.Lib, `Iris.BI.Lib, `Iris.HeapLang.Lib, `Iris.Instances.Lib] -/-- -Modules that are deliberately not imported by the entry point of their directory, -e.g. `Iris/Std/DumpPortingData.lean` is the root of an executable rather than a part of -the library proper. --/ -private def detachedModules : Array Name := - #[`Iris.Std.DumpPortingData, `Iris.ProofMode.Porting] - /-- 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 := @@ -138,8 +130,7 @@ private def checkEntryPoints (root : Name) (all : Array Name) 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) && - !detachedModules.contains 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 \ diff --git a/Iris/Iris/Std/DumpPortingData.lean b/scripts/DumpPortingData.lean similarity index 100% rename from Iris/Iris/Std/DumpPortingData.lean rename to scripts/DumpPortingData.lean