automatically generate ProjectName.lean

Stream: general

[Kevin Buzzard]

In Lean 3 there was a straightforward command (I don't remember but it might have been lean --make) which would just build all the files in src. This default functionality would be all that I'd ever need with a mathematics project.

Now we have a different set-up whereby whenever I add a new file to mathlib I have to edit Mathlib.lean. I don't want to go through all this with FLT.lean. So what do I want to do here? I suspect I need some kind of "trigger" which, whenever I e.g. push or commit or whatever triggers this, something should go through the FLT directory and create FLT.lean based on the current contents of the FLT directory. What should I be doing here?

[Yaël Dillies]

I have a script for that in APAP: https://github.com/YaelDillies/LeanAPAP/blob/master/scripts/mk_all.sh

[Yaël Dillies]

So instead of running lake build I run ./scripts/mk_all.sh; lake build

[Yaël Dillies]

And since I build my project I push commits (because I don't use bors, so I discipline myself to keep the build green), LeanAPAP.lean is always up to date.

[Eric Wieser]

You can also just not create FLT.lean at all

[Eric Wieser]

It only matters if you expect people to write import FLT rather than working in your repository directly

[Rémy Degenne]

I think leanblueprint needs that file in order to check that the lean declarations referenced in the blueprint actually exist in the project.

[Eric Wieser]

It would be pretty easy to teach leanblueprint to iterate over FLT/**/*.lean and import everything instead

[Eric Wieser]

It's unfortunate that it can't just ask lake to give it the list of files (it's already easy to tell Lake to have this glob behavior)

[Kevin Buzzard]

What I want is a way to compile all the files in the project. But now I remember that there's a way to do this in the lakefile.

[Michael Stoll]

something like

@[default_target]
lean_lib «EulerProducts» where
  globs := #[.submodules `EulerProducts]
  -- add any library configuration options here

(replace EulerProducts by FLT).

[Asei Inoue]

@Kevin Buzzard I have a script for this purpose.

https://github.com/Seasawher/import-all

[Yaël Dillies]

Actually, could we have a simple script inside mathlib to do this job? It's kind of annoying to do by hand every time.

[Yaël Dillies]

And we could replace the review-dog suggestions (which are often off by one) by a suggestion to use the script.

[Damiano Testa]

In some sense, the script is already there, since CI uses it:

(
  cd "$(git rev-parse --show-toplevel)" || exit 1
  for gp in Mathlib MathlibExtras Mathlib/Tactic Counterexamples Archive
  do
   git ls-files "$gp/*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > "$gp.lean"
  done
)

[Damiano Testa]

To make it a bit more stable, there could be a first step [Edit: added above already] that makes sure to run from the git-root directory (which is guaranteed during CI, but may not be running it locally).

[Damiano Testa]

But also, what would be the problem if the step that builds these "global" files did not trigger a CI error if it notices differences?

CI produces the file and builds mathlib against it. The files are in master and you download them when you upgrade mathlib anyway. If anyone wants to get the files synchronized locally, great, but if they are not, it simply means that import Mathlib locally may not mean the same as import Mathlib on master.

[Yaël Dillies]

I think the issues are that

1. If you add a leaf file, CI won't know about it unless you add it to Mathlib (that can be fixed by tweaking the lakefile)
2. We don't know how to make bors run this "Update Mathlib" once on each batch

[Damiano Testa]

It is fine to not change this, but if you create in CI the files they will contain all leaf files and then wouldn't lake build build them as well? Anyway, as I said, I am not trying to push for this change: I do in fact use a script that I run that automatically updates those files anyway.

[Yaël Dillies]

Yes, but that means you (= beginners, mostly) won't see the build errors until the PR is handed to bors. Of course this already happens because mathlib keeps on changing, but it's easy to not make it worse (eg by instructing lake build to build all submodules of mathlib, rather than just Mathlib)

[Damiano Testa]

Anyway, the code above is essentially the script that will make the "local" files exactly the same as the ones that CI checks. So simply PRing that as a further scripts/mk_all.sh file could work, right?

[Yaël Dillies]

Certainly, at least for the short term

[Damiano Testa]

#11781

[Yaël Dillies]

@Kevin Buzzard, after #11853, you will be able to run lake exe mkAll and your file FLT.lean will be automatically generated

[Yaël Dillies]

@Kevin Buzzard, update: It has landed!

[Yaël Dillies]

lake exe mk-all in FLT as much as you want

[Michael Rothgang]

lake exe mk_all, right?

[Ruben Van de Velde]

I'll push a mathlib bump in a little bit

[Ruben Van de Velde]

(FLT#96)

[Yaël Dillies]

Michael Rothgang said:

lake exe mk_all, right?

Oh yeah, I couldn't call it mk-all for some unknown reason

[Damiano Testa]

I think that - is simply not allowed in declaration names. I'm not completely sure why is that. Maybe we could have forced it with \f<<>>?

[Floris van Doorn]

I just tried lake exe mk_all for the first time, and I ran into an error. This occurs both in Mathlib and on a downstream project:

$ lake exe mk_all --help
✔ [3/8] Built Mathlib.Util.GetAllModules:c.o
✔ [4/8] Built Cli.Basic
✔ [5/8] Built mk_all
✔ [6/8] Built Cli.Basic:c.o
✔ [7/8] Built mk_all:c.o
✖ [8/8] Building mk_all
trace: .> c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe -o .\.\.lake/packages\mathlib\.lake\build\bin\mk_all.exe .\.\.lake/packages\mathlib\.lake\build\ir\mk_all.c.o.noexport .\.\.lake/packages\Cli\.lake\build\ir\Cli\Basic.c.o.export .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export -leanshared
info: stderr:
ld.lld: error: undefined symbol: l_Lake_logToStream
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs___lambda__1)
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs___lambda__1___boxed)

ld.lld: error: undefined symbol: l_Lake_findInstall_x3f
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: l_Lake_LakeOptions_mkLoadConfig
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: l_Lake_CliError_toString
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: l_Lake_OutStream_get
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: l_Lake_AnsiMode_isEnabled
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: l_Lake_loadWorkspace
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: l_Lake_MainM_runLogIO_replay
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(l_getLeanLibs)

ld.lld: error: undefined symbol: initialize_Lake_CLI_Main
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(initialize_Mathlib_Util_GetAllModules)

ld.lld: error: undefined symbol: l_Lake_defaultConfigFile
>>> referenced by .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export:(.refptr.l_Lake_defaultConfigFile)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe' exited with code 1
Some builds logged failures:
- mk_all
error: build failed

[Utensil Song]

This looks like your cache is still broken. Did you force fetch cache after reinstalling the Lean toolchain?

[Floris van Doorn]

Good point. It might be related to the errors I had earlier. I'll try it fresh now.

[Floris van Doorn]

I now tried it again on a copy of Mathlib that I haven't touched earlier today, and I get the same errors, even after running lake exe cache get!. lake build succeeds normally.

Can you check that lake exe mk_all works for you on Mathlib master?

[Sebastian Ullrich]

Very few programs import Lake so it's not unthinkable that this is a new, Windows-only issue with linking against Lake

[Floris van Doorn]

That was my alternative guess, that it is a Windows-only issue. Let me know if I can provide other information that is useful.

[Sébastien Gouëzel]

Same error on master on my (windows) computer.

[Damiano Testa]

On Linux the command works for me (and it is also used by CI).

[Utensil Song]

I think this might be related to lean4#3601 which has extra requirements to link on Windows.

image.png

[Kim Morrison]

Damiano, can we leave it to you to summon whatever help is needed to get this fixed?

[Damiano Testa]

I can try, but it would help if someone who uses windows can do some testing, since I do not have any windows computer.

[Damiano Testa]

In fact, if someone who uses windows is willing to have a session where we try to work this out during a call, that might be the easiest.

[Michael Rothgang]

Wild guess, but: is supportInterpreter := true required for mk_all? (Perhaps the answers is "yes, obviously" and I don't understand that flag well - in which case I'll be happy to be enlightened.)

[Utensil Song]

Utensil Song said:

I think this might be related to lean4#3601 which has extra requirements to link on Windows.

image.png

@Floris van Doorn Maybe you can try copying these 2 DLL files into where mk_all is located, and see if it runs?

[Floris van Doorn]

If I copy these two files to mathlib/scripts (where mk_all.lean is located), then I get the same error when running lake exe mk_all. I looked into mathlib/.lake/build/bin/ where mk_all.exe is supposed to be(?). Putting the DLL files there gives the same error as well. That folder does not contain mk_all.exe, btw. It does contain cache.exe, shake.exe and mk_all.exe.log.json. The last file contains (roughly) the error message that is output when running lake exe mk_all.

[Utensil Song]

The changelog indicates that the DLLs has to be colocated with the exe, to verify if it's the case, we need to find the exe. The fact that it's not there with other built exe is weird. I'll do some more investigation later today on Github Actions Windows CI as I haven't turned on my Windows computer for months.

[Floris van Doorn]

I believe the build errors while building the exe, not when executing it.

[Utensil Song]

OK, I can reproduce the same build error on Windows CI, while the same works on Ubuntu and Mac CI. And lake env lake exe mk_all can't save it, too (it rescued my other Windows FFI build).

[Utensil Song]

The missing symbols are in .elan/toolchains/leanprover--lean4---v4.9.0-rc1/lib/lean/libLake.a

nm -gU libLake.a | grep "l_Lake_logToStream"
0000000000003644 T _l_Lake_logToStream
0000000000003878 T _l_Lake_logToStream___boxed

Judging by the command trace: .> c:\Users\runneradmin\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe -o .\.\.lake/packages\mathlib\.lake\build\bin\mk_all.exe .\.\.lake/packages\mathlib\.lake\build\ir\mk_all.c.o.noexport .\.\.lake/packages\Cli\.lake\build\ir\Cli\Basic.c.o.export .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Util\GetAllModules.c.o.export -leanshared

It should be that it misses -lLake ? One example of adding this flag is here.

[Utensil Song]

@Floris van Doorn Can you try locally modify .lake/packages/mathlib/lakefile.lean so it looks like

/-- `lake exe mk_all` constructs the files containing all imports for a project. -/
lean_exe mk_all where
  srcDir := "scripts"
  supportInterpreter := true
  weakLinkArgs := #["-lLake"]

and run lake -R exe mk_all?

I have successfully run it on Windows CI.

image.png

[Sebastian Ullrich]

Thanks for the investigation, I now see the bug

[Floris van Doorn]

Utensil Song said:

Floris van Doorn Can you try locally modify .lake/packages/mathlib/lakefile.lean so it looks like

/-- `lake exe mk_all` constructs the files containing all imports for a project. -/
lean_exe mk_all where
  srcDir := "scripts"
  supportInterpreter := true
  weakLinkArgs := #["-lLake"]

and run lake -R exe mk_all?

I have successfully run it on Windows CI.

image.png

With that it works without error!

One note: it does change the order of the imports in Mathlib.lean, where . is sorted after any letter (I hope that is not platform-dependent?), e.g.:

-import Mathlib.GroupTheory.Order.Min
 import Mathlib.GroupTheory.OrderOfElement
+import Mathlib.GroupTheory.Order.Min

[Damiano Testa]

I am so happy that this works! Thank you all for helping debug this issue!

[Damiano Testa]

Wrt sorting, the previous shell script specifically used a flag to "uniformize" the sorting. The lake executable uses the docs#System.FilePath.walkDir (or git ls-files '*.lean') and may not do an "internal" sorting of the output of either. Maybe this should be added.

[Damiano Testa]

Actually, it does sort internally.

[Damiano Testa]

Floris, I am not sure that I am reading your diff correctly, but the webserver sorts the two files as follows:

import Lean.Elab.Command

run_cmd Lean.Elab.Command.liftTermElabM do
  let pair := #["Mathlib.GroupTheory.OrderOfElement", "Mathlib.GroupTheory.Order.Min"]
  guard <| pair ≠ pair.qsort (· < ·)

so ...Min comes earlier.

[Floris van Doorn]

After running lake exe mk_all there are modifications to my copy of Mathlib.lean, and it contains

[...]
import Mathlib.GroupTheory.NoncommPiCoprod
import Mathlib.GroupTheory.OrderOfElement
import Mathlib.GroupTheory.Order.Min
import Mathlib.GroupTheory.PGroup
[...]

[Floris van Doorn]

Mathlib commit dd36c71ca81 (5 days ago).

[Damiano Testa]

Can you try running the code above, to see if it passes the check?

[Damiano Testa]

(On my computer with Linux, the test above passes and so does on the webserver.)

[Floris van Doorn]

Yes, that code snippet passes without errors.

#eval #["Mathlib.GroupTheory.OrderOfElement", "Mathlib.GroupTheory.Order.Min"].qsort (· < ·)

gives

#["Mathlib.GroupTheory.Order.Min", "Mathlib.GroupTheory.OrderOfElement"]

[Damiano Testa]

And this is what I see in Mathlib.lean around where you mention:

import Mathlib.GroupTheory.NoncommCoprod
import Mathlib.GroupTheory.NoncommPiCoprod
import Mathlib.GroupTheory.Order.Min
import Mathlib.GroupTheory.OrderOfElement
import Mathlib.GroupTheory.PGroup

[Damiano Testa]

Hmmm

[Floris van Doorn]

But we're comparing a System.FilePath coerced to strings in your linked code, and that seems like it would use \ not .

[Damiano Testa]

Ah, or / on a Unix system?

[Floris van Doorn]

probably!?

[Damiano Testa]

This is the ordering for some characters that might be relevant for me:

#eval
  let arr := #[".", "/", "M", "\\"]
  arr == arr.qsort (· < ·)

[Floris van Doorn]

That evaluates to true for me, and seems like it would explain the difference :-)

[Damiano Testa]

Maybe the comparison should first replace the docs#System.FilePath.pathSeparator with . and then do the sorting.

[Damiano Testa]

Let me PR that!

[Michael Rothgang]

IIRC, there's some function toModuleName (or similar) in lake, which mk_all also uses for this purpose. (Or did you mean to do this already?)

[Damiano Testa]

Are you thinking of docs#moduleNameOfFileName? It is a little inconvenient to use it in the qsort, since the function is in IO, but the sort is pure.

[Damiano Testa]

#13777
I tested it locally and it does not change the order of the files on my computer. It also passed the relevant CI step, so CI is also on the same order.

If someone using Windows/MacOS wants to try it out, checking out the branch adomani/sort_all_files and running lake exe mk_all (or lake exe mk_all --git if you have random files in your Mathlib dir) should report No update necessary.

[Richard Osborn]

I would map Lean.moduleNameOfFileNameover allModules first and then sort afterwards. It's clunky doing it at the same time.

[Damiano Testa]

But then you would have to convert back from Name to FilePath, right?

[Damiano Testa]

(and you would need to catch errors, in case the path does not exist, but this is a step that happens later anyway, so it would just be shuffling code around)

[Richard Osborn]

Yea, sorry. I didn't see that getAllModules is what is returning the module strings. It would make most sense to sort there. (Not really sure why they are sorting preemptively). The long term solution would be to write a proper sort for System.FilePath.

[Michael Rothgang]

Sebastian Ullrich said:

Thanks for the investigation, I now see the bug

Is this bug still present? (Does it need a fix in mathlib?) I'd like to recommend mk_all more widely, and working on Windows would be nice for this :-)

[Sebastian Ullrich]

Why not just apply the workaround from above for now?

[Damiano Testa]

Eventually, the script could disengage completely from Mathlib, in fact.

[Michael Rothgang]

Sebastian Ullrich said:

Why not just apply the workaround from above for now?

That is, adding sorting to the script and applying the patch from this message to mathlib? Sounds like two mathlib PRs then (the first of which is 13777).

[Michael Rothgang]

By the way: why does mkAll need supportsInterpreter? Is this some obvious detail I'm not seeing?

[Damiano Testa]

I suspect that the supportInterpreter was cargo-culted (Yaël wrote most of the executable part of the command, so they may be able to comment on this better).

[Yaël Dillies]

Yeah that was not a conscious choice

[Michael Rothgang]

I just checked: it is in fact needed -> let me PR the patch above.

[Michael Rothgang]

Filed #13850 to fix mkAll and pole on Windows.
Can some Windows users (e.g. @Floris van Doorn @Utensil Song) help me test this?

• head to the PR, check out the branch
• run lake exe mk_all resp. lake exe pole
  Tell me if this runs without errors. Would be much appreciated!

[Utensil Song]

I think it's worth it to set up a Ubuntu/Windows/Mac CI for simple tools like this. I've been testing this via CI anyway.

[Rida Hamadani]

I've tested mathlib4#13850 and mathlib4#13854 on my windows laptop.
Both gave very similar errors:

Γ£û [5/8] Building mk_all
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\User\.elan\toolchains\leanprover--lean4---v4.9.0-rc2\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false .\.\.\scripts\mk_all.lean -R .\.\.\scripts -o .\.\.lake\build\lib\mk_all.olean -i .\.\.lake\build\lib\mk_all.ilean -c .\.\.lake\build\ir\mk_all.c --json
error: .\.\.\scripts\mk_all.lean:6:0: failed to read file '.\.\.lake/packages\Cli\.lake\build\lib\Cli\Basic.olean', invalid header
error: .\.\.\scripts\mk_all.lean:17:5: unknown namespace 'Lean'
error: .\.\.\scripts\mk_all.lean:19:5: unknown namespace 'Lake'
error: .\.\.\scripts\mk_all.lean:24:18: unknown identifier 'IO'
error: .\.\.\scripts\mk_all.lean:24:18: unknown constant 'sorryAx'
error: .\.\.\scripts\mk_all.lean:26:33: expected token
error: .\.\.\scripts\mk_all.lean:35:5: unknown namespace 'IO.FS'
error: .\.\.\scripts\mk_all.lean:38:21: unknown identifier 'Parsed'
error: .\.\.\scripts\mk_all.lean:38:21: unknown constant 'sorryAx'
error: .\.\.\scripts\mk_all.lean:46:35: expected token
error: .\.\.\scripts\mk_all.lean:67:20: '`'; expected '`('
error: .\.\.\scripts\mk_all.lean:67:12: unknown identifier 'Cmd'
error: .\.\.\scripts\mk_all.lean:81:17: unknown identifier 'List'
error: .\.\.\scripts\mk_all.lean:81:17: unknown constant 'sorryAx'
error: Lean exited with code 1
Some builds logged failures:
- mk_all
error: build failed

[Rida Hamadani]

I would be happy to get into a call with screen sharing in order to investigate this.

[Yaël Dillies]

I think I've figured out how to fix this one: Delete .lake, then run the command again

[Yaël Dillies]

It seems that somehow lake calls the outdated executable instead of recompiling?

[Rida Hamadani]

Nice, that worked on my machine too!

[Michael Rothgang]

To summarize: the code with the PR works on your machine, which runs Windows? That is excellent news, thanks a lot for testing!

[Rida Hamadani]

Noo sorry for the misunderstanding!

[Rida Hamadani]

The code didn't work until I did Yaël's suggestion, which is to delete .lake first.

[Rida Hamadani]

Before doing so, I had the error that I showed above

[Michael Rothgang]

That I understood - what happened after deleting .lake?

[Rida Hamadani]

It worked. I thought you read the last message only. :sweat_smile:
But is it possible to make it so that we don't have to delete .lake?

[Michael Rothgang]

Good question, I don't know. Perhaps that's a one-time event which will not be too disruptive?

[Rida Hamadani]

Also, I've only tried mk_all, trying pole, it gave me the following error:

uncaught exception: object file '.\.\.lake\build\lib\Mathlib.olean' of module Mathlib does not exist

[Michael Rothgang]

Wild guess: that sounds like a need to clear .lake again

[Rida Hamadani]

Got the same error after deleting .lake

[Utensil Song]

You need lake -R build after such modification to the lakefile as demonstrated in my Windows CI.

[Utensil Song]

When dealing with such a delicate matter, a reproducible CI workflow is your friend and any local success could be volatile.

[Utensil Song]

If you have used -R, you wouldn't need to delete .lake, now you need to fetch Mathlib cache again.

[Floris van Doorn]

With -R these commands work withour error for me.

Floris@Dell-E MINGW64 ~/projects/mathlibf (MR-fix-mkall-windows)
$ lake exe -R mk_all
✔ [2/8] Built Cli.Basic
✔ [4/8] Built mk_all
✔ [5/8] Built Cli.Basic:c.o
✔ [6/8] Built Mathlib.Util.GetAllModules:c.o
✔ [7/8] Built mk_all:c.o
✔ [8/8] Built mk_all
Updating 'Mathlib.lean'

Floris@Dell-E MINGW64 ~/projects/mathlibf (MR-fix-mkall-windows)
$ lake exe -R pole
✔ [21/66] Built Batteries.Classes.BEq:c.o
✔ [24/66] Built Batteries.Lean.Name:c.o
✔ [25/66] Built Batteries.Lean.SMap:c.o
✔ [27/66] Built Batteries.Classes.SatisfiesM:c.o
✔ [28/66] Built Batteries.Data.Array.Monadic:c.o
✔ [29/66] Built Batteries.Data.Nat.Basic:c.o
✔ [30/66] Built Batteries.Data.String.Basic:c.o
✔ [34/66] Built Batteries.Data.AssocList:c.o
✔ [35/66] Built Batteries.Lean.Position:c.o
✔ [36/66] Built Batteries.CodeAction.Deprecated:c.o
✔ [37/66] Built ImportGraph.Lean.Name
✔ [38/66] Built LongestPole.SpeedCenterJson
✔ [39/66] Built Mathlib.Data.String.Defs:c.o
✔ [40/66] Built ImportGraph.CurrentModule
✔ [41/66] Built Cli.Extensions
✔ [42/66] Built Batteries.Lean.NameMap:c.o
✔ [43/66] Built ImportGraph.RequiredModules:c.o
✔ [44/66] Built Batteries.Data.List.Init.Lemmas:c.o
✔ [45/66] Built Batteries.CodeAction.Attr:c.o
✔ [46/66] Built Batteries.Lean.IO.Process:c.o
✔ [47/66] Built Batteries.Lean.Util.Path:c.o
✔ [48/66] Built ImportGraph.Imports:c.o
✔ [49/66] Built Batteries.CodeAction.Basic:c.o
✔ [50/66] Built Batteries.Data.HashMap.Basic:c.o
✔ [51/66] Built LongestPole.SpeedCenterJson:c.o
✔ [52/66] Built ImportGraph.Lean.Name:c.o
✔ [53/66] Built Mathlib.Mathport.Rename:c.o
✔ [54/66] Built Batteries.Tactic.Alias:c.o
✔ [55/66] Built Cli.Extensions:c.o
✔ [56/66] Built Batteries.Data.List.Basic:c.o
✔ [57/66] Built Cli
✔ [58/66] Built ImportGraph.CurrentModule:c.o
✔ [59/66] Built ImportGraph.Cli
✔ [60/66] Built Cli:c.o
✔ [61/66] Built ImportGraph.Cli:c.o
✔ [62/66] Built ImportGraph
✔ [63/66] Built LongestPole.Main
✔ [64/66] Built ImportGraph:c.o
✔ [65/66] Built LongestPole.Main:c.o
✔ [66/66] Built pole
Analyzing Mathlib at 78f57a416ef003c0b6e4d974faf97020ffd83425
http://speed.lean-fro.org says: could not find run
Try moving to an older commit?

[Yaël Dillies]

But what if you first run them on a different Lean version, then switch versions and run them again?

[Floris van Doorn]

The things I did were

• checkout branch (from a much older Lean version)
• lake exe cache get
• then the displayed commands above

So with -R this just works.

[Yaël Dillies]

Does that mean you ran lake exe mk_all on two different Lean versions?

[Floris van Doorn]

Oh, I see what you mean... No I didn't do that...

[Yaël Dillies]

Disclaimer: I think there are actually two bugs going on in this thread, and I suspect you have found a way to fix the one I didn't report

[Utensil Song]

I guess .lake has the old lakefile.olean before the branch switch, so -R is required.

[Kim Morrison]

@Mac Malone, what are our prospects of getting rid of lakefile.olean entirely? This is still causing much suffering. :-)

[Mac Malone]

@Kim Morrison I have a plan on how to remove the need for -R altogether, but I have not found the time to implement it.