Citation for the metaprogramming book

Stream: lean4

[Tomaz Gomes]

Does anybody have a .bibtex file for citing the metaprogramming book? I tried to do it myself, but the only information I could find about the book was the list of authors

[Scott Morrison]

I would just provide the AUTHORS, TITLE, and URL field. There's no further information available than that!

[François G. Dorais]

While highly condensed, Scott's advice is right. This extensive discussion on MathOverflow might help (or confuse) you about the difficulty of making good BibTeX references to online materials.

The long story is that BibTeX is extremely outdated. BibTeX originated in 1985 and it has been stuck at version 0.99d since 2010. The previous version 0.99c is from 1988. Version 1.0 is unlikely to ever happen. Over the years, there have been numerous extensions to BibTeX with limited and often incompatible support. So, while Scott recommends using the URL field, this is not actually a standard BibTeX field and it is not universally supported. For broader support, you should use the NOTE field instead. However, for practical purposes, you should't do that since using both the NOTE and URL fields will often result in the url being printed twice.

There's no universal winning recipe with BibTeX. Unfortunately, while many alternatives do exist, none are as ubiquitous.

All that said, here you go:

@MISC {leanmetaprogrammingbook,
TITLE = {A Lean 4 Metaprogramming Book},
AUTHOR = {Arthur Paulino and Damiano Testa and Edward Ayers and Evgenia Karunus and Henrik B{\"o}ving and Jannis Limperg and Siddhartha Gadgil and Siddharth Bhat},
HOWPUBLISHED = {GitHub},
NOTE = {URL:\url{https://github.com/leanprover-community/lean4-metaprogramming-book} (visited on 2023-08-23)},
URL = {https://github.com/leanprover-community/lean4-metaprogramming-book},
URLDATE = {2023-08-23},
}

[Mac Malone]

@François G. Dorais The mathoverflow link got left in your adapted example's URL field. :wink:

[François G. Dorais]

Just fixed that! Thanks! (Well, Zulip and I had a bit of a battle just now but I think I won :smile:)

[Mauricio Collares]

Mildly off-topic: Does the author order carry extra information? It looks like lexicographical sorting (by first name, which is somewhat unusual), except that Siddharth and Siddhartha are swapped.

[Damiano Testa]

The initiator of the book is @Arthur Paulino and when I made my (tiny) contributions, he insisted that I added my name as an author, and in alphabetical order by first name.

I do not know about the Siddharth-a ordering.

[Henrik Böving]

François G. Dorais said:

While highly condensed, Scott's advice is right. This extensive discussion on MathOverflow might help (or confuse) you about the difficulty of making good BibTeX references to online materials.

The long story is that BibTeX is extremely outdated. BibTeX originated in 1985 and it has been stuck at version 0.99d since 2010. The previous version 0.99c is from 1988. Version 1.0 is unlikely to ever happen. Over the years, there have been numerous extensions to BibTeX with limited and often incompatible support. So, while Scott recommends using the URL field, this is not actually a standard BibTeX field and it is not universally supported. For broader support, you should use the NOTE field instead. However, for practical purposes, you should't do that since using both the NOTE and URL fields will often result in the url being printed twice.

There's no universal winning recipe with BibTeX. Unfortunately, while many alternatives do exist, none are as ubiquitous.

All that said, here you go:

@MISC {leanmetaprogrammingbook,
TITLE = {A Lean 4 Metaprogramming Book},
AUTHOR = {Arthur Paulino and Damiano Testa and Edward Ayers and Evgenia Karunus and Henrik B{\"o}ving and Jannis Limperg and Siddhartha Gadgil and Siddharth Bhat},
HOWPUBLISHED = {GitHub},
NOTE = {URL:\url{https://github.com/leanprover-community/lean4-metaprogramming-book} (visited on 2023-08-23)},
URL = {https://github.com/leanprover-community/lean4-metaprogramming-book},
URLDATE = {2023-08-23},
}

yay I'm a latex special case now.

[Arthur Paulino]

Mauricio Collares said:

Mildly off-topic: Does the author order carry extra information? It looks like lexicographical sorting (by first name, which is somewhat unusual), except that Siddharth and Siddhartha are swapped.

The swapping is a typo! Feel free to fix that :pray:

[Tomas Skrivan]

github supports citation file*.cff https://citation-file-format.github.io/ It might be worth setting this up for the book

[Tomas Skrivan]

you can also generate DOI with Zenodo https://docs.github.com/en/repositories/archiving-a-github-repository/referencing-and-citing-content

[Julian Berman]

you can also generate DOI with Zenodo

(IIRC we discussed this at some point. Zenodo requires version numbers to create DOIs. The book currently basically versions itself by replacing a single version over and over again, mostly because that was the most convenient way to automate "build PDF on every merge to master" without a separate release step. Obviously this is changeable, but yeah just pointing out that'd need to change at least slightly to get Zenodo to work with the setup.)