chore: Init.lean and some related refactoring

[alvinylt]

Description

Several sets of changes to align with conventions in Lean, Mathlib and Iris-Rocq, as well as to prepare for the linter setup.

Init.lean as the Initial Module

A follow-up on #552 (comment).

Similar to Init.lean in Mathlib, this module is imported by all modules within the project (except by the modules listed in Init.lean, obviously). Mathlib's documentation for Init.lean explains how it is used. In particular, linter modules can be imported here to enable them throughout the project in the future.

As our plan is to adopt linting gradually (see #445 (comment)), Init.lean along with the recent overhaul of linter configurations in Lean 4.32 makes the setup a lot easier. I have been doing some experiments with the linters in a separate branch, and it seems to be the case that we can simply toggle some options to choose what built-in/Batteries linters to use. The code style linters are trickier as they are located within Mathlib. We can perhaps consider porting some of those linter modules into Iris/Std if needed.

Besides linting setup, the immediate benefit of having Init.lean is that we are now able to remove imports of Iris.Std.RocqPorting scattered around in the project. Some 50+ unnecessary imports are removed as a result.

Commits: 73fd66d, e5626e5, 3e99009

Extending the Script for Init.lean

A follow-up on #589.

The script is now able to check two requirements:

• Check that Iris.lean imports all modules (existing feature).
• Check that all modules import Init.lean (new feature in this PR).

There are now several valid ways to use the script:

lake exe check-imports Iris  # Performs both checks
lake exe check-imports --entry-points-only Iris  # Performs the first check only
lake exe check-imports --init-only Iris  # Performs the second check only
lake exe check-imports --minimal-init Iris  # Return the minimal set of modules that should import Init.lean
lake exe check-imports --entry-points-only IrisMath  # Performs the first check for IrisMath

With the option --minimal-init, one immediately gets a list of modules that would satisfy the check.

The CI script is updated to run lake exe check-imports Iris and lake exe check-imports --entry-points-only IrisMath.

In case there is a need for the same feature but only for a submodule, then one can create Init.lean under the subdirectory (e.g. Iris/Algebra/Init.lean), and the script run (e.g. lake exe check-imports Iris.Algebra) works exactly the same.

@lzy0505 I'm making Iris/ProofMode/Porting.lean and Iris/Std/DumpPortingData.lean modules so that the script does not have to make exceptions for them. Is this change reasonable? The CI run fails with the latter being a module of Iris. However, it works if we move DumpPortingData.lean to scripts/, alongside CheckImports.lean.

Commits: 73fd66d, 0bae996, bbf29ce, 04d42bd, 055a536

Moving Test Directories and Test Driver Setup

Currently the tests are located under the directories Iris/Iris/Tests/ and Iris/IrisMath/Tests/, with the tests built as part of the Iris module and under the Iris namespace.

My suggestion is to relocate them to Iris/IrisTest/ and Iris/IrisMathTest/. This aligns with how the code in Iris-Rocq and Mathlib are organised.

• In Iris-Rocq, the core modules are located under iris/iris/ (e.g. iris/iris/algebra, iris/iris/bi) while tests are located under iris/tests.
• Mathlib and MathlibTest are both top-level directories in the Mathlib repository.

As a side note, the existing lakefile.toml already has the following setup (even though IrisTest does not exist as a directory).

defaultTargets = ["Iris", "IrisTest"]

For some reason, lake build does not throw any error, which is why we have never been aware of the issue so far. However, other tools such as lake shake complains about the missing directory.

Upon relocating the tests, my suggestion is to update lakefile.toml with the following:

defaultTargets = ["Iris"]
testDriver = "IrisTest"

Then, lake build builds the core Iris modules under Iris/, while lake test runs the tests under IrisTest/ (after building Iris, if not up-to-date). Same as in Mathlib.

The CI specifically has the infrastructure for tests:

- uses: leanprover/lean-action@v1
  with:
    lake-package-directory: Iris
    build-args: "--wfail"
    test: true                     # Run tests

Commits: cb9a0e2, 6c7771e

Remove Unnecessary Imports

lake shake offers some useful suggestions, but it is not desirable to apply all of them directly. So I've manually gone through some suggestions and removed plenty of unnecessary imports. In particular, there are lots of redundant meta import declarations (some of those modules do not involve metaprogramming at all).

Commits: 2bae2c0, 4090f72

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[alvinylt]

For reference, I tried enabling linter.all, linter.extra and weak.linter.style globally as an experiment. Here is a count of warnings:

Occurrences	Linter option
1943	linter.missingDocs
429	linter.style.longLine
146	linter.style.lambdaSyntax
101	linter.style.missingEnd
89	linter.style.show
85	linter.style.dollarSyntax
55	linter.extra.unusedDecidableInType
36	linter.omit
34	linter.extra.dupNamespace
30	linter.extra.unnecessarySeqFocus
14	linter.redundantVisibility
14	linter.extra.unreachableTactic
6	linter.style.cdot
6	linter.loopingSimpArgs
2	linter.style.openClassical

So here's my idea: instead of gradually adopting the linter by tweaking it to ignore some modules, we can perhaps create an issue listing the linter options we’d like to enable. This way we avoid having to deal with complicated module dependencies, and we don't have decide what linter features to adopt all at once.

[MackieLoeffel]

This looks good to me. I also like the idea of enabling the linters one at a time. @markusdemedeiros @lzy0505 Do you have thoughts on this PR?