ideas for speeding up CI

Stream: mathlib4

[Scott Morrison]

We have quite a few CI runs in which either nothing, or only a handful of files, needs to be compiled. Typical timings for such runs are:

• 30s of get cache
• 10s of build
• 20s of upload cache
• 150s of archive
• 30s of counterexamples
• 60s of test
• 900s of lint

I think there is some low hanging fruit here!

• When would it be safe to skip the lint step? Presumably if there is nothing to compile at all, it is safe to skip the linting step? (Unless we are tweaking the linter script itself?)
• Can we just cache the archive, thereby saving much of the 150s for most runs? I recall when we ported the archive there was some objection to doing so, but I forget the reasoning.

[Ruben Van de Velde]

I think the argument might have been "nobody depends on anything from the archive", but it could also be something else

[Ruben Van de Velde]

I wonder if it's easy to profile where all the lint time goes

[Johan Commelin]

Most likely the simpNF linter

[Eric Wieser]

I assume the hesitation in caching the archive is just that it's a waste of storage space in some sense?

[Eric Wieser]

Do we have any way currently to ask our cache server "how much disk space are you using for each Lean package?"?

[Damiano Testa]

Do the "lean" linters run on Archive/Counterexamples? If they do not, then running them on PRs that only change files in these folders would not be needed, since these files are not imported back by Mathlib, right?

[Damiano Testa]

Also, most of the times, I want to see that mathlib builds. It would be nice if there were at least the option of skipping the builds of Archive/Counterexamples/test/final linting. Something like a flag "just build mathlib".

[Damiano Testa]

Moreover, I know that I have been surprised several times by the global effects of changes in mathlib files, but, if I modify a leaf file, can the simpNF linter fail on a declaration not in the leaf file? Does it need to run on the unmodified files to know its effect on the new leaf? Maybe there is something that the linting can cache that would allow it to run just on a fragment of mathlib? (I know that I am talking about things that I do not understand, so this may be nonsense.)

[Eric Wieser]

@Damiano Testa, I don't really follow why you need flags because you "want to see that mathlib builds."; you can just click the build job and see a green tick next to the mathlib step

[Damiano Testa]

Eric, I do that. My suggestion was in order to avoid running extra checks that I normally do not care about until later in the PR process. I normally wait until there is a mathlib cache and after that I am happy!

[Damiano Testa]

Although maybe the thread was "speeding up CI but not giving up on doing all the checks".

[Scott Morrison]

The simpNF really is global, and without careful thinking/extra work needs to see the whole library, and can't assume that local changes have local effects.

[Scott Morrison]

@Damiano Testa, the extra checks already only run later in the PR process?

[Scott Morrison]

I guess we should be able to refactor to parallelize archive / counterexamples / test / lint.

[Scott Morrison]

I don't think there are actual dependencies between those.

[Damiano Testa]

Ok, my suggestions were "I would be happy to give up on some checks most of the times and would be happy to have the option of not running them sometimes". I realize now that this was not the idea of this thread.

[Scott Morrison]

I think one reason we haven't previously been caching archive is because this would postpone upload cache, but of course this could be solved simply by doing an upload step separately after build / archive / counterexample.

[Damiano Testa]

One thing that I think can be done is not building Archive/Counterexamples unless they import a file that is changed by the current PR, right?

[Jireh Loreaux]

That already happens, we build incrementally.

[Scott Morrison]

That's true. But if we could decide that it's okay to cache the oleans in archive and counterexamples, then there is a simple way to do this without any new logic.

[Damiano Testa]

So, if I add a leaf file, then Archive/Counterexample and maybe also test should not be affected.

[Scott Morrison]

@Jireh Loreaux I think the problem is that we always rebuild archive and countexamples from scratch, because they are not cached.

[Jireh Loreaux]

Oh I see

[Scott Morrison]

Working out how to do incremental building for test might be a good idea. Can we just make test a proper subproject like archive and counterexample, rather than just a "please run everything" makefile?

[Damiano Testa]

I find that in a lot of my PRs, building mathlib takes way less time than either one of Archive/Counterexamples/test. Of course, this depends on how "deep" the PR is, but all those checks are usually unnecessary.

[Scott Morrison]

Here's an idea that could speed up the linter, I think, despite the non-locality. We could synthesize a new file that imports all changed files and everything downstream of the changed files, and only run the linter on that.

Sometimes of course this would end up being very close to import Mathlib. But often it would not, for "side branches" of Mathlib.

[Damiano Testa]

Does anyone have an example of a change in a later file that can make linting fail on an earlier file? I know that you can add a module doc in a later file to appease the docs-linter, for instance, but I am wondering about the opposite: if the linter was happy without the later file, can it become unhappy on the earlier file by adding the new one?

[Matthew Ballard]

Scott Morrison said:

I guess we should be able to refactor to parallelize archive / counterexamples / test / lint.

Can’t everything after build be done in parallel?

[Yaël Dillies]

Yes, Damiano. Simply duplicate an earlier simp lemma in a later file and tag it simp as well. simp_nf will complain. In fact, you can do that with any two files, so Scott's "side branches of mathlib" idea doesn't for simp_nf.

[Eric Wieser]

Matthew Ballard said:

Scott Morrison said:

I guess we should be able to refactor to parallelize archive / counterexamples / test / lint.

Can’t everything after build be done in parallel?

No, the linter in principle needs to run on all of archive/counterexamples/mathlib simultaneously

[Eric Wieser]

Maybe we only lint mathlib for now though

[Eric Rodriguez]

Damiano, it's even possibly non-trivially - I somehow did it with the little wedderburn PR (that is, cause simpnf changes whilst changing a leaf file) - I didn't even need simp lemmas, just some instance!

[Mario Carneiro]

I think the obvious solution to the Archive build situation is to just make it a separate project, with its own update schedule with a lower frequency than mathlib master

[Eric Wieser]

I'm not sure that's a good idea; a big part of reviewing new archive submissions is "this lemma looks useful, can you move it to mathlib proper?". This is a lot harder if new contributors now have to learn how to bump mathlib in the archive repo

[Mario Carneiro]

mathlib maintainers (or CI) would be responsible for bumping the archive

[Mario Carneiro]

the situation is fairly analogous to mathlib bumps of std

[Mario Carneiro]

generally, an archive PR would not involve bumping mathlib

[Kevin Buzzard]

Archive submissions represent an extremely small proportion of PRs to mathlib and if they're causing a disproportionate amount of slowdown then perhaps the disadvantages outweigh the advantages.

[Damiano Testa]

@Yaël Dillies I think that this is different from the example that I wanted. I was looking for a failure on the old file. I understand that errors in the new file may depend on what the file imports. I was just wondering if it was possible that something would be flagged as failing on the earlier file, because of something in the later file.

[Damiano Testa]

@Eric Rodriguez that sounds like it might be an example: can you be more specific about what broke earlier?

[Damiano Testa]

Basically, my question is "can you cache something smallish from a previous run of the linter so that adding a leaf, means you only have to process the leaf, using the cached information, instead of having to recompute everything from scratch.

I suspect that the answer is "you cannot do this", but I do not have a clear example of what can go wrong.

[Jireh Loreaux]

I do think having linting as a separate step that must be triggered manually could be helpful, even though bors would still require it before merging. That is by far the biggest time suck.

[Eric Rodriguez]

Damiano Testa said:

Eric Rodriguez that sounds like it might be an example: can you be more specific about what broke earlier?

I think the instance of field from finite division ring broke stuff in instance search and made it slower, therefore causing the linter to go past timeout. But I wasn't able to investigate easily, because I think the notations for the brackets in algebra.adjoin collide with the notation manifolds people use for C(infty) and such like, so importing one file into the other broke a lot

[Eric Rodriguez]

So I'm not fully sure what's happened

[Damiano Testa]

Eric, thanks for the details! Anyway, I was just trying to find out whether keeping a tally of a bunch of data from a previous run might make it quicker for a later run. However, whether this is reasonable and achievable is something that requires a very deep knowledge of the linters and, to be honest, I do not even know what it is that they check... :shrug:

[Eric Wieser]

Kevin Buzzard said:

Archive submissions represent an extremely small proportion of PRs to mathlib and if they're causing a disproportionate amount of slowdown then perhaps the disadvantages outweigh the advantages.

Note that the slowdown is only disproportionate for

CI runs in which either nothing, or only a handful of files, needs to be compiled.

which also represent a reasonable small proportion of PRs to mathlib

[Eric Wieser]

As I see it, we have a choice between:

1. Pay the 150s build time cost by doing nothing
2. Pay the unknown storage space cost by turning on caching for Archive
3. Pay the maintenance and contribution burden of having separate repos

It would be good to have an estimate available for option 2 to decide whether the cost is negligable, before deciding on option 3.
Certainly for the CI runs in question, the storage cost is zero (since the archive wouldn't be rebuilt at all). A more reasonable metric would be the total (compressed) olean size of Archive vs the rest of mathlib as a whole

[Kevin Buzzard]

re archiving archive: I have never been bothered by build time costs because I am never in a hurry, I just reacted because I've never really felt that the archive was part of mathlib, but somehow that's probably another debate (and one which we've had before).

[Mario Carneiro]

Note that option 2 won't actually save us the build time cost, because it still has to be rebuilt on most commits to mathlib

[Mario Carneiro]

Also option 3 is not the only way to achieve the build savings of option 3 - we can just not build the archive on most builds. The drawback is that it's awkward to have an archive that builds on a version of mathlib which doesn't match the one in the adjacent folder

[Eric Wieser]

Mario Carneiro said:

Note that option 2 won't actually save us the build time cost, because it still has to be rebuilt on most commits to mathlib

I'm not sure how true that is. At the extreme end of the spectrum, we seem to bump Std almost every day, which means we end up with an hour of rebuild anyway. 2.5min/hour isn't much overhead

[Eric Wieser]

Perhaps we should temporarily turn the cache on and see whether people notice?

[Kyle Miller]

Re Mario's suggestion for 3: Could we have it where CI doesn't build the archive but bors does? (Could we have a command issued in a PR comment to build the archive? That way a reviewer can get an assurance that it builds before merging.)

Without really understanding all the issues, I like Scott's suggestion from earlier, where we build mathlib, archive, and counterexample, and upload the cache after each. Maybe they could each do their own get cache? I wouldn't mind if by default lake exe get cache only gets the main mathlib cache and if you had to do something special to download the archive and counterexample ones.

[Damiano Testa]

Besides, when I open a file in VSCode, I get the impression that it gets processed whether or not there is an available cache: the cache seems to prevent dependencies of that file from being processed, but not the file itself, right? Since the files in Archive/Counterexamples are shallow, in the sense that they (only?) import files from Mathlib, their cache seems to be never used locally anyway... is this correct?

[Damiano Testa]

Ah, except probably lake build would notice if there is or not a cache for such files.

[Mario Carneiro]

There isn't much point in loading that cache though:

• If the archive file has changed, it needs to be rebuilt and the cache is useless
• If the dependencies have changed and the archive has not, it needs to be rebuilt and the cache is useless (only the mathlib cache is used)
• If the dependencies have not changed and the archive file has not, it does not need to be rebuilt and if we aren't making an archive cache then we don't need to do anything, and the cache is useless

[Kyle Miller]

If the archive file has changed, it needs to be rebuilt and the cache is useless

If one file is changed in the archive, why wouldn't a cache prevent the rest of the files from being rebuilt?

only the mathlib cache is used

Is it the case that if any of mathlib is changed, then that would invalidate the entire archive cache? (I guess because it depends on Mathlib.lean?)

[Mario Carneiro]

More precisely, what lake actually needs is the trace for the file dependency job, which only includes the hash of the file contents and the combined hash of the includes. If you upload that trace file (just a file with a number in it), then lake will not rebuild it

[Mario Carneiro]

but also, we could just hack lake if necessary if it doesn't have the right behavior

[Scott Morrison]

Mario Carneiro said:

• If the dependencies have not changed and the archive file has not, it does not need to be rebuilt and if we aren't making an archive cache then we don't need to do anything, and the cache is useless

@Mario Carneiro, I don't understand this point. If neither Mathlib nor archive have changed, currently we build all of archive.

[Mario Carneiro]

@Scott Morrison I'm not describing the current setup, I'm describing the minimum build requirements assuming we have everything working as intended

[Mario Carneiro]

If neither mathlib nor archive has changed, of course we need to build nothing and we don't need the cache either since we aren't building anything

[Scott Morrison]

But just thinking about Mathlib: if nothing has changed, the way we avoid building anything is by having the cache available!

[Mario Carneiro]

determining that neither mathlib nor the archive has changed requires the mathlib cache (to see that the imports are still good), plus hashing the archive files (the .lean files)

[Scott Morrison]

Okay. My instinct is that you're suggesting we build extra tooling which is fairly specific to the archive, and I just care less about the archive and would like an easy path to getting it out of every CI run.

[Mario Carneiro]

that is, a hypothetical "archive cache" would want to store a list of hashes of (mathlib imports to file Archive.X + text of Archive.X) which have successfully been compiled

[Mario Carneiro]

and no oleans

[Mario Carneiro]

I think the "easy path" is moving it from mathlib to a separate project :shrug:

[Scott Morrison]

So it seems the alternatives are:

• with very little effort, we turn on olean caching for the archive, and the problem goes away, at the expense of some wasted disk and network resources
• a hypothetical person implements this hypothetical archive cache. :-)

[Scott Morrison]

That (moving it to a separate project) I can agree with. :-)

[Scott Morrison]

The steps there are:

• get agreement to move to a separate project (mathlib maintainers?)
• rip everything out into a separate repo
• let it sit there until someone asks to be the designated maintainer of the archive
• mathlib maintainers say "yes please" and hand it off?

[Mario Carneiro]

I have already implemented many features in lean-cache to support more flexibility of caching, but it's near the limit of what can be done without actually doing some deployment and testing

[Mario Carneiro]

(reminder, it already ticks the "fast no-op" box, it's about 190ms on mathlib)

[Scott Morrison]

How about we do everything?

• I make a PR (today?) that just turns on the current caching infrastructure for archive, with a big nerd-sniping comment on it saying "This is dumb, we shouldn't be caching these oleans just to avoid building."
• We plan that if /Archive/ still exists by the time lean-cache is deployed, it will replace that hack.
• Simultaneously we begin seeing if there is consensus for splitting out the archive / finding a maintainer?

[Mario Carneiro]

it's very easy to modify lake exe cache so that it doesn't upload the olean files for the archive, only the olean.trace files. I haven't tested that lake will do the desired thing in that case though

[Ruben Van de Velde]

Isn't the whole point of the archive that it's maintained along with mathlib?

As a simple solution, would it help to move the archive under Mathlib/?

[Mario Carneiro]

mathport is also maintained along with mathlib but that doesn't mean it has to track every single commit

[Scott Morrison]

I would be happy to spin up the CI that tries to bump the lean-toolchain and Mathlib dependency of an Archive repository daily, and emails/zulips the relevant maintainers if there is a failure.

[Kyle Miller]

I like the friendliness of a monorepo. If we split off Archive, I expect we'll see the following:

• there will be fewer contributions because people will be less aware of it
• its PR queue will get significantly less attention by maintainers
• reviews will be much less likely to suggest moving useful bits into mathlib because of how much more of a pain it is dealing with multiple projects (and my impression is that many people who contribute to mathlib are exposed to git for the first time via mathlib)
• refactors will rarely take into consideration how they break the Archive (I've redesigned refactors because of this before)

I've found the Archive to also be useful as an extra test suite of more realistic Lean code than what's in the test folder.

@Scott Morrison Wouldn't moving it into a separate project be sort of going in a direction opposite of your previous comments that ideally big Lean projects should be contributed to mathlib?

Maybe instead of splitting it off it'd be better if we scavenged the archive for more library code, if even after turning on caching it's taking a large amount of CI time.

[Scott Morrison]

My goal in this thread is to get rid of the 150s in every CI run spent on Archive. I am mostly very happy to keep Archive, and I think we've now demonstrated that we're not getting rid of it. Thus I think there are two good plans, which can be executed simultaneously:

• I make a PR (today?) that just turns on the current caching infrastructure for archive, with a big nerd-sniping comment on it saying "This is dumb, we shouldn't be caching these oleans just to avoid building."
• We plan that by the time lean-cache is deployed, it will replace that hack.

[Johan Commelin]

Sounds good to me

[Scott Morrison]

Eric Wieser said:

Can’t everything after build be done in parallel?

No, the linter in principle needs to run on all of archive/counterexamples/mathlib simultaneously

@Eric Wieser, I think this is false, and the mathlib linter actually ignores archive and counterexamples.

[Eric Wieser]

the "in principle" was load bearing :)

[Scott Morrison]

Archive.Imo.Imo1960Q1 takes much longer than the rest of the Archive to build, if anyone would like to investigate that.

[Scott Morrison]

Ugh, it is a brute force search that probably shouldn't have been merged in the first place.

[Scott Morrison]

It was much faster in mathlib3.

[Yaël Dillies]

@Bhavik Mehta has been discussing this on Xena. We haven't yet managed to pinpoint what exactly makes those proofs so slow. Very weird...

[Johan Commelin]

theorem left_direction (n : ℕ) (spn : SolutionPredicate n) : ProblemPredicate n := by
  -- Porting note: This is very slow
  -- rcases spn with (rfl | rfl) <;> refine' ⟨_, _, _⟩ <;> norm_num
  rcases spn with (rfl | rfl) <;> refine' ⟨_, by decide, _⟩ <;> rfl

Using norm_num reduces this from ~20s to ~8s on my laptop.

[Johan Commelin]

But that still seems ridiculously slow.

[Johan Commelin]

Of course this is the "easy" direction.

[Bhavik Mehta]

Scott Morrison said:

It was much faster in mathlib3.

Yes, there are a ton of searches involving Lists/Finsets that are significantly slower in mathlib4 than in mathlib3 - @Chris Hughes condensed one of my examples to

theorem parts_property :
    ∀ (y : Fin 4 → Fin 2)
      (_ : y ∈ ({![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0]} :
        List (Fin 4 → Fin 2))), True := by
  decide

which times out in Lean 4 but is very fast in Lean 3. (My actual case was a brute force search for a problem where the proof on paper is "brute force search", to help prove values of small ramsey numbers, it's fast in Lean 3 after doing appropriate reductions but massively slow in Lean 4).

One difference is that Lean 4 doesn't infer the Decidable instance as List.decidableBall, but rather something else (which imo is a sign we should increase the priority of this instance and similar ones); but even increasing the priority of this instance locally it's still way slower in Lean 4. This is one of the main blockers to porting one of my projects to Lean 4...

[Scott Morrison]

It would be great to have a mathlib-free minimisation!

[Bhavik Mehta]

I agree! I've been trying but I haven't quite figured one out yet... but I'll stop talking about this slowdown in this particular thread to avoid derailing

[Johan Commelin]

@Scott Morrison Do you agree that a brute force computation is a morally correct formal solution to this IMO problem? Or should we go for a more theoretical solution anyways?

[Johan Commelin]

81 cases seems legit to me. We should support such solutions, I think.

[Scott Morrison]

I think for an IMO problem a brute force search should at least be fast for the computer.

[Johan Commelin]

Right. But this particular solution ought to check in < 1s. And probably even < 0.1s. So I'm inclined to keep it as is, as a benchmark.

[Scott Morrison]

I agree. When I complained above it this being merged in the first place I incorrectly assumed it was always slow.

Porting a benchmark by adding a huge maxHeartbeats maybe wasn't ideal. :-)

[Johan Commelin]

Well, we wanted to get the port done. But we should certainly track this issue. Maybe even with a GH issue.

[Scott Morrison]

Here's a surprising result. Guess which is the slowest linter (by worst case)?

[Scott Morrison]

430.063014 unusedArguments RingHom.RespectsIso.ofRestrict_morphismRestrict_iff
201.888680 simpNF AlgebraicGeometry.StructureSheaf.isLocallyFraction_pred
182.304759 simpNF Rep.MonoidalClosed.linearHomEquivComm_hom
179.932156 simpNF Rep.MonoidalClosed.linearHomEquiv_hom
145.505241 simpNF Matrix.linfty_op_nnnorm_row
119.100756 simpNF lp.infty_coeFn_nat_cast
118.556040 simpNF CategoryTheory.OplaxNatTrans.whiskerRight_naturality_comp_assoc
118.393575 simpNF lp.infty_coeFn_int_cast
116.262702 simpNF Matrix.linfty_op_norm_col
95.031026 simpNF CategoryTheory.OplaxFunctor.bicategory_comp_naturality
94.551145 simpNF AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv

[Scott Morrison]

I'll post the full results somewhere shortly when sort finishes. :-)

[Bhavik Mehta]

Scott Morrison said:

I think for an IMO problem a brute force search should at least be fast for the computer.

I'm not sure it's fair to classify this direction as a brute force search by the way (unless I'm missing something), it's only checking 2 numbers and doing numeric calculations on them...

[Yaël Dillies]

I'm... not surprised :grinning_face_with_smiling_eyes:

[Johan Commelin]

@Bhavik Mehta It's running through 82 cases. That's not what a pen-and-paper proof would look like (hopefully).

[Johan Commelin]

So I think it's an example of brute force search. Even if it is only a very mild example.

[Scott Morrison]

https://gist.github.com/semorrison/77099dc8a5743b2b53715ddf8fdcd615 is the top 1000 slowest lints. If anyone wants the complete output I can send them a 62mb gzip. :-)

[Johan Commelin]

That top entry is certainly surprising! But otherwise, lots of simpNF, as expected.

[Scott Morrison]

Bhavik Mehta said:

theorem parts_property :
    ∀ (y : Fin 4 → Fin 2)
      (_ : y ∈ ({![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0]} :
        List (Fin 4 → Fin 2))), True := by
  decide

@Bhavik Mehta, do you have the imports for this?

[Bhavik Mehta]

Johan Commelin said:

Bhavik Mehta It's running through 82 cases. That's not what a pen-and-paper proof would look like (hopefully).

left_direction is only running through two cases - which is the one with the porting note that you profiled above

[Bhavik Mehta]

Scott Morrison said:

Bhavik Mehta said:

theorem parts_property :
    ∀ (y : Fin 4 → Fin 2)
      (_ : y ∈ ({![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0], ![1, 1, 0, 0]} :
        List (Fin 4 → Fin 2))), True := by
  decide

Bhavik Mehta, do you have the imports for this?

import Mathlib.Data.Matrix.Notation

[Johan Commelin]

@Bhavik Mehta I see. I thought the discussion had shifted to the decl with the maxHeartbeats option.

[Bhavik Mehta]

More importantly, however, I'm pretty sure the slowdowns in this file are caused by something different to the one I mentioned and have been discussing with Yaël, so parts_property was a genuine derail. Apologies!

[Bhavik Mehta]

Johan Commelin said:

Bhavik Mehta I see. I thought the discussion had shifted to the decl with the maxHeartbeats option.

Perhaps it had and I misunderstood!

[Scott Morrison]

Okay, doing the naive thing caching Archive and Counterexamples speeds up 180s to about 45s. #6945

[Notification Bot]

11 messages were moved from this topic to #mathlib4 > diagnosing timeouts in RingHom.RespectsIso.ofRestrict_mor... by Scott Morrison.