cache misses aesop

Stream: mathlib4

[Yaël Dillies]

Am I the only one having to rebuild all of aesop every time I restart the server?

[Rida Hamadani]

I had to rebuild everything when I worked on gitpod today, which has never happened to me before.

[Ruben Van de Velde]

Yeah, batteries as well

[Peter Nelson]

Me too - I have to rebuild everything (not just aesop) even after a fresh clone and lake exe cache get.

[Ruben Van de Velde]

I'm thinking we should revert #13808 @Kim Morrison

[Ruben Van de Velde]

Though the output looks like

✔ [956/4954] Built Aesop.Main:c.o
✔ [957/4954] Built Aesop.Main:dynlib
✔ [959/4954] Built Aesop:c.o
✔ [960/4954] Built Aesop:dynlib

I wonder...

[Ruben Van de Velde]

False accusation, it starts with #13789

[Ruben Van de Velde]

-testDriver = "test"
-precompileModules = false # We would like to turn this on, but it breaks the Mathlib cache.
+testDriver = "AesopTest"
+precompileModules = true

[Ruben Van de Velde]

@Jannis Limperg

[Matthew Ballard]

It breaks the benchmarking also

[Jannis Limperg]

I'll revert. @Mac Malone it seems precompilation breaks the Mathlib cache after all.

[Jannis Limperg]

#13835

[Jannis Limperg]

Sorry for the disruption.

[Sebastian Ullrich]

It seems the "check the cache" test did not catch this as it only tries to restore Mathlib .oleans https://github.com/leanprover-community/mathlib4/actions/runs/9511124129/job/26216720180#step:16:6

[Sebastian Ullrich]

And here I was wondering why live.lean-lang.org spent all morning repeatedly recompiling Mathlib

[Peter Nelson]

How long until this is fixed from the perspective of a regular mathlib user? I'm teaching lean in front of a class in a couple of hours.

[Ruben Van de Velde]

Can you use a mathlib from yesterday?

[Peter Nelson]

That gives me the 'wrong infoview' bug to contend with, which is also not ideal.

[Yaël Dillies]

Peter Nelson said:

How long until this is fixed from the perspective of a regular mathlib user? I'm teaching lean in front of a class in a couple of hours.

I think it will be fixed when @Kim Morrison does the update, which is once a day

[Ruben Van de Velde]

@Peter Nelson this should work now

[Peter Nelson]

Thanks!

[Mac Malone]

Jannis Limperg said:

I'll revert. Mac Malone it seems precompilation breaks the Mathlib cache after all.

This is because mathlib does not yet set platformIndependent := true in its lakefile.

[Mac Malone]

(Lake defaults to asssuming packages are platform-dependent.)

[Kim Morrison]

Yaël Dillies said:

Peter Nelson said:

How long until this is fixed from the perspective of a regular mathlib user? I'm teaching lean in front of a class in a couple of hours.

I think it will be fixed when Kim Morrison does the update, which is once a day

Which update? Dependency updates are now (at least, should be, new CI is invariably broken) automatic.

[Yaël Dillies]

Oh sorry I thought you had closed the PR, but I now remember that this the PR about shake. I can't see the automatic update though. https://github.com/leanprover-community/mathlib4/commit/7fa489a5cbf3c4f08d36e1e0b5dee4d761fdbd9b doesn't seem very automatic.

[Kim Morrison]

It's in .github/workflows/update_dependencies.yml. I haven't had a chance to look if it is working. If you would like to debug, help appreciated. :-)

[Yaël Dillies]

I actually don't know where the logs go to, nor where I should be expecting to run ("every hour" okay, but there isn't always something to update)

[Jannis Limperg]

Mac Malone said:

Jannis Limperg said:

I'll revert. Mac Malone it seems precompilation breaks the Mathlib cache after all.

This is because mathlib does not yet set platformIndependent := true in its lakefile.

Should this be done and should we then try again? Precompiled Aesop is ~30% faster on the test suite, though likely somewhat less on Mathlib.

[Sebastian Ullrich]

Let's test it on separate branches first?

[Jannis Limperg]

#13891 sets platformIndependent := true in Mathlib and enables Aesop precompilation. In my manual tests, the cache works, both when I check out the PR branch in a new clone of Mathlib and when I create a new project that depends on Mathlib.

However, the speed center's benchmarking script appears to break.

[Jannis Limperg]

Actually, the cache also doesn't work. Repro:

$ git clone https://github.com/leanprover-community/mathlib4
$ cd mathlib4
$ git switch jannis/aesop-precompilation
$ lake exe cache get
-- succeeds
$ lake build
-- compiles Aesop (expected) and all files depending on Aesop (unexpected)

@Mac Malone could you take a look?

[Mac Malone]

@Jannis Limperg I suspect the problem is that Aesop itself does not use platformIndependent = true.

[Jannis Limperg]

Ah, okay. Btw what's the meaning of this flag exactly?

[Jannis Limperg]

Nvm, found the docs. Thanks for the help!

[Mac Malone]

@Jannis Limperg If you still encounter a problem once Aesop is also platform-independent, feel free to ping me again!

[Sebastian Ullrich]

@Jannis Limperg When you have a fixed version of the branch, I'm happy to look at the benchmarking failure. It seems to be the proxy of leanc is broken, as it has never been necessary before

[Jannis Limperg]

@Mac Malone The issue unfortunately seems to persist when I set platformIndependent = true in Aesop's lakefile.toml. :( The repro above is still relevant.

[Mac Malone]

@Jannis Limperg :cry: I will debug and see if I can fix the issue.

[Mac Malone]

@Jannis Limperg Found the bug. Fix is at lean4#4478. Added a test to prevent this problem in the future. If you want, I can bump aesop / the mathlib PR to this toolchain to verify everything works as expected before this goes live.

[Yaël Dillies]

The problem is back on rc2 :sweat:

[Kim Morrison]

@Yaël Dillies, could you clarify? It seems unlikely this has regressed.

[Yaël Dillies]

Okay, I thought it was fixed by the bump to rc2 but apparently it was fixed a bit later? My branch seems to have been on that intermediate version

[Jannis Limperg]

Yes, it was fixed in dc44afb4353b441dfdbca70458574c5b4be98b32.

[Jannis Limperg]

Mac Malone said:

Jannis Limperg Found the bug. Fix is at lean4#4478. Added a test to prevent this problem in the future. If you want, I can bump aesop / the mathlib PR to this toolchain to verify everything works as expected before this goes live.

Beautiful, ty! I'll test with the PR toolchain.

[Jannis Limperg]

Seems to work now: lake exe cache succeeds and lake build only builds the platform-specific Aesop code. :tada:

[Sebastian Ullrich]

Do we have a Mathlib !bench yet? lake exe cache get && lake build overhead would also be interesting

[Jannis Limperg]

!bench is running: http://speed.lean-fro.org/mathlib4/task-detail/725191f8-ef40-4b90-ab00-2763d647e258

[Jannis Limperg]

On my system and with my internet connection, lake exe cache get takes ~40s with a clean checkout and clean ~/.cache/mathlib. lake build then takes another 50s. So the overhead is not great.

[Jannis Limperg]

!bench failed, same error as before: leanc reports unknown command /usr/bin/time.

[Jannis Limperg]

Sebastian fixed the benchmark script, so we now have a performance comparison between no precompilation and precompilation. Copying my comment from #13891:

• Aesop -40%
• build wall-clock +7%
• interpretation +10%
• open Mathlib task-clock +1000%, wall-clock +225%, instructions +109%

So a loss overall. But where do these crazy numbers for open Mathlib come from? And why does interpretation get slower?