CI Lean Environment Check

Stream: Equational

[Shreyas Srinivas]

If we start using AI, we must be careful and add leanchecker in the CI

[Terence Tao]

I'm not familiar with this tool. What does it do?

By the way, I was informed that there was a run by a major AI company performed on the implications in this project, which achieved a completion rate slightly better than our current state of 99.9%; but the proofs were very lengthy and not suitable for uploading directly in the project. They are hoping to make some more targeted contributions in the near future.

[Shreyas Srinivas]

I hope I don't botch up this explanation because it is a bit subtle. Hopefully @Joachim Breitner can correct me about it. Here is a link to the tool: https://github.com/leanprover/lean4checker

While Lean remains perfectly sound, Lean's metaprogramming system is very powerful and allows some flexibility in adding declarations to the "environment". Here, the environment is the ambient context of assumptions, hypotheses, etc. It is possible for a malicious actor to sneak in a proof of False while doing this and evade #print_axioms. This will seemingly allow exfalso quodlibet proofs.

Lean4checker replays the environment from scratch, this time checking each insertion of a hypothesis into the environment, thus ensuring that no False hypothesis has been inserted into the environment.

[Shreyas Srinivas]

The reason I didn't insist on this until now is that we have been using good old fashioned AI in the form of z3, Vampire etc.

[Shreyas Srinivas]

And these have produced proof certificates. We have essentially been reconstructing their proofs. The room for human error in this has been small.

[Shreyas Srinivas]

With modern AI being unpredictable as it is, we need to add this final layer of certainty since it might discover these metaprogramming sorceries

[Terence Tao]

I see. Would you expect implementing LeanChecker to noticeably increase the CI time? If not then it seems like a no-brainer to implement it, AI or no AI

[Shreyas Srinivas]

It is definitely going to increase the CI time a bit. We should be able to use mathlib's CI action for lean4checker more or less as it is. One thing that needs checking is how it interacts with cached mathlib build files.

[Shreyas Srinivas]

Because there are some underlying C libraries that lean uses that need to matches exactly with the machine that produces mathlib's binary files.

[Shreyas Srinivas]

I can check it out now in a PR.

[Terence Tao]

As long as the CI time is still on the order of minutes instead of hours, I'd say it's worth it to have the extra guarantee. (Note to future self reading this thread: when writing the final paper, make a note of the extra layers of checking we have beyond the core Lean compiler, for instance we also have a separate check that no extra axioms are being inserted (equational#242).)

It might be good to "red team" and brainstorm for any other potential ways in which this project could be compromised, either by a glitchy AI or by some mischevious human.

[Shreyas Srinivas]

This is already part of the standard mathlib check

[Shreyas Srinivas]

@Mario Carneiro : sorry for tagging you here, but I want to make sure I understand lean4checker correctly

[Shreyas Srinivas]

Do we need to delete the entire mathlib cache and rebuild it to run lean4checker on this repo?

[Mario Carneiro]

I should first caution that lean4checker is not an "external checker", it's actually just reusing the original lean checker but from a separate process. If there is a bug in the kernel then both lean and lean4checker will be compromised

[Shreyas Srinivas]

Another thing is how frequently would you advice we run lean4checker? We have gigantic PRs with 70-80k lines of code coming in, largely of lemmas and proofs from automatic provers. There is a chance of modern AI provers soon joining the fray

[Mario Carneiro]

The time taken by lean4checker is usually negligible, for mathlib it's around 5-10% of build time

[Shreyas Srinivas]

But mathlib's cache builds come from the same machine on which lean4checker runs correct?

[Shreyas Srinivas]

here we are using lake exe cache to get mathlib oleans

[Mario Carneiro]

I don't think it is in anyone's benefit to reduce the rate of running a trusted kernel

[Shreyas Srinivas]

Mathlib runs it once in 24 hours

[Shreyas Srinivas]

We might have to build mathlib in our CI from scratch to make sure that the machine bignum libraries match

[Mario Carneiro]

I'm aware, but mathlib also runs a lot of side runs and things. I don't think it was a good decision even then

[Mario Carneiro]

if you want high assurance the first thing you should be doing is actually running the piece of software that promises the high assurance

[Mario Carneiro]

lean4checker will check what you configure it to check. It can check everything including the parts of mathlib you depend on if you want it to

[Shreyas Srinivas]

If we configure it to only check the code we write, is that safe? and does that help us avoiding rebuilding mathlib from scratch locally?

[Mario Carneiro]

While we're on the subject, I'll also mention lean4lean, which is actually an external checker, and has the same interface as lean4checker

[Mario Carneiro]

Neither of these tools requires that you rebuild mathlib

[Mario Carneiro]

they work based on the produced .olean files

[Shreyas Srinivas]

The lean4checker explicitly advises against using cached oleans

[Mario Carneiro]

oleans that cause lean4checker to have problems also cause lean to have problems

[Mario Carneiro]

so as long as the cache is working for you there is not much to worry about

[Mario Carneiro]

the text there actually says that it will fail if you give it oleans for the wrong OS

[Mario Carneiro]

which is fine, that's failing in the right direction

[Notification Bot]

34 messages were moved here from #Equational > Thoughts and impressions thread by Shreyas Srinivas.

[Mario Carneiro]

in any case, when you use lake exe cache get you aren't downloading .oleans directly, you are downloading a cross platform format .lgz which is unpacked into .oleans suitable for your OS

[Shreyas Srinivas]

I am now considering setting up lean4lean

[Shreyas Srinivas]

If we want high assurance, we might as well go for the highest assurance

[Shreyas Srinivas]

Is there like a general instruction file on how to use lean4lean on other projects?

[Mario Carneiro]

the instructions are in the readme, LMK if they need improvement

[Shreyas Srinivas]

okay, I will get on with it and if I succeed, we should have lean4lean checking each PR

[Shreyas Srinivas]

@Mario Carneiro : I tested lean4lean locally

[Shreyas Srinivas]

Initially it failed on the equations project

[Shreyas Srinivas]

Then I tried it on a fresh batteries clone and it reported failures

[Shreyas Srinivas]

Turns out the toolchains need to match

[Shreyas Srinivas]

I got it working for batteries toolchain v4.12.0-rc1

[Shreyas Srinivas]

This is the latest toolchain on lean4lean

[Mario Carneiro]

yes, you need to rebuild it with the same toolchain as the project

[Mario Carneiro]

same for lean4checker btw

[Shreyas Srinivas]

yeah but Kim keeps lean4checker up to date

[Shreyas Srinivas]

Can I push an update and a regular CI script to keep the toolchain up to date?

[Mario Carneiro]

Shreyas Srinivas said:

yeah but Kim keeps lean4checker up to date

I don't think so? The script to run lean4checker on your project just rebuilds it, and it doesn't break often

[Mario Carneiro]

Shreyas Srinivas said:

Can I push an update and a regular CI script to keep the toolchain up to date?

Sure. Is lean-action able to do this?

[Shreyas Srinivas]

I tried building lean4lean on 4.13.0-rc3

[Shreyas Srinivas]

It fails on batteries dependencies

[Shreyas Srinivas]

I'll try deleting the manifest

[Shreyas Srinivas]

It still errors, this time on Verify

[Shreyas Srinivas]

First error:

error: ././././Lean4Lean/Verify/Axioms.lean:10:36: invalid field 'data', the environment does not contain 'Array.data'
  x✝
has type
  Array α

[Shreyas Srinivas]

I got the lean4lean cli to build, but I did not have to do this on 4.12.0-rc1

[Mario Carneiro]

wow, apparently lean core is still struggling with backward compatibility

[Mario Carneiro]

I'll deal with this, not right now

[Shreyas Srinivas]

Oh and lean4lean managed to crash my system

[Shreyas Srinivas]

To be fair equational_theories has some huge files

[Mario Carneiro]

you have to be careful, the multithreaded mode tends to use up all your memory if you don't limit the number of threads because it has to build a bunch of mathlibs in memory

[Mario Carneiro]

I can usually only run it in single threaded mode

[Shreyas Srinivas]

Yes. 28 GB out of 32GB ram

[Shreyas Srinivas]

It went upto 35 and started using swap

[Shreyas Srinivas]

I have never been in that territory with this machine

[Shreyas Srinivas]

It did find a problem in ProofWidgets.Component.Recharts

[Shreyas Srinivas]

README doesn't suggest an option to limit threads.

[Mario Carneiro]

env LEAN_NUM_THREADS=n lean4lean ...

[Shreyas Srinivas]

Okay. I started it with taskset

[Mario Carneiro]

(BTW IIRC lean4checker has exactly the same behavior in terms of memory usage)

[Mario Carneiro]

maybe there is something more that can be done about it

[Shreyas Srinivas]

The taskset solution worked for a while, but memory started filling up very quickly

[Shreyas Srinivas]

Now trying the env method you suggested

[Shreyas Srinivas]

A few observations about lean4lean run on the project.

1. I ran it with 2 threads starting at roughly 3:25 am. As of 3:48 am lean4lean is still running. This means CI runs are going to be very very long.
2. It takes upto 10 GB of RAM on an 9th gen i9 processor with 32 GB RAM. While not exactly brand new, this processor is rather powerful. I am guessing github doesn't run its CI allocating such resources.
3. The threads seem to be unevenly used at times. I can't explain why. This is especially close to files for which lean4lean posts large numbers inside the occasional "lean4lean took xxxx" updates
4. About the updates. On the one hand it serves as a nice progress counter. On the other hand if lean4lean finds a problem, it simply logs them in the same stream of outputs.
5. The units of lean4lean took xxxx are unclear and I would guess milliseconds. I would also venture a guess that it reports whenever a file takes more than 1000 milliseconds or so
6. Could we have an option to get only the summary of problematic files in the end?

[Mario Carneiro]

there shouldn't be any problematic files, unless by problematic you mean taking a long time

[Shreyas Srinivas]

lean4lean found a problem in ProofWidgets.Component.Recharts

[Shreyas Srinivas]

The only one so far

[Mario Carneiro]

there should be an error after that?

[Mario Carneiro]

actually it should immediately exit after printing that

[Shreyas Srinivas]

None. lean4lean continues running and posting updates for files and lean4lean took xxxx where xxxx > 1000 always

[Shreyas Srinivas]

This one has the largest xxxx : Mathlib.Analysis.Complex.UpperHalfPlane.Metric:thmDecl UpperHalfPlane.isometry_vertical_line: lean4lean took 25603

[Mario Carneiro]

the times are in ms as you predicted

[Shreyas Srinivas]

Here's a screenshot:
Screenshot from 2024-10-06 03-58-02.png

[Shreyas Srinivas]

should have cropped that

[Mario Carneiro]

oh note that the error is printed to stderr, while the rest goes to stdout, so there could be some races between the prints

[Shreyas Srinivas]

It's still running so it didn't quit after the error

[Mario Carneiro]

try changing Main.lean:288 to IO.eprintln s!"lean4lean found a problem in {m}: {e.toString}" and see if you get any more information

[Shreyas Srinivas]

I still want to find out how many minutes it takes to finish the run

[Shreyas Srinivas]

I'll try after this run

[Mario Carneiro]

I don't think I've ever tried to build mathlib in that configuration

[Mario Carneiro]

the paper claims it can do mathlib in 58 minutes

[Shreyas Srinivas]

Two more 10k+ champions:

Mathlib.NumberTheory.RamificationInertia:thmDecl Ideal.powQuotSuccInclusion_injective: lean4lean took 11703
Mathlib.NumberTheory.FactorisationProperties:thmDecl Nat.weird_seventy: lean4lean took 14217

[Mario Carneiro]

(in case it wasn't clear, this is not the configuration you want for CI. It's spending all its time checking mathlib instead of your project)

[Mario Carneiro]

I think you want lean4lean Equational where Equational is replaced by the name of the root module

[Shreyas Srinivas]

Oh I see

[Mario Carneiro]

also with LEAN_NUM_THREADS set to something low

[Mario Carneiro]

the default behavior is to check every .olean file in .lake

[Shreyas Srinivas]

I terminated the older run at 4:10 am

This new run on the project was instantaneous

[Shreyas Srinivas]

but gave no success message

[Shreyas Srinivas]

Mario Carneiro said:

try changing Main.lean:288 to IO.eprintln s!"lean4lean found a problem in {m}: {e.toString}" and see if you get any more information

Tried this suggestion on the older run (equivalent to --fresh I guess)

[Shreyas Srinivas]

Got a longer error message

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

[Shreyas Srinivas]

But lean4lean hasn't quit

[Shreyas Srinivas]

The good news in all this is that the project is sound so far

[Mario Carneiro]

ah right, I remember this issue. ProofWidgets has a flag saying to download a release, even though it contains out of date olean files. lake exe cache replaces them with correct olean files, but some files are left over and not overwritten, for lean files that have since been deleted

[Mario Carneiro]

these files are basically dead and unused, but lean4lean just checks everything in the folder because it doesn't do dependency analysis in the default mode because it doesn't know what the target is

[Mario Carneiro]

when you do lean4lean Equational it will check only the dependencies of Equational module, so make sure all the results you want checked are transitively reachable from it

[Shreyas Srinivas]

will do. I need to catch some sleep. I will put the CI up tomorrow

[Mario Carneiro]

Shreyas Srinivas said:

Can I push an update and a regular CI script to keep the toolchain up to date?

I pushed an update, but you are welcome to add the CI script

[Shreyas Srinivas]

@Mario Carneiro : Is it okay if I add tags to lean4lean? From the equational_theories side, it makes a lot of sense to clone the repository at the matching tag and if one is not found then complain about it.

[Shreyas Srinivas]

The alternative is to read the lean4lean file's lean-toolchain

[Shreyas Srinivas]

@Terence Tao : I am sorry it took me a couple of days, since I have been chasing other deadlines in my day job (PhD). I'll get this CI integrated now

[Shreyas Srinivas]

At the very least there will be a script to check the project with lean4lean soon.

[Shreyas Srinivas]

The CI PR is up already. Currently it only applies lean4lean if the toolchains match and if a freshly cloned lean4lean builds.

[Shreyas Srinivas]

@Mario Carneiro : in equational#421 we have CI action which invokes a python script that runs lean4lean on the project.

[Shreyas Srinivas]

One thing that bothers me is that lean4lean seems to run nearly instantaneously

[Mario Carneiro]

how did you invoke it?

[Shreyas Srinivas]

I want to make sure the script is doing the right thing.

[Shreyas Srinivas]

env LEAN_NUM_THREADS=2 lake env <lean4lean_bin_path> --verbose equational_theories

[Shreyas Srinivas]

Important point : The script is called as a step in the blueprint.yml CI where the project has already been built

[Shreyas Srinivas]

@Mario Carneiro : quick reminder about this.

[Shreyas Srinivas]

I was reading that script and realised it would be pointless to run lake update when trying to match toolchains