can an attribute access the Syntax of a decl?

Stream: lean4

[David Renshaw]

Attributes can see their own syntax: https://github.com/leanprover/lean4/blob/be977579821440a5529dc1c216fab58f854b2db8/src/Lean/Attributes.lean#L50-L51

Is there a way for attributes to see the syntax of the declarations that they decorate?

@[my_attribute]
def foo := 11

Like, I want my implementation of my_attribute to have access to the Syntax of def foo := 11.

[David Renshaw]

The approach I've landed on is: I'm going to define my own attribute-like thing using slightly different syntax:

#[my_pseudoattribute]
def foo := 11

Then I can do anything I want in the elaboration of my_pseudoattribute, including stashing the syntax of the decl that it adorns.

[Henrik Böving]

What do you want to do with the syntax? You can easily get access to the elaborated version through meta programming.

[David Renshaw]

This is for https://github.com/dwrensha/math-puzzles-in-lean4
I want the checked-in code for a problem to contain the full solution code, and I want to be able to extract problem-only versions of the code from that.
So I want to replace the bodies of certain definitions with sorry.

[David Renshaw]

My pseudoattribute approach looks promising: I'll store source code spans for the code that I want to end up in the extracted file.

[Eric Wieser]

Note that MIL solves this via text processing and --SOLUTION/--BOTH markers

[Joachim Breitner]

Instead of an attribute, I'd probably implement this using a custom tactic and/or term elaborator, which stores the source code spans of it's argument. This way you could even hide only parts of a definition/proof.
(Not that I know how to do it, I'd just hope I would find out :-))

[Eric Wieser]

I would imagine that the #Lean for teaching stream has other solutions to this problem

[David Renshaw]

text processing sounds imprecise :)

[Joachim Breitner]

But yes, comments and regexes may be the better solution :sweat_smile:

[David Renshaw]

besides, I can't resist the opportunity to abuse Lean's metaprogramming facilities (and to learn more about them in the process)

[Patrick Massot]

The comments and python processing approach is clearly a hack and I would love to get rid of it in MIL.

[David Renshaw]

I got a basic version of my pseudo-attributes to work: https://github.com/dwrensha/math-puzzles-in-lean4/commit/86b0f57678c3e1e8790908b1319ec5aea458c739

[David Renshaw]

this dashboard is the result: https://dwrensha.github.io/math-puzzles-in-lean4/

[David Renshaw]

click on a problem name to get an extracted solution-less version of it

[David Renshaw]

click on the check or x-mark next to it to go to the source code, possibly containing a full solution

[Mac Malone]

@David Renshaw I would be worried about the fact that #[...] clashes with the #[...] used for Array literals. I would suggest using @@[...] or @[[...]] instead.

[David Renshaw]

Fair point. @@[...] looks good to me, though I am a bit sad about needing one extra keystroke

[David Renshaw]

alternative: %[...], where the percent sign stands for pseudo-attribute

[Mac Malone]

@David Renshaw Yeah, I considered %[...[, my concern there is that if Lean, Std, etc. needs and other List/Array style literal in the future it may use %[...] and the pseudo-attribute would then clash with it. Whereas, t is very unlikely add a @@[...] / @[[...]] except for a similar purpose (and attribute variant).

[Thomas Murrills]

I might suggest @%[...], because % usually connotes something to do with elaboration, and suggests that the @tribute works “on the same level” as elaboration/has access to syntax

[Mario Carneiro]

I'd rather just use @[...] and pass along the syntax

[Mac Malone]

@Mario Carneiro That cannot work in general. Attributes may (and are) applied in places where the syntax of the target is unavailable (e.g., attribute [foo] bar).

[Mac Malone]

Though, looking into it more, in @David Renshaw's case, since the token he is using is the complete attribute (e.g., #[problem_statement]), any of @[], #[], %[], etc. would work without clashing since that token will always take precedence.

[Mario Carneiro]

Mac Malone said:

Mario Carneiro That cannot work in general. Attributes may (and are) applied in places where the syntax of the target is unavailable (e.g., attribute [foo] bar).

That seems fine, you would just pass the syntax of the command, whatever it is

[Thomas Murrills]

You could pass an Option Syntax to make handling those “nonlocal” attribute applications easier on the person writing the attribute (so attribute [foo] bar would pass none, and you could easily throw an error)

[David Renshaw]

I got rid of my #[problem_statement] pseudo-attribute and now instead have declared problem to be a synonym of theorem (similar to how Mathlib does this for lemma): https://github.com/dwrensha/math-puzzles-in-lean4/commit/4115c93f3c03645420bc5dd84fccc160606416b2

[David Renshaw]

I intend to do something similar with #[solution_data], but it's less clear what to do with #[problem_setup], which can adorn any command (e.g. infix, open, ...).

[James Gallicchio]

is there a way you can use sections?

[David Renshaw]

Maybe! That was in fact going to be my next line of investigation.

[David Renshaw]

something like problem_setup_section gets included in an extracted problem, while everything else gets excluded by default