v4.19.0-rc2

Stream: general

[Kim Morrison]

Downstream libraries using Lean.importModules should note a change of behaviour

If loadExts is true (false by default), we initialize the environment extensions using the imported data. Doing so may use the interpreter and thus is only safe to do after calling enableInitializersExecution; see also caveats there. If not set, every extension will have its initial value as its state. While the environment's constant map can be accessed without loadExts, many functions that take Environment or are in a monad carrying it such as CoreM may not function properly without it.

Uses should be carefully reviewed as the default behaviour has changed!

[František Silváši 🦉]

The 'release notes' link is broken for me (i.e. https://lean-lang.org/doc/reference/latest/releases/v4.19.0-rc2/).
I can access this without the -rc2 suffix tho, i.e. https://lean-lang.org/doc/reference/latest/releases/v4.19.0.

[Kim Morrison]

@František Silváši 🦉 , fixed, thank you!

[pandaman]

#general > v4.18.0 regression on well-founded recursion seems not fixed in v4.19.0. Filed https://github.com/leanprover/lean4/issues/7826.

[Bhavik Mehta]

The post on release notes appears to be talking about v4.19.0 rather than v4.19.0-rc2, is this intentional? The phrasing of this page indicates that it's about v4.19.0, and even links to a different place to look for release candidates.

[Kyle Miller]

(For convenience) Announcement thread: #announce > v4.19.0-rc2 @ 💬

[Kyle Miller]

Some structure/class changes that I'd like to highlight so that people can take advantage of them (or report issues that these changes may have caused!):

• It's now possible to change the binder kinds for the type's parameters. I'm looking forward to cleanups of all the primed fields in mathlib, where an auxiliary definition is created just to make certain arguments be explicit. See this thread.
• The types of fields are reduced when fields are elaborated. No more { x := v, y := w }.x in expected types. Most cases of dsimp only and beta_reduce at the starts of proofs can be removed.
• All class parents are now used when filling in fields (if you do #print C and look at "field notation resolution order", all the classes in this list except for C are used). Previously, only those parents that happened to be represented as "subobject fields" could be used this way. Many cases of __ := in mathlib can be cleaned up because of this. Currently, it is synthesizing parents in a pass before any of the provided field values are elaborated, but in future releases this will be improved, with parent synthesis being a process that will interleave with field elaboration. (Why? Parents can have types that depend on the class's fields. In the current release, this is only supported in the case where those fields can be solved for by using another parent instance.)
• All parents can be assigned. If toParentName is the parent projection, then you just need to write { toParentName := v, ... } to assign it.
• Both opt-param and auto-param fields can be overridden now, and they are inherited according to the resolution order that's listed under "field notation resolution order" in #print. Diamond inheritance no longer causes issues here.
• The pretty printer now knows about default values for structures, and fields containing default values are omitted. Using set_option pp.structureInstances.defaults true makes the fields print regardless.
• The project initiated by @Matthew Ballard in #2478 has reached a new milestone: we now aggressively eta reduce all structure constructors created using {...}/where notation. There are still some things we can do in this direction to optimize structure layouts, e.g., be aware of proof irrelevance when eta reducing, allow parent structures to overlap on proof fields, unfolding inferred instances when eta reducing, etc. In a benchmark, the new structure elaborator saves 0.99% instructions when building mathlib.

[Yaël Dillies]

I don't have a precise bug report, but v4.19.0-rc2 feels a lot less snappy than v4.18.0. Actually, it feels less snappy only when errors are present. Furthermore, the infoview, syntax highlighting, etc become slower and slower to update when editing a file. It's as if Lean were spawning more and more processes when errors are present, and those processes take a long time to die out.

[Yaël Dillies]

Performance also seems to be degraded when editing >= 5 files simultaneously, but I have less empirical evidence than the "editing a file makes it slow" remark above.

[Yaël Dillies]

In fact, editing almost anything is excruciatingly slow now. We're talking ~15s to replace \l with ←

[Henrik Böving]

Yaël Dillies said:

In fact, editing almost anything is excruciatingly slow now. We're talking ~15s to replace \l with ←

When you do what? Just open a file and type it point blank?

[Yaël Dillies]

Currently I am replacing a bunch of deprecated lemmas by their replacement, so each time I start with a declaration that builds but throws a warning, I perform a sequence of five or so simple edits, the declaration should work again but instead everything becomes sluggish and it takes 30s for the orange bar to leave the declaration

[Henrik Böving]

When I do those type of actions in Lean core files or on a random mathlib file everything is still pretty fast for me :/ Can you provide a clearer reproducer maybe?

[Kevin Buzzard]

I guess maybe a video might also be useful?

[Bhavik Mehta]

I'm also curious if others are experiencing this - a portion of my experiences of the form "Lean is being sluggish" have been caused by working over ssh, and particularly since you're working on gitpod which is currently dying, I wonder if that's a factor in what you're experiencing?

[Kim Morrison]

I haven't noticed this so far (having been using v4.19.0-rc2 on nightly testing for a month now), but I work on machines with many cores and it's possible users on smaller machines are experiencing something else due to all the new parallelism. Good reproducers would be very helpful!

[Marc Huisinga]

@Yaël Dillies When this happens and it gets really bad, a screenshot of the VS Code process explorer would also be very helpful. You can open it via 'Help' > 'Open Process Explorer' in VS Code.

[Marc Huisinga]

Another useful bit of information would be whether these issues remain if you temporarily downgrade the Lean 4 VS Code extension to 0.0.195, because it tells us whether it's just v4.19.0-rc2 causing the issue or the combination of the VS Code extension update and v4.19.0-rc2.

[Yaël Dillies]

I am on the lookout for the next time it noticeably happens, and I'll try these tips, thanks!

[Sebastian Ullrich]

@Yaël Dillies How many cores does this (Gitpod?) machine have?

[Yaël Dillies]

4 cores, 8GB RAM

[Yaël Dillies]

If Amazon or the FRO is willing to sponsor my absolutely ginormous use of gitpod, I wouldn't stop them :blush:

[Bhavik Mehta]

For what it's worth I haven't had this particular thing happen, on 4 cores and 4GB RAM

[Sebastian Ullrich]

Thanks, that's good to know. This is Gitpod as well?

[Bhavik Mehta]

This is local

[David Loeffler]

For what it's worth, I have also run into the same performance issues as Yaël (while running on a local machine, not Gitpod etc). While working on a moderately (but not absurdly) complicated proof, if I hesitated a few times in the middle of typing some line of the proof – so Lean repeatedly re-started compilation of the proof when it was in an invalid, mid-editing state – it would frequently just freeze, with the orange progress bar failing to move at all despite waiting several minutes. The only way I found of getting things moving again was to restart compilation of the entire file.

I'm no expert either in Lean's internals or in parallel programming, but Yael's interpretation

It's as if Lean were spawning more and more processes when errors are present, and those processes take a long time to die out.

does seem to match what I'm seeing.

[Kevin Buzzard]

This sounds the same as my #count_heartbeats complaint from recently and I just checked that this is not v4.19.0-rc2-specific, my issue also occurs on v4.18.0.

[Sebastian Ullrich]

@David Loeffler There is a big difference between being sluggish and freezing (for which we've identified a relevant bug). As a first step, please check if any kind of process (Lean or VS Code) actually consumes CPU when that happens.

[David Loeffler]

Just hit this again with a (one-line) proof that takes a full 30 seconds to fail with a "max heartbeats" error, eating up the full capacity of two CPU cores in the interim. @Sebastian Ullrich While I have this in front of me, what can I do to help you debug?

[Sebastian Ullrich]

Thanks, that's already good info. A debugger stack trace would be best depending on your OS, or a reproducer of course!

[David Loeffler]

Here's a MWE (or rather MnotWE):

import Mathlib.Topology.Algebra.InfiniteSum.Group

variable {α K : Type*} [CommMonoid K] [TopologicalSpace K]

example {f : α → K} (hc : Multipliable f) : False :=
  (hc.congr_cofinite hs hs').tprod_eq

This fails because Multipliable.congr_cofinite doesn't exist doesn't apply in this case (it was a typo for another lemma which does apply); but it takes an inordinately long time to fail.

[Sebastian Ullrich]

That doesn't even have a parallel theorem :big_smile: . Thanks, will take a look. It's fast in 4.18?

[David Loeffler]

Wait, perhaps this is not actually the same performance issue I wanted to report. I definitely noticed a slowdown in 4.19 that wasn't there in 4.18, but I am not 100% sure that this particular example is part of that – it might be a different kind of slowness.

[David Loeffler]

Apologies – this is indeed a different issue which is not specific to 4.19. (This is an example of "typeclass instance search taking a long time to fail" which is a long-standing problem.)

[Jovan Gerbscheid]

That's a strange heartbeats error. The trace shows that it keeps trying to synthesize the same (CommGroup) instance (which is cached, so it is fast). But it doesn't stop trying to synthesize it.

[Kevin Buzzard]

I also recently saw a trace where typeclass inference failing to infer some LinearOrderedCommRing about 50 times in a row (but very very quickly, and I also don't know if this was v4.19.0-rc2-specific)

[Marc Huisinga]

If anyone else runs into the same issue as @Yaël Dillies where all VS Code extension features (e.g. Unicode input) suddenly freeze up for a long time, I'd be very interested in a VS Code extension profile for the period of time where the issue is occurring, which helps me diagnose which parts of the VS Code extension are causing the slowdown.

When the issue starts happening, you can record a profile as follows:

1. Open the developer extension overview via Ctrl+Shift+P > Developer: Show Running Extensions
2. In the top right, click the black / white circle icon that is labeled "Start Extension Host Profile"
3. Navigate back to your file that is frozen and wait until VS Code recovers
4. Navigate back to the 'Running Extensions' tab and click the square in the top right that is labeled "Stop Extension Host Profile"
5. Click the 'Save Extension Host Profile' button in the top right and send me the resulting file in a DM

I don't know if this will work in Gitpod.

Here's a .gif demonstrating the process:
Recording VS Code extension profiles

[Sebastian Ullrich]

David Loeffler said:

Wait, perhaps this is not actually the same performance issue I wanted to report. I definitely noticed a slowdown in 4.19 that wasn't there in 4.18, but I am not 100% sure that this particular example is part of that – it might be a different kind of slowness.

Many thanks to @David Loeffler for providing me with a clear reproducer for this issue, this is now fixed in lean#7882 and I assume we'll likely make a backport available soon!

[Yaël Dillies]

Thanks David! I never managed to reproduce the issue consistently

[Sebastian Ullrich]

Here is a general recipe I figured out: in a file with an expensive proof at the end (e.g. with the remainder commented out), make a whitespace change to it and undo it after a small pause. Without the fix, I'm seeing 200% CPU usage from this, with it, usage quickly falls to 100%.

[David Loeffler]

Hooray, many thanks to Sebastian for getting to the bottom of this! I'm glad my rather scatter-shot attempts to find a reliable test case did eventually turn out to be helpful.

[David Loeffler]

Do I understand correctly that my test case was showing two bugs at once – a pre-existing issue with typeclass synthesis being slow to fail, worsened by a new 4.19-specific bug causing multiple threads to run into the typeclass synth bug simultaneously? And you have fixed the second, but the first remains to be solved?

[Sebastian Ullrich]

Yes, though I would like to be cautious about labelling automation taking a long time as a clear bug in general :)

[Eric Wieser]

Marc Huisinga said:

1. In the top right, click the black / white circle icon that is labeled "Start Extension Host Profile"

This doesn't appear for me on gitpod unfortunately

[Eric Wieser]

I'm finding that there is still an issue in rc3; if I open Mathlib/MeasureTheory/Function/SimpleFunc.lean, and make edits around 240 (type and backspace a few characters in a proof to break it), that VSCode can get stuck building the whole file for each intermediate edit

[Eric Wieser]

While this is happening, the \ abbreviation input hangs, as does even using the terminal in gitpod!

[Kim Morrison]

Can't reproduce on macos.

[Marc Huisinga]

Eric Wieser said:

I'm finding that there is still an issue in rc3; if I open Mathlib/MeasureTheory/Function/SimpleFunc.lean, and make edits around 240 (type and backspace a few characters in a proof to break it), that VSCode can get stuck building the whole file for each intermediate edit

I tried to reproduce this in GitPod, but no luck unfortunately.

[Marc Huisinga]

Could you paste the output of top -c when this happens? This should work fine in Gitpod.

[Yaël Dillies]

I am back at this again. Things are still very slow whenever I type things. In fact, they seem to be slow proportionally to how many lines there are below in the file

[Yaël Dillies]

I am quite worried, given that it is almost the end of the month, and simultaneously it is Easter

[Yaël Dillies]

I can reproduce Eric's slowdown by eg replacing some of the => in docs#MeasureTheory.SimpleFunc.bind with ↦. It first looks like this:
image.png
then by the point the language server actually performs the replacements, it gets confused:
image.png

[Yaël Dillies]

Here's the output of top -c when it is still reparsing the file one keystroke at a time:

top - 09:06:37 up 4 days, 10 min,  0 users,  load average: 28.72, 18.69, 12.55
Tasks:  16 total,   2 running,  14 sleeping,   0 stopped,   0 zombie
%Cpu(s): 55.8 us, 19.3 sy,  0.0 ni, 24.1 id,  0.3 wa,  0.0 hi,  0.5 si,  0.0 st
MiB Mem :  64297.9 total,   6681.5 free,  34731.5 used,  22885.0 buff/cache
MiB Swap: 384000.0 total, 382981.3 free,   1018.7 used.  28700.4 avail Mem

    PID USER      PR  NI    VIRT    RES    SHR S  %CPU  %MEM     TIME+ COMMAND
  52144 gitpod    15  -5 9447044   1.1g 602968 S 139.5   1.7   2:41.91 /home/gitpod/.elan/toolchains/leanprover--lean4---v4.19.0-rc3/bin/lean --worker file:///workspace/mathlib4/Mathlib/MeasureTheory+
    106 gitpod    15  -5   31.5g 352552  22524 S  21.6   0.5   2:04.97 /ide/node --dns-result-order=ipv4first /ide/out/bootstrap-fork --type=extensionHost --transformURIs --useHostProxy=false
     76 gitpod    15  -5   21.3g 104300  19268 S   7.0   0.2   0:22.18 /ide/node /ide/out/server-main.js --log=info --install-builtin-extension gitpod.gitpod-theme --install-builtin-extension github.+
  52131 gitpod    15  -5 2738416 953808  16396 S   6.6   1.4   0:24.01 /home/gitpod/.elan/toolchains/leanprover--lean4---v4.19.0-rc3/bin/lean --server /workspace/mathlib4

[Yaël Dillies]

I don't want to sound dramatic, but IMO there is still a major regression compared from 4.18 lurking in there. I am willing to hop on as many calls as the FRO wants if it helps resolve the situation.

[Yaël Dillies]

Marc Huisinga said:

I tried to reproduce this in GitPod, but no luck unfortunately.

How quick was your typing? If I replace one => every 4-5 seconds, it seems to be fine. If I replace one => every two seconds, it is not fine anymore

[Kim Morrison]

@Yaël Dillies, could you give me a GitPod URL to use? I don't ever use it, and can't work out how to instantly... but I'm happy to try to repro.

[Yaël Dillies]

There you go: http://gitpod.io/#https://github.com/leanprover-community/mathlib4/

[Kevin Buzzard]

How many gigs does this virtual machine have?

[Yaël Dillies]

8GB

[Kim Morrison]

I can't repro.

I went to SimpleFunc.lean, as indicated above, went to line 240, and deleted and restored the first => many times as quickly as I could. Every time, the file snaps back to life as soon as I stop touching it...

[Yaël Dillies]

What if you try changing several of them in turn? How many gigabytes did you give your VM?

[Kim Morrison]

I didn't do anything, I just clicked the link you gave me and clicked the big button!

[Yaël Dillies]

That's crazy. What is going on? :half_frown:

[Kim Morrison]

Changing the two alternately doesn't cause any problem.

[Kim Morrison]

Are you working in browser, or tranferring the gitpod session across to a local VSCode window?

[Kim Morrison]

(I don't see how that could do anything, but ...)

[Yaël Dillies]

Working in the browser

[Kim Morrison]

(me too)

[Sebastian Ullrich]

(for anyone else confused, it's docs#MeasureTheory.SimpleFunc.bind)

[Sebastian Ullrich]

I can't reproduce either. @Yaël Dillies Does it reproduce for you immediately after a Restart Server? Could you attach a screen recording with top open?

[Jovan Gerbscheid]

(I can't reproduce it either)

[Yaël Dillies]

(edited)

[Yaël Dillies]

I tried the repro again, and I hit the exact same issue

[Kim Morrison]

Okay, I think we need a screen recording from top to bottom in order to try to repro.

[Yaël Dillies]

Here's something I have just discovered: If I SSH into the same gitpod instance from my local vscode, then the slowdowns vanish :explode:

[Sebastian Ullrich]

Have you considered that your browser is cursed?

[Sébastien Gouëzel]

What happens if you try with another browser (chrome instead of firefox, or vice versa)? I just tried it, couldn't reproduce either.

[Michael Rothgang]

If you use some kind of Firefox set-up (custom add-ons, existing profile with lots of data, certain configuration): what happens in a new profile? Does the issue still appear? Some of my bugs disappear when using vanilla Firefox.

[Marc Huisinga]

@Yaël Dillies Do you have any other extensions in your Gitpod setup other than the Lean 4 extension? For example, are you using the Vim extension?

[Marc Huisinga]

The other thing to try is whether downgrading the extension to 0.0.195 fixes the issue on Gitpod for you.

[Marc Huisinga]

(... and if you're using the Vim extension, try disabling it before downgrading)

[Yaël Dillies]

Yes, I have all the extensions that come with the gitpod setup and a few more. The full list is:

• Docker
• Error Lens
• Jupyter
• Jupyter Cell Tags
• Jupyter Keymap
• Jupyter Notebook Renderers
• Jupyter Slideshow
• Python Debugger
• LaTeX Workshop (currently disabled)

[Marc Huisinga]

Ah, so no Vim extension. That's good.

[Marc Huisinga]

If you can still reproduce it consistently: Is the issue still reproducible for you on 0.0.195 of the extension?

[Yaël Dillies]

How do I downgrade?

[Marc Huisinga]

image.png