Module setup recommendations for a multi-package repository

Stream: new members

[pandaman]

Hi! I’m considering adopting the module system for lean-regex, but the setup is a bit unusual, so I’d appreciate some advice.

The repository currently contains multiple Lake packages:

• regex: the main implementation, with no dependencies
• correctness: depends on regex and Mathlib, and proves theorems about the implementation
• (docbuild also exists for documentation, but it’s not relevant here)

My main constraints are:

• I don’t want regex to depend on Mathlib. Lean projects that use it purely as a programming language shouldn’t need Mathlib just to use regex. Ideally, it should even be possible for Mathlib to depend on lean-regex (e.g. for linters).
• The correctness package is expected to rely on the exact implementation details of regex. Breakages are acceptable, since I can update both packages in a single PR.

Given this setup, it seems that I would effectively need to expose all definitions from regex. If that’s the case, is there still a benefit to adopting the module system?

An alternative I’m considering is moving equalities that characterizes regex definitions into regex instead of correctness (example). I'm curious if it's a clearer design.

I'd appreciate any suggestions or experience with similar setups. Thanks!

[Robin Arnez]

You can also not expose the definitions but use import all in correctness. This used to be disallowed but it should be possible now.

[pandaman]

Just to confirm, are you suggesting allowImportAll?
https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#Lake___PackageConfig-allowImportAll

[Robin Arnez]

I don't think you need anything, see lean4#12045; unless I missed a more recent change?

[pandaman]

Nice!

Progress: I started the porting but I cannot access String.singleton_append_inj in v4.28.0 for some reason. v4.29.0-rc2 seems fine, so it might be that I just need to wait for a few days.

module -- comment out to make the following pass
#check String.singleton_append_inj

#eval Lean.versionString

[Robin Arnez]

You can also public import Init.Data.String.Lemmas.Basic in the meanwhile but yeah, it seems like the orphaned modules checker doesn't account for the module system