Stream: General

Topic: No PDF output

Wolfgang Jeltsch (Jun 28 2021 at 16:02):

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.

Lukas Stevens (Jun 28 2021 at 16:06):

I had a similar issue. Can you try building with isabelle build -o document=pdf -P output -D .?

Fabian Huch (Jun 28 2021 at 16:08):

You can probably also specify document_outputin your ROOT file.

Wolfgang Jeltsch (Jun 28 2021 at 16:09):

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 (Jun 28 2021 at 16:09):

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

Fabian Huch (Jun 28 2021 at 16:10):

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 = "."?

Wolfgang Jeltsch (Jun 28 2021 at 16:11):

Well, then the file ends up in the current directory and not in the standard location, which is under $ISABELLE_BROWSER_INFO.

Fabian Huch (Jun 28 2021 at 16:17):

That's the standard directory for html -- if you build with -o browser_info -o document=pdf, the pdfs should also be there.

Wolfgang Jeltsch (Jun 28 2021 at 16:20):

Yes, this works. Is the -P option new? What is its purpose? Shouldn’t the setting document=pdf already enable PDF output?

Wolfgang Jeltsch (Jun 28 2021 at 16:20):

It’s also the standard directory for PDFs.

Lukas Stevens (Jun 28 2021 at 16:23):

The -P output specifies the output directory.

Wolfgang Jeltsch (Jun 28 2021 at 16:27):

No, it “enables output”, according to the documentation. It’s the document_output option that specifies the output directory.

Lukas Stevens (Jun 28 2021 at 16:29):

Lukas Stevens said:

The -P output specifies the output directory.

That is what @Manuel Eberl told me anyway :shrug:

Manuel Eberl (Jun 28 2021 at 16:35):

All I know is I do -P : and that works.

Last updated: Apr 18 2024 at 08:19 UTC