slow build

Stream: Equational

[David Renshaw]

A local lake build is now very slow for me on this project. Yesterday a clean build took less than 2 minutes. Now it takes more than 10 minutes.

I tried git bisect and the first bad commit is equational#427

[Zoltan A. Kocsis (Z.A.K.)]

Seconded, my laptop is really struggling with building the project now :(

[Johan Commelin]

Was mathlib or lean bumped in the mean time?

[Andrés Goens]

same here (and same on CI)

[Johan Commelin]

In other words, do we expect that this is a problem of the project itself, or the tooling and libraries below it?

[Pietro Monticone]

Yes, it takes more than 50 minutes for the project to build in CI. https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/.E2.9C.94.20Do.20we.20need.20to.20build.20EquationalSearch.20files.3F

[David Renshaw]

Johan Commelin said:

Was mathlib or lean bumped in the mean time?

no

[David Renshaw]

Now it takes more than 10 minutes.

This was a lower bound. I still haven't actually let it run to completion.

[Andrés Goens]

notably, these issues seem to be before equational#427 from the other thread? (probably compounding effects)

[David Renshaw]

When I did git bisect, I tried a clean build at adc92cbf5229250038e8a6591180e959eedb357d, and killed it after 10 minutes.

[David Renshaw]

commits before that take less than 2 minutes (on my local machine)

[Johan Commelin]

https://github.com/teorth/equational_theories/commit/adc92cbf5229250038e8a6591180e959eedb357d

[Johan Commelin]

It is modifying the equation command. Maybe something went wrong there, and now it takes 0.5s per equation? With ~5000 equation commands, that would take ~50m?

[Andrés Goens]

the weird thing is that from a clean build, Equations.lean seems to build relatively reasonably, which seems odd if the elaboration seems to be the culprit (e.g. following a comment by @Eric Wieser in the PR)

[Shreyas Srinivas]

Did the modification of the equation command have something to do with it?

[Andrés Goens]

it's building new theorems for every equation, and doing so by re-elaborating a bunch of stuff

[Shreyas Srinivas]

oh sorry, zulip just decided to reconnect to the network. I see this is being discussed already

[Shreyas Srinivas]

I suggest reverting equational#427 and the dependent equational#429 if someone can confirm this

[Shreyas Srinivas]

If it is agreed, I can do this right away

[Andrés Goens]

Shouldn't we be fixing instead of reverting?

[Shreyas Srinivas]

A new PR could do it yes.

[Shreyas Srinivas]

Let's do it the right way

[Shreyas Srinivas]

I'll setup a task

[Andrés Goens]

e.g. like @Eric Wieser suggested:

It might be better to do this in a more low-level way, rather than re-elaborating the law repeatedly. A hybrid approach would be to elaborate the law once and use Expr.toSyntax to repeat it.

[Andrés Goens]

I don't think that's just it though:

lake lean equational_theories/AllEquations.lean  141,60s user 2,40s system 97% cpu 2:27,18 total

[Andrés Goens]

it takes about 2 mins and a bit to build through AllEquations.lean on my laptop (not a particularly good one tbh), so where are the other 46 coming from?

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/issues/464 is up for claiming and discussions

[Andrés Goens]

Johan Commelin said:

It is modifying the equation command. Maybe something went wrong there, and now it takes 0.5s per equation? With ~5000 equation commands, that would take ~50m?

how did you measure that? on my machine it takes about 2 mins for all 5000

[Shreyas Srinivas]

Is the command being used outside All Equations?

[Andrés Goens]

seems just Equations.lean and AllEquations.lean (Confluence has some commented out)

[Pietro Monticone]

Running equational_theories.Generated.All4x4Tables seems to take a lot of time.

[Shreyas Srinivas]

That's a lot of runs of decideFin

[David Renshaw]

I don't have an explanation, but commenting out two lines brings the build time back down to the reasonable range for me (under 3 minutes): equational#465

[Zoltan A. Kocsis (Z.A.K.)]

@Pietro Monticone
There have only been 4 new contributions to All4x4Tables in the last 4 days. We're only proving like 5 equations about the new magmas, and only one of them is large. Unless this file takes an extreme amount of time, I doubt that recent regressions come from there.

[Shreyas Srinivas]

@David Renshaw : Please claim equational#464 and propose the PR. The CI automation will handle the process and close the issue when equational#465 is merged automatically

[Shreyas Srinivas]

(deleted)

[Johan Commelin]

Pietro Monticone said:

Yes, it takes more than 50 minutes for the project to build in CI. https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/.E2.9C.94.20Do.20we.20need.20to.20build.20EquationalSearch.20files.3F

@Andrés Goens I didn't measure anything, I was just conjecturing, based on :this:
I should have been more clear, sorry

[Shreyas Srinivas]

By claim I mean commenting claim and after that commenting propose PR #465

[Andrés Goens]

David Renshaw said:

I don't have an explanation, but commenting out two lines brings the build time back down to the reasonable range for me (under 3 minutes): equational#465

This sounds like it's the environment extension that's gathering the equations. Maybe having them in the enivroment slows everything else down beacuse this enviroment has to be pouplated into memory even though it's not being used?

[Pietro Monticone]

Shreyas Srinivas said:

By claim I mean commenting claim and after that commenting propose PR #465

propose #PR_NUMBER is also allowed now btw.

[Andrés Goens]

I did get a lot of trouble with my computer running out of memory lately with this project, so that would also fit with this hypothesis :thinking:

[Anand Rao Tadipatri]

If it is the environment extension, I could try to remove it and find another way of gathering the laws, for example by traversing the environment.

[David Renshaw]

An environment extension with ~5000 entries shouldn't cause this kind of slowdown, unless the entries are somehow huge.

[Andrés Goens]

equational#465 did see a ~20 min reduction of the CI time, if I'm seeing it correctly

[Andrés Goens]

and that's just removing the enviroment extension

[Terence Tao]

Given how this issue is impacting the entire project, I'm going to go ahead and approve equational#465 for now and hopefully we can find a more permanent solution later.

[Mario Carneiro]

The environment extension is using an Array instead of a List, this is very bad as it is used persistently

[Mario Carneiro]

I'm not able to reproduce a slowness caused by the two lines in equational#465. (On my branch equational#472 which splits up AllEquations into less monolithic pieces,) the first 1000 equations elaborate in 28.5s with the two lines in question commented out, and 27.7s with them included, so basically within the noise margin

[David Renshaw]

Mario Carneiro said:

The environment extension is using an Array instead of a List, this is very bad as it is used persistently

can you please elaborate on this?

[Mario Carneiro]

In this declaration

initialize magmaLawExt : PersistentEnvExtension Name (Name × NatMagmaLaw) (Array (Name × NatMagmaLaw)) ←
  registerPersistentEnvExtension {
    mkInitial := pure .empty
    addImportedFn := Array.concatMapM <| Array.mapM <| fun n ↦ do return (n, ← mkNatMagmaLaw n)
    addEntryFn := Array.push
    exportEntriesFn := .map Prod.fst
  }

you can see that Array.push is used as the addEntryFn. This function will almost always be called when the input value is shared (because the whole list of all intermediate environments is collected), so this will involve a deep copy of the array every time, resulting in quadratic time and space. If you compare with other PersistentEnvExtension implementations you will see that the running state for values in the current file is always a List or other persistent data structure

[Mario Carneiro]

that said, as I mentioned I have not been able to confirm that this is the source of the performance issue because I can't measure the issue to begin with

[Edward van de Meent]

presumably, using something like docs#Lean.SimplePersistentEnvExtension might be idiomatic use?

[Edward van de Meent]

and perhaps look at how Batteries.Util.LibraryNote.libraryNoteExt is implemented? it does a semi-similar thing...

[David Renshaw]

hm. I'll try switching to List and see if I can observe any difference

[David Renshaw]

If I switch to SimplePersistentEnv then I can uncomment the updateEnv lines and it still builds in a reasonable amount of time.

[Andrés Goens]

David Renshaw said:

If I switch to SimplePersistentEnv then I can uncomment the updateEnv lines and it still builds in a reasonable amount of time.

is this with equational#472?

[Andrés Goens]

or even before?

[David Renshaw]

I did not pull that in.

[David Renshaw]

This is on main.

[David Renshaw]

equational#476

[David Renshaw]

though note my comment about not understanding the purpose of the existing logic in addImportedFn

[David Renshaw]

I updated the PR summary. The main lesson, I think, is that PersistentEnvExtension has a complex interface that is easy to use suboptimally, and that we were using it suboptimally.

[Anand Rao Tadipatri]

If a file has two imports which in turn import AllEquations.lean, then maybe the extension gets computed twice, contributing to a slowdown.

[Anand Rao Tadipatri]

Thank you for your help in diagnosing and fixing the issue, and I'm sorry for the slowdown that this PR has caused.

[David Renshaw]

If a file has two imports which in turn import AllEquations.lean, then maybe the extension gets computed twice, contributing to a slowdown.

I believe that Lean is smarter than that about transitive imports.

[David Renshaw]

(or at least i hope so!)

[Joachim Breitner]

Your hope may be too optimistic:

The addImportedFn runs at the beginning of elaboration for every module

Did you see the docs at https://leanprover-community.github.io/mathlib4_docs/Lean/Environment.html#Lean.PersistentEnvExtension?

[Joachim Breitner]

So yes, it seems prudent for addImportedFn to simply store the array of arrays as it is, so that import is quick, and then only in getMagmaLaws do actual work.

[David Renshaw]

It depends on the relative costs, right?
Such as:

1. How much work is it to serialize/deserialize NatMagmaLaw data?
2. How much space does NatMagmaLaw data take on disk and in memory?
3. How much work does mkNatMagmaLaw take?
4. How often will we be calling getMagmaLaws?

If (1) and (2) are sufficiently large and (3) and (4) are sufficiently small, then I agree with your assessment.

[David Renshaw]

But unless we have evidence that we are in that regime, I feel like we should stick to the simpler setup (SimplePersistentEnvExtension).

[Mario Carneiro]

I have a new version of the equation command (equational#478), which only takes 6s instead of 28s to elaborate the first 1000 equations. Regarding the env extension, I replaced it with a tag extension because we can recover the MagmaLaw object on the fly by interpreting the stored Expr for it.

[Shreyas Srinivas]

The CI is definitely going to fail on the AllEquations split PR unless every script relying on that file is altered. The diagram generating scripts are run separately on the CI, so lake build will still pass unless something in the lean code is broken.

[Shreyas Srinivas]

It seems there is breakage in lean files too (not related to the above) : https://github.com/teorth/equational_theories/actions/runs/11264558737/job/31324777398?pr=478

[Mario Carneiro]

I already changed every script relying on that file in the PR

[Mario Carneiro]

unless there are more scripts not in the repo

[Shreyas Srinivas]

The CI in equational#472 is breaking on one of these scripts

[Shreyas Srinivas]

Here

[Shreyas Srinivas]

There are three unusual steps in the blueprint action file of this project which use non-lean scripts:

 - name: Generate home_page/implications/implications.js
        run: |
          ~/.elan/bin/lake exe extract_implications outcomes > /tmp/out.json
          pip install markdown
          python scripts/generate_equation_implication_js.py /tmp/out.json

      - name: Generate the Finite Magma Explorer website
        run: |
          mkdir -p home_page/fme
          cp -r tools/fme/dist/* home_page/fme
          ~/.elan/bin/lake exe extract_implications unknowns > home_page/fme/unknowns.json
          COMMIT_HASH=$(git rev-parse --short HEAD)
          sed -i "s/VERSION_UNKNOWN/$COMMIT_HASH/g" home_page/fme/index.html

  - name: Generate home_page/graphiti/graph.json
        run: |
          ~/.elan/bin/lake exe extract_implications --json > /tmp/implications.json
          ~/.elan/bin/lake exe extract_implications unknowns > /tmp/unknowns.json
          ruby scripts/generate_graphiti_data.rb /tmp/implications.json /tmp/unknowns.json > home_page/graphiti/graph.json

[Mario Carneiro]

it looks like I just forgot to save that file

[Shreyas Srinivas]

In equational#478, the docs build has a number of warnings like:

 WARNING: Failed to calculate equational lemmata for Lean.PrettyPrinter.Delaborator.mkDelabAttribute: (kernel) invalid declaration, it uses unsafe declaration 'Lean.PrettyPrinter.Delaborator.mkDelabAttribute'

[Shreyas Srinivas]

Is this expected?

[Mario Carneiro]

no, I have not seen that error message before

[Mario Carneiro]

I think this might be normal, it also occurs on master

[Mario Carneiro]

it seems like docgen is just pretty chatty and/or doesn't know not to generate equational lemmas for unsafe declarations

[Shreyas Srinivas]

Yeah it is also present in past runs of the CI

[Shreyas Srinivas]

equational#478 builds in 26 minutes. If it can be merged independent of equational#472 , I would like to do it right away

[lyphyser]

could also keep the monolithic AllEquations.lean file but not actually include it in the build

[Shreyas Srinivas]

Then it is an unbuilt file that passes CI not matter what

[Shreyas Srinivas]

equational#472 fails CI

[Shreyas Srinivas]

This was one of those scripts. Additionally merging equational#478 creates a merge conflict

[Amir Livne Bar-on]

We can switch these scripts to use the output of "export_equations"

[Terence Tao]

I would prefer not to have two copies of AllEquations as it greatly increases the chance that any subsequent update (eg., transferring an equation from AllEquations to Equations) will be done incorrectly.

There was at some point a tool added that could export AllEquations to JSON format in https://github.com/teorth/equational_theories/pull/429 . I was thinking that it might better in the long term to have all other tooling based on such a JSON file, so that any future refactoring of AllEquations only needs to update the export to JSON, but perhaps the current ad hoc fix of manually adjusting all tools that import from AllEquations is sufficient.

[Shreyas Srinivas]

I would like to request the authors of the scripts for please check equational#472 which makes changes to them and confirm that the changes are fine.

1. The implications script
2. The finite magma explorer
3. The graphiti feature

[Vlad Tsyrklevich]

Graphiti script update looks fine

[Shreyas Srinivas]

I merged equational#472, because fixing issues arising from these scripts will be easier with a faster CI (also CI passes for now). But please do check for 1 and 2.

[Michael Bucko]

Every time I build (had to do it multiple times) on a Macbook lake buildtakes at least 3 hours (testing now again - Oct 19th).

Is it maybe common for Lean projects to have their docker releases? Or are we expecting that lake build should always take max 20 minutes or so?

[Shreyas Srinivas]

Did you first run lake exe cache get?

[Pietro Monticone]

@Michael Bucko consider running scripts/run_before_push.

[Shreyas Srinivas]

Without running the cache command, lake build will also be building all of Mathlib and its dependencies

[Michael Bucko]

Shreyas Srinivas schrieb:

Did you first run lake exe cache get?

I did it earlier, but not this time. I'll make sure to always run this one, too.

[Michael Bucko]

Pietro Monticone schrieb:

Michael Bucko consider running scripts/run_before_push.

Thank you. Gonna check it out, too!