Email Gateway (Aug 22 2022 at 16:08): 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
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: Nov 21 2024 at 12:39 UTC