[isabelle-dev] Error in "cite" anitquotation
makarius at sketis.net
Sat Jan 21 18:17:07 CET 2023
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:
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).
More information about the isabelle-dev