Reference

Stream: mathlib4

[Xavier Roblot]

I am not sure I understand how bibliographic references work in Mathlib docs. For example, looking at the Function field file. Only one reference listed there actually points to the corresponding entry of the References page. However, looking at the file references.bib in the docs folder, I can see that a reference with the key marcus1977number is indeed there. (The reference to Samuel's book is incorrect though since the key should be samuel1967). Something similar happens in this file.

So, why isn't the reference to Marcus found and how to fix that?

[Kevin Buzzard]

I am really quite surprised that even though mathlib has many many references https://leanprover-community.github.io/mathlib4_docs/references.html the last one alphabetically apparently starts with L. This might have something to do with it...

[Ruben Van de Velde]

I meant to debug this a while ago but didn't get around to it, so thanks for bringing it up!

[Ruben Van de Velde]

Hmm, I thought we'd see that no references after the last one in references.bib were included, but that's not it

[Ruben Van de Velde]

Hypothesis: something throws an exception (or similar) while processing the references, after they've been sorted by author, on the reference that comes after Lack

[Xavier Roblot]

That sounds like a reasonable hypothesis

[Ruben Van de Velde]

Can't test it right now, and the ci logs don't seem to have anything obviously wrong

[Xavier Roblot]

I created a LaTex file and used references.biband everything works fine :thinking:

[Kevin Buzzard]

What is the reference after Lack--Sobocinski alphabetically? Does your experiment reveal that?

[Xavier Roblot]

If I get it right, it's

@Book{            lam_1999,
  series        = {Graduate Texts in Mathematics},
  title         = {Lectures on Modules and Rings},
  doi           = {10.1007/978-1-4612-0525-8},
  publisher     = {Springer New York, NY},
  author        = {T. Y. Lam},
  year          = {1999}
}

[Kevin Buzzard]

looks fine to me :shrug:

[Xavier Roblot]

I came to the same conclusion.

[Xavier Roblot]

How is the page Reference generated from this file?

[Kevin Buzzard]

short answer is https://github.com/leanprover/doc-gen4 ; longer answer is "I have no idea"

[Kevin Buzzard]

Heh, FLT also uses doc-gen4 and in the FLT version of the mathlib function field file all three of the references are broken

[Ruben Van de Velde]

Maybe it's just looking for the bib file in the wrong place in that case

[Jz Pan]

Most probably https://github.com/dupuisf/BibtexQuery does not like the bib files in mathlib. Unfortunately the bib processing code in it does not print messages if it encounters thing it cannot process; it just silently quits.

Run lake exe bibtex-query l references.bib > output.txt to see what entry makes it unhappy.

[Jz Pan]

The bug was introduced in #21688. The reason is simple: bibkey contains non-ASCII characters!

[Jz Pan]

bibtex-query should really report errors on such things, instead of silently errors.

[Jz Pan]

#22755

[Ruben Van de Velde]

Can we have a comment at the top of the file to warn people as well?

[Jz Pan]

Ruben Van de Velde said:

Can we have a comment at the top of the file to warn people as well?

Sure.

[Jz Pan]

Maybe we can add scripts to https://github.com/leanprover-community/mathlib4/blob/master/scripts/lint-bib.sh to detect such things

[Jz Pan]

bibtool --pass.comments=on -- 'select{$key "[^-.:A-Za-z0-9_]+"}' references.bib -o out.bib can filter entries whose key contains non-ASCII characters.

[Jz Pan]

There are any such entries if and only if the out.bib is not 0 bytes

[Jz Pan]

the linter is at #22757

[Jz Pan]

Run ./scripts/lint-bib.sh
+ bibtool --pass.comments=on -- 'select{$key "[^-.:A-Za-z0-9_]+"}' docs/references.bib -o docs/non-ascii.bib
+ '[' -s docs/non-ascii.bib ']'
+ echo 'ERROR: There are items in references.bib with keys containing non-ASCII characters:'
+ echo
+ cat docs/non-ascii.bib
ERROR: There are items in references.bib with keys containing non-ASCII characters:


@Book{        hytönen_vanneerven_veraar_wies_2016,
  author    = {Hytönen, Tuomas and Van Neerven, Jan and Veraar, Mark and
          Weis, Lutz},
  title     = {Analysis in Banach spaces},
  series    = {A Series of Modern Surveys in Mathematics},
  publisher = {Springer Cham},
  year      = {2016},
  pages     = {xvii+614},
  isbn      = {978-3-319-48520-1},
  doi       = {10.1007/978-3-319-48520-1},
  url       = {https://doi.org/10.1007/978-3-319-48520-1}
}
+ rm docs/non-ascii.bib
+ exit 1
Error: Process completed with exit code 1.

It works

[Jz Pan]

The linter is at #22757 and is ready for review.

[Xavier Roblot]

References are now fixed! Thanks

[Ruben Van de Velde]

Ruben Van de Velde said:

Hypothesis: something throws an exception (or similar) while processing the references, after they've been sorted by author, on the reference that comes after Lack

(so this was wrong)

[Ruben Van de Velde]

Xavier Roblot said:

(The reference to Samuel's book is incorrect though since the key should be samuel1967).

You want to fix this, then? :)

[Xavier Roblot]

Ruben Van de Velde said:

Xavier Roblot said:

(The reference to Samuel's book is incorrect though since the key should be samuel1967).

You want to fix this, then? :smile:

I'll put it on my TODO list but you're welcome to do it first :wink:

[Ruben Van de Velde]

Ditto :innocent:

[Michael Rothgang]

I just did it: #22763

[Michael Rothgang]

The first commit should be clearly good; the second commit (to file#Mathlib/RingTheory/Spectrum/Prime/Basic) is more speculative: I'd be glad if a domain expert could double-check.

[Xavier Roblot]

It looks good to me

[Ruben Van de Velde]

Much more comprehensive than I would have been, thanks :)

[Jz Pan]

I have to say that, if I remembered correctly, the syntax [samuel1967, § 3.3, Lemma 3] is not recognized by doc-gen and will be rendered as-is.

[Jz Pan]

[samuel1967], § 3.3, Lemma 3 is not ideal, but at least the [samuel1967] will be linked correctly to bibliography (with system auto-generated last name + year tag).

[Ruben Van de Velde]

I think you're right, I should've caught that (but it's no worse than before)

[Jz Pan]

Michael Rothgang said:

the second commit (to file#Mathlib/RingTheory/Spectrum/Prime/Basic) is more speculative

In order to link from docstring to the bibliography page, it's not necessary to always add a References section to module docstring. For example, if your sole purpose is to make the following samuel1967 works, then it's enough to write a [samuel1967], § 3.3, Lemma 3 in the theorem docstring, and that's enough. Hope this clarifies.

[Michael Rothgang]

(I added that reference also for good measure: if a file follows a reference, we might as well say so.)