Stream: Beginner Questions

Topic: building a document

view this post on Zulip Gergely Buday (Nov 08 2022 at 12:11):

I ran an old ROOT file for a document, I set document_build = pdf but it did not build the pdf, in spite of having a build script. Only when I ran the build script manually in output/document, then it created the pdf. What did I miss in the ROOT file?

view this post on Zulip Gergely Buday (Nov 08 2022 at 12:39):

What is outdated yet in my ROOT file?

session "proposal" = "HOL" +
  options [document_build = pdf, document_output = "output"]
  sessions
    "HOL-Nominal"
  theories
    "Proposal"
  document_files
    "root.tex" "build" "celldiagram.png"
  document_files ( in "../.." )
    "GergelyBuday.bib"

view this post on Zulip Gergely Buday (Nov 08 2022 at 13:03):

I have managed to run an isabelle document session verbosely, it talked about creating the root.pdf file, but I do not find the result. What does happen here?

view this post on Zulip Simon Roßkopf (Nov 08 2022 at 14:27):

I am by no means an expert on the Isabelle build process, but I think the options you give are wrong.

document_build (appears first in Isabelle2021-1 as far as I can tell) specifies the build engine used (See 3.3 of the system manual). By default Isabelle provides lualatex. pdflatexand build. The first two use standard latex tools to build your document, while the third allows you to supply a custom build script. pdfis not a (built in) build engine, and on my machine Isabelle complains about this when I try to add this option: `*** Bad document_build engine "pdf". You control whether you want a pdf with the document``option.

I suspect you want something like options [document = pdf, document_build = build, document_output = "output"].

view this post on Zulip Gergely Buday (Nov 08 2022 at 14:30):

Thanks. In the meantime I managed to give the necessary options to isabelle document.And yes, I used document_build = build .

Last updated: Apr 23 2024 at 08:19 UTC