Email Gateway (Jun 28 2021 at 13:36): Email Gateway (Jun 28 2021 at 13:36):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!
Until a few hours ago, I used Isabelle2019. I could build a session
with option document=pdf and get the PDF file in the browser_info
directory.
Now I use Isabelle2021, and I don’t get the PDF file anymore. Isabelle
shows me “Preparing ⟨session-name⟩/document ...”, but I cannot find the
PDF file anywhere. The browser_info directory is completely absent,
and searching my entire home directory for files with modification time
during the last 24 hours and name ending in .pdf doesn’t reveal
anything.
Any ideas how I can get the PDF output?
All the best,
Wolfgang
Email Gateway (Jun 28 2021 at 15:37):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
I found out meanwhile that at least TeX is run. I changed my theory
files such that they contained an undefined TeX command in the
documentation, and when building I got a corresponding error message
from TeX.
With some trick I managed to detect the directory in which lualatex
was run, which I guess is the directory where the PDF file is put. It
was of the form /tmp/isabelle-⟨user-name⟩/document⟨some-digits⟩.
Sadly, while other directories were present in /tmp/isabelle-⟨user-
name⟩, this one was not.
All the best,
Wolfgang
Email Gateway (Jun 28 2021 at 16:47):From: Jakub Kądziołka <kuba@kadziolka.net>
Wolfgang,
I believe you need to set the document_output option. For example,
options [document = pdf, document_output = "output"]
Regards,
Jakub Kądziołka
Email Gateway (Jun 28 2021 at 21:49):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Yes, it works if I set the document_output option, as I meanwhile
found out, but from how I understand the documentation, this shouldn’t
be necessary, because it should be document=pdf that switches on
document generation.
Also, it’s not immediately obvious how to use document_output to place
the PDF file in the standard location. In fact, my understanding is that
document_output is precisely for placing the PDF file in a location
other than the standard one.
That said, I meanwhile found out with the help of the people on Zulip
that the -P command line option can be used to get a PDF file. When
used with :, that is, when saying -P :, the PDF file will be placed
in the standard location.
I have no idea why the -P option is necessary and what its exact
meaning is (the documentation says that it “enables” a directory). My
understanding was that the document option is used for switching on or
off document generation and the document_output option is used for
selecting a destination. The -P command line option looks to me a bit
like a combination of both, but why should such a combination be
necessary? Maybe somebody can clarify.
All the best,
Wolfgang
Last updated: Jan 04 2025 at 20:18 UTC