Anyone able to help me with this one: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-June/msg00041.html? In short: Isabelle2021 doesn’t produce PDF files for me, where Isabelle2019 did.
I had a similar issue. Can you try building with isabelle build -o document=pdf -P output -D .
?
You can probably also specify document_output
in your ROOT file.
Yes, it works this way. However, I’d like to have the PDF file in the standard location. Specifying the standard location by hand seems a bit awkward to me.
Lukas Stevens said:
I had a similar issue. Can you try building with
isabelle build -o document=pdf -P output -D .
?
the -P output
was the thing I had to add
Wolfgang Jeltsch said:
Yes, it works this way. However, I’d like to have the PDF file in the standard location. Specifying the standard location by hand seems a bit awkward to me.
How about document_output = "."
?
Well, then the file ends up in the current directory and not in the standard location, which is under $ISABELLE_BROWSER_INFO
.
That's the standard directory for html -- if you build with -o browser_info -o document=pdf
, the pdfs should also be there.
Yes, this works. Is the -P
option new? What is its purpose? Shouldn’t the setting document=pdf
already enable PDF output?
It’s also the standard directory for PDFs.
The -P output
specifies the output directory.
No, it “enables output”, according to the documentation. It’s the document_output
option that specifies the output directory.
Lukas Stevens said:
The
-P output
specifies the output directory.
That is what @Manuel Eberl told me anyway :shrug:
All I know is I do -P :
and that works.
Last updated: Dec 07 2024 at 16:22 UTC