From 44cae2e6314639ef4416a7caae0f11d8bdfe9f04 Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 4 Dec 2022 00:09:29 +0100 Subject: [PATCH] More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports --- etc/options | 6 - examples/CENELEC_50128/mini_odo/ROOT | 3 +- examples/CENELEC_50128/mini_odo/mini_odo.thy | 1 + .../IsaDofApplications.thy | 1 + .../2018-cicm-isabelle_dof-applications/ROOT | 4 +- examples/scholarly_paper/2020-iFM-CSP/ROOT | 3 +- .../scholarly_paper/2020-iFM-CSP/paper.thy | 1 + .../Isabelle_DOF-Manual/03_GuidedTour.thy | 2 - .../Isabelle_DOF-Manual.thy | 1 + .../technical_report/Isabelle_DOF-Manual/ROOT | 4 +- .../TR_my_commented_isabelle/ROOT | 3 +- .../TR_MyCommentedIsabelle.thy | 2 +- src/DOF/Isa_DOF.thy | 122 ++++++++++++------ .../CENELEC_50128/CENELEC_50128.thy | 2 + .../scholarly_paper/scholarly_paper.thy | 4 +- .../technical_report/technical_report.thy | 2 + src/scala/dof.scala | 6 - src/scala/dof_document_build.scala | 13 +- src/scala/dof_mkroot.scala | 21 +-- src/tests/Isabelle2022.thy | 2 +- 20 files changed, 124 insertions(+), 79 deletions(-) delete mode 100644 etc/options diff --git a/etc/options b/etc/options deleted file mode 100644 index f65510f..0000000 --- a/etc/options +++ /dev/null @@ -1,6 +0,0 @@ -(* :mode=isabelle-options: *) - -section "Isabelle/DOF" - -public option dof_ontologies : string = "Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper" - -- "Isabelle/DOF ontologies (separated by blanks)" diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT index 3d7f079..4aa5813 100644 --- a/examples/CENELEC_50128/mini_odo/ROOT +++ b/examples/CENELEC_50128/mini_odo/ROOT @@ -1,6 +1,5 @@ session "mini_odo" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = dof, - dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128"] + options [document = pdf, document_output = "output", document_build = dof] sessions "Physical_Quantities" theories diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index 003ca1d..a658212 100644 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -20,6 +20,7 @@ imports "Physical_Quantities.SI" "Physical_Quantities.SI_Pretty" begin use_template "scrreprt-modern" +use_ontology technical_report and CENELEC_50128 declare[[strict_monitor_checking=true]] define_shortcut* dof \ \\dof\ isadof \ \\isadof{}\ diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index 1c95829..dec9a27 100644 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -17,6 +17,7 @@ theory IsaDofApplications begin use_template "lncs" +use_ontology "scholarly_paper" open_monitor*[this::article] declare[[strict_monitor_checking=false]] diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT index 8ddbbc4..7a5c7af 100644 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT @@ -1,7 +1,5 @@ session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = dof, - dof_ontologies = "Isabelle_DOF.scholarly_paper", - quick_and_dirty = true] + options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true] theories IsaDofApplications document_files diff --git a/examples/scholarly_paper/2020-iFM-CSP/ROOT b/examples/scholarly_paper/2020-iFM-CSP/ROOT index 9c9066a..8e68278 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/ROOT +++ b/examples/scholarly_paper/2020-iFM-CSP/ROOT @@ -1,6 +1,5 @@ session "2020-iFM-csp" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = dof, - dof_ontologies = "Isabelle_DOF.scholarly_paper"] + options [document = pdf, document_output = "output", document_build = dof] theories "paper" document_files diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index ec82981..d3f6790 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -4,6 +4,7 @@ theory "paper" begin use_template "scrartcl" +use_ontology "scholarly_paper" open_monitor*[this::article] diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index ae53d4a..a721da7 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -159,8 +159,6 @@ replaced by built-in document templates.\ for users are: \<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}. In addition to the standard features of, this file also contains \<^isadof> specific configurations: - \<^item> \<^boxed_bash>\dof_ontologies\ a list of (fully qualified) ontologies, separated by spaces, used - by the project. \<^item> \<^boxed_bash>\document_build=dof\ needs to be present, to tell Isabelle, to use the Isabelle/DOF backend for the document generation. \<^item> The file \<^boxed_bash>\preamble.tex\\<^index>\preamble.tex\, which allows users to add additional diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy index a72b1b8..5af293d 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy @@ -16,6 +16,7 @@ theory "Isabelle_DOF-Manual" imports "05_Implementation" begin use_template "scrreprt-modern" +use_ontology "technical_report" and "CENELEC_50128" close_monitor*[this] check_doc_global text\Resulting trace in \<^verbatim>\doc_item\ ''this'': \ diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT index 7187427..25b8598 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/ROOT +++ b/examples/technical_report/Isabelle_DOF-Manual/ROOT @@ -1,7 +1,5 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = dof, - dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", - quick_and_dirty = true] + options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true] theories "Isabelle_DOF-Manual" document_files diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index d5c539d..e3b9b3c 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -1,6 +1,5 @@ session "TR_MyCommentedIsabelle" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = dof, - dof_ontologies = "Isabelle_DOF.technical_report", quick_and_dirty = true] + options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true] theories "TR_MyCommentedIsabelle" document_files diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 86b5b0e..1f90b61 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -14,10 +14,10 @@ (*<*) theory TR_MyCommentedIsabelle imports "Isabelle_DOF.technical_report" - begin use_template "scrreprt" +use_ontology "technical_report" define_shortcut* isabelle \ \Isabelle/HOL\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 00b88c2..c70a8ef 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -43,8 +43,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) and "text*" "text-macro*" :: document_body and "term*" "value*" "assert*" :: document_body - and "use_template" :: thy_decl - and "define_template" :: thy_load + and "use_template" "use_ontology" :: thy_decl + and "define_template" "define_ontology" :: thy_load and "print_doc_classes" "print_doc_items" "print_doc_class_template" "check_doc_global" :: diag @@ -2886,10 +2886,15 @@ ML \ signature DOCUMENT_CONTEXT = sig val template_space: Context.generic -> Name_Space.T + val ontology_space: Context.generic -> Name_Space.T val print_template: Context.generic -> string -> string - val check_template: Context.generic -> xstring * Position.T -> {name: string, text: string} - val use_template: Context.generic -> xstring * Position.T -> unit + val print_ontology: Context.generic -> string -> string + val check_template: Context.generic -> xstring * Position.T -> string * string + val check_ontology: Context.generic -> xstring * Position.T -> string * string val define_template: binding * string -> theory -> string * theory + val define_ontology: binding * string -> theory -> string * theory + val use_template: Context.generic -> xstring * Position.T -> unit + val use_ontology: Context.generic -> (xstring * Position.T) list -> unit end; structure Document_Context: DOCUMENT_CONTEXT = @@ -2897,11 +2902,17 @@ struct (* theory data *) +local + structure Data = Theory_Data ( - type T = string Name_Space.table; - val empty = Name_Space.empty_table "document_template"; - val merge = Name_Space.merge_tables; + type T = string Name_Space.table * string Name_Space.table; + val empty : T = + (Name_Space.empty_table "document_template", + Name_Space.empty_table "document_ontology"); + fun merge ((templates1, ontologies1), (templates2, ontologies2)) = + (Name_Space.merge_tables (templates1, templates2), + Name_Space.merge_tables (ontologies1, ontologies2)); ); fun naming_context thy = @@ -2909,25 +2920,59 @@ fun naming_context thy = |> Proof_Context.map_naming (Name_Space.root_path #> Name_Space.add_path "Isabelle_DOF") |> Context.Proof; -val template_space = Name_Space.space_of_table o Data.get o Context.theory_of; +fun get_space which = Name_Space.space_of_table o which o Data.get o Context.theory_of; -fun print_template context = - Name_Space.markup_extern (Context.proof_of context) (template_space context) +fun print which context = + Name_Space.markup_extern (Context.proof_of context) (get_space which context) #> uncurry Markup.markup; -fun check_template context arg = - let val (name, text) = Name_Space.check context (Data.get (Context.theory_of context)) arg - in {name = name, text = text} end; +fun check which context arg = + Name_Space.check context (which (Data.get (Context.theory_of context))) arg; + +fun define (get, ap) (binding, arg) thy = + let + val (name, table') = + Data.get thy |> get |> Name_Space.define (naming_context thy) true (binding, arg); + val thy' = (Data.map o ap) (K table') thy; + in (name, thy') end; + +fun strip prfx sffx (path, pos) = + (case try (unprefix prfx) (Path.file_name path) of + NONE => error ("File name needs to have prefix " ^ quote prfx ^ Position.here pos) + | SOME a => + (case try (unsuffix sffx) a of + NONE => error ("File name needs to have suffix " ^ quote sffx ^ Position.here pos) + | SOME b => b)); + +in + +val template_space = get_space fst; +val ontology_space = get_space snd; + +val print_template = print fst; +val print_ontology = print snd; + +val check_template = check fst; +val check_ontology = check snd; + +val define_template = define (fst, apfst); +val define_ontology = define (snd, apsnd); fun use_template context arg = - let val {text, ...} = check_template context arg - in Export.export (Context.theory_of context) \<^path_binding>\dof/root.tex\ [XML.Text text] end; + let val xml = arg |> check_template context |> snd |> XML.string + in Export.export (Context.theory_of context) \<^path_binding>\dof/root.tex\ xml end; -fun define_template (binding, text) thy = +fun use_ontology context args = let - val (name, data') = Data.get thy |> Name_Space.define (naming_context thy) true (binding, text); - val thy' = Data.put data' thy; - in (name, thy') end; + val xml = args + |> map (check_ontology context) + |> let open XML.Encode in list (pair string string) end; + in Export.export (Context.theory_of context) \<^path_binding>\dof/ontologies\ xml end; + +val strip_template = strip "root-" ".tex"; +val strip_ontology = strip "DOF-" ".sty"; + +end; (* Isar commands *) @@ -2938,30 +2983,33 @@ val _ = (Parse.position Parse.name >> (fn arg => Toplevel.theory (fn thy => (use_template (Context.Theory thy) arg; thy)))); +val _ = + Outer_Syntax.command \<^command_keyword>\use_ontology\ + "use DOF document ontologies (as defined within theory context)" + (Parse.and_list1 (Parse.position Parse.name) >> (fn args => + Toplevel.theory (fn thy => (use_ontology (Context.Theory thy) args; thy)))); + val _ = Outer_Syntax.command \<^command_keyword>\define_template\ - "define DOF document template (via LaTeX style file)" + "define DOF document template (via LaTeX root file)" (Parse.position Resources.provide_parse_file >> (fn (get_file, pos) => Toplevel.theory (fn thy => let - fun err msg = error (msg ^ Position.here pos); - - val (file, thy1) = get_file thy; - val file_name = Path.file_name (#src_path file); - val file_prefix = "root-"; - val file_suffix = ".tex"; - val bname = - (case try (unprefix file_prefix) file_name of - NONE => err ("File name needs to have prefix " ^ quote file_prefix) - | SOME file_name' => - (case try (unsuffix file_suffix) file_name' of - NONE => err ("File name needs to have suffix " ^ quote file_suffix) - | SOME bname => bname)); - val binding = Binding.make (bname, pos); + val (file, thy') = get_file thy; + val binding = Binding.make (strip_template (#src_path file, pos), pos); val text = cat_lines (#lines file); - val (name, thy2) = define_template (binding, text) thy1; - val _ = writeln ("Defined template " ^ quote (print_template (Context.Theory thy2) name)); - in thy2 end))); + in #2 (define_template (binding, text) thy') end))); + +val _ = + Outer_Syntax.command \<^command_keyword>\define_ontology\ + "define DOF document ontology (via LaTeX style file)" + (Parse.position Resources.provide_parse_file >> + (fn (get_file, pos) => Toplevel.theory (fn thy => + let + val (file, thy') = get_file thy; + val binding = Binding.make (strip_ontology (#src_path file, pos), pos); + val text = cat_lines (#lines file); + in #2 (define_ontology (binding, text) thy') end))); end; \ diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 6c61f9c..5e1aa3b 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -28,6 +28,8 @@ theory CENELEC_50128 imports "Isabelle_DOF.technical_report" begin +define_ontology "DOF-CENELEC_50128.sty" + (* this is a hack and should go into an own ontology, providing thingsd like: - Assumption* - Hypothesis* diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 60fa809..ada1d8d 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -17,9 +17,11 @@ theory scholarly_paper imports "Isabelle_DOF.Isa_COL" keywords "author*" "abstract*" "Definition*" "Lemma*" "Theorem*" :: document_body - begin +define_ontology "DOF-scholarly_paper.sty" +define_ontology "DOF-scholarly_paper-thm.sty" + text\Scholarly Paper provides a number of standard text - elements for scientific papers. They were introduced in the following.\ diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 0876379..f2b3ff8 100644 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -17,6 +17,8 @@ theory technical_report imports "Isabelle_DOF.scholarly_paper" begin +define_ontology "DOF-technical_report.sty" + (* for reports paper: invariant: level \ -1 *) section\More Global Text Elements for Reports\ diff --git a/src/scala/dof.scala b/src/scala/dof.scala index 7afec65..d8f797e 100644 --- a/src/scala/dof.scala +++ b/src/scala/dof.scala @@ -47,12 +47,6 @@ object DOF { val session = "Isabelle_DOF" - def implode_ontologies(list: List[String]): String = Word.implode(list) - def explode_ontologies(text: String): List[String] = Word.explode(text) - val ontologies: List[String] = - explode_ontologies("Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper") - val template = "Isabelle_DOF.scrreprt-modern" - val latest_version = "1.3.0" val latest_isabelle = "Isabelle2021-1" val latest_doi = "10.5281/zenodo.6810799" diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index cad7fc4..c85177b 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -72,7 +72,7 @@ object DOF_Document_Build val isabelle_dof_dir = context.session_context.sessions_structure(DOF.session).dir - // root.tex from exported template + // root.tex from exports File.write(directory.doc_dir + Path.explode("root.tex"), the_document_entry(context, "dof/root.tex", "use_template").text) @@ -83,10 +83,15 @@ object DOF_Document_Build file => file.getName.endsWith(".sty"), include_dirs = true)) .foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file)) - // create ontology.sty - val ontologies = DOF.explode_ontologies(options.string("dof_ontologies")) + // ontologies.tex from exports + val ontologies = { + val xml = the_document_entry(context, "dof/ontologies", "use_ontology").uncompressed_yxml + import XML.Decode._ + list(pair(string, string))(xml) + } File.write(directory.doc_dir + Path.explode("ontologies.tex"), - ontologies.map(name => "\\usepackage{DOF-" + Long_Name.base_name(name) + "}\n").mkString) + (for ((name, _) <- ontologies) + yield { "\\usepackage{DOF-" + Long_Name.base_name(name) + "}\n" }).mkString) // create dof-config.sty File.write(directory.doc_dir + Path.explode("dof-config.sty"), """ diff --git a/src/scala/dof_mkroot.scala b/src/scala/dof_mkroot.scala index 8acba78..2b41889 100644 --- a/src/scala/dof_mkroot.scala +++ b/src/scala/dof_mkroot.scala @@ -40,12 +40,15 @@ object DOF_Mkroot { /** mkroot **/ + val default_ontologies: List[String] = List("technical_report", "scholarly_paper") + val default_template = "scrreprt-modern" + def mkroot( session_name: String = "", session_dir: Path = Path.current, init_repos: Boolean = false, - ontologies: List[String] = DOF.ontologies, - template: String = DOF.template, + ontologies: List[String] = default_ontologies, + template: String = default_template, progress: Progress = new Progress): Unit = { Isabelle_System.make_directory(session_dir) @@ -67,8 +70,7 @@ object DOF_Mkroot File.write(root_path, "session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ + - options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """ - + quote(DOF.implode_ontologies(ontologies)) + """] + options [document = pdf, document_output = "output", document_build = dof] (*theories [document = false] A B*) @@ -85,6 +87,7 @@ object DOF_Mkroot begin use_template """ + quote(template) + """ +use_ontology """ + ontologies.map(quote).mkString(" and ") + """ end """) @@ -147,8 +150,8 @@ Now use the following command line to build the session: var init_repos = false var help = false var session_name = "" - var ontologies = DOF.ontologies - var template = DOF.template + var ontologies = default_ontologies + var template = default_template val getopts = Getopts(""" Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY] @@ -158,15 +161,15 @@ Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY] -h print help -n NAME alternative session name (default: directory base name) -o NAMES list of ontologies, separated by blanks - (default: """ + quote(DOF.implode_ontologies(DOF.ontologies)) + """) - -t NAME template (default: """ + quote(DOF.template) + """) + (default: """ + quote(Word.implode(default_ontologies)) + """) + -t NAME template (default: """ + quote(default_template) + """) Prepare session root directory for Isabelle/DOF (default: current directory). """, "I" -> (_ => init_repos = true), "h" -> (_ => help = true), "n:" -> (arg => session_name = arg), - "o:" -> (arg => ontologies = DOF.explode_ontologies(arg)), + "o:" -> (arg => ontologies = Word.explode(arg)), "t:" -> (arg => template = arg)) val more_args = getopts(args) diff --git a/src/tests/Isabelle2022.thy b/src/tests/Isabelle2022.thy index ef84f17..d421565 100644 --- a/src/tests/Isabelle2022.thy +++ b/src/tests/Isabelle2022.thy @@ -44,7 +44,7 @@ text \ we see more and more alternatives, e.g. system options or services in Isabelle/Scala (see below). - \<^item> \<^file>\$ISABELLE_DOF_HOME/etc/options\ should not be used for regular + \<^item> \<^path>\$ISABELLE_DOF_HOME/etc/options\ should not be used for regular Isabelle/DOF applications: thus it works properly within Isabelle/AFP, where the component context is missing. \