leanblueprint web warnings

Stream: FLT

[Kevin Buzzard]

I ran leanblueprint web on the command line on FLT and looked carefully at the output. To my surprise there were some ERRORs about unresolved labels (which I am now in the process of fixing; these are declarations whose name has changed but I'm still talking about them in \uses), and then there are some WARNINGs which I can't understand:

...
INFO: Using the vector imager "dvisvgm".
 [ index.html [ sect0001.html ] [ ch_reductions.html
WARNING: Using default renderer for underline
WARNING: Bibliography item "mazur-torsion" has no entry
 ] [ ch_frey.html
WARNING: Bibliography item "silverman1" has no entry
WARNING: Bibliography item "silverman2" has no entry
WARNING: Bibliography item "ddt" has no entry
WARNING: Bibliography item "edix" has no entry
WARNING: Bibliography item "edix" has no entry
WARNING: Bibliography item "katz-mazur" has no entry
WARNING: Bibliography item "mazur-torsion" has no entry
WARNING: Bibliography item "serrepropgal" has no entry
WARNING: Bibliography item "serrepropgal" has no entry
 ] [ ch_overview.html
WARNING: Bibliography item "moret-bailly" has no entry
WARNING: Bibliography item "taylor-mero-cont" has no entry
WARNING: Bibliography item "toby-modularity" has no entry
WARNING: Bibliography item "blggt" has no entry
 ] [ sect0002.html ] [ sect0003.html ] [ sect0004.html ]
 [ Adele_miniproject.html ] [ Haar_char_project.html ]
 [ Fujisaki_project.html
WARNING: Bibliography item "voightbook" has no entry
 ] [ Quat_alg_project.html ] [ ch_bestiary.html
WARNING: Bibliography item "cf" has no entry
WARNING: Bibliography item "serre-galcoh" has no entry
WARNING: Bibliography item "serre-galcoh" has no entry
WARNING: Bibliography item "serre-galcoh" has no entry
WARNING: Bibliography item "serre-galcoh" has no entry
WARNING: Bibliography item "serre-galcoh" has no entry
WARNING: Bibliography item "cf" has no entry
WARNING: Bibliography item "corvallis1" has no entry
WARNING: Bibliography item "corvallis1" has no entry
WARNING: Bibliography item "corvallis2" has no entry
WARNING: Bibliography item "mazur-torsion" has no entry
WARNING: Bibliography item "moret-bailly" has no entry
 ] [ sect0005.html ] ]pre-processing DVI file (format version 2)
processing page 1
...

One might imagine from these warnings that I've messed up with the bibliography somehow, but everything seems to work fine; for example serre-galcoh is Serre's book on Galois cohomology and all 5 warnings above seem to correspond to links which work fine in both the pdf and the web version of the blueprint (see for example the proof of Theorem 12.4 ). Right now I propose fixing the errors but ignoring the warnings. I've seen LaTeX warnings about references before when a document is being compiled during the latex; latex; bibtex; latex dance, however the warnings are just at the beginning of the dance and disappear later. The warnings I quote above seem to occur right at the end of the web compilation process so I was surprised.

[Ruben Van de Velde]

I think I've been similarly confused in the past

[Pietro Monticone]

I do not see the warning WARNING: Bibliography either locally or in the log of the GitHub Actions workflow here. I can't reproduce that.

[Kevin Buzzard]

Oh that's weird! You're right that they are not visible in the logs.

[Patrick Massot]

plasTeX relies on LaTeX to generate bbl files, so you need to compile everything. leanblueprint all should do that.

[Patrick Massot]

Simply running leanblueprint pdf before leanblueprint web should be enough actually.

[Kevin Buzzard]

This does not make the warnings go away for me. Given that they are not there in the CI logs and that Pietro doesn't see them, this is clearly a "me" problem. But I am not remotely bothered about it; the only reason I even mentioned it was that I noticed them and thought "I should fix them" and then I realised that they didn't seem to be broken and I was confused.