Modulizing batteries

Stream: batteries

[Sebastian Ullrich]

As an early heads-up, I would soon like to start with porting batteries to the module system (I am open to help of course but also prepared to do it myself). The PR would target nightly-testing until at least the next RC cycle. Any concerns or other comments?

[François G. Dorais]

I was just about to create an issue about doing just that! Let me know how I can help!

[François G. Dorais]

I created a stub issue at batteries#1345

[Kim Morrison]

@Sebastian Ullrich, are you planning on making module allowed in nightlies for this release cycle? On Batteries' nightly-testing branch I still get "module keyword is experimental and not enabled here".

(Noting that the next release is delayed by two weeks as we move to the mid-month release schedule.)

[Sebastian Ullrich]

Yes, that could be in scope for the next cycle. But also projects we're actively supporting in the move shouldn't shy away from putting experimental.module=true in their lakefiles

[Kim Morrison]

Ahha! I didn't know about that option. I'm in that class of users who needs every warning controllable by an option to mention the option!

[Kim Morrison]

I started looking at using module, in batteries#1362 (note this is a PR to nightly-testing).

I've run into a "Not a definitional equality" error that I don't know how to resolve.

[Sebastian Ullrich]

Either ofBits needs to be exposed or the simp theorem should be changed to hold only propositionally, via := (rfl). Perhaps the latter given the definition is not that trivial?

[Sebastian Ullrich]

I was planning to write automation for at the very least adapting module headers, though questions like this will likely need be left to humans :)

[Kim Morrison]

:= (rfl) gives a type mismatch error instead.

[Kim Morrison]

(and @[expose] doesn't help)

[Sebastian Ullrich]

Ah, Fin.foldr is not exposed either. simp [ofBits] does the trick.

[Kim Morrison]

Okay. Say I now want to pause on my module-izing adventure, and PR this to Batteries as is.

Batteries/Data/Int.lean fails because it can't see Nat.ofBits_lt_two_pow from Batteries/Data/Nat/Lemmas.lean.

Without adding any more module keywords, how do I finish?

[Mario Carneiro]

I think you have to import all when a non-module wants to see a module's guts

[Kim Morrison]

But I can't use import all in a non-module.

[Mario Carneiro]

hm... actually I recall non-modules acting as though they import all'd all of their imports? Is this function supposed to be public?

[Mario Carneiro]

I assume Batteries.Data.Int in this scenario is a non-module importing private lemma Nat.ofBits_lt_two_pow from module Batteries.Data.Nat.Lemmas

[Mario Carneiro]

I reread the reference manual and I can't find much of a description of non-modules at all

[Mario Carneiro]

I think Nat.ofBits_lt_two_pow should be public to begin with

[Mario Carneiro]

in fact almost all lemmas in Batteries should be public

[Mario Carneiro]

I think you should use public section in the default preamble of every module in Batteries other than meta stuff

[Mario Carneiro]

likewise in mathlib

[Mario Carneiro]

the problem here is that you marked the module as a module but didn't do anything else, so everything in it is private

[Mario Carneiro]

using public section means that definition signatures and theorems will be public by default, which is the right default for batteries and mathlib. Definitions will still have private bodies, so we will either need to use @[expose] public section or put @[expose] on every definition. I think we should experiment a bit there to decide which is a better default

[Kim Morrison]

Okay, but adding public section at the top of Batteries/Data/Nat/Lemmas.lean causes errors everywhere... :-(

[Mario Carneiro]

like what?

[Mario Carneiro]

you might need public import in the imports of Batteries.Data.Nat.Lemmas

[Mario Carneiro]

Hopefully you shouldn't need import all unless the upstream module was poorly annotated or there is genuine coupling of modules

[Mario Carneiro]

One thing which I'm wondering about is whether here

-- Before we started introducing the module system in Batteries, this was a `rfl` lemma.
-- There is probably little downside to it no longer being a `rfl` lemma,
-- but if anyone wants to restore it we will need to add @[expose] to `Fin.foldr`.
@[simp] theorem ofBits_zero (f : Fin 0 → Bool) : ofBits f = 0 := by simp [ofBits]

it is actually the case that we can't add @[expose] post facto to Fin.foldr, given that import all would do basically that

[Sebastian Ullrich]

import all affects only the current module, a post-hoc expose would have to affect all downstream modules

[Mario Carneiro]

public import all impacts all downstream modules though

[Sebastian Ullrich]

It does not:

public import all M behaves like public import M followed by import all M, i.e. the all modifier becomes irrelevant for downstream modules.

I will remove that shorthand, it is too confusing

[Kim Morrison]

If anyone wants to checkout batteries#1362 and try to fix it that would be great. I don't understand the errors after adding public section at the top of Batteries/Data/Nat/Lemmas.lean, and don't know another way to proceed.

[Sebastian Ullrich]

You are trying to use Nat.recAuxOn in a public theorem type but it has not been imported publicly. You should always start porting by bumping existing imports to public import, which is what the scrappy version of the automation that I've been using and want to rewrite does

[Kim Morrison]

Okay.

In Batteries/Data/Nat/Lemmas.lean I've changed import all Batteries.Data.Nat.Basic to public import all Batteries.Data.Nat.Basic, and I've added a lot of @[expose] statements in Batteries.Data.Nat.Basic, and Batteries compiles now.

[Kim Morrison]

I really only want the @[expose] statements to last until Batteries.Data.Nat.Lemmas: one might hope that the theorems proved there are then sufficient for downstream users. Or do we have to re-arrange things to put theorems in the same file as the definition to achieve this?

In this case it wouldn't be bad, but I fear we do have places where the characterising theorems for a definition really do belong in a separate file.

[Sebastian Ullrich]

You can elide the [expose]s then and leave it to import all but some definitional equalities will not hold publicly anymore, so you will need to change their proofs to (rfl) if you think it is okay to break them.

[Sebastian Ullrich]

The last part would be a change that would affect all downstream users, not just modules

[Kim Morrison]

Any Batteries contributors want to chime in here? My inclination is to break all the definitional equalities and see if anything goes wrong. :-)

[Sebastian Ullrich]

For the aux recursors, hiding their bodies is probably not worth it - the bodies are barely more complex than their types and very unlikely to change. And their defeqs may certainly be helpful.

[Sebastian Ullrich]

It's more for definitions like ofBits where some actual complexity and implementation detail can be hidden

[Kim Morrison]

@Sebastian Ullrich, what about the common pattern of "defs in Defs, characterizing lemmas which need the bodies in Lemmas, but afterwards the bodies are not needed"? Can I do this?

[Kim Morrison]

I guess I would be happy to proceed for now on batteries#1362 (note that at this point it's still a PR to nightly-testing).

[Kim Morrison]

Also -- shake is going to need to be updated for the module system. We don't actually run shake in Batteries CI yet, so it's not an immediate obstacle.

[Sebastian Ullrich]

Kim Morrison said:

Sebastian Ullrich, what about the common pattern of "defs in Defs, characterizing lemmas which need the bodies in Lemmas, but afterwards the bodies are not needed"? Can I do this?

Yes, this is exactly what import all is for. You might just need to break some of these public dsimp lemmas in that case.

[Sebastian Ullrich]

I think I'll roll up my porting automation into a module-aware version of shake since it's already manipulating module headers

[Kim Morrison]

Shall we proceed with "feat: begin using the module system" batteries#1362. If this looks okay we can get the rest of the module headers in soon, and open the way to people exploring module in Mathlib with the next release.

[Sebastian Ullrich]

LGTM

[Mario Carneiro]

Kim Morrison said:

Any Batteries contributors want to chime in here? My inclination is to break all the definitional equalities and see if anything goes wrong. :-)

Sorry I missed this part of the thread; as I've said a few times now I think for these functions about which there are characterizing theorems, they should by and large be @[expose]. The only definitions in batteries which actually have steps taken to block their defeqs are Rat.add and friends

[Mario Carneiro]

I don't think there are any definitions in Nat.Basic which should be opaque

[Paul Reichert]

I might have missed this part, but why do you think definitions with characterizing lemmas should be exposed? One big advantage of the module system is to help building stable APIs, and it is much easier to keep definitions stable propositionally instead of definitionally. Definitions with characterizing lemmas seem like especially good candidates to keep them unexposed because unfolding them can be avoided more often.

It's possible that there are reasons why things need to be different in Batteries, though -- I might not have enough overview over Batteries. I would be interested in the rationale, though.

[Mario Carneiro]

I think it needs to be taken case by case, but IME the majority of mathematical definitions are supposed to have an exposed definition

[Mario Carneiro]

It's very rare to have a definition where unfolding is more than "medium-strong discouraged"

[Mario Carneiro]

I get very worried about potential use cases I'm blocking to say that unfolding should be made impossible for a given definition

[Mario Carneiro]

and proof by rfl for derived definitions applied to literals is an especially important case

[Yaël Dillies]

The only examples of such definitions that shouldn't be unfolded I can think of are docs#TensorProduct and other universal constructions

[Mario Carneiro]

when a definition is mathematical and also not noncomputable, I think someone will surely request it to be exposed sooner or later

[Paul Reichert]

Thanks for explaining it to me. Seems that I underestimated the amount of required defeq use in mathematics.

[Mario Carneiro]

Paul Reichert said:

One big advantage of the module system is to help building stable APIs, and it is much easier to keep definitions stable propositionally instead of definitionally.

Mathlib goes to great lengths to ensure that definitions line up to definitional equality and not just propositional equality, because of diamond issues. It's definitely not the case that we don't care about definitional equality, even though it is used in API boundaries and we tell people not to exploit definitional equality. This is a discouragement and not an iron wall

[Eric Wieser]

Yaël Dillies said:

The only examples of such definitions that shouldn't be unfolded I can think of are docs#TensorProduct and other universal constructions

I don't even agree with that, to the extent that I think lift f (tmul x y) = f x y should be a defeq, just like it is for simpler Quotient types.