mathport

Stream: mathlib4

[Yury G. Kudryashov]

Hi, did something happen to mathport? The last commit that went through is #19062

[Yury G. Kudryashov]

Indeed, https://github.com/leanprover-community/mathport/actions/runs/5100946585 says that "process completed with exit code 1".

[Yury G. Kudryashov]

@Mario Carneiro Is it possible that your changes from 2 days ago broke it?

[Kyle Miller]

This is a curious error:

remote: error: File Mathbin/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
is 278.63 MB; this exceeds GitHub's file size limit of 100.00 MB

[Yury G. Kudryashov]

Where did you find the error?

[Yury G. Kudryashov]

And how did we get such a huge file?

[Kyle Miller]

I clicked "Mathport" on that link, clicked "update port repos (master)" then scrolled down

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathport/actions/runs/5091663507/jobs/9151993679

[Yury G. Kudryashov]

The first failure :up: no space left on device

[Eric Wieser]

I think we need to stop outputting the warning messages in the lean files themselves

[Eric Wieser]

Or at least, truncate each one to 100kb

[Yury G. Kudryashov]

Who can run it locally and see what happens? AFAIR, it needs more RAM than I have.

[Yury G. Kudryashov]

I'm OK with truncating each one to 1kb.

[Eric Wieser]

I'd be ok with truncating each one to 0b; I don't think anyone is using them at all...

[Eric Wieser]

Kyle Miller said:

This is a curious error:

remote: error: File Mathbin/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
is 278.63 MB; this exceeds GitHub's file size limit of 100.00 MB

I wonder if reverting !4#4384 fixes the problem

[Yury G. Kudryashov]

No, the problem started before that

[Yury G. Kudryashov]

I linked to the first failure above.

[Yury G. Kudryashov]

BTW, did mathport change align logic some time ago? 9cb92e8c581bb6d7a1f3c106109eeaeb56437f8a changes some Preorder.toLE in warnings to Preorder.toHasLE.

[Yury G. Kudryashov]

It's May 16

[Yury G. Kudryashov]

No, it's !4#4000 removed some #aligns

[Eric Wieser]

Yury G. Kudryashov said:

The first failure :up: no space left on device

This sounds like we just need to delete some junk from our CI machines

[Yury G. Kudryashov]

You can go through all actions at https://github.com/leanprover-community/mathport/actions

[Yury G. Kudryashov]

I'm going to add some #aligns back

[Yury G. Kudryashov]

!4#4427

[Eric Wieser]

Thankfully it looks like the predata step is still running fine, so one we fix this we'll get a new mathport output in 2 hours rather than at the end of the day

[Mario Carneiro]

just pushed a fix

[Pol'tta / Miyahara Kō]

Foo! Mathport have finished running now!

[Mario Carneiro]

I'm curious how much mathlib3port decreased in size

[Mario Carneiro]

764.4MB -> 236.6MB

[Mario Carneiro]

and exactly the same line count, which is fun

[Mario Carneiro]

the savings isn't as much as I was hoping, it seems that a 10k limit per message is still enough to cause a lot of text since in many files almost every declaration is marked as dubious

[Mario Carneiro]

I pushed another fix to just turn off the dubious message entirely, since I think it is too late to change our processes to keep these messages under control

[Mario Carneiro]

without the dubious translation messages, it has decreased again from 236.5MB to 104.2MB

[Eric Wieser]

On the assumption they don't block the port, is the intent then to write off any truly dubious (i.e. incorrect) translations as the cost of porting, and hope that either the changes are cosmetic, or in the case of dropped Sort/Type generalizations something that a mathlib4 user will eventually PR again anyway? Or is there still some vague hope of using mathport to ask "did we port everything correctly"?

[Mario Carneiro]

I think the main blocker for mathport dubious translation messages at this stage are all the unaligned instances

[Mario Carneiro]

although if we had #aligns for all of the autogenerated instance names I'm sure we'd be back to 700MB in no time

[Eric Wieser]

I thought the main blocker was universe arguments being in the wrong order everywhere?

[Mario Carneiro]

TBH it's hard to tell from the error messages

[Mario Carneiro]

that was certainly a problem, no idea if it's the main one

[Mario Carneiro]

it all feels pretty hopeless at this point to get defeq somehow

[Mario Carneiro]

I would be okay with just not trying to use mathport to check our work and just rely on the internal coherence of the library

[Eric Wieser]

Perhaps just checking everything in mathlib3 is aligned is good enough, without checking if the alignment is perfect

[Damiano Testa]

After all, the trust in the mathlib3 library also comes mostly from cohesion -- just like in informal mathematics! :upside_down:

[Yury G. Kudryashov]

I think that open_locale should be translated as open scoped, not open

[Yury G. Kudryashov]

E.g., in !4#4453, opening NNReal was a bad idea.

[Eric Wieser]

The builds still seem to be failing, see this log

[Eric Wieser]

uncaught exception: failed to port Mathbin:MeasureTheory.Function.Jacobian with imports [Leanbin.Init.Default, Mathbin.Analysis.Calculus.Inverse, Mathbin.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap, Mathbin.MeasureTheory.Covering.BesicovitchVectorSpace, Mathbin.MeasureTheory.Measure.Lebesgue.EqHaar, Mathbin.Analysis.NormedSpace.Pointwise, Mathbin.MeasureTheory.Constructions.Polish]:
import Mathbin.Topology.MetricSpace.Polish failed, environment already contains '_proof_3' from Mathbin.Analysis.InnerProductSpace.PiL2

[Mario Carneiro]

that error looks to be unrelated to the archive/ stuff

[Eric Wieser]

Yes; I was not intending to make a connection there

[Eric Wieser]

I guess it's also unrelated to the "100k of error message is too much error message" stuff

[Mario Carneiro]

is MeasureTheory.Function.Jacobian a new file?

[Eric Wieser]

My guess is that this was broken by us porting port-status#analysis/inner_product_space/pi_L2

[Mario Carneiro]

I don't see MeasureTheory.Function.Jacobian in the last successful run

[Eric Wieser]

port-status#measure_theory/function/jacobian

[Damiano Testa]

It is one of the targets of the port progress, I think.

[Eric Wieser]

The file has existed for ages

[Mario Carneiro]

I mean new to mathlib4 since the last mathport run

[Eric Wieser]

The file shouldn't be in mathlib4 yet

[Eric Wieser]

What's new to mathlib4 is PiL2

[Mario Carneiro]

yeah, most likely changes in either Topology.MetricSpace.Polish or Analysis.InnerProductSpace.PiL2 are to blame

[Mario Carneiro]

compared to the autogenerated versions of these files

[Yury G. Kudryashov]

mathport doesn't work again

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathport/actions

[Yury G. Kudryashov]

Some updates failed, then many jobs are "Queued"

[Eric Wieser]

image.png

[Kevin Buzzard]

What happened to 4 and 5?

[Eric Wieser]

I think they might be owned by leanprover rather than leanprover-community

[Scott Morrison]

Eric's screenshot was from https://github.com/leanprover-community/mathlib4/settings/actions/runners. Everything looks healthier now!

[Scott Morrison]

As far as I can tell we haven't actually been running mathlib4 CI on the Hoskinson machines at all yet. !4#4539 turns this on.

[Yury G. Kudryashov]

Now we can see that mathport actually fails

[Yury G. Kudryashov]

On MeasureTheory.Function.Jacobian

[Mario Carneiro]

yeah, that's the same failure that was reported before

[Mario Carneiro]

I ran mathport locally to diagnose, but I'm still at the stage "well, I guess _proof_3 is in both of those oleans" until I can figure out how to load the oleans or the tleans to find out who put it there

[Mario Carneiro]

Aha: [translateName] orthonormal_basis.has_coe_to_fun._proof_3 -> _proof_3

[Mario Carneiro]

my guess is that orthonormal_basis.has_coe_to_fun has been #noaligned, which is stored as an alignment to .anonymous, and so its _proof_3 subproof was translated to just plain _proof_3

[Mario Carneiro]

(because spoilers, mathport doesn't actually do anything about #noalign)

[Mario Carneiro]

pushed a fix

[Mario Carneiro]

import Archive.Imo.Imo2005Q4 failed, environment already contains 'Imo.a' from Archive.Imo.Imo1998Q2

seems the archive is still not fixed

[Mario Carneiro]

and now it's on mathport master so we should probably get this fixed soonish

[Damiano Testa]

Ah, I used imo as namespace for the files in imo, so that the theorem names that were the actual full imo problem name would not cause duplicates. I can fix this, but I'm not sure that I'll have time tomorrow. On Monday for sure, though.

[Damiano Testa]

Probably the simplest is to use the filename as namespace and possibly turn off the repeated namespace linter (if it even complains).

[Eric Wieser]

I think we can drop the .imo. part of the namespace if the namespace is archive.imo2005Q4

[Damiano Testa]

Note that namespace imo and end imo should be the only lines that need changing.

[Damiano Testa]

Eric, I did not use archive, just imo.

[Damiano Testa]

A possible solution would be to sed the lines mentioned above with something like sed -i "s=^namespace imo$=namespace ${filename}=" "${filename}" and similarly with end.

[Damiano Testa]

Btw, why was the name clash not picked up by the linter that Eric mentioned?

[Damiano Testa]

To summarise, my mistake has been that I introduced a namespace that would shield src names from names in archive, but it does not shield names clashes between different imo files. For that, using a file-dependent namespace would solve the issue.

[Eric Wieser]

Damiano Testa said:

Btw, why was the name clash not picked up by the linter that Eric mentioned?

Because the linter ran in mathlib3 where the names are a and A

[Eric Wieser]

And mathport is translating them both to a then failing

[Eric Wieser]

Can we solve this by just committing a dummy file to mathlib4 that aligns A to A?

[Eric Wieser]

I would guess the IMO problems want to ignore mathlib naming conventions and actually use the same case as the real problem anyway

[Mario Carneiro]

The naming here is clearly not sustainable. what if another IMO problem has a variable or sequence named a or A?

[Scott Morrison]

This was why I put every IMO problem in its own namespace, but for some reason people didn't like this.

[Yaël Dillies]

I liked this idea, personally. This is what I've already done for the Oxford invariants problem when it was first PRed iirc.

[Mario Carneiro]

I actually thought it was the namespace archive that was considered unnecessary

[Eric Wieser]

Yes, putting every IMO problem in its own namespace was the part of your PR l liked most Scott!

[Damiano Testa]

Ok, #19152 replaces the blanket imo namespace with imoYYYY_qX. I also added nolint dup_namespace profusely and sometimes unnecessarily. Once it passes linting, I will remove the unnecessary nolint attributes.

[Damiano Testa]

The PR passed CI in its first form, with all the nolint dup_namespace. I have now removed the nolint on the declarations that are in fact not actually duplicated.

[Eric Wieser]

@Mario Carneiro, what's next in the process of actually making archive files available to port? It doesn't look like https://github.com/leanprover-community/mathlib3port/commit/4db5aed14bfb7740f99faa340ab2c7dec1c4a72c worked

[Eric Wieser]

Do we just need to change the git add Mathbin upstream-rev README.md lake-manifest.json line?

[Mario Carneiro]

I think so, I just did that

[Yury G. Kudryashov]

One more spacing issue: mathport outputs ∫ x in a.1 ..b.1, f x for an interval integral but Lean 4 accepts only ∫ x in a.1..b.1, f x (no space before ..). Not sure which side needs to be fixed. Note that we also have notation ∫ x in s, f x for an integral over a set, so relaxing the interval notation too much is not an option.

[Scott Morrison]

mathport failed overnight due to the new proofwidgets dependency in mathlib4. Hopefully should be fixed by https://github.com/leanprover-community/mathport/pull/241.

[Yury G. Kudryashov]

Now mathlib3port has Archive/ etc but start_port.sh doesn't support these folders.

[Eric Wieser]

I have a PR open for that

[Eric Wieser]

But right now it's a feature; if you add archive files manually they won't actually be tested in mathlib4 CI yet

[Mario Carneiro]

mathport is down again (expected because of the lean bump), but I'm not having any success using the downloaded cache files: lean crashes with error code 139 on startup, even on files that have already been pre-built from mathlib

[Mario Carneiro]

it seems to work fine in CI though

[Yury G. Kudryashov]

Does lake clean; killall lean; lake exe cache get help?

[Yury G. Kudryashov]

Another thing to try: clean your local cache and redownload.

[Mario Carneiro]

I did rm -rf lake-packages; lake exe cache get and it didn't seem to help

[Mario Carneiro]

currently building mathlib locally to see whether it makes a difference

[Yury G. Kudryashov]

What about ~/.cache/mathlib/?

[Mario Carneiro]

ah, that could be it

[Mario Carneiro]

Just FYI, I have reduced the rate of the "mathport" workflow (which updates mathlib4) to 1/day. It is still useful to keep it running, as it breaks every once in a while due to mathlib4 tactic changes, but it isn't being hammered constantly anymore so this seems like a better use of resources