[isabelle-dev] Error in "cite" anitquotation

[Makarius]

On 21/01/2023 12:58, Lawrence Paulson wrote:
> The attached error is clearly caused by a missing root.bib. The file was always missing, so presumably some recent change is now detecting this situation.

I've addressed that already here: https://isabelle-dev.sketis.net/rAFP65313718e1fe

GoedelGod is one of very few entries that don't have a .bib file, but inlined 
.bbl results in root.tex --- odd.

Right now, Isabelle/d0151eb9ecb0 + AFP/735f4be0a671 should work properly, but 
a few unchecked \cite macros remain.


> Fortunately there is a root.bib containing the missing entries. So I added it to the document dir, and to ROOT, and even added it to the repository, but the error messages don’t change.

If you have some a .bib file, please add it to the session.

With uniform bib database + formal cite antiquotations everywhere, we gain 
some structural integrity. Moreover, we can eventually make an HTML 
presentation of the bibliography, e.g. with the bib2xhtml tool that is already 
bundled with Isabelle.

Presently, bib2xhtml is only used for HTML preview of .bib files in 
Isabelle/jEdit. To see that, open e.g. $ISABELLE_HOME/src/Doc/manual.bib and 
then invoke the action isabelle.preview (e.g. via the menu Plugins / Isabelle 
/ Show preview in browser).


> I didn’t even know we had an antiquotation “cite”, so any clues what to do would be welcome.

There are some recent NEWS here: 
https://isabelle-dev.sketis.net/source/isabelle/browse/default/NEWS;1e31ddcab45$24

The regular documentation is in isar-ref for the antiquotation "cite" (e.g. 
see the index).


I did not announce the recent changes to cite so far, because I am still not 
finished with it: there are always some new surprises.

The reason, why I've revisited all this is interactive document preparation in 
Isabelle/jEdit. It allows to omit theories from the document, but this could 
leave the bibliography empty and bibtex would complain.

So now in Isabelle/34219d664854, citations for excluded theories are taken 
from unprocessed source and turned into \nocite commands. This works, because 
the notation \<^cite>CARTOUCHE is easily detected, even without formal 
checking of the theory.


This approach could be pushed one step further: instead of latex + bibtex + 
latex on the whole document to produce the initial root.aux + root.bbl, it 
could be done on the empty template with \nocite commands. Then a final latex 
run on the document together with the generated root.aux/bbl would be 
sufficient (but page references would require one more latex run).


	Makarius