lean4checker found a problem in ProofWidgets.Data.Svg

Stream: new members

[Adomas Baliuka]

I'm trying to use lean4checker. In a basically empty project that depends on Mathlib, I get a "problem" reported in ProofWidgets.Data.Svg. Does anyone know how to investigate this? It doesn't seem like Lean4checker has built-in ways to get more information?

> lake env ../lean4checker/.lake/build/bin/lean4checker
lean4checker found a problem in ProofWidgets.Data.Svg

[Joachim Breitner]

Likely this issue:
The ProofWidgets “cloud release”, which you download for the .js files, contains .oleans that may not be compatible with your version of lean/lean4checker, but are still picked up because lean4checker simply checks all of **/*.olean.

A work-around (also used by mathlib ci) is to delete

rm -rf .lake/packages/proofwidgets/.lake/build/lib
rm -rf .lake/packages/proofwidgets/.lake/build/ir

More context in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235

[Adomas Baliuka]

Thanks! Now I get no issues locally but on GitHub Actions I get "lean4checker found a problem in Mathlib", which is weirdly unspecific. Could it be due to the .oleans downloaded in the cache being incompatible somehow? On the other hand, people use lean4checker in GitHub Actions, so I'm puzzled...

[Mario Carneiro]

"lean4checker found a problem in Mathlib" isn't actually unspecific, it's saying it found a problem in the root file, which is also the first file read, so probably there is some issue that affects every .olean file

[Mario Carneiro]

The most likely issue is that your lean4checker is not built for the same version of lean as the olean files you are downloading

[Mario Carneiro]

try setting the lean-toolchain of lean4checker to match mathlib and recompile it

[Adomas Baliuka]

I did copy over the toolchain from mathlib to lean4checker (even in the CI).

[Adomas Baliuka]

For reference, this is my Github workflow:

      - name: Get cache
        run: ~/.elan/bin/lake -Kenv=dev exe cache get

      - name: Build project
        run: ~/.elan/bin/lake -Kenv=dev build Lean4Hacking

      - name: check that all files are imported
        run: git diff --exit-code

      - name: check environments using lean4checker
        id: lean4checker
        run: |
          git clone https://github.com/leanprover/lean4checker
          cd lean4checker
          git checkout toolchain/v4.5.0-rc1
          # Now that the git hash is embedded in each olean,
          # we need to compile lean4checker on the same toolchain
          cp ../lean-toolchain .
          ~/.elan/bin/lake build
          # sed -i 's/lake/~\/.elan\/bin\/lake/g' ./test.sh
          # ./test.sh
          cd ..

          # Remove proofwidgets because it uses oleans built on another system, which lean4checker rejects
          rm -rf .lake/packages/proofwidgets/.lake/build/lib
          rm -rf .lake/packages/proofwidgets/.lake/build/ir
          ~/.elan/bin/lake env lean4checker/.lake/build/bin/lean4checker

[Mario Carneiro]

git checkout toolchain/v4.5.0-rc1

Isn't mathlib on v4.6.0-rc1 now?

[Adomas Baliuka]

I copied this from some other CI... but yeah, that might be a problem. Will look at the versions

[Mario Carneiro]

I think it's okay, it's saying that this is the 4.5.0-rc1 version of leanchecker but the toolchain is replaced afterwards so as long as the build works it should be fine

[Mario Carneiro]

can you replicate the issue locally?

[Adomas Baliuka]

Mario Carneiro said:

can you replicate the issue locally?

Unfortunately not

[Mario Carneiro]

do you have a CI run you can link to?

[Adomas Baliuka]

Mario Carneiro said:

do you have a CI run you can link to?

https://github.com/adomasbaliuka/lean4-hacking/actions/runs/7811927086/job/21307917732

[Mario Carneiro]

your lean-toolchain says v4.5.0

[Adomas Baliuka]

Is that a problem? There's too many versions of things that are confusing me. There's the Lean versions used to build Mathlib, lean4checker and my project, and then there's the versions of lean4checker and Mathlib themselves...

[Mario Carneiro]

I think it's not a problem

[Mario Carneiro]

lean4checker is not particularly chatty. Can you run something like xxd ./.lake/build/lib/Mathlib.olean | head -5 and xxd ./lean4checker/.lake/build/lib/Lean4Checker.olean | head -5?

[Adomas Baliuka]

Is there a way to single-thread lean4checker? Locally it runs out of memory for me. (So I can't reproduce neither the positive nor negative outcome locally, it just passes individual modules)

[Mario Carneiro]

env LEAN_NUM_THREADS=1 lake env lean4checker

[Mario Carneiro]

there might also be an option in lean4checker itself, but that affects any lean threadpools

[Adomas Baliuka]

Tough luck... it still crashes with out-of-memory locally. 25GB is not enough. I'm running the xxd, so far got

xxd: ./.lake/build/lib/Mathlib.olean: No such file or directory
xxd: Broken pipe
00000000: 6f6c 6561 6e01 3161 3330 3231 6639 3865  olean.1a3021f98e
00000010: 3535 6132 3734 3231 3762 3362 6266 3932  55a274217b3bbf92
00000020: 6232 6434 3439 6261 6538 3433 6333 0000  b2d449bae843c3..
00000030: 0000 e4a1 4b4e 0000 b829 e4a1 4b4e 0000  ....KN...)..KN..
00000040: 0000 0000 0100 00f9 0500 0000 0000 0000  ................

[Adomas Baliuka]

Weird the Mathlib olean isn't there... (it's also not there locally, so at least that makes sense)

[Mario Carneiro]

it should have been downloaded by lake exe cache get?

[Mario Carneiro]

oh it's at .lake/packages/Mathlib/.lake/build/lib/Mathlib.olean

[Adomas Baliuka]

New output in CI

00000000: 6f6c 6561 6e01 3161 3330 3231 6639 3865  olean.1a3021f98e
00000010: 3535 6132 3734 3231 3762 3362 6266 3932  55a274217b3bbf92
00000020: 6232 6434 3439 6261 6538 3433 6333 0000  b2d449bae843c3..
00000030: 0000 a102 490f 0000 e8f8 a602 490f 0000  ....I.......I...
00000040: 0000 0000 0100 00f9 0500 0000 0000 0000  ................

00000000: 6f6c 6561 6e01 3161 3330 3231 6639 3865  olean.1a3021f98e
00000010: 3535 6132 3734 3231 3762 3362 6266 3932  55a274217b3bbf92
00000020: 6232 6434 3439 6261 6538 3433 6333 0000  b2d449bae843c3..
00000030: 0000 e4a1 4b4e 0000 b829 e4a1 4b4e 0000  ....KN...)..KN..
00000040: 0000 0000 0100 00f9 0500 0000 0000 0000  ................

Meanwhile locally, (which seems identical)

>  xxd .lake/packages/mathlib/.lake/build/lib/Mathlib.olean | head -5
00000000: 6f6c 6561 6e01 3161 3330 3231 6639 3865  olean.1a3021f98e
00000010: 3535 6132 3734 3231 3762 3362 6266 3932  55a274217b3bbf92
00000020: 6232 6434 3439 6261 6538 3433 6333 0000  b2d449bae843c3..
00000030: 0000 a102 490f 0000 e8f8 a602 490f 0000  ....I.......I...
00000040: 0000 0000 0100 00f9 0500 0000 0000 0000  ................

> xxd ../lean4checker/.lake/build/lib/Lean4Checker.olean | head -5
00000000: 6f6c 6561 6e01 3161 3330 3231 6639 3865  olean.1a3021f98e
00000010: 3535 6132 3734 3231 3762 3362 6266 3932  55a274217b3bbf92
00000020: 6232 6434 3439 6261 6538 3433 6333 0000  b2d449bae843c3..
00000030: 0000 e4a1 4b4e 0000 b829 e4a1 4b4e 0000  ....KN...)..KN..
00000040: 0000 0000 0100 00f9 0500 0000 0000 0000  ................

[Mario Carneiro]

I tried locally running it after editing the line s!"lean4checker found a problem in {m}" to s!"lean4checker found a problem in {m}: {e}", and got

lean4checker found a problem in ProofWidgets: failed to read file './.lake/packages/proofwidgets/.lake/build/lib/ProofWidgets.olean', invalid header

[Mario Carneiro]

so looking for header mismatches seems to be the right idea

[Mario Carneiro]

but there is no header mismatch in the Mathlib.olean you have just shown

[Adomas Baliuka]

Doesn't my CI delete proofwidgets anyway?

[Mario Carneiro]

ah, maybe I should have done that

[Adomas Baliuka]

You can just run lean4checker locally on this? How much RAM does it use?

[Mario Carneiro]

oh, you should probably put the lines

          rm -rf .lake/packages/proofwidgets/.lake/build/lib
          rm -rf .lake/packages/proofwidgets/.lake/build/ir

before getting the cache so that you get the right version

[Mario Carneiro]

no, I also have difficulty running that command locally, but it does give that output before it eats all the memory on my system

[Adomas Baliuka]

I thought the point of deleting those is so they are not checked at all

[Mario Carneiro]

well if you just remove them then I'm not sure you get a consistent state

[Mario Carneiro]

because there are other files that want to import it

[Mario Carneiro]

Running lean4checker without arguments is equivalent to running lean4checker Mod for every module with an olean in the directory

[Adomas Baliuka]

Indeed, the Mathlib CI script linked in that issue mentioned by Joachim Breitner also does it in that order. Now I'm really confused though what the deletion actually does.

[Mario Carneiro]

and running lean4checker Mathlib results in

uncaught exception: unknown package 'ProofWidgets'

[Mario Carneiro]

which is probably the lean4checker found a problem in Mathlib error

[Mario Carneiro]

the deletion is supposed to remove olean files unpacked from the proofwidgets release

[Mario Carneiro]

because we want to instead get these olean files from the mathlib cache

[Adomas Baliuka]

That's still really confusing to me... why does the mathlib cache not either 1) get the right version even if the files are present or 2) leave those files alone even if they are missing?

[Adomas Baliuka]

The cache is Mathlib-specific, right? Usually packages don't have something like this. So proofwidgets also doesn't have a separate cache? Where do the files I'm deleting come from?

[Mario Carneiro]

proofwidgets uses lake upload, which is a separate cache-like mechanism built directly into lake, and it doesn't play well with cache

[Mario Carneiro]

this is annoying and a cause of several issues but we need it because the proofwidgets cache contains .js files and without it you would need npm to compile it

[Mario Carneiro]

why does the mathlib cache not either 1) get the right version even if the files are present

Because the mathlib cache only gets files which are actually imported by mathlib, but lean4checker checks all .olean files it sees, meaning that any dangling proofwidgets files will still be out of date

[Adomas Baliuka]

Thanks for the explanation. Now I get a "problem in ProofWidgets" again...

[Mario Carneiro]

you have to run the rm after running lake once to download everything

[Mario Carneiro]

like lake exe cache should suffice

[Mario Carneiro]

the CI script from before uses lake build cache

[Adomas Baliuka]

Alright, seems like it's now trying to actually check something! Thanks