Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2015-RC5 ignores document files

Email Gateway (Aug 22 2022 at 09:54):

From: "C. Diekmann" <diekmann@in.tum.de>
Hi,

I just wanted to document an `error' I observed when testing with
Isabelle-2015. In fact, it is not an error but document in the NEWS:

• Session ROOT specifications require explicit 'document_files' for
  robust dependencies on LaTeX sources. Only these explicitly given
  files are copied to the document output directory, before document
  processing is started.

Suggested fix: The NEWS file should declare this as minor INCOMPATIBILITY.

My story:
it seems like Isabelle 2015 does not automatically consider the files
in the document folder anymore.
My document folder contains: mathpartir.sty root.tex

I was building my session

$ isabelle build -v -o document=pdf -d . Session_Name
Started at Sa 23. Mai 15:16:13 CEST 2015 (polyml-5.5.2_x86-linux on xps12)
ISABELLE_BUILD_OPTIONS=""

[...]
Timing Iptables_Semantics (2 threads, 150.063s elapsed time, 298.445s
cpu time, 25.342s GC time, factor 1.99)
Session_Name FAILED
(see also [...]/.isabelle/Isabelle2015-RC5/heaps/polyml-5.5.2_x86-linux/log/Session_Name)

[completely inconclusive error message here. The message looked like a
failed proof]
"$ISABELLE_TOOL" document -c -o 'pdf' -n 'document' -t ''
'[...]/.isabelle/Isabelle2015-RC5/browser_info/Session_Name/Session_Name/document'
2>&1
*** Bad file 'root.tex'
*** Document preparation failure in directory
'[...]/.isabelle/Isabelle2015-RC5/browser_info/Session_Name/Session_Name/document'

*** Failed to build document
"[...]/.isabelle/Isabelle2015-RC5/browser_info/Session_Name/Session_Name/document.pdf"
Session_Name CANCELLED

Both, the root.tex and mathpartir.sty were not in the
'[...]/.isabelle/Isabelle2015-RC5/browser_info/Session_Name/Session_Name/document'
directory. When I copied both to that directory, pdflatex can build
the document without any problems.

Adding the following to the ROOT fixes everything.
document_files
"root.tex"
"mathpartir.sty"

My main problem was the completely inconclusive error message and that
searching the NEWS for incompatibilities did not get me to the right
point.

Regards,
Cornelius

Email Gateway (Aug 22 2022 at 09:54):

From: Makarius <makarius@sketis.net>
This NEWS entry is actually from Isabelle2014. The tiny "IDE" for NEWS in
Isabelle/jEdit of Isabelle2015 helps to see this historical context in
SideKick. In Isabelle2014, 'document_files' were officially required, but
the absence tolerated as a legacy feature. The general hope is that users
always eliminate legacy stuff when they see the system warning about it.
This does not work, though, when older material is ported to a much newer
Isabelle release.

Here is a newly added snipped for Isabelle2015/NEWS:

• Specification of 'document_files' in the session ROOT file is
  mandatory for document preparation. The legacy mode with implicit
  copying of the document/ directory is no longer supported. Minor
  INCOMPATIBILITY.

  Makarius

Last updated: Apr 19 2024 at 08:19 UTC