An external Lean 4 checker (and a book)

Stream: lean4

[Chris Bailey]

For those who are interested in this side of things, the rust flavored external type checker is now up to date with Lean 4 and can be used to check Lean 4 export files. It includes optional support for the Nat and String literal kernel extensions, and supports a basic form of axiom whitelists to address a common concern in earlier discussions.

I also published the first draft of a book about the kernel, trust/export matters, and writing your own external checker. I know there are many domain experts here with very deep knowledge of this domain, so please consider contributing if that's you.

I would like to add that this work was done with the support of the Lean FRO.

[Kim Morrison]

We've being talking about changing our current CI for Mathlib, so that rather than running lean4checker on every push, we only run it on staging commits.

Ideally we would actually run multiple checkers there, including nanoda. What do we need to do to run nanoda in Mathlib CI?

[Chris Bailey]

You need cargo to build the program itself, and for now you need to use this fork of lean4export to produce the export file. There's an open PR to move these changes upstream.

The other thing you need is to set up a config file to pass to the binary. There any community standards for pretty printers yet, so if a human reviewer isn't going to check the pretty printer output you can just omit printing and run the checker; an example config would be:

{
    "export_file_path": "<path to export file>",
    "use_stdin": false,
    "num_threads": <num threads>,
    "permitted_axioms": [
        "propext",
        "Classical.choice",
        "Quot.sound",
        "Lean.trustCompiler"
    ],
    "unpermitted_axiom_hard_error": false,
    "nat_extension": true,
    "string_extension": true,
    "print_success_message": true
}

Or you can leave out export_file_path, set use_stdin to true, and pipe the output of lean4export into stdin instead.

One soft issue that comes up with developments that depend on core is that sorryAx, Lean.ofReduceBool and Lean.ofReduceNat are part of the exported environment, but they're not used by anything. The current options are to just let the checker ignore them entirely, or to put them in the whitelist which will check them, but would also let them be used by subsequent declarations. The config above just ignores them. If the exporter is modified to allow exclusions, excluding them from export would also be an option.

[Mario Carneiro]

If you make releases in github CI, mathlib CI could download it instead of building it every time

[Mario Carneiro]

see the leangz workflow, which is used to build leantar which is a rust program used by mathlib CI

[Chris Bailey]

Thanks, I'll look into that and report back.

[Chris Bailey]

@Mario Carneiro I set up a release action, so the release assets should be available. Let me know if I didn't get the right target triple for the Mathlib CI or something.

[Floris van Doorn]

We should add a link to this book to https://leanprover-community.github.io/learn.html#more-on-foundations

[Patrick Massot]

Wait, isn't it there already? It seems to have been added two weeks ago already.

[Chris Bailey]

That PR was accepted, and I'm able to see it in the More on Foundations section. The vote of confidence from Floris van Doorn is still greatly appreciated.

[Patrick Massot]

And I voted twice: once when I approved Floris's suggestion above and once when I merged the PR two weeks ago...

[Kim Morrison]

What do we still need to do to have this run during Mathlib CI?

[Chris Bailey]

I set up a job to create/offer binaries for releases which gets rid of the cargo/rustc stuff, so this minus the cargo requirement. Get the appropriate build artifact from the release, use the linked fork of lean4export to build the export file, and then run the checker against the export file.

[Floris van Doorn]

Patrick Massot said:

Wait, isn't it there already? It seems to have been added two weeks ago already.

Oh, my bad. I didn't read carefully enough!

[Mauricio Collares]

Can the answer at https://lean-lang.org/lean4/doc/faq.html#is-lean-sound-how-big-is-the-kernel-should-i-trust-it be updated to contain this information?

[Kim Morrison]

If someone suggests a blob of text to add, I can make the change.