Zulip Chat Archive

Stream: mathlib4

Topic: lake exe cache get broken?

Scott Morrison (Jun 08 2023 at 02:16):

I think lake exe cache get is broken (or rather, the cache it downloads is not being used), ever since we merged ProofWidgets.

Scott Morrison (Jun 08 2023 at 02:16):

Would someone mind running lake clean && lake exe cache get && lake build to verify they see the same thing?

Mario Carneiro (Jun 08 2023 at 02:18):

It worked for me last I checked (working on a std bump now)

Damiano Testa (Jun 08 2023 at 02:23):

This is what I saw, running your code on a freshly pulled master:

/mathlib4 (master)$ lake clean && lake exe cache get && lake build
info: Downloading proofwidgets/v0.0.10/linux-64.tar.gz
info: Unpacking proofwidgets/v0.0.10/linux-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 2637 file(s)
Downloaded: 2637 file(s) [attempted 2637/2637 = 100%] (100% success)
Decompressing 3063 file(s)
[230/1160] Building ProofWidgets.Data.Json
[385/3086] Compiling Std.Util.TermUnsafe
[385/3086] Compiling Std.Tactic.Lint.Basic
[385/3086] Compiling Std.Lean.NameMapAttribute
[385/3086] Compiling Std.Data.Array.Init.Basic
[385/3086] Compiling Std.Tactic.OpenPrivate
[386/3086] Compiling Std.Data.Ord
[387/3086] Compiling Std.Data.List.Init.Lemmas
[388/3086] Compiling Std.Tactic.NoMatch
[389/3086] Compiling Std.Util.LibraryNote
[390/3086] Compiling Std.Tactic.Lint.Simp
[391/3086] Compiling Std.Tactic.Lint.TypeClass
[392/3086] Compiling Std.Tactic.Lint
[393/3086] Compiling Std.Data.Array.Basic
[394/3086] Compiling Std.Tactic.Lint.Misc
[394/3086] Compiling Std.Tactic.Lint.Frontend
[401/3086] Building scripts.runLinter
[403/3086] Building ProofWidgets.Compat
[1113/3086] Compiling scripts.runLinter
[1509/3086] Building ProofWidgets.Component.Basic
[2398/3086] Building ProofWidgets.Component.Panel
[2398/3086] Building ProofWidgets.Data.Html
[2612/3086] Linking runLinter
[2992/3086] Building ProofWidgets.Component.PenroseDiagram
[2992/3086] Building ProofWidgets.Presentation.Expr
stdout:
./lake-packages/proofwidgets/././ProofWidgets/Presentation/Expr.lean:85:14: warning: `ProofWidgets.getExprPresentation` has been deprecated
[2994/3086] Building ProofWidgets.Component.SelectionPanel

Scott Morrison (Jun 08 2023 at 02:27):

Interesting... for me it keeps building random subsets of mathlib4.

Damiano Testa (Jun 08 2023 at 02:29):

My experience with lake exe cache get is that it works fairly well, but maybe I have not been trying to rough it out too much...

Damiano Testa (Jun 08 2023 at 02:30):

In fact, especially when porting a new file, I usually skip the final lake build step, since I trust that everything else has been downloaded, and start editing directly in VSCode.

Scott Morrison (Jun 08 2023 at 02:38):

A lake exe cache clean! seems to have resolved my difficulties, sorry for the noise.

Mauricio Collares (Jul 12 2023 at 09:56):

Lately I've been running for f in ~/.cache/mathlib/*.gz; do gzip -t "$f" || rm "$f"; done quite often due to bad internet connectivity (curl stalls, I press Ctrl-C to restart it and pending files aren't removed). Maybe a new command lake exe cache check (or get!?) could do this?

Wrenna Robson (Jul 13 2023 at 11:32):

I'm having the issue that it seems to download the files but I don't get any kind of "Building" or "Compiling" message. And then when I try and run vs code it is clearly not using the cache.

Wrenna Robson (Jul 13 2023 at 11:32):

I've tried a lake exe cache clean! and it still isn't working.

Johan Commelin (Jul 13 2023 at 11:32):

Is this on master from 1 second ago?

Wrenna Robson (Jul 13 2023 at 11:33):

I'm trying to add Mathlib to a separate project to be clear.

Wrenna Robson (Jul 13 2023 at 11:33):

Using https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

Johan Commelin (Jul 13 2023 at 11:33):

Ok... because the commit that was causing trouble was reverted about half an hour ago.

Johan Commelin (Jul 13 2023 at 11:34):

That's why I was asking whether these problems were recent or very recent

Wrenna Robson (Jul 13 2023 at 11:37):

Oh I just now had the issue. But I need to update lake or something?

Wrenna Robson (Jul 13 2023 at 11:37):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ lake exe cache get!
Attempting to download 3568 file(s)
Downloaded: 3568 file(s) [attempted 3568/3568 = 100%] (100% success)
Decompressing 3568 file(s)

Wrenna Robson (Jul 13 2023 at 11:37):

This just happened (it did nothing further than this).

Wrenna Robson (Jul 13 2023 at 11:38):

If there's something I can run to diagnose what my whatsit is on lmk.

Johan Commelin (Jul 13 2023 at 11:40):

@Mario Carneiro @Scott Morrison Is there a chance that artifacts on Azure are now corrupt?

Johan Commelin (Jul 13 2023 at 11:40):

So that even after reverting the commit, we're still downloading a broken cache?

Sebastian Ullrich (Jul 13 2023 at 11:41):

They shouldn't because they use different file extensions, right?

Johan Commelin (Jul 13 2023 at 11:41):

I guess that's right

Wrenna Robson (Jul 13 2023 at 11:42):

I'll run lake exe cache get! just to be sure.

Wrenna Robson (Jul 13 2023 at 11:47):

Like... is it maybe the case that I need to link Mathlib in more clearly? I'm just totally confused and very frustrated.

Ruben Van de Velde (Jul 13 2023 at 11:48):

The only Building/Compiling messages lake exe cache should print are the eight or so to build the cache tool itself (and those only if it isn't built yet)

Scott Morrison (Jul 13 2023 at 11:48):

Wrenna, could you post your lakefile, and the output of git status?

Ruben Van de Velde (Jul 13 2023 at 11:49):

Wrenna Robson said:

wrobson:~/projects/verifying-cmce/lean4/controlbits$ lake exe cache get!
Attempting to download 3568 file(s)
Downloaded: 3568 file(s) [attempted 3568/3568 = 100%] (100% success)
Decompressing 3568 file(s)

This output looks correct

Wrenna Robson (Jul 13 2023 at 11:49):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ cat lakefile.lean
import Lake
open Lake DSL

package «controlbits» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «Controlbits» {
  -- add any library configuration options here
}

Ruben Van de Velde (Jul 13 2023 at 11:50):

Please also paste what's in your lean-toolchain and lake-manifest.json

Wrenna Robson (Jul 13 2023 at 11:50):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ git status
On branch master

No commits yet

Untracked files:
  (use "git add <file>..." to include in what will be committed)
        .gitignore
        Controlbits.lean
        lake-manifest.json
        lakefile.lean
        lean-toolchain

nothing added to commit but untracked files present (use "git add" to track)

Wrenna Robson (Jul 13 2023 at 11:50):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ cat lean-toolchain
leanprover/lean4:nightly-2023-07-12

Wrenna Robson (Jul 13 2023 at 11:50):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ cat lake-manifest.json
{"version": 4,
 "packagesDir": "lake-packages",
 "packages":
 [{"git":
   {"url": "https://github.com/EdAyers/ProofWidgets4",
    "subDir?": null,
    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
    "name": "proofwidgets",
    "inputRev?": "v0.0.11"}},
  {"git":
   {"url": "https://github.com/mhuisi/lean4-cli.git",
    "subDir?": null,
    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
    "name": "Cli",
    "inputRev?": "nightly"}},
  {"git":
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "subDir?": null,
    "rev": "aeaebdd3d43b60b0d771c9a457131c72cc20a811",
    "name": "mathlib",
    "inputRev?": null}},
  {"git":
   {"url": "https://github.com/gebner/quote4",
    "subDir?": null,
    "rev": "e6ca4e7e6b13ceee845e40a904c1a71ed9866574",
    "name": "Qq",
    "inputRev?": "master"}},
  {"git":
   {"url": "https://github.com/JLimperg/aesop",
    "subDir?": null,
    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
    "name": "aesop",
    "inputRev?": "master"}},
  {"git":
   {"url": "https://github.com/leanprover/std4",
    "subDir?": null,
    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
    "name": "std",
    "inputRev?": "main"}}]}

Wrenna Robson (Jul 13 2023 at 11:50):

Thank you for help.

Wrenna Robson (Jul 13 2023 at 11:51):

Also here's my actual file I was trying to use Mathlib in.

Wrenna Robson (Jul 13 2023 at 11:51):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ cat Controlbits.lean
import Mathlib

structure ControlBits (m : Nat) where
  bits : Fin ((2*m + 1) <<< m) → Bool

Wrenna Robson (Jul 13 2023 at 11:51):

I opened this file in VS Code yesterday and I still had orange bars after 40 minutes

Ruben Van de Velde (Jul 13 2023 at 11:52):

Thanks. Now if only I saw something wrong :sweat_smile:

Wrenna Robson (Jul 13 2023 at 11:52):

Yeah it is really baffling.

Ruben Van de Velde (Jul 13 2023 at 11:56):

I tried to reproduce with the files you pasted and it works

Wrenna Robson (Jul 13 2023 at 11:57):

OK. How did you check that it works?

Wrenna Robson (Jul 13 2023 at 11:58):

Perhaps it is a problem with my VS Code setup? So if there's some way of testing it outside of that...

Ruben Van de Velde (Jul 13 2023 at 11:58):

I opened vs code and the infoview worked

Ruben Van de Velde (Jul 13 2023 at 11:59):

Try changing something in Controlbits.lean and running lake build, it should show

$ lake build
[3566/3567] Building Controlbits

and nothing else

Wrenna Robson (Jul 13 2023 at 12:11):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ lake build
[3566/3567] Building Controlbits

Wrenna Robson (Jul 13 2023 at 12:11):

I do indeed have this

Wrenna Robson (Jul 13 2023 at 12:12):

But it is then just... hanging at the command line, clearly working.

Wrenna Robson (Jul 13 2023 at 12:12):

No output. Is there a verbose build mode?

Scott Morrison (Jul 13 2023 at 12:12):

You mean it never returns to the command line?

Wrenna Robson (Jul 13 2023 at 12:12):

Correct.

Wrenna Robson (Jul 13 2023 at 12:13):

Essentially as I'd expect it to behave if it was running some kind of very intensive program, the fan is going 15 to the dozen (this is a laptop, mind), and yes, it hasn't returned to the command line.

Wrenna Robson (Jul 13 2023 at 12:13):

Note that without the "import Mathlib" I don't get this behaviour.

Matthew Ballard (Jul 13 2023 at 12:17):

Are there orphaned lean processes still running?

Wrenna Robson (Jul 13 2023 at 12:17):

It has now returned!

Wrenna Robson (Jul 13 2023 at 12:18):

I do tend to run "killall lean" to prevent this

Wrenna Robson (Jul 13 2023 at 12:18):

Wrenna Robson said:

It has now returned!

I'm now trying VS code.

Wrenna Robson (Jul 13 2023 at 12:18):

Orange bars.

Wrenna Robson (Jul 13 2023 at 12:18):

Heavy fan, as if it's building the whole file again.

Wrenna Robson (Jul 13 2023 at 12:19):

Which should be trivial...

Wrenna Robson (Jul 13 2023 at 12:19):

I feel like I must have some part of my setup borked.

Wrenna Robson (Jul 13 2023 at 12:20):

wrobson:~/projects/verifying-cmce/lean4/controlbits$ lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-07-12)

wrobson:~/projects/verifying-cmce/lean4/controlbits$ elan --version
elan 2.0.0 (001eb2cfe 2023-07-03)

wrobson:~/projects/verifying-cmce/lean4/controlbits$ lean --version
Lean (version 4.0.0-nightly-2023-07-12, commit 6e904421304c, Release)

For reference.

Wrenna Robson (Jul 13 2023 at 12:20):

Will do anything to fix this :(

Wrenna Robson (Jul 13 2023 at 12:22):

Oh! It's not orange.

Wrenna Robson (Jul 13 2023 at 12:23):

I have no idea why it now works. Potentially this cache fix you did has done it and I just needed to give it a bit.

Ruben Van de Velde (Jul 13 2023 at 12:24):

Strange, but glad to hear it works now

Sebastian Ullrich (Jul 13 2023 at 12:24):

If it needs more a few seconds to load, there still seems to be something quite wrong

Vincent Beffara (Jul 13 2023 at 14:16):

Mauricio Collares said:

Lately I've been running for f in ~/.cache/mathlib/*.gz; do gzip -t "$f" || rm "$f"; done quite often due to bad internet connectivity (curl stalls, I press Ctrl-C to restart it and pending files aren't removed). Maybe a new command lake exe cache check (or get!?) could do this?

How about simply passing the --remove-on-error flag to curl? Then at least there won't be wrong partial downloads when interrupted

Sebastian Ullrich (Jul 13 2023 at 14:21):

https://github.com/leanprover-community/mathlib4/blob/aeaebdd3d43b60b0d771c9a457131c72cc20a811/Cache/Requests.lean#L86

Sebastian Ullrich (Jul 13 2023 at 14:22):

Are you sure it does anything on SIGINT?

Vincent Beffara (Jul 13 2023 at 14:39):

Not sure of that, but at least it should work for dropped connections

Sebastian Ullrich (Jul 13 2023 at 14:41):

So should the code I linked to

Wrenna Robson (Jul 14 2023 at 13:11):

So oddly it was working fine for a bit, and now - and I ran an update of the cache just to be sure, but it was doing it spontaneously before - I am in orange bar hell again.

Wrenna Robson (Jul 14 2023 at 13:12):

So it's very odd - it's like suddenly building my file is really hard for it. But I cannot see why.

Sebastian Ullrich (Jul 14 2023 at 13:22):

Is it reproducible with lake build?

Wrenna Robson (Jul 14 2023 at 13:56):

In that lake build takes an age to complete, yes.

Sebastian Ullrich (Jul 14 2023 at 14:00):

On the last step again? Could you try this then?

time lake env lean --profile Controlbits.lean

Peter Nelson (Jul 14 2023 at 14:13):

I'm having a problem that seems related. I cloned a fresh copy of mathlib4, then ran lake update and lake exe cache get in the folder. Then lake build takes a long time and gives errors. If I do the same thing without lake update, it works fine (builds mathlib quickly).

Wrenna Robson (Jul 14 2023 at 14:16):

Running the above now.

Ruben Van de Velde (Jul 14 2023 at 14:18):

No no no, don't run lake update within mathlib

Wrenna Robson (Jul 14 2023 at 14:21):

I'm not, personally: I was following the instructions here. https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

Peter Nelson (Jul 14 2023 at 14:25):

That was probably for me. Understood!

Wrenna Robson (Jul 14 2023 at 14:30):

FWIW it is still running 15 minutes later.

Wrenna Robson (Jul 14 2023 at 15:22):

Still running...

Wrenna Robson (Jul 14 2023 at 15:22):

This is the output thus far:

wrobson:~/projects/verifying-cmce/lean4/controlbits$ time lake env lean --profile Controlbits.lean
interpretation of Mathlib.Prelude.Rename.binportTag took 79.3s
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 2.22s
import took 156s
elaboration took 284ms
compilation new took 108ms
typeclass inference of CoeFun took 619ms

But it hasn't yet returned to the command line.

Wrenna Robson (Jul 14 2023 at 15:31):

Still going. I think this is past the point I would give up, @Sebastian Ullrich...

Wrenna Robson (Jul 14 2023 at 15:32):

I am a little worried that nobody seems able to replicate my issue.

Sebastian Ullrich (Jul 14 2023 at 15:34):

I think it's safe to say at this point that there must be something special about your setup. Is your project on a network drive, or some other exotic configuration?

Wrenna Robson (Jul 14 2023 at 15:55):

No, it's literally just running on my laptop.

Wrenna Robson (Jul 14 2023 at 15:55):

Oh! Well, I mean, it's on WSL?

Wrenna Robson (Jul 14 2023 at 15:55):

But that was never a problem for lean before.

Wrenna Robson (Jul 14 2023 at 15:56):

Is it possible I could spin up a gitpod VM or something - literally just to confirm that things work normally there?

Sebastian Ullrich (Jul 14 2023 at 15:56):

And the project is on the Linux drive?

Wrenna Robson (Jul 14 2023 at 15:57):

Yes.

Wrenna Robson (Jul 14 2023 at 15:58):

That is where I do all my work from.

Yaël Dillies (Jul 14 2023 at 15:58):

gitpod.io/new/#https://github.com/leanprover-community/mathlib4

Wrenna Robson (Jul 14 2023 at 16:32):

That puts me in a mathlib4 directory - I should create my project outside that, right?

Wrenna Robson (Jul 14 2023 at 16:32):

It's using as a dependency I want.

Yaël Dillies (Jul 14 2023 at 16:34):

Sure yeah. One way is to create a github repo containing a new project depending on mathlib4

Sebastian Ullrich (Jul 14 2023 at 16:38):

If you test

time lake env lean --profile lake-packages/mathlib/Mathlib.lean

and even that is slow, we know it's not your project but it must be your setup that's somehow misbehaving

Sebastian Ullrich (Jul 14 2023 at 16:41):

If you can find the PID of the busy process (e.g. in htop), it might be interesting to dump a stacktrace of it using

gdb -batch -ex bt -p <PID>

Wrenna Robson (Jul 14 2023 at 16:42):

I'll try that. Thank you for your patience.

Wrenna Robson (Jul 14 2023 at 16:44):

For reference, running time lake env lean --profile Controlbits.lean but on the gitpod is having similar issues. Running that stacktrace now, as the command you just suggested (run in the project directory) is being slow.

Wrenna Robson (Jul 14 2023 at 16:45):

Incoming:

wrobson:~/projects/verifying-cmce/lean4/controlbits$ gdb -batch -ex bt -p 30573
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
0x00007f5de7937f26 in l_Array_forInUnsafe_loop___at_Lean_importModules___spec__10 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#0  0x00007f5de7937f26 in l_Array_forInUnsafe_loop___at_Lean_importModules___spec__10 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#1  0x00007f5de793a23c in l_Array_forInUnsafe_loop___at_Lean_importModules___spec__12 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#2  0x00007f5de793bdf4 in l_Lean_importModules___lambda__3 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#3  0x00007f5de9afdb2f in lean_apply_2 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#4  0x00007f5de9afcd7d in lean_apply_1 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#5  0x00007f5de7944073 in l_Lean_withImporting___rarg () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6  0x00007f5de793cd9c in l_Lean_importModules___lambda__4___boxed () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#7  0x00007f5de9afdb2f in lean_apply_2 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#8  0x00007f5de9afcd7d in lean_apply_1 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#9  0x00007f5de88a028e in l_Lean_profileitIOUnsafe___rarg___lambda__1 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#10 0x00007f5de88a048f in l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#11 0x00007f5de9afcd69 in lean_apply_1 () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#12 0x00007f5de9a447f4 in lean_profileit () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#13 0x00007f5de88a03b0 in l_Lean_profileitIOUnsafe___rarg () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#14 0x00007f5de793cbf8 in lean_import_modules () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#15 0x00007f5de861cbd5 in l_Lean_Elab_processHeader () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#16 0x00007f5de8281201 in lean_run_frontend () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#17 0x00007f5de99df68d in lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > > const&) () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#18 0x00007f5de99e2208 in lean_main () from /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#19 0x00007f5de6295083 in __libc_start_main (main=0x55f5bddce8b0 <main>, argc=3, argv=0x7ffe75fc6958, init=<optimized out>, fini=<optimized out>, rtld_fini=<optimized out>, stack_end=0x7ffe75fc6948) at ../csu/libc-start.c:308
#20 0x000055f5bddce7e5 in _start ()
[Inferior 1 (process 30573) detached]

Sebastian Ullrich (Jul 14 2023 at 16:48):

Ok, at least that's confirmation that the import itself is slow. Which usually should not take more than a few seconds.

$ lake env lean --profile Mathlib.lean
interpretation of Mathlib.Prelude.Rename.binportTag took 320ms
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 412ms
import took 5.5s
cumulative profiling times:
    elaboration 0.0252ms
    import 5.5s
    initialization 15.2ms
    interpretation 964ms
    linting 0.0255ms
    parsing 0.00132ms

Wrenna Robson (Jul 14 2023 at 16:52):

Running lake env lean --profile lake-packages/mathlib/Mathlib.lean on the gitpod is fine. So it's something on my local machine I guess.

Wrenna Robson (Jul 14 2023 at 16:52):

But I have no idea what.

Wrenna Robson (Jul 14 2023 at 16:55):

Running lake env lean --profile Controlbits.lean on the gitpod with this file doesn't finish though. So possibly also something is up with my file.

import Mathlib

structure ControlBits (m : Nat) where
  bits : Fin (2*m + 1) → (Fin m → Bool) → Bool

section ControlBits

def myT (m : ℕ) : Fin (2*m + 1) → Fin (m + 1) := sorry

def myFunkyThing (m : ℕ) (c : ControlBits m) (i : Fin (2*m + 1)) :
(Fin (m + 1) → Bool) → (Fin (m + 1) → Bool) := fun k => k ^ (Pi.single (myT i) (c i (Fin.succAbove (myT i) ∘  k)))

end ControlBits

Sebastian Ullrich (Jul 14 2023 at 16:56):

Trying removing everything but import Mathlib

Wrenna Robson (Jul 14 2023 at 16:56):

I was hoping (as I was used to in lean 3) that the typechecker would quickly identify if there was any issues here. I was accustomed to using it as a quick tool to help me refine the correct expressions.

Sebastian Ullrich (Jul 14 2023 at 16:57):

That is how it works for most users, yes

Wrenna Robson (Jul 14 2023 at 16:57):

Yep, that's fine in gitpod.

Vincent Beffara (Jul 14 2023 at 16:57):

Do ./lean-toolchain and ./lake-packages/mathlib/lean-toolchain match?

Wrenna Robson (Jul 14 2023 at 16:58):

Yes

Wrenna Robson (Jul 14 2023 at 16:58):

leanprover/lean4:nightly-2023-07-12

Sebastian Ullrich (Jul 14 2023 at 16:58):

I am a bit stupefied. I don't know if many other people have tried using mathlib4 as a dependency in WSL2 but there should basically be no difference in compiling Mathlib.lean vs compiling a file that does nothing but import Mathlib

Wrenna Robson (Jul 14 2023 at 16:59):

To be clear - neither of those are working in WSL2.

Wrenna Robson (Jul 14 2023 at 16:59):

And both of those are working in gitpod.

Wrenna Robson (Jul 14 2023 at 16:59):

So that is at least saner.

Sebastian Ullrich (Jul 14 2023 at 17:00):

Ah, I missed that. I'm pretty sure other people have successfully worked on mathlib4 in WSL before though

Wrenna Robson (Jul 14 2023 at 17:01):

There seem to be two separate things:
a) something about the file I quote above is so broken that it just doesn't even fail to compile, but hangs.
b) My import of Mathlib locally is really slow/also I can't compiled Mathlib locally. But it was working at some point, and I didn't substantively change anything.

From my point of view, actually, I made the edits to the file that broke it for a)... and thereafter was also experiencing b). Like the failure at a) caused some poisoning somehow.

Wrenna Robson (Jul 14 2023 at 17:04):

(I think the error in that file, on some experimentation in github, is that I've used the wrong symbol for xor.)

Sebastian Ullrich (Jul 14 2023 at 18:40):

Perhaps your .olean files somehow got corrupted. Does re-running lake exe cache get change anything?

Mauricio Collares (Jul 14 2023 at 19:06):

Sorry for repeating myself, but for f in ~/.cache/mathlib/*.gz; do gzip -t "$f" || rm "$f"; done might be useful to delete corrupted files (which won't be redownloaded by lake exe cache get)

Yury G. Kudryashov (Jul 14 2023 at 19:11):

Or lake exe cache clean!

Yury G. Kudryashov (Jul 14 2023 at 19:11):

(this will delete all cached files)

Wrenna Robson (Jul 17 2023 at 11:26):

I did try these but can't hurt to do it again

Wrenna Robson (Jul 17 2023 at 11:54):

Could I check what the right versions of lean/lake etc. should be? I'm almost wondering should I try and uninstall elan, lean, lake etc. from scratch.

Wrenna Robson (Jul 17 2023 at 11:55):

But I don't know how to do that or indeed what the right install process now is. Advice there would be useful.

Wrenna Robson (Jul 17 2023 at 15:10):

OK, so, I do seem to be able to use Mathlib locally OK. It seems the issue is in creating a project depeneding on it.

Evgenia Karunus (Jul 18 2023 at 08:51):

Just had the same issue (I executed lake exe cache get, but cache wasn't getting used) and lake exe cache clean! fixed that.

Scott Morrison (Jul 19 2023 at 04:19):

On current master lake exe cache get! && lake build is building everything from Mathlib.Algebra.Star.Pi onwards for me. Can anyone else confirm?

Mario Carneiro (Jul 19 2023 at 04:59):

what OS?

Mario Carneiro (Jul 19 2023 at 05:01):

works for me on x86 linux

Mario Carneiro (Jul 19 2023 at 05:01):

try rm -rf build and rerun (if your build files are corrupt but the trace files are correct then leantar won't unpack / replace them)

Mario Carneiro (Jul 19 2023 at 05:17):

#5991

Christopher Hoskin (Aug 21 2023 at 22:14):

For the last few days, I've been finding that lake build still has work to do, often lots of it, after I've run lake exe cache get, whereas previously it would return immediately if the branch had built successfully in CI.

I thought something might be broken in my configuration, so I did a fresh install of Ubuntu 22.04 in a VM, ran:

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

and then

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
lake exe cache get
lake build

It started building from file 47 of 3810 - Std.Util.TermUnsafe

Mario Carneiro (Aug 21 2023 at 22:16):

The usual cause of this is that you are using a different lean-toolchain than mathlib

Mario Carneiro (Aug 21 2023 at 22:19):

try cp lake-packages/mathlib/lean-toolchain lean-toolchain and then lake exe cache get; lake build again

Kevin Buzzard (Aug 21 2023 at 22:21):

Wait I've seen lean spend 5 or so seconds compiling std files, and then it finishes quickly and everything works. What happens after 47/3810? Is it 1345/3810?

Christopher Hoskin (Aug 21 2023 at 22:21):

Mario Carneiro said:

The usual cause of this is that you are using a different lean-toolchain than mathlib

All I have is:

ls lake-packages/
aesop  Cli  proofwidgets  Qq  std

There is no lake-packages/mathlib/lean-toolchain?

Mario Carneiro (Aug 21 2023 at 22:21):

oh I see, you are working on mathlib itself - in that case my advice doesn't apply

Christopher Hoskin (Aug 21 2023 at 22:26):

Kevin Buzzard said:

Wait I've seen lean spend 5 or so seconds compiling std files, and then it finishes quickly and everything works. What happens after 47/3810? Is it 1345/3810?

lake build
[47/3810] Compiling Std.Util.TermUnsafe
[48/3810] Compiling Std.Lean.NameMapAttribute
[49/3810] Compiling Std.Tactic.OpenPrivate
[50/3810] Compiling Std.Data.List.Init.Lemmas
[51/3810] Compiling Std.Data.Ord
[52/3810] Compiling Std.Util.LibraryNote
[53/3810] Compiling Std.Lean.Command
[54/3810] Compiling Std.Tactic.Unreachable
[55/3810] Compiling Std.Lean.TagAttribute
[56/3810] Compiling Std.Tactic.ByCases
[57/3810] Compiling Std.Tactic.SeqFocus
[58/3810] Compiling Std.Lean.Name
[59/3810] Compiling Std.Lean.Position
^C

lake build
warning: waiting for prior `lake build` invocation to finish... (remove './build/lake.lock' if stuck)
^C
cat ./build/lake.lock
3960
ps aux | grep 3960
mans0954    4486  0.0  0.1  17736  2432 pts/0    S+   23:22   0:00 grep --color=auto 3960
rm ./build/lake.lock
lake build
[52/3661] Building ProofWidgets.Data.Json
[65/3810] Compiling Std.Lean.Position
[66/3810] Compiling Std.Lean.Parser
[67/3810] Compiling Std.Lean.Meta.Basic
[68/3810] Compiling Std.Lean.Tactic
[69/3810] Compiling Std.Tactic.RCases
[70/3810] Compiling Std.WF
[71/3810] Compiling Std.Classes.BEq
[72/3810] Compiling Std.Lean.Delaborator
[73/3810] Compiling Std.Classes.Dvd
[74/3810] Compiling Std.Lean.Meta.LCtx
[75/3810] Compiling Std.Util.ExtendedBinder
[76/3810] Compiling Std.Lean.InfoTree
[77/3810] Compiling Std.Control.ForInStep.Basic
[78/3810] Compiling Std.Tactic.HaveI
[79/3810] Compiling Std.Data.Option.Init.Lemmas
[80/3810] Compiling Std.Data.DList
[81/3810] Compiling Std.Data.MLList.Basic
[82/3810] Compiling Std.Data.Prod.Lex
[83/3810] Compiling Std.Lean.Expr
[84/3810] Compiling Std.Lean.HashMap
[85/3810] Compiling Std.Lean.HashSet
[86/3810] Compiling Std.Lean.Meta.Expr
[87/3810] Compiling Std.Lean.PersistentHashMap
[88/3810] Compiling Std.Lean.Meta.Inaccessible
[89/3810] Compiling Std.Lean.MonadBacktrack
[90/3810] Compiling Std.Lean.PersistentHashSet
[91/3810] Compiling Std.Tactic.Exact
[92/3810] Compiling Std.Tactic.Instances
[93/3810] Compiling Std.Tactic.Where
[110/3810] Compiling Std.Classes.SetNotation
[111/3810] Compiling Std.Lean.Format
[112/3810] Compiling Std.Tactic.NoMatch
[113/3810] Compiling Std.Lean.AttributeExtra
[114/3810] Compiling Std.Util.Pickle
[115/3810] Compiling Std.CodeAction.Attr
[116/3810] Compiling Std.Tactic.GuardExpr
[117/3810] Compiling Std.Lean.Meta.InstantiateMVars
[118/3810] Compiling Std.Lean.Meta.Clear
[119/3810] Compiling Std.Lean.Meta.AssertHypotheses
[120/3810] Compiling Std.Tactic.PrintDependents
[121/3810] Compiling Std.Tactic.CoeExt
[122/3810] Compiling Std.Data.Int.Basic
[123/3810] Compiling Std.Data.Nat.Basic
[124/3810] Compiling Std.Data.Char
[125/3810] Compiling Std.Control.ForInStep.Lemmas
[196/3810] Compiling Std.Linter.UnreachableTactic
[197/3810] Compiling Std.Tactic.Lint.Basic
[198/3810] Compiling Std.Lean.Meta.SavedState
[199/3810] Compiling Std.Tactic.Ext.Attr
[200/3810] Compiling Mathlib.Util.WhatsNew
[201/3810] Compiling Mathlib.Tactic.PPWithUniv
[202/3810] Compiling Mathlib.Mathport.Attributes
[203/3810] Compiling Mathlib.Tactic.Alias
[204/3810] Compiling Mathlib.Mathport.Rename
[209/3810] Compiling Std.Tactic.Simpa
[210/3810] Building ProofWidgets.Compat
[214/3810] Compiling Std.CodeAction.Basic
[215/3810] Compiling Std.Tactic.NormCast.Ext
[216/3810] Compiling Std.Control.ForInStep
[252/3810] Compiling Std.Tactic.TryThis
[253/3810] Compiling Std.Data.Array.Init.Basic
[254/3810] Compiling Std.Linter.UnnecessarySeqFocus
[255/3810] Compiling Std.Tactic.Lint.Frontend
[256/3810] Compiling Std.Classes.Cast
[263/3810] Compiling Std.Classes.Order
[264/3810] Building ProofWidgets.Component.Basic
[268/3810] Compiling Std.Tactic.Lint.Simp
[270/3810] Compiling Std.CodeAction.Misc
[271/3810] Compiling Std.Tactic.NormCast.Lemmas
[281/3810] Compiling Std.Tactic.SimpTrace
[282/3810] Compiling Std.Tactic.ShowTerm
[283/3810] Compiling Std.Linter
[284/3810] Compiling Std.Tactic.GuardMsgs
[288/3810] Compiling Std.Data.Array.Basic
[289/3810] Building ProofWidgets.Component.Panel
[290/3810] Building ProofWidgets.Data.Html
[294/3810] Compiling Std.CodeAction
[297/3810] Compiling Std.Tactic.SqueezeScope
[300/3810] Compiling Std.Tactic.Lint.Misc
[301/3810] Compiling Std.Tactic.Lint.TypeClass
[302/3810] Building ProofWidgets.Component.PenroseDiagram
[303/3810] Building ProofWidgets.Presentation.Expr
[305/3810] Building ProofWidgets.Component.SelectionPanel
[309/3810] Compiling Std.Tactic.Lint
[311/3810] Compiling Std.Tactic.Basic
[315/3810] Compiling Std.Logic
[317/3810] Compiling Std.Tactic.Ext
[323/3810] Compiling Std.Data.PairingHeap
[324/3810] Compiling Std.Data.Nat.Init.Lemmas
[325/3810] Compiling Std.Classes.LawfulMonad
[329/3810] Compiling Std.Tactic.Congr
[330/3810] Compiling Std.Data.RBMap.Basic
[333/3810] Compiling Std.Data.Fin.Basic
[338/3810] Compiling Std.Data.RBMap.WF
[339/3810] Compiling Std.Data.Nat.Lemmas
[340/3810] Compiling Std.Data.Option.Basic
[342/3810] Compiling Std.Data.Array.Init.Lemmas
[348/3810] Compiling Std.Data.RBMap
[349/3810] Compiling Std.Data.RBMap.Alter
[350/3810] Compiling Std.Data.BinomialHeap.Basic
[351/3810] Compiling Std.Data.String.Basic
[352/3810] Compiling Std.Data.Nat.Gcd
[356/3810] Compiling Std.Data.Array.Merge
[357/3810] Compiling Std.Data.List.Basic
^C

Mario Carneiro (Aug 21 2023 at 22:30):

those are Compiling not Building, that is expected

Mario Carneiro (Aug 21 2023 at 22:31):

the cache does not include compilation artifacts (.o files) as those are architecture specific

Mario Carneiro (Aug 21 2023 at 22:32):

the better question is why you need to compile all that, this normally only happens when building an executable

Christopher Hoskin (Aug 21 2023 at 22:43):

Mario Carneiro said:

the better question is why you need to compile all that, this normally only happens when building an executable

Oh right? What command should I run to check that there are no errors?

Mario Carneiro (Aug 21 2023 at 22:45):

just let it run to completion

Mario Carneiro (Aug 21 2023 at 22:45):

what are the final products toward the end?

Mario Carneiro (Aug 21 2023 at 22:45):

It will not take 3 hours to run, don't worry

Christopher Hoskin (Aug 21 2023 at 23:09):

 time lake build
[47/3810] Compiling Std.Util.TermUnsafe
[48/3810] Compiling Std.Lean.NameMapAttribute
[49/3810] Compiling Std.Tactic.OpenPrivate
[50/3810] Compiling Std.Data.List.Init.Lemmas
[51/3810] Compiling Std.Data.Ord
[52/3810] Compiling Std.Util.LibraryNote
[53/3810] Compiling Std.Lean.Command
[54/3810] Compiling Std.Tactic.Unreachable
[55/3810] Compiling Std.Lean.TagAttribute
[56/3810] Compiling Std.Tactic.ByCases
[57/3810] Compiling Std.Tactic.SeqFocus
[58/3810] Compiling Std.Lean.Name
[59/3810] Compiling Std.Lean.Position
[60/3810] Compiling Std.Lean.Parser
[61/3810] Compiling Std.Lean.Meta.Basic
[62/3810] Compiling Std.Lean.Tactic
[63/3810] Compiling Std.Tactic.RCases
[64/3810] Compiling Std.WF
[65/3810] Compiling Std.Classes.BEq
[66/3810] Compiling Std.Lean.Delaborator
[67/3810] Compiling Std.Classes.Dvd
[68/3810] Compiling Std.Lean.Meta.LCtx
[69/3810] Compiling Std.Util.ExtendedBinder
[70/3810] Compiling Std.Lean.InfoTree
[71/3810] Compiling Std.Control.ForInStep.Basic
[72/3810] Compiling Std.Tactic.HaveI
[73/3810] Compiling Std.Data.Option.Init.Lemmas
[74/3810] Compiling Std.Data.DList
[75/3810] Compiling Std.Data.MLList.Basic
[76/3810] Compiling Std.Data.Prod.Lex
[77/3810] Compiling Std.Lean.Expr
[78/3810] Compiling Std.Lean.HashMap
[79/3810] Compiling Std.Lean.HashSet
[80/3810] Compiling Std.Lean.Meta.Expr
[81/3810] Compiling Std.Lean.PersistentHashMap
[82/3810] Compiling Std.Lean.Meta.Inaccessible
[83/3810] Compiling Std.Lean.MonadBacktrack
[84/3810] Compiling Std.Lean.PersistentHashSet
[85/3810] Compiling Std.Tactic.Exact
[86/3810] Compiling Std.Tactic.Instances
[87/3810] Compiling Std.Tactic.Where
[93/3810] Building ProofWidgets.Data.Json
[110/3810] Compiling Std.Classes.SetNotation
[111/3810] Compiling Std.Lean.Format
[112/3810] Compiling Std.Tactic.NoMatch
[113/3810] Compiling Std.Lean.AttributeExtra
[114/3810] Compiling Std.Util.Pickle
[115/3810] Compiling Std.CodeAction.Attr
[116/3810] Compiling Std.Tactic.GuardExpr
[117/3810] Compiling Std.Lean.Meta.InstantiateMVars
[118/3810] Compiling Std.Lean.Meta.Clear
[119/3810] Compiling Std.Lean.Meta.AssertHypotheses
[120/3810] Compiling Std.Tactic.PrintDependents
[121/3810] Compiling Std.Tactic.CoeExt
[122/3810] Compiling Std.Data.Int.Basic
[123/3810] Compiling Std.Data.Nat.Basic
[124/3810] Compiling Std.Data.Char
[125/3810] Compiling Std.Control.ForInStep.Lemmas
[197/3810] Compiling Std.Linter.UnreachableTactic
[198/3810] Compiling Std.Tactic.Lint.Basic
[199/3810] Compiling Std.Lean.Meta.SavedState
[200/3810] Compiling Std.Tactic.Ext.Attr
[201/3810] Compiling Mathlib.Util.WhatsNew
[202/3810] Compiling Mathlib.Tactic.PPWithUniv
[203/3810] Compiling Mathlib.Mathport.Attributes
[204/3810] Compiling Mathlib.Tactic.Alias
[205/3810] Compiling Mathlib.Mathport.Rename
[209/3810] Building ProofWidgets.Compat
[210/3810] Compiling Std.Tactic.Simpa
[214/3810] Compiling Std.CodeAction.Basic
[215/3810] Compiling Std.Tactic.NormCast.Ext
[216/3810] Compiling Std.Control.ForInStep
[252/3810] Compiling Std.Tactic.TryThis
[253/3810] Compiling Std.Data.Array.Init.Basic
[254/3810] Compiling Std.Linter.UnnecessarySeqFocus
[255/3810] Compiling Std.Tactic.Lint.Frontend
[256/3810] Compiling Std.Classes.Cast
[263/3810] Building ProofWidgets.Component.Basic
[264/3810] Compiling Std.Classes.Order
[268/3810] Compiling Std.Tactic.Lint.Simp
[270/3810] Compiling Std.CodeAction.Misc
[271/3810] Compiling Std.Tactic.NormCast.Lemmas
[281/3810] Compiling Std.Tactic.SimpTrace
[282/3810] Compiling Std.Tactic.ShowTerm
[283/3810] Compiling Std.Linter
[284/3810] Compiling Std.Tactic.GuardMsgs
[288/3810] Compiling Std.Data.Array.Basic
[289/3810] Building ProofWidgets.Component.Panel
[290/3810] Building ProofWidgets.Data.Html
[294/3810] Compiling Std.CodeAction
[297/3810] Compiling Std.Tactic.SqueezeScope
[300/3810] Compiling Std.Tactic.Lint.Misc
[301/3810] Compiling Std.Tactic.Lint.TypeClass
[302/3810] Building ProofWidgets.Component.PenroseDiagram
[303/3810] Building ProofWidgets.Presentation.Expr
[305/3810] Building ProofWidgets.Component.SelectionPanel
[309/3810] Compiling Std.Tactic.Lint
[311/3810] Compiling Std.Tactic.Basic
[315/3810] Compiling Std.Logic
[317/3810] Compiling Std.Tactic.Ext
[323/3810] Compiling Std.Data.PairingHeap
[324/3810] Compiling Std.Data.Nat.Init.Lemmas
[325/3810] Compiling Std.Classes.LawfulMonad
[329/3810] Compiling Std.Tactic.Congr
[330/3810] Compiling Std.Data.RBMap.Basic
[333/3810] Compiling Std.Data.Fin.Basic
[338/3810] Compiling Std.Data.RBMap.WF
[339/3810] Compiling Std.Data.Nat.Lemmas
[340/3810] Compiling Std.Data.Option.Basic
[342/3810] Compiling Std.Data.Array.Init.Lemmas
[348/3810] Compiling Std.Data.RBMap
[349/3810] Compiling Std.Data.RBMap.Alter
[350/3810] Compiling Std.Data.BinomialHeap.Basic
[351/3810] Compiling Std.Data.String.Basic
[352/3810] Compiling Std.Data.Nat.Gcd
[356/3810] Compiling Std.Data.Array.Merge
[357/3810] Compiling Std.Data.List.Basic
[359/3810] Compiling Std.Data.Option.Lemmas
[363/3810] Compiling Std.Data.Fin.Lemmas
[364/3810] Compiling Std.Data.BinomialHeap.Lemmas
[366/3810] Compiling Std.Data.Int.Lemmas
[372/3810] Compiling Mathlib.Lean.Meta
[373/3810] Compiling Mathlib.Lean.Expr.Basic
[374/3810] Compiling Std.Data.AssocList
[380/3810] Compiling Std.Data.BinomialHeap
[383/3810] Compiling Std.Data.Int.DivMod
[384/3810] Compiling Std.Lean.Meta.DiscrTree
[396/3810] Compiling Mathlib.Lean.Elab.Tactic.Basic
[397/3810] Compiling Mathlib.Tactic.Relation.Symm
[398/3810] Compiling Mathlib.Tactic.Relation.Rfl
[399/3810] Compiling Mathlib.Tactic.Cases
[401/3810] Compiling Std.Data.List.Lemmas
[404/3810] Compiling Std.Data.HashMap.Basic
[412/3810] Compiling Mathlib.Tactic.Relation.Trans
[415/3810] Compiling Std.Data.Rat.Basic
[417/3810] Compiling Std.Data.RBMap.Lemmas
[418/3810] Compiling Std.Data.Range.Lemmas
[421/3810] Compiling Std.Data.Array.Lemmas
[427/3810] Compiling Std.Data.String.Lemmas
[428/3810] Compiling Std.Data.Rat.Lemmas
[429/3810] Compiling Std.Classes.RatCast
[439/3810] Compiling Std.Data.HashMap.WF
[440/3810] Compiling Std.Data.String
[441/3810] Compiling Std.Data.Rat
[448/3810] Compiling Std.Data.HashMap
[449/3810] Compiling Std.Lean.Meta.UnusedNames
[538/3810] Compiling Std
[541/3810] Compiling Mathlib.Tactic.Basic
[554/3810] Compiling Mathlib.Init.Logic
[565/3810] Compiling Mathlib.Init.Align
[576/3810] Compiling Mathlib.Tactic.ToLevel
[580/3810] Compiling Mathlib.Tactic.DeriveToExpr
[586/3810] Compiling Mathlib.Tactic.ToExpr
[590/3810] Building scripts.checkYaml
[591/3810] Building scripts.runLinter
[594/3810] Compiling scripts.checkYaml
[595/3810] Compiling scripts.runLinter
[778/3810] Linking checkYaml
[778/3810] Linking runLinter

real    1m21.224s
user    1m1.064s
sys 0m5.662s

Okay, that's not too bad - but it was taking 10s of minutes on one of my branches earlier in the week - but perhaps that was a separate problem.

Mario Carneiro (Aug 21 2023 at 23:24):

oh crap, apparently scripts.checkYaml has unnecessarily added a dependency on all of Std transitively via Mathlib.Tactic.Basic, cc: @Eric Wieser

Eric Wieser (Aug 21 2023 at 23:26):

Oops, I assumed the burden would be paid only by CI

Mario Carneiro (Aug 21 2023 at 23:26):

runLinter too I guess, via Mathlib.Tactic.ToExpr -> Mathlib.Tactic.DeriveToExpr -> Mathlib.Tactic.ToLevel -> Mathlib.Init.Align -> Mathlib.Init.Logic -> Mathlib.Tactic.Basic -> Std

Eric Wieser (Aug 21 2023 at 23:27):

Align -> Std seems like the bad link there

Gabriel Ebner (Aug 21 2023 at 23:32):

We could also remove the @[default_target] from checkYaml and runLinter (the other scripts are only built when necessary).

Mario Carneiro (Aug 21 2023 at 23:43):

I think that is reasonable for mathlib, although I think it is orthogonal to the issue of decreasing the compile dependencies of those targets

Mario Carneiro (Aug 21 2023 at 23:45):

I think we might want to rethink our imports more generally so that non-tactic files get Std in bulk and init files and tactics import only what they need

Mario Carneiro (Aug 21 2023 at 23:56):

Actually I think the Mathlib.Tactic.ToLevel -> Mathlib.Init.Align was the mistaken one, I think someone was trying to get the #align command but that is supplied by Mathlib.Mathport.Rename, Mathlib.Init.Align is basically "all of lean 3 core"

Mario Carneiro (Aug 22 2023 at 00:06):

#6716

Last updated: Dec 20 2023 at 11:08 UTC