Email Gateway (Aug 19 2022 at 16:46): Email Gateway (Aug 19 2022 at 16:46):From: Gergely Buday <gbuday@gmail.com>
Hi,
if I go to output/document and I run
pdflatex
bibtex
pdflatex
pdflatex
I get a proper root.pdf.
However running
isabelle build -D .
does not result in proper citations in document.pdf, no matter how
many times I run it.
How should I use document preparation so that bibtex runs?
Email Gateway (Aug 19 2022 at 16:46):From: Makarius <makarius@sketis.net>
"isabelle document" that is used implicitly here is smart enough to do it
all, but you need to observe a canonical setup for the document. I guess
that above you don't have root.bib, but some other file.
There are many existing examples in the Isabelle distribution and AFP.
Makarius
http://stop-ttip.org 1,063,902 people so far
Email Gateway (Aug 19 2022 at 16:47):From: Gergely Buday <gbuday@gmail.com>
Indeed, I had to symlink my bib file and it worked.
The next thing might be nitpicking but I better mention it: if I
change document/root.bib isabelle build does not produce a new pdf.
For that I need to change theory file like adding a space. Could
isabelle build check for the change of other files such as root.bib?
Email Gateway (Aug 19 2022 at 16:48):From: Makarius <makarius@sketis.net>
This should work if all document files are declared in ROOT via
document_files. See also this NEWS entry:
You should also purge your generated output directory to be sure that the
dependencies are exactly right.
In Isabelle2014 there is still a legacy mode with non-robust dependencies
on LaTeX sources, but that will be no longer there in the next release.
Makarius
https://stop-ttip.org/signatures-member-states
Last updated: Apr 20 2024 at 08:16 UTC