[isabelle] Isabelle2015-RC5 ignores document files



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.