Make some macro-introduced identifiers visible outside

Stream: lean4

[Adrien Champion]

I'm learning macros and read most of the beyond notations paper. I am wondering if it's possible to export some identifiers introduced in a macro_rules so that they are visible outside.

[Adrien Champion]

Maybe with an attribute telling lean I actively want to export some identifiers, I still want hygiene on everything but a few idents.

[Adrien Champion]

My use case is that I want to add to the namespace associated to some type I don't know, but I want what I add to be available. It's more of an exercise than a real vital thing I need at this point

[Adrien Champion]

syntax "implStaticLen!" "(" term "," term ("in" ident)? ")": command
macro_rules
  | `(
    implStaticLen! ( $value, $ty )
  ) => `(
    def staticLen: Nat := $value
    #check staticLen
  )
  | `(
    implStaticLen! ( $value, $ty in $nSpace )
  ) => `(
    namespace $nSpace
      implStaticLen! ( $value, $ty )
    end $nSpace
  )

structure Arr2 (Elm : Type u) where
  inner : Elm × Elm
implStaticLen! ( 2, Arr2 in Arr2 )
-- `#check` inside the macro gives `Map.Spec.Range.Arr2.staticLen✝ : Nat`
#check Arr2.staticLen
-- `unknown constant 'Map.Spec.Range.Arr2.staticLen'`

[Sebastian Ullrich]

You can use use docs4#Lean.mkIdent to create a syntactic identifier without hygiene information

[Adrien Champion]

Wait, mathlib4 is up? At least the lean4 part I mean?

[Adrien Champion]

It wasn't the last time I did a deep dive in lean4 (main reason I stopped diving)

But now I can stop spending my time rg-ing lean4's sources. Thanks!

[Adrien Champion]

I'm surprised it's not linked in the "official" documentation page though

[Adrien Champion]

Sebastian Ullrich said:

You can use use docs4#Lean.mkIdent to create a syntactic identifier without hygiene information

Also, thank you for your answer. It seems it's exactly what I need, but lean4's sources don't seem to use it in a macro_rules. At least now I'm on the right track, I'll figure it out

Thank you so much :smiley_cat:

[Sebastian Ullrich]

There is this slightly silly example: https://github.com/leanprover/lean4/blob/master/tests/lean/run/kevin.lean
You might need to make the syntax kind explicit after def: def $(mkIdent `staticLen):ident ...

[Mario Carneiro]

@Adrien Champion mathlib4 has been around for almost a year, but we still don't have the "real thing", it's just a grab bag of tactics and preparatory material. But it is getting better as a collection of example use cases of lean 4 metaprogramming

[Adrien Champion]

Sebastian Ullrich said:

There is this slightly silly example: https://github.com/leanprover/lean4/blob/master/tests/lean/run/kevin.lean
You might need to make the syntax kind explicit after def: def $(mkIdent `staticLen):ident ...

You really did solve everything for me :thank_you:

[Adrien Champion]

Mario Carneiro said:

Adrien Champion mathlib4 has been around for almost a year, but we still don't have the "real thing", it's just a grab bag of tactics and preparatory material. But it is getting better as a collection of example use cases of lean 4 metaprogramming

Sounds that way, although simply having lean's documentation in a nice searchable way is already going to make my life significantly easier. I really think it should be on the github.io "Documentation" page!

I heard contributing matlab4 and to the matlab3 → matlab4 transition (tactics in particular) is a great way to learn. Do you know if there are enough low-hanging fruits left at this point?

[Mario Carneiro]

the name seems to be mutating in your posts. mathlib != matlab

[Adrien Champion]

Mario Carneiro said:

the name seems to be mutating in your posts. mathlib != matlab

That was before my coffee sorry. I'm very, very glad mathlib is not the same as matlab and we're not spec/ver-ifying math stuff in simulink

[Mario Carneiro]

there are still plenty of low hanging fruits. The main thing we're working on at the moment is porting tactics listed in Mathport/Syntax.lean

[Adrien Champion]

I see, I checked for "easy first issue"-like tags in the repo's issues but to my surprise there's only 3 open ones. I quickly checked for a "contributing" thing but did not find one

[Adrien Champion]

Should I just pick on and try to write a PR then?

[Adrien Champion]

notices there's a mathlib4 channel

I should probably just take a look there

[Adrien Champion]

Sebastian Ullrich said:

There is this slightly silly example: https://github.com/leanprover/lean4/blob/master/tests/lean/run/kevin.lean
You might need to make the syntax kind explicit after def: def $(mkIdent `staticLen):ident ...

I'm wondering if there's a resource I missed for macros that would help me understand what I can and can't do. Is there?

For instance this does not work

syntax
  "repeat " "in " ident "("
    (
      declModifiers
      "fn " ident bracketedBinder* (":" term)?
      ":=" term ";"
    )*
  ")"
: command
macro_rules
| `(
  repeat in $ns (
    $[
      $fMods:declModifiers
      fn $fId:ident $fParams:bracketedBinder* $[: $fTy:term]? := $fBody:term;
    ]*
  )
) => `(
  namespace $ns:ident
--  v~~~~~ expected ')'
    $[
      $fMods:declModifiers
      def $fId:ident $fParams:bracketedBinder* $[: $fTy:term]? := $fBody:term
    ]*
  end $ns:ident
)


repeat in Dummy (
  fn blah := 7;
  fn something: Nat := 11;
)

The RHS of the macro_rules rule is rejected on the $[. I'm not sure why, I feel like I'm still missing a lot of context to understand macros and their restrictions

[Arthur Paulino]

@Adrien Champion in this case try defining a separate syntax for the thing you're signaling with multiple occurrences.

Something along the lines of syntax declModifierSyntax := declModifiers "fn " ident ...

[Arthur Paulino]

There's something strange in your syntax. I will test it on my computer in a few minutes

[Sebastian Ullrich]

I'm afraid splicing a sequence of commands is not implemented right now

#check `($cs:command*)

Please file a bug

[Arthur Paulino]

@Adrien Champion just to mention since you're interested in learning about the topic and documentation: we've kicked off a book for metaprogramming in Lean 4. I took the initiative to start the repo but it's a collaborative effort. Many of those topics are still beyond my competence but, as you said, porting mathlib4 tactics is a good way to learn. I also play with side projects to help me gather knowledge to produce more content. Help is welcome!

[Adrien Champion]

Arthur Paulino said:

Adrien Champion just to mention since you're interested in learning about the topic and documentation: we've kicked off a book for metaprogramming in Lean 4. I took the initiative to start the repo but it's a collaborative effort. Many of those topics are still beyond my competence but, as you said, porting mathlib4 tactics is a good way to learn. I also play with side projects to help me gather knowledge to produce more content. Help is welcome!

This sounds pretty interesting, I'll take a look at the book see if it helps and/or if I can contribute. Feel free to send me (DM or here) more links of lean4 codebases a noob like myself can contribute to :smiley_cat:

[Adrien Champion]

Sebastian Ullrich said:

I'm afraid splicing a sequence of commands is not implemented right now

#check `($cs:command*)

Please file a bug

I will try to do that shortly no problem :thumbs_up:

[Siddhartha Gadgil]

(deleted)