Email Gateway (May 23 2024 at 04:32): Email Gateway (May 23 2024 at 04:32):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Eugene,
in the ROOT file you can specify the output directory with
document_ouput, like:
options [document_output = tex]
Then you can compile the files by hand with lualatex.
Mathias
Email Gateway (May 23 2024 at 10:16):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Thank you.
I can now see that the LaTeX sources will get produced by:
isabelle document -S xxx session_name
It is apparently necessary to explicitly give the -S option and specify an output directory.
If the -S option is not given, nothing is created, not even in the default .browser_info directory.
I find this confusing. The last time I had to do this (some years ago now) I seem to recall that
on a failure the LaTeX sources in question were just left somewhere in the .browser_info area
where they could be examined and the issue debugged. The various documentation just sort of
mentions these options like they just modify defaults or something. They don't prominently say:
"Hey, if you want to see any TeX source files, you better give this option or you can just
forget all about it."
Email Gateway (May 23 2024 at 16:05):From: "\"Eugene W. Stark\"" <cl-isabelle-users@lists.cam.ac.uk>
Thank you.
I can now see that the LaTeX sources will get produced by:
isabelle document -S xxx session_name
It is apparently necessary to explicitly give the -S option and specify an output directory.
If the -S option is not given, nothing is created, not even in the default .browser_info directory.
I find this confusing. The last time I had to do this (some years ago now) I seem to recall that
on a failure the LaTeX sources in question were just left somewhere in the .browser_info area
where they could be examined and the issue debugged. The various documentation just sort of
mentions these options like they just modify defaults or something. They don't prominently say:
"Hey, if you want to see any TeX source files, you better give this option or you can just
forget all about it."
Email Gateway (May 23 2024 at 20:38):From: Makarius <makarius@sketis.net>
That was discontinued a long time ago. It was very dirty in the sense that old
and outdated source could be left behind.
I am currently trying to solve a> LaTeX failure and the error message
output during the run
By "run" you probably mean the old-fashioned way via "isabelle build -o
document". If you augment that a little, you get a full copy of the document
sources:
isabelle build -o document -o document_output
An alternative is to use the "Document" panel in Isabelle/jEdit: it allows to
focus on interesting theories to be presented. Error messages should normally
be accurate wrt. the original Isabelle sources, not the generated LaTeX
sources. Thus you normally won't need the latter.
The command-line tool "isabelle document" is also fine, but rarely used, I guess.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC