Email Gateway (Jan 21 2023 at 11:58): Email Gateway (Jan 21 2023 at 11:58):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
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.
I didn’t even know we had an antiquotation “cite”, so any clues what to do would be welcome. I haven’t pushed the changes so far, but could (I’d prefer to remove the redundant bibtex entries, since this file contains 172).
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 21 2023 at 17:17):From: Makarius <makarius@sketis.net>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 21 2023 at 19:24):From: Lawrence Paulson <lp15@cam.ac.uk>
I used the one in Types_Tableaus_and_Goedels_God with some modifications and one entry of my own. Seems to work.
For the future, do we need to prohibit entries with explicit bibliographies?
Larry
Email Gateway (Jan 21 2023 at 20:17):From: Makarius <makarius@sketis.net>
It would indeed be better to standardize everything towards proper root.bib +
regular bibtex setup (which is implicit in the document build process).
We have very few exceptions so far, it should be easy to upgrade them.
That is mainly a matter to search for unchecked \cite or \bibitem commands,
but we also need proper bibtex entries from somewhere.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 28 2024 at 12:28 UTC