nightly-testing

Stream: mathlib4

[Joachim Breitner]

CI has been failing for a while on nightly-testing (since Dec 20). What are the processes around that?
Do people just push fixes there when they are sufficiently annoyed?
Who can do that, and who usually does?
Can you push directly, or use normal PRs with nightly-testing as the base?
Do they have to be the fix that will eventually be suitable for master, or is it common to take shortcuts to get CI going again?
(Is there a FTFM answering these that I missed?)

[Yaël Dillies]

Is this not mostly Scott's doing? and the continuous failing related to Scott's holidays?

[Joachim Breitner]

That’s what I feared, and I’d like to know how and if (and how) I can help :-)

I’ll just start to try to fix issues, and see how that goes.

Let’s see what CI thinks of #9438

[Joachim Breitner]

Could someone with permissions to push to ProofWidgets label latest main (i.e. 8dd18350791c85c0fc9adbd6254c94a81d260d35) as v0.0.25-pre1? That would help me with getting the mathlib CI running again. @Wojciech Nawrocki probably; who else might have access?

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

Done, except that I named it v0.0.25 since the release is ready. You will have to wait a bit for the artifacts to be built. @Joachim Breitner

[Joachim Breitner]

Much appreciated!

[Jeremy Tan]

Now failing at Mathlib/RingTheory/Polynomial/Hermite/Basic.lean

[Jeremy Tan]

Now failing in the check environments step:
lean4checker found a problem in ProofWidgets.Demos.Macro

[Joachim Breitner]

It seems that the proofwidgets oleans that cache get gets are built with a different version of lean?

~/build/lean/mathlib4 $ lake env lean --version
Lean (version 4.6.0-nightly-2024-01-03, commit 504b6dc93f46, Release)
~/build/lean/mathlib4 $ xxd /home/jojo/.elan/toolchains/leanprover--lean4---nightly-2024-01-03/lib/lean/Init/Prelude.olean|head -n 2
00000000: 6f6c 6561 6e01 3530 3462 3664 6339 3366  olean.504b6dc93f
00000010: 3436 3738 3563 6364 6462 3863 3566 6634  46785ccddb8c5ff4
~/build/lean/mathlib4 $ xxd ./.lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Demos/Macro.olean|head -n 2
00000000: 6f6c 6561 6e01 6236 3134 6666 3164 3132  olean.b614ff1d12
00000010: 6263 3338 6633 3930 3737 6639 6365 3966  bc38f39077f9ce9f

But why does cache get download them then?
(This is after rm -rf .lake/ && lake exec cache get)

I have seen discussions scroll by about bad proofwidget oleans in the cache, is that a known issue?

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

It's strange that lean4checker is even looking at that file. It is not imported from ProofWidgets.lean, and is part of a separate lean_lib.

[Joachim Breitner]

It’s not imported _anywhere_ it seems. Why does cache even try to download it? And who pushed it? Very mysterious.

[Joachim Breitner]

It is not unpacked when I run lake exec cache unpack again

[Mario Carneiro]

It is unpacked by the proofwidgets release

[Mario Carneiro]

because lake just zips the whole .lake folder to produce the release

[Mario Carneiro]

These files have been causing problems for cache for a while

[Mario Carneiro]

lake unpacks it whenever it gets the proofwidgets library for the first time

[Joachim Breitner]

Ouch. Is that just a missing file filter in the call to zip, or is there a good reason to include them in the release?

[Mario Carneiro]

I don't think lake even knows how to filter it

[Joachim Breitner]

Ah, it’s also lake that makes the “release”.

[Mario Carneiro]

this is lake upload

[Mario Carneiro]

cache could almost completely do without the proofwidgets release, except it needs the js files

[Joachim Breitner]

Indeed. I was expecting the release to only contain the .js files.

[Mario Carneiro]

in particular all of the olean files are counterproductive because (1) cache already caches them, (2) they are frequently out of date and have to be recompiled anyway, and (3) if any are left over they can end up in the next cache put call (because cache put also can't tell the difference between untouched bad files and freshly built good files and assumes everything in the .lake folder is good) and get redistributed which causes crashes downstream

[Mario Carneiro]

And this is run as a pre-build step of lake exe cache get (the part where it compiles Cache.Main and first has to download all the dependencies) so by the time cache is running the damage is already done

[Joachim Breitner]

Yeah, this is all kinda weird. Is there an issue already? Should Proofwidgets start to simply use tar to make the releases, and include only the .js files?

[Mario Carneiro]

For pure lake usage of ProofWidgets, the release is moderately sensible: it caches the build artifacts for the stated version of lean, and lake will invalidate it if you use another version

[Joachim Breitner]

So the issue is more that lake4checker runs blindly on all .oleans, even those that we never created or touched?

[Mario Carneiro]

but I think it needs to be more careful about ensuring random olean files are not left around in the build directory, because at least lean4checker assumes that doesn't happen

[Joachim Breitner]

For the purposes of unblocking nightly-testing in #9438 I added a workaround to the workflow there, deleting the unwanted contents of the proofwidget release.

[Mario Carneiro]

I think lean4checker's behavior is somewhat defensible, it is trying to also check orphan files or multiple projects in the same repo

[Joachim Breitner]

Somewhat defensible, but I’d consider it a violation of the principle of least surprise; it shouldn’t and usually doesn’t affect tools what cruft I have laying around in random places. I’d intuitively expect it to use the default lake target, unless I pass it one. Also, isn’t .lake content supposed to be an implementation detail of lake, I thought.

(I guess it is consistent with lake’s behavior of uploading everything from .lake/build as a release ;-))

[Mario Carneiro]

The problem is that people might be using lean4checker without knowing what the root is and just wanting to check "everything"

[Mario Carneiro]

and/or some files are hidden because they are not transitively imported by some package or other and hiding badness

[Mario Carneiro]

I think that's pretty surprising

[Mario Carneiro]

I don't think people generally want to regard the build job that adds everything to Mathlib.lean as soundness critical

[Joachim Breitner]

But then it suddenly depends upon what they lake build before, with which targets, and when, so also strangely stateful. Users who reliably navigate that complexity can probably deal with having to be explicit what they want to have checked.

Maybe lean4checker should always expect .olean paths or module names, then lake check should exist as an analogue to build that also makes sure the files are up-to-date (to reduce the risk of checking an old .olean), and likewise a VSCode action “check this file” for those not interacting with the CLI.

[Notification Bot]

A message was moved from this topic to #mathlib4 > lean4checker CI job by Joachim Breitner.

[Joachim Breitner]

https://github.com/leanprover-community/mathlib4/pull/9438 is green, and can be merged if deemed useful.

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

Mario Carneiro said:

and/or some files are hidden because they are not transitively imported by some package or other and hiding badness

Any such badness could not take effect as part of import Mathlib until the files are imported from Mathlib.lean, at which point they would be checked by a lean4checker-directed that only goes through imported files, right? Or is the worry that someone puts an incorrect proof into some archive/ folder that isn't imported?

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

I'm happy to change the release-packaging job for PW4 to include nothing but *.js, I'm just somewhat inclined to agree with Joachim here that random leftover .oleans (which I think should be a sort of output-only cache) shouldn't break things like this.

[Mario Carneiro]

I blame lake for this, not proofwidgets

[Mario Carneiro]

mathlib should be able to tell lake that it doesn't want the proofwidgets release, and will fetch it itself

[Mario Carneiro]

It's not even a dependency of Cache, so getting it is premature

[Joachim Breitner]

How would that help? It'd still contain the wrong oleans?

[Joachim Breitner]

In my PR I use lake build cache to get and clean the release before lake exec cache get

[Mario Carneiro]

It can unpack it selectively as you did in #9438, because mathlib knows the context in which it wants this file

[Mario Carneiro]

IMO the design where libraries specify preferRelease := true and downstream deps have no opt-out is bad

[Mario Carneiro]

The main thing that proofwidgets can do to avoid this (possibly in conjunction with mathlib maintainers) is to stay on the same version as mathlib and be released together

[Mario Carneiro]

these issues recur every time mathlib gets ahead of proofwidgets because that's when mathlib has to rebuild proofwidgets (which mostly works but has various sporadic issues), when proofwidgets is up to date none of this is an issue

[Joachim Breitner]

That doesn't help when you want to test lean PR releases, does it? The ability to swap the toolchain without changing all dependencies (if they happen to still build) seems quite important

[Mario Carneiro]

but it's a bit of a weird situation because we can only work on fixing the sporadic issues when proofwidgets is not up to date so that they actually manifest

[Mario Carneiro]

We want it to work either way

[Joachim Breitner]

Why should it have to be different than any other library - except for fetching the js files - in the first place?

[Mario Carneiro]

It's the only mathlib dependency that uses lake upload, which is a separate caching mechanism which does not play well with lake exe cache and is much less sophisticated

[Mario Carneiro]

I think a MVP feature to solve most of the issues would be a way for lake to allow downstream projects like mathlib to override preferRelease in dependencies

[Mario Carneiro]

otherwise it's not really a preference

[Mario Carneiro]

Alternatively, proofwidgets could stop using the lake upload feature altogether (it is already partly hacking around it by uploading the same tarball as all 3 supported OSs even though they were not built the same)

[Mario Carneiro]

and instead just have a custom job which downloads a tarball of js files

[Joachim Breitner]

Job as in lake update hook?

[Mario Carneiro]

I think it would be a pre-build dep

[Mario Carneiro]

I mean there is a way to express it in the language of lake build dependencies: elaboration of certain lean files requires certain js files, getting js files requires unpacking them from a certain zip file, getting the zip file requires downloading it from a specified source

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

Mario Carneiro said:

Alternatively, proofwidgets could stop using the lake upload feature altogether (it is already partly hacking around it by uploading the same tarball as all 3 supported OSs even though they were not built the same)

This is no longer true btw, we build all platforms in CI now

[Mario Carneiro]

Oh, that makes me even more worried

[Mario Carneiro]

because cache needs them to have the same hash

[Mario Carneiro]

otherwise they will not be used by lake when unpacked

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

What do you mean by 'them' and 'they'?

[Joachim Breitner]

Joachim Breitner said:

https://github.com/leanprover-community/mathlib4/pull/9438 is green, and can be merged if deemed useful.

Oh, I just noticed that nightly-testing is not a protected branch and I could just merge myself… but I guess it’s prudent to wait for a :thumbs_up: from a maintainer first. Scott should also be around soon.

[Kim Morrison]

Amazing work, @Joachim Breitner. I've just merged your PR to nightly testing. I was actually back yesterday, but didn't get to nightly-testing quite yet. :-)

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

Reviving this thread, I can adjust the PW4 build but need some consensus on what it should do!

Mario Carneiro said:

I mean there is a way to express it in the language of lake build dependencies: elaboration of certain lean files requires certain js files, getting js files requires unpacking them from a certain zip file, getting the zip file requires downloading it from a specified source

Unfortunately there is no way to register with Lake that a given Lean module depends on a custom target at the moment. This has been a bit of a pain point that requires manual lake clean when the .js changes.

[Mario Carneiro]

Is there a lake issue for this?

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

It appears there is not! Just made lean4#3153.