citing Metaprogramming in Lean 4

Stream: metaprogramming / tactics

[Mathis Bouverot-Dupuis]

Hello ! What is the accepted way of citing the 'Metaprogramming in Lean 4' book (e.g. in .bib format) ? Is it even common practice to cite it (or is it still being written) ?

[Kim Morrison]

There is an author list in the README at https://github.com/leanprover-community/lean4-metaprogramming-book

[Kim Morrison]

It is still being worked on, but only slowly. I don't think @David Thrane Christiansen is planning on writing about metaprogramming in the new language reference in the short term (few months), but may possibly be in the medium term? Not sure.

[Mathis Bouverot-Dupuis]

Thanks !

[David Thrane Christiansen]

I think that it'd be a bad idea to promise a specific timeline. This is absolutely a topic that is high on the list, but not highest.

[David Thrane Christiansen]

It certainly won't be during the first quarter of the year, though