v4.22.0-rc2

Stream: general

[Kim Morrison]

This thread is for discussion of the v4.22.0-rc2 release.

(I anticipate that there'll be discussion in other threads about grind -- please try to use those for grind specific questions.)

[Mario Carneiro]

Other thread about grind: #mathlib4 > `grind` is available. What should Mathlib users expect? @ 💬

[Asei Inoue]

my lean-update action is no longer needed?
(sorry for late developing)

[Asei Inoue]

Is there an example for new monadic verification framework?

[Kevin Buzzard]

What is "the new module system"? What even is a module?

[Asei Inoue]

I’m interested in new module system, too.
Could you show us an code example?

[Siddhartha Gadgil]

As far as I understand (from having used Agda and Idris) a module is an extension of a namespace but which can be parametrized. The parameters will be like variable statements from within the module but when a module is imported specific values can be plugged in. For instance, a module about graphs may have V and E as parameters.

[Kim Morrison]

No, that's not it.

[Kim Morrison]

I'm not going to write the explanation now, sorry, but perhaps someone else will soon :-). It is a collection of keywords associated to import statements that control the visibility of declarations and their bodies in downstream files. Looking at src/Init/ in the Lean repository, where this is already being deployed, is the best I can offer at this moment.

[Asei Inoue]

@Kim Morrison

my lean-update action is no longer needed?
(sorry for late developing)

[Malvin Gattinger]

Trying to update my project I am running into PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:464:4: duplicate normalized declaration name endNodesOf vs. endNodesOf where endNodesOf is a definition in my file. Are there known issues related to this? Should I upload the backtrace somewhere to debug this? Or better wait for a non-rc version?

[Sebastian Ullrich]

I don't know of any open issues related to that, please open one!

[Malvin Gattinger]

Ok, I fear making an MWE will be tricky, so I'll first try to at least reproduce it in the CI of my project.

[Malvin Gattinger]

Here is the PANIC in a CI action that does lake build Bml. Just above it there is this error which makes me wonder if something that previously could "see" that LR = (LR.1, LR.2) now got more strict :thinking:

error: Bml/Tableau.lean:706:0: Cannot derive endNodesOf.eq_def
  invalid let declaration, term
    endNodesOf._proof_2 LR C ruleA c c_inhas type
    lengthOfTNode c < lengthOfTNode (LR.1, LR.2) : Prop
  but is expected to have type
    lengthOfTNode c < lengthOfTNode LR : Prop

and below it there is a long backtrace.

(I hope the CI action log is public, it seems GitHub does not show it when I am not logged in.)

Update: I managed to work around this problem by replacing c with (c.1, c.2) and similar things, but I have no idea why this helps. And here is a similar PANIC that I ran into next.

Update update: maye related https://github.com/leanprover/lean4/issues/8627

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kim Morrison said:

No, that's not it.

I really wish that were it, though! Maybe one day we'll have parameterized modules

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Kim Morrison drawing your attention to this.

[Kim Morrison]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

Kim Morrison drawing your attention to this.

Thanks, it has since been fixed. I had everything pointing to nightly-testing versions of dependencies.

[Kim Morrison]

Kevin Buzzard said:

What is "the new module system"? What even is a module?

Sebastian has been working on documentation, it will be coming soon!

[Kevin Buzzard]

"The module system is an experimental feature that allows for more fine-grained control over what information is exported from, and imported into, modules."

I am still at a loss about what a "module" is. Sorry for my ignorance!

[Kim Morrison]

A module is simply a lean file that begins with the module keyword. It then affects (more specifically, allows you to control) what information from that file is available in other modules which import it.

[Kevin Buzzard]

by "import (a module)" you just mean "import the file"?

[Kim Morrison]

Yes

[Kevin Buzzard]

I see, so for example I can't make any file in FLT into a module right now because I'm typically importing thousands of mathlib files which are not modules.

[Kim Morrison]

Yes.

[Kim Morrison]

We're not anticipating mathematicians will be significant users of this feature in the near term.

[Kevin Buzzard]

Oh! Anyway thanks for the link, I now feel like I understand much better what's going on.

[Kim Morrison]

All of Batteries, and probably the Logic and Data (or at least, what should be in Data) directories of Mathlib should become modules asap. This will unblock non-mathematical users adopting module.

[Kim Morrison]

Using module all through Mathlib is eventually a great idea. But we will need more tooling help to make this viable. It is at least as difficult a task as carefully deciding what should be irreducible, which we're already years behind on.

[Kevin Buzzard]

Aah the penny is dropping -- this is the solution to "I want about 3 things from mathlib in my project but I really don't want to depend on mathlib because it's massive".

[Kim Morrison]

I'm not sure if it's "the solution", but it does help.

[Kim Morrison]

A really important feature of the module system is that it allows you to approximate "non-transitive imports", i.e. to import a file, in a way that doesn't mean that downstream files can see.

[Jonathan Chan]

Not sure if this is the place to ask, but I noticed that upgrading from 4.21.0 to 4.22.0-rc1/-rc2 seems to have broken my ⇓ notation: the following used to parse fine

infix:40 "⇓" => Eq
theorem test {n : Nat} : Nat.add n 0 ⇓ n := by rfl

but now requires parentheses around (Nat.add n 0). (fwiw the error message is unexpected token ':='; expected '↦', '=>', which doesn't make sense to me.) None of my other infix notations are broken, so I assume this notation is shadowed somewhere, but I'm not importing Mathlib or anything else, and not even setting (priority := high) (or any other big number, idk how high they go) works. Is there some way around this so that I don't have to add the parentheses in? Or should I file an issue?

[Aaron Liu]

looks like we have docs#Std.Do.Syntax.totalPostCond now, I have no idea what it's supposed to do

[Jonathan Chan]

hmm. Okay so I do import Lean.Elab.Tactic.Induction somewhere for something else, which I suppose must import Lean.Elab.Tactic.Do. Why can't I override the notation? I also can't find any info about builtin_term_parser or meta def in the language ref or in the search

[Kim Morrison]

You'd have to ping @Sebastian Graf here; this is notation use by the new monadic verification framework.

I think the answer may just be "Lean core is claiming this notation; sorry".

[Eric Wieser]

Is it possible to have notation that is only scoped to do blocks, or is that not how things work?

[Kim Morrison]

This notation appears in theorem statements using Hoare triples, not inside do blocks. But I'll leave this to Sebastian to answer.

[Sebastian Graf]

Sorry about breaking your notation. I'll scope it to Std.Do, like a lot of other notation. Won't be fixed in time for 4.22.0 though.

[Kim Morrison]

Mathlib (and upstream repositories) are now all on v4.22.0-rc3, which includes many grind and compiler bug fixes.

[Robin Carlier]

Screenshot_04-Jul_09-35-11_25073.png
Thanks for fixing the issue with @[grind ←=]! Works like a charm now.

[Patrick Massot]

Thank you very much to the whole team! This release is so much packed with fantastic new features that having many release candidates isn’t surprising at all.

[Eric Wieser]

Can I request that https://github.com/leanprover/lean4/pull/9181 make it into rc4, on the assumption such an RC is created?

[Sebastian Ullrich]

Kim Morrison said:

Kevin Buzzard said:

What is "the new module system"? What even is a module?

Sebastian has been working on documentation, it will be coming soon!

The docs are now available at https://lean-reference-manual-review.netlify.app/The-Module-System/#module-system

[Mario Carneiro]

def myInternalHelper (x : Nat) : String := ...

public instance : ToString Nat where
  toString x := private myInternalHelper x

What is the meaning of private in this code? I would think that since myInternalHelper is already public with private body (the default), this would do nothing

[Mario Carneiro]

or maybe I'm misreading it and that private is not term operator like unsafe and that's just where you put the modifier for private fields (which I find a bit weird, considering that most other modifiers come before the identifier like private toString := ...)

[Sebastian Ullrich]

Is

abbrev and instance always expose their body. For instance, individual field values can be marked private, which can be useful for programming purposes

not clear? Private is only the default for def

[Sebastian Ullrich]

Making instance implementations private by default felt like too much of a gotcha as they often must participate in unfolding. Even when purely programming, people usually keep the code inline inside instances small, so not much is lost by exposing it by default.

[Sebastian Ullrich]

(and speaking of "inline", inlining them during codegen is usually important as well, though that is not necessarily linked to language-leve visibility)

[Mario Carneiro]

I understood that part and don't object to the design decision, I'm just wondering about the syntax toString x := private myInternalHelper

[Mario Carneiro]

which to my eye has a private in a strange place

[Sebastian Ullrich]

Ah, I misread your comment. Note that myInternalHelper is private, which is the default in modules outside public section!

As for := private, it does not have any pendant to existing syntax but as it semantically belongs to the body and private in front of a field name already exists anyway with a quite different meaning, I believe it is the most sensible placement.

[Mario Carneiro]

The module system's import all is more powerful than import without the module system. It makes imported private definitions accessible directly by name, as if they were defined in the current module. Thus another use case of import all is to make declarations available that need to be used in multiple modules but should not leak outside the current library.

It sounds like this is going to be an alternative to open private. Any advice on which one to use when? (Notwithstanding that open private is not officially supported by core, it has use cases that can't be done otherwise and I'm glad this is being recognized.)

[Mario Carneiro]

Do non-modules also have "public and private scope" since private is also legal in non-modules?

[Mario Carneiro]

in general, how do non-modules work with the module system?

[Sebastian Ullrich]

Non-modules can import modules and will ignore all module-system-specific annotations.

So really the only relevant thing to them is private (or non-public outside public sections), which for them has the same meaning as before; no new checks outside module as demonstrated by 4.22.0 not breaking the world

[Mario Carneiro]

no I'm asking the other way around, what happens when a module imports a non-module

[Sebastian Ullrich]

They don't:

modules can only import other modules so adoption has to be done top-down

[Mario Carneiro]

oh so adoption is really forced then...

[Sebastian Ullrich]

There is no sound way around that

[Mario Carneiro]

?

[Mario Carneiro]

is it really impossible to have a default moduleish behavior for non-modules?

[Mario Carneiro]

or a combination of special scopes to make it possible to exactly represent non-module semantics from within the module system

[Sebastian Ullrich]

public @[expose] section gets you close. After that most breakage comes from now-detected-ill-scoped use of private and necessary meta imports, which are comparatively small hurdles

[Eric Wieser]

Sebastian Ullrich said:

They don't:

modules can only import other modules so adoption has to be done top-down

I'd argue this should say "bottom up", but it's a matter of interpretation

[Sebastian Ullrich]

Your leaves are at the top!?

[Aaron Liu]

sometimes my leaves are at the bottom too

[Mario Carneiro]

but it's not starting from the leaves, it's starting from init

[Mario Carneiro]

we would not usually call Init.Prelude a leaf file

[Sebastian Ullrich]

Now you got me confused as well for a moment, hah... edited

[Eric Wieser]

Sebastian Ullrich said:

Your leaves are at the top!?

:tree:, :evergreen_tree:, and :palm_tree: suggest this is a reasonable interpretation :)

[Aaron Liu]

I hear "downstream" and "upstream" often so if a river flows downhill then the leaves are at the bottom

[Mario Carneiro]

The meta import section is a bit incomplete, it doesn't cover all the ways one can combine meta and non-meta imports or declarations. IIRC there was a module doc (ha!) which covers this better

[Eric Wieser]

Perhaps "by upstream files before downstream ones" would resolve my confusion. I assume this was quoted from the release notes / docs?

[Mario Carneiro]

In this case, there is no readily available trace for debugging; consider using @[expose] sections generously on the closure of relevant modules.

this is going to be fun when we port mathlib to the module system

[Sebastian Ullrich]

How many proof-by-reflection-like tactics are there in Mathlib? How many where the extent of reduction is not immediately clear?

[Mario Carneiro]

Sebastian Ullrich said:

public @[expose] section gets you close. After that most breakage comes from now-detected-ill-scoped use of private and necessary meta imports, which are comparatively small hurdles

I think you misunderstand. I want a way to add a dependency which maybe I don't want to touch and which is not upgraded to the module system, without needing to debug it, while my own code is using the module system. So I want lean to apply the necessary shimming automatically when I import a non-module

[Mario Carneiro]

without this, we get into a bad situation where any library not on the module system is now unable to work with clients on the module system, and so clients may decide against upgrading in order to use a dependency, slowing adoption

[Sebastian Ullrich]

Mario Carneiro said:

In this case, there is no readily available trace for debugging; consider using @[expose] sections generously on the closure of relevant modules.

this is going to be fun when we port mathlib to the module system

But in general, yes, we'll have to see what becomes an issue and what not. There should be various ways we can support problematic porting parts via changes in core.

[Mario Carneiro]

Sebastian Ullrich said:

How many proof-by-reflection-like tactics are there in Mathlib? How many where the extent of reduction is not immediately clear?

main source of this kind of reduction is proofs by decide and rfl

[Mario Carneiro]

and lots of code in mathlib is implicated, in principle anything that is not noncomputable

[Mario Carneiro]

in general I expect mathlib will almost always want to @[expose]

[Mario Carneiro]

we might even want to make it a project level default if possible

[Aaron Liu]

Sebastian Ullrich said:

How many proof-by-reflection-like tactics are there in Mathlib? How many where the extent of reduction is not immediately clear?

git grep -o "by decide" Mathlib/* | find /c /v "" gives me 400

[Mario Carneiro]

those are the uses, you have to look at the things those uses reduce

[Sebastian Ullrich]

Both these tactics reduce in the elaborator first, so the specific issue quoted does not apply. That controlling unfolding will need annotations and thinking about them is still true of course.

[Mario Carneiro]

I assume the error will still happen, but you are saying the message is better?

[Mario Carneiro]

I don't think mathlib ever does proofs by reduction that aren't elaborator checked

[Sebastian Ullrich]

You can use traces and we have better options to improve the message, yes. decide already does a lot of reduction debugging.

[Edward van de Meent]

something which might be nice is if #check or #print displays all these properties of declarations. similarly, maybe #where can show what import is what kind, what kind of section the command is in, etc? i imagine that might help with debugging?

[Sebastian Ullrich]

Certainly! #print already shows most of these. For keeping track of sections I recommend the sticky scroll feature in VS Code but extending #where makes sense as well.

[Notification Bot]

5 messages were moved from this topic to #general > unused simp argument linter feedback by Joachim Breitner.

[Eric Wieser]

I just noticed that the speedcenter graph says there is a noticeable performance drop in v4.22.0; is it easy to locate the exact numbers for that commit? (edit: here, via #rss > Benchmark results for mathlib4 @ 💬 )

[Yaël Dillies]

Is the performance drop due to switching to the new compiler and reenabling compilation of a lot of previously noncomputable stuff?

[Yuyang Zhao]

The build time of my repository has increased from 36s to 56s.

upd: It turned out that the reason was that I forgot to update a get_elem_tactic_trivial to get_elem_tactic_extensible :face_palm: .

[Harald Husum]

Kim Morrison said:

• there is a v4.21.0 tag

This is a typo, right?

[Yaël Dillies]

Some more grind love: https://github.com/leanprover-community/mathlib4/pull/25836/files/8fe8fdcdb90c2ee6b593e40e134a3e32f9d0006a..44ab3f6559fd46c5c82ba041bebbd33fc9adeff3

[Chris Henson]

Yaël Dillies said:

Some more grind love: https://github.com/leanprover-community/mathlib4/pull/25836/files/8fe8fdcdb90c2ee6b593e40e134a3e32f9d0006a..44ab3f6559fd46c5c82ba041bebbd33fc9adeff3

We've also had some PRs this week to use grind in CSLib, such as cslib#35. It's been great for simplifying proofs.

[Floris van Doorn]

The better handling of dots in lean#8784 is very nice, and means that we can drop the parentheses in ∫ x in (0)..a, f x (#29017)