Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with document preparation


view this post on Zulip Email Gateway (Aug 22 2022 at 16:08):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

today I experienced the following strange behaviour with Isabelle 2016-1:

Consider the following root-file:

session Test = HOL +
theories
Test
document_files
"root.tex"
"root.bib"
“external.aux"

If I invoke

isabelle build -o"document=pdf" -d. -c Test

then I get a document, where “external.aux” was NOT copied to the target document directory
(~/.isabelle/Isabelle2016-1/browser_info/Unsorted/Test/document), and consequently, the
external references that are described in “external.aux” will all be invalid in the PDF.

If instead I invoke Isabelle with an explicit document-output-directory by

isabelle build -o"document=pdf" -o"document_output=output" -d. -c Test

then I get the intended document, since “external.aux” was copied into the right directory.

I’m surprised by the difference,
René

PS: Attached are the sources.
test.zip

view this post on Zulip Email Gateway (Aug 22 2022 at 16:09):

From: Makarius <makarius@sketis.net>
This is due to the internal invocation of "isabelle document -c" for
$ISABELLE_HOME_USER/browser_info output, but that option has changed its
meaning slightly over time. It does more than just purge the document
output directory after use.

I have already changed that here
https://bitbucket.org/isabelle_project/isabelle-release/commits/74a1b722507e
so it will be in Isabelle2017-RC3, which is anticipated for the next 1-2
days.

Makarius


Last updated: Mar 29 2024 at 01:04 UTC