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)