option document_build refers to build engine in Isabelle/Scala;
pdflatex is back as legacy build engine, e.g. for published proceedings;
--- a/NEWS Mon May 17 20:37:42 2021 +0200
+++ b/NEWS Mon May 17 23:30:25 2021 +0200
@@ -34,6 +34,23 @@
*** Document preparation ***
+* Option "document_build" determines the document build engine, as
+defined in Isabelle/Scala (as system service). The subsequent engines
+are provided by the Isabelle distribution:
+
+ . "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
+ build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX
+
+ . "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
+ special LaTeX styles)
+
+ . "build": delegate to the executable "./build pdf", using
+ ISABELLE_LUALATEX by default
+
+The presence of a "build" command within the document output directory
+explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
+adjust session ROOT options.
+
* Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").
--- a/etc/options Mon May 17 20:37:42 2021 +0200
+++ b/etc/options Mon May 17 23:30:25 2021 +0200
@@ -13,6 +13,8 @@
-- "alternative document variants (separated by colons)"
option document_tags : string = ""
-- "default command tags (separated by commas)"
+option document_build : string = "lualatex"
+ -- "document build engine (e.g. lualatex, pdflatex, build)"
option thy_output_display : bool = false
-- "indicate output as multi-line display-style material"
--- a/etc/settings Mon May 17 20:37:42 2021 +0200
+++ b/etc/settings Mon May 17 23:30:25 2021 +0200
@@ -34,6 +34,10 @@
isabelle_scala_service 'isabelle.Simplifier_Trace$Handler'
isabelle_scala_service 'isabelle.Server_Commands'
+isabelle_scala_service 'isabelle.Document_Build$LuaLaTeX_Engine'
+isabelle_scala_service 'isabelle.Document_Build$PDFLaTeX_Engine'
+isabelle_scala_service 'isabelle.Document_Build$Build_Engine'
+
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
@@ -57,10 +61,16 @@
###
-### Document preparation (cf. isabelle latex/document)
+### Document preparation (cf. isabelle latex)
###
-ISABELLE_PDFLATEX="lualatex --file-line-error"
+if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
+ ISABELLE_PDFLATEX="pdflatex -c-style-errors"
+else
+ ISABELLE_PDFLATEX="pdflatex -file-line-error"
+fi
+
+ISABELLE_LUALATEX="lualatex --file-line-error"
ISABELLE_BIBTEX="bibtex"
ISABELLE_MAKEINDEX="makeindex"
ISABELLE_EPSTOPDF="epstopdf"
--- a/src/Doc/ROOT Mon May 17 20:37:42 2021 +0200
+++ b/src/Doc/ROOT Mon May 17 23:30:25 2021 +0200
@@ -1,7 +1,7 @@
chapter Doc
session Classes (doc) in "Classes" = HOL +
- options [document_variants = "classes", quick_and_dirty]
+ options [document_build = "build", document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
theories Classes
document_files (in "..")
@@ -17,7 +17,7 @@
"style.sty"
session Codegen (doc) in "Codegen" = HOL +
- options [document_variants = "codegen", print_mode = "no_brackets,iff"]
+ options [document_build = "build", document_variants = "codegen", print_mode = "no_brackets,iff"]
sessions
"HOL-Library"
theories [document = false]
@@ -44,7 +44,7 @@
"style.sty"
session Corec (doc) in "Corec" = Datatypes +
- options [document_variants = "corec"]
+ options [document_build = "build", document_variants = "corec"]
theories
Corec
document_files (in "..")
@@ -60,7 +60,7 @@
"style.sty"
session Datatypes (doc) in "Datatypes" = HOL +
- options [document_variants = "datatypes"]
+ options [document_build = "build", document_variants = "datatypes"]
sessions
"HOL-Library"
theories [document = false]
@@ -80,7 +80,7 @@
"style.sty"
session Eisbach (doc) in "Eisbach" = HOL +
- options [document_variants = "eisbach", quick_and_dirty,
+ options [document_build = "build", document_variants = "eisbach", quick_and_dirty,
print_mode = "no_brackets,iff", show_question_marks = false]
sessions
"HOL-Eisbach"
@@ -104,7 +104,8 @@
"style.sty"
session Functions (doc) in "Functions" = HOL +
- options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
+ options [document_build = "build", document_variants = "functions",
+ skip_proofs = false, quick_and_dirty]
theories Functions
document_files (in "..")
"prepare_document"
@@ -121,7 +122,8 @@
"style.sty"
session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL +
- options [document_variants = "how_to_prove_it", show_question_marks = false]
+ options [document_build = "build", document_variants = "how_to_prove_it",
+ show_question_marks = false]
theories
How_to_Prove_it
document_files
@@ -130,7 +132,7 @@
"prelude.tex"
session Intro (doc) in "Intro" = Pure +
- options [document_variants = "intro"]
+ options [document_build = "build", document_variants = "intro"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -146,7 +148,7 @@
"root.tex"
session Implementation (doc) in "Implementation" = HOL +
- options [document_variants = "implementation", quick_and_dirty]
+ options [document_build = "build", document_variants = "implementation", quick_and_dirty]
theories
Eq
Integration
@@ -174,7 +176,8 @@
"style.sty"
session Isar_Ref (doc) in "Isar_Ref" = HOL +
- options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
+ options [document_build = "build", document_variants = "isar-ref",
+ quick_and_dirty, thy_output_source]
sessions
"HOL-Library"
theories
@@ -210,7 +213,7 @@
"style.sty"
session JEdit (doc) in "JEdit" = HOL +
- options [document_variants = "jedit", thy_output_source]
+ options [document_build = "build", document_variants = "jedit", thy_output_source]
theories
JEdit
document_files (in "..")
@@ -247,7 +250,7 @@
"theories.png"
session Sugar (doc) in "Sugar" = HOL +
- options [document_variants = "sugar"]
+ options [document_build = "build", document_variants = "sugar"]
sessions
"HOL-Library"
theories Sugar
@@ -260,7 +263,8 @@
"root.tex"
session Locales (doc) in "Locales" = HOL +
- options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
+ options [document_build = "build", document_variants = "locales",
+ thy_output_margin = 65, skip_proofs = false]
theories
Examples1
Examples2
@@ -274,7 +278,7 @@
"root.tex"
session Logics (doc) in "Logics" = Pure +
- options [document_variants = "logics"]
+ options [document_build = "build", document_variants = "logics"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -293,7 +297,7 @@
"syntax.tex"
session Logics_ZF (doc) in "Logics_ZF" = ZF +
- options [document_variants = "logics-ZF", print_mode = "brackets",
+ options [document_build = "build", document_variants = "logics-ZF", print_mode = "brackets",
thy_output_source]
sessions
FOL
@@ -319,7 +323,7 @@
"root.tex"
session Main (doc) in "Main" = HOL +
- options [document_variants = "main"]
+ options [document_build = "build", document_variants = "main"]
theories Main_Doc
document_files (in "..")
"prepare_document"
@@ -329,7 +333,7 @@
"root.tex"
session Nitpick (doc) in "Nitpick" = Pure +
- options [document_variants = "nitpick"]
+ options [document_build = "build", document_variants = "nitpick"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -340,7 +344,7 @@
"root.tex"
session Prog_Prove (doc) in "Prog_Prove" = HOL +
- options [document_variants = "prog-prove", show_question_marks = false]
+ options [document_build = "build", document_variants = "prog-prove", show_question_marks = false]
theories
Basics
Bool_nat_list
@@ -363,7 +367,7 @@
"svmono.cls"
session Sledgehammer (doc) in "Sledgehammer" = Pure +
- options [document_variants = "sledgehammer"]
+ options [document_build = "build", document_variants = "sledgehammer"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -374,7 +378,7 @@
"root.tex"
session System (doc) in "System" = Pure +
- options [document_variants = "system", thy_output_source]
+ options [document_build = "build", document_variants = "system", thy_output_source]
sessions
"HOL-Library"
theories
@@ -401,7 +405,8 @@
"root.tex"
session Tutorial (doc) in "Tutorial" = HOL +
- options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
+ options [document_build = "build", document_variants = "tutorial",
+ print_mode = "brackets", skip_proofs = false]
directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
"Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
theories [document = false]
@@ -494,7 +499,7 @@
"types0.tex"
session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
- options [document_variants = "typeclass_hierarchy"]
+ options [document_build = "build", document_variants = "typeclass_hierarchy"]
sessions
"HOL-Library"
theories [document = false]
--- a/src/Pure/Thy/document_build.scala Mon May 17 20:37:42 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Mon May 17 23:30:25 2021 +0200
@@ -156,6 +156,14 @@
def session: String = info.name
def options: Options = info.options
+ def document_build: String = options.string("document_build")
+
+ def get_engine(): Engine =
+ {
+ val name = document_build
+ engines.find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
+ }
+
def get_export(theory: String, name: String): Export.Entry =
db_context.get_export(hierarchy, theory, name)
@@ -214,8 +222,9 @@
val root_name1 = "root_" + doc.name
val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
- val sources =
- SHA1.digest_set(File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest))
+ val option_digests = List(doc.print, get_engine().name).map(SHA1.digest)
+ val file_digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
+ val sources = SHA1.digest_set(option_digests ::: file_digests)
/* derived material */
@@ -270,6 +279,74 @@
}
+ /* build engines */
+
+ lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine])
+
+ abstract class Engine(val name: String) extends Isabelle_System.Service
+ {
+ override def toString: String = name
+
+ def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory
+ def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output
+ }
+
+ abstract class Bash_Engine(name: String) extends Engine(name)
+ {
+ def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
+ context.prepare_directory(dir, doc)
+
+ def bash_script(context: Context, directory: Directory): String =
+ {
+ val build_required = name == "build"
+ val build_provided = (directory.doc_dir + Path.explode("build")).is_file
+
+ if (!build_required && build_provided) {
+ error("Unexpected document build script for option document_build=" +
+ quote(context.document_build))
+ }
+ else if (build_required && !build_provided) error("Missing document build script")
+ else if (build_required) "./build pdf " + Bash.string(directory.doc.name)
+ else {
+ def root_bash(ext: String): String = Bash.string(directory.root_name + "." + ext)
+
+ def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
+ "isabelle latex -o " + Bash.string(fmt) + " " + root_bash(ext)
+
+ List(
+ latex_bash(),
+ "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
+ "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
+ latex_bash(),
+ latex_bash()).mkString(" && ")
+ }
+ }
+
+ def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output =
+ {
+ val settings =
+ if (name == "pdflatex") Nil
+ else List("ISABELLE_PDFLATEX" -> Isabelle_System.getenv("ISABELLE_LUALATEX"))
+
+ val result =
+ context.progress.bash(
+ bash_script(context, directory),
+ cwd = directory.doc_dir.file,
+ env = Isabelle_System.settings() ++ settings,
+ echo = verbose,
+ watchdog = Time.seconds(0.5))
+
+ val log = result.out_lines ::: result.err_lines
+ val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
+ directory.make_document(log, errors)
+ }
+ }
+
+ class LuaLaTeX_Engine extends Bash_Engine("lualatex")
+ class PDFLaTeX_Engine extends Bash_Engine("pdflatex")
+ class Build_Engine extends Bash_Engine("build")
+
+
/* build documents */
def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
@@ -282,10 +359,10 @@
context: Context,
output_sources: Option[Path] = None,
output_pdf: Option[Path] = None,
- verbose: Boolean = false,
- verbose_latex: Boolean = false): List[Document_Output] =
+ verbose: Boolean = false): List[Document_Output] =
{
val progress = context.progress
+ val engine = context.get_engine()
val documents =
for (doc <- context.documents)
@@ -295,60 +372,20 @@
progress.echo("Preparing " + context.session + "/" + doc.name + " ...")
val start = Time.now()
-
- // prepare directory
-
- output_sources.foreach(context.prepare_directory(_, doc))
- val directory = context.prepare_directory(tmp_dir, doc)
- val doc_dir = directory.doc_dir
- val root = directory.root_name
-
-
- // prepare document
+ output_sources.foreach(engine.prepare_directory(context, _, doc))
+ val directory = engine.prepare_directory(context, tmp_dir, doc)
- context.old_document(directory) getOrElse {
- // bash scripts
-
- def root_bash(ext: String): String = Bash.string(root + "." + ext)
-
- def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
- "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
-
- def bash(items: String*): Process_Result =
- progress.bash(items.mkString(" && "), cwd = doc_dir.file,
- echo = verbose_latex, watchdog = Time.seconds(0.5))
-
-
- // prepare document
+ val document =
+ context.old_document(directory) getOrElse
+ engine.build_document(context, directory, verbose)
- val result =
- if ((doc_dir + Path.explode("build")).is_file) {
- bash("./build pdf " + Bash.string(doc.name))
- }
- else {
- bash(
- latex_bash(),
- "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
- "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
- latex_bash(),
- latex_bash())
- }
+ val stop = Time.now()
+ val timing = stop - start
- val stop = Time.now()
- val timing = stop - start
-
-
- // result
+ progress.echo("Finished " + context.session + "/" + doc.name +
+ " (" + timing.message_hms + " elapsed time)")
- val log = result.out_lines ::: result.err_lines
- val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
- val document = directory.make_document(log, errors)
-
- progress.echo("Finished " + context.session + "/" + doc.name +
- " (" + timing.message_hms + " elapsed time)")
-
- document
- }
+ document
})
}
@@ -429,7 +466,7 @@
{
build_documents(context(session, deps, db_context, progress = progress),
output_sources = output_sources, output_pdf = output_pdf,
- verbose = true, verbose_latex = verbose_latex)
+ verbose = verbose_latex)
})
}
})