the metaprogramming book

Stream: lean4

[Scott Morrison]

How is the metaprogramming book supposed to work? There are lots of intentional errors in the code, but it is essentially impossible to bump to a new toolchain, because one would have to review every error separately and decide if they are meant to be there or not!

Any ideas? I would love to bump this to nightly-2023-08-19 (which is rapidly becoming the first official release candidate). Any authors of the book want to advise? :-)

[Mario Carneiro]

regarding https://github.com/leanprover-community/lean4-metaprogramming-book I guess

[Mario Carneiro]

Is there working CI on the repo?

[Mario Carneiro]

I see a green checkmark but I'm not sure if it's running any lean

[Henrik Böving]

The CI only generates a PDF based on the markdown files AFAIK. With respect to the update I dont think there is a simpler way to do it than to read the files. Maybe we could add a command that checks that a failure with a certain message occurred such that this process is easier in the future?

[James Gallicchio]

is there a way to metaprogram a section of a lean file to say "this section of commands won't compile -- show the errors but revert the environment at the section end and don't report it as a compile error"?

seems useful for LeanInk and co, unless they already have a way for handling snippets that are expected to produce error?

[Mario Carneiro]

IIRC David Thrane Christiansen set up a process for validating error messages for FPIL

[Scott Morrison]

There is #guard_msgs in, which we use extensively in testing (and would like to use to replace all noisy tests).

[Scott Morrison]

Two options:

• use #guard_msgs, with some postprocessing that removes it from the book?
• have a .expected.out file, and CI that verifies the error messages match.

[James Gallicchio]

(personally, I would find it nice to have something in the snippet that indicates "this doesn't compile, but...". Is there a reason to postprocess it out?)

[Sebastian Ullrich]

Perhaps we do need our own Ferris
image.png

[Mario Carneiro]

https://leanprover.github.io/functional_programming_in_lean/introduction.html has something similar (without the mascot)

[Damiano Testa]

My first guess was also to use #guard_msgs, but would unique fvarmvar names cause problems anyway? (I'm on mobile and cannot check right now)

[Mario Carneiro]

FPIL also normalizes mvar names to address that issue

[Mario Carneiro]

(fvar names are generally not visible in error messages)

[Asei Inoue]

Simply using #check_failure instead of #check can eliminate errors in some places. Not sure what to do in other places.

Using #guard_msgs will probably eliminate a lot of errors, but not all. I would like to ask for other opinions on this.

see: https://github.com/leanprover-community/lean4-metaprogramming-book/pull/131

[Asei Inoue]

@Julian Berman @Arthur Paulino

Sorry for the abrupt mention. But I would like to hear your opinion on this matter.

For future updates, it is necessary to check the correctness of the code with CI. It needs a way to show ”code that should be in error" without actually making an error...

[Asei Inoue]

For example, could metaprogramming be used to create tools to assist with this?

[Julian Berman]

I'm afraid I don't know enough metaprogramming to have an educated opinion! The concept (that tests shouldn't be noisy, and that the book currently is noisy when it's showing errors) certainly makes sense to me though

[Julian Berman]

I haven't looked at that PR but I can (likely not this weekend, trying to disconnect a bit), but I will look at it sometime in the next few days if no one else gets to it first.

[David Thrane Christiansen]

I'm in the processs of using metaprogramming to create tools to assist with this over at https://github.com/leanprover/verso - but it's not quite ready yet. The setup I used for FPiL was reasonable in the meantime, though.

It's some Lean metaprograms that basically do variations on #guard_msgs, but with much uglier syntax: https://github.com/leanprover/fp-lean/blob/master/examples/Examples/Support.lean

The goal of the ugly syntax is to make it easy to extract the various bits with Python regexps and include them in the book: https://github.com/leanprover/fp-lean/tree/master/functional-programming-lean/scripts

It's a giant hack, but it works pretty well. I'll make noise when Verso is ready for this use case.

[Asei Inoue]

@Kim Morrison

I submitted a PR to show intentional errors in the code without error and it was merged. I think your concerns have been resolved.

see: https://github.com/leanprover-community/lean4-metaprogramming-book/pull/131