Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] running bibtex through document preparation


view this post on Zulip 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?

view this post on Zulip 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


view this post on Zulip 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?

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC