From 6a9472874755c993c4336f871630b943c3546fdb Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 17 Jul 2022 20:47:17 +0100 Subject: [PATCH 01/13] Port to development version of Isabelle. --- src/DOF/RegExpInterface.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy index 81c81f7..873ac27 100644 --- a/src/DOF/RegExpInterface.thy +++ b/src/DOF/RegExpInterface.thy @@ -118,7 +118,7 @@ ML\ fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f)) val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args) val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files)) - val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files + val ml_content = map (fn f => Syntax.read_input (Bytes.content (#content f))) ml_files fun eval ml_content = fold (fn sml => (ML_Context.exec (fn () => ML_Context.eval_source ML_Compiler.flags sml))) ml_content From f40d33b9ed400d0a1dbb6d75b4e771d8e623d1e6 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 17 Jul 2022 22:46:56 +0100 Subject: [PATCH 02/13] Ad-hoc port to development version of Isabelle. --- src/DOF/Isa_DOF.thy | 33 +++++++++++++++++++++++++-------- 1 file changed, 25 insertions(+), 8 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 915e37a..4b7e64f 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay + * 2019-2022 The University of Exeter + * 2018-2022 The University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -1947,6 +1947,23 @@ fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args val output_text = Document_Output.output_document ctxt {markdown = markdown} text; in markup (output_meta @ output_text) end; + val output_name = (* was available as Latex.output_name in Isabelle 2021-1 and earlier *) + translate_string + (fn "_" => "UNDERSCORE" + | "'" => "PRIME" + | "0" => "ZERO" + | "1" => "ONE" + | "2" => "TWO" + | "3" => "THREE" + | "4" => "FOUR" + | "5" => "FIVE" + | "6" => "SIX" + | "7" => "SEVEN" + | "8" => "EIGHT" + | "9" => "NINE" + | s => s); + + fun document_output_reports name {markdown, body} meta_args text ctxt = let val pos = Input.pos_of text; @@ -1956,7 +1973,7 @@ fun document_output_reports name {markdown, body} meta_args text ctxt = (pos, Markup.plain_text)]; fun markup xml = let val m = if body then Markup.latex_body else Markup.latex_heading - in [XML.Elem (m (Latex.output_name name), xml)] end; + in [XML.Elem (m (output_name name), xml)] end; in document_output {markdown = markdown, markup = markup} meta_args text ctxt end; @@ -2332,7 +2349,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc {unchecked = false, define= false} (* default *); -val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)) +val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Parse.embedded_input)) : ({define:bool,unchecked:bool} * Input.source) context_parser; @@ -2781,7 +2798,7 @@ fun string_2_theory_text_antiquotation ctxt text = end fun gen_text_antiquotation name reportNcheck compile = - Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -2832,12 +2849,11 @@ fun theory_text_antiquotation name = fun environment_delim name = - ("%\n\\begin{" ^ Latex.output_name name ^ "}\n", - "\n\\end{" ^ Latex.output_name name ^ "}"); + ("%\n\\begin{" ^ Monitor_Command_Parser.output_name name ^ "}\n", + "\n\\end{" ^ Monitor_Command_Parser.output_name name ^ "}"); fun environment_block name = environment_delim name |-> XML.enclose; - fun enclose_env verbatim ctxt block_env body = if Config.get ctxt Document_Antiquotation.thy_output_display then if verbatim @@ -2848,6 +2864,7 @@ fun enclose_env verbatim ctxt block_env body = end \ + ML\ local val parse_literal = Parse.alt_string || Parse.cartouche From 2c1b56d2779100d1f30e1ea8be9bb18c6c9918ed Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 23 Jul 2022 16:14:14 +0100 Subject: [PATCH 03/13] Port to development version of Isabelle. --- .../TR_MyCommentedIsabelle.thy | 20 ++++++++----------- 1 file changed, 8 insertions(+), 12 deletions(-) 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 bf6510d..2282ae8 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019-2021 The University of Exeter - * 2018-2021 The University of Paris-Saclay + * 2019-2022 The University of Exeter + * 2018-2022 The University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -23,7 +23,7 @@ open_monitor*[this::report] (*>*) title*[tit::title]\My Personal, Eclectic Isabelle Programming Manual\ -subtitle*[stit::subtitle]\Version : Isabelle 2020\ +subtitle*[stit::subtitle]\Version : Isabelle 2022\ text*[bu::author, email = "''wolff@lri.fr''", affiliation = "\Université Paris-Saclay, LRI, France\"]\Burkhart Wolff\ @@ -1183,7 +1183,7 @@ text\ The extensibility of Isabelle as a system framework depends on a num \<^item> \<^ML>\Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\ adjoins a theory transformer. \<^item> \<^ML>\Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\ - \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.exit: Toplevel.transition -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.ignored: Position.T -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.present_local_theory: (xstring * Position.T) option -> @@ -1845,6 +1845,7 @@ text\The second part is much more high-level, and can be found under \<^ML This is perhaps meant with the fairly cryptic comment: "Quasi-inner syntax based on outer tokens: concrete argument syntax of attributes, methods etc." at the beginning of this structure.\ +ML\open Args\ text\ Some more combinators \<^item>\<^ML>\Args.symbolic : Token.T parser\ @@ -1865,12 +1866,11 @@ Common Isar Syntax \<^item>\<^ML>\Args.name_position: (string * Position.T) parser\ \<^item>\<^ML>\Args.cartouche_inner_syntax: string parser\ \<^item>\<^ML>\Args.cartouche_input: Input.source parser\ -\<^item>\<^ML>\Args.text_token: Token.T parser \ Common Isar Syntax -\<^item>\<^ML>\Args.text_input: Input.source parser\ -\<^item>\<^ML>\Args.text : string parser\ +\<^item>\<^ML>\Parse.embedded_input: Input.source parser\ +\<^item>\<^ML>\Parse.embedded : string parser\ \<^item>\<^ML>\Args.binding : Binding.binding parser\ Common Stuff related to Inner Syntax Parsing @@ -1893,8 +1893,7 @@ Common Isar Syntax \<^item>\<^ML>\Args.named_source: (Token.T -> Token.src) -> Token.src parser\ \<^item>\<^ML>\Args.named_typ : (string -> typ) -> typ parser\ \<^item>\<^ML>\Args.named_term : (string -> term) -> term parser\ -\<^item>\<^ML>\Args.text_declaration: (Input.source -> declaration) -> declaration parser\ -\<^item>\<^ML>\Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\ +\<^item>\<^ML>\Args.embedded_declaration: (Input.source -> declaration) -> declaration parser\ \<^item>\<^ML>\Args.typ_abbrev : typ context_parser\ \<^item>\<^ML>\Args.typ: typ context_parser\ \<^item>\<^ML>\Args.term: term context_parser\ @@ -1903,8 +1902,6 @@ Common Isar Syntax \<^item>\<^ML>\Args.named_source: (Token.T -> Token.src) -> Token.src parser\ \<^item>\<^ML>\Args.named_typ : (string -> typ) -> typ parser\ \<^item>\<^ML>\Args.named_term: (string -> term) -> term parser\ -\<^item>\<^ML>\Args.text_declaration: (Input.source -> declaration) -> declaration parser\ -\<^item>\<^ML>\Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\ Syntax for some major Pure commands in Isar \<^item>\<^ML>\Args.prop: term context_parser\ @@ -2132,7 +2129,6 @@ Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to \<^item>\<^ML>\Latex.string: string -> Latex.text\ \<^item>\<^ML>\Latex.text: string * Position.T -> Latex.text\ -\<^item>\<^ML>\Latex.output_name: string -> string\ \<^item>\<^ML>\Latex.output_ascii: string -> string\ \<^item>\<^ML>\Latex.output_symbols: Symbol.symbol list -> string\ From 7f500dc25791f181da6303ad79549ea21433121a Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 11 Aug 2022 23:04:07 +0100 Subject: [PATCH 04/13] Migration to latest Isabelle development version. --- src/scala/dof_document_build.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index be9ba11..a005560 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -52,8 +52,8 @@ object DOF_Document_Build // produced by alternative presentation hook (workaround for missing Toplevel.present_theory) for (name <- context.document_theories) { val path = Path.basic(Document_Build.tex_name(name)) - val xml = - YXML.parse_body(context.get_export(name.theory, Export.DOCUMENT_LATEX + "_dof").text) + val entry = context.session_context(name.theory, Export.DOCUMENT_LATEX + "_dof", permissive = true) + val xml = YXML.parse_body(entry.text) if (xml.nonEmpty) { File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) .write(directory.doc_dir) From 0c8a0e1d63eef778a5df8e4363d9d6e0df25213a Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:30:49 +0200 Subject: [PATCH 05/13] Adapted to Isabelle/1ac2416e8432 -- approx. Isabelle2022 release. --- .../TR_MyCommentedIsabelle.thy | 12 ++++-------- src/DOF/Isa_COL.thy | 2 +- src/DOF/Isa_DOF.thy | 8 ++++---- src/DOF/RegExpInterface.thy | 2 +- src/scala/dof_document_build.scala | 14 +++++++------- src/tests/OutOfOrderPresntn.thy | 6 +++--- 6 files changed, 20 insertions(+), 24 deletions(-) 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 bf6510d..e892b5e 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -1183,7 +1183,7 @@ text\ The extensibility of Isabelle as a system framework depends on a num \<^item> \<^ML>\Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\ adjoins a theory transformer. \<^item> \<^ML>\Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\ - \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.exit: Toplevel.transition -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.ignored: Position.T -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.present_local_theory: (xstring * Position.T) option -> @@ -1865,12 +1865,11 @@ Common Isar Syntax \<^item>\<^ML>\Args.name_position: (string * Position.T) parser\ \<^item>\<^ML>\Args.cartouche_inner_syntax: string parser\ \<^item>\<^ML>\Args.cartouche_input: Input.source parser\ -\<^item>\<^ML>\Args.text_token: Token.T parser \ Common Isar Syntax -\<^item>\<^ML>\Args.text_input: Input.source parser\ -\<^item>\<^ML>\Args.text : string parser\ +\<^item>\<^ML>\Parse.embedded_input: Input.source parser\ +\<^item>\<^ML>\Parse.embedded : string parser\ \<^item>\<^ML>\Args.binding : Binding.binding parser\ Common Stuff related to Inner Syntax Parsing @@ -1893,8 +1892,7 @@ Common Isar Syntax \<^item>\<^ML>\Args.named_source: (Token.T -> Token.src) -> Token.src parser\ \<^item>\<^ML>\Args.named_typ : (string -> typ) -> typ parser\ \<^item>\<^ML>\Args.named_term : (string -> term) -> term parser\ -\<^item>\<^ML>\Args.text_declaration: (Input.source -> declaration) -> declaration parser\ -\<^item>\<^ML>\Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\ +\<^item>\<^ML>\Args.embedded_declaration: (Input.source -> declaration) -> declaration parser\ \<^item>\<^ML>\Args.typ_abbrev : typ context_parser\ \<^item>\<^ML>\Args.typ: typ context_parser\ \<^item>\<^ML>\Args.term: term context_parser\ @@ -1903,8 +1901,6 @@ Common Isar Syntax \<^item>\<^ML>\Args.named_source: (Token.T -> Token.src) -> Token.src parser\ \<^item>\<^ML>\Args.named_typ : (string -> typ) -> typ parser\ \<^item>\<^ML>\Args.named_term: (string -> term) -> term parser\ -\<^item>\<^ML>\Args.text_declaration: (Input.source -> declaration) -> declaration parser\ -\<^item>\<^ML>\Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\ Syntax for some major Pure commands in Isar \<^item>\<^ML>\Args.prop: term context_parser\ diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 409269a..9440515 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -206,7 +206,7 @@ fun check_latex_measure _ src = handle Fail _ => error ("syntax error in LaTeX measure") ) in () end -val parse_latex_measure = Args.text_input >> (fn src => (check_latex_measure () (* dummy arg *) src; +val parse_latex_measure = Parse.embedded_input >> (fn src => (check_latex_measure () (* dummy arg *) src; (fst o Input.source_content) src ) ) end\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 1164ebf..b2047c1 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -2364,7 +2364,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc {unchecked = false, define= false} (* default *); -val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)) +val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Parse.embedded_input)) : ({define:bool,unchecked:bool} * Input.source) context_parser; @@ -2835,7 +2835,7 @@ fun string_2_theory_text_antiquotation ctxt text = end fun gen_text_antiquotation name reportNcheck compile = - Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -2848,7 +2848,7 @@ fun std_text_antiquotation name (* redefined in these more abstract terms *) = (* should be the same as (2020): fun text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val _ = report_text ctxt text; @@ -2864,7 +2864,7 @@ fun std_theory_text_antiquotation name (* redefined in these more abstract terms (* should be the same as (2020): fun theory_text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val keywords = Thy_Header.get_keywords' ctxt; diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy index 81c81f7..873ac27 100644 --- a/src/DOF/RegExpInterface.thy +++ b/src/DOF/RegExpInterface.thy @@ -118,7 +118,7 @@ ML\ fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f)) val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args) val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files)) - val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files + val ml_content = map (fn f => Syntax.read_input (Bytes.content (#content f))) ml_files fun eval ml_content = fold (fn sml => (ML_Context.exec (fn () => ML_Context.eval_source ML_Compiler.flags sml))) ml_content diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index be9ba11..22fd697 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -50,14 +50,14 @@ object DOF_Document_Build val directory = context.prepare_directory(dir, doc, latex_output) // produced by alternative presentation hook (workaround for missing Toplevel.present_theory) - for (name <- context.document_theories) { + for { + name <- context.document_theories.iterator + entry <- context.session_context.get(name.theory, Export.DOCUMENT_LATEX + "_dof") + } { val path = Path.basic(Document_Build.tex_name(name)) - val xml = - YXML.parse_body(context.get_export(name.theory, Export.DOCUMENT_LATEX + "_dof").text) - if (xml.nonEmpty) { - File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) - .write(directory.doc_dir) - } + val xml = YXML.parse_body(entry.text) + File.content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) + .write(directory.doc_dir) } val dof_home= Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME")); // print(context.options.string("dof_url")); diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index fd8207e..dc37733 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -244,7 +244,7 @@ fun string_2_theory_text_antiquotation ctxt text = end fun gen_text_antiquotation name reportNcheck compile = - Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -257,7 +257,7 @@ fun std_text_antiquotation name (* redefined in these more abstract terms *) = (* should be the same as (2020): fun text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val _ = report_text ctxt text; @@ -273,7 +273,7 @@ fun std_theory_text_antiquotation name (* redefined in these more abstract terms (* should be the same as (2020): fun theory_text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val keywords = Thy_Header.get_keywords' ctxt; From 15feeb7d92a946da245c8c42bfbc007e52da2c5e Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:38:01 +0200 Subject: [PATCH 06/13] More standard package name: appears to work properly in Isabelle2022. --- etc/build.props | 4 ++-- src/scala/dof_document_build.scala | 2 +- src/scala/dof_mkroot.scala | 2 +- src/scala/dof_tools.scala | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/etc/build.props b/etc/build.props index af46f5e..dc6522d 100644 --- a/etc/build.props +++ b/etc/build.props @@ -8,5 +8,5 @@ sources = \ src/scala/dof_mkroot.scala \ src/scala/dof_tools.scala services = \ - isabelle_dof.DOF_Tools \ - isabelle_dof.DOF_Document_Build$Engine + isabelle.dof.DOF_Tools \ + isabelle.dof.DOF_Document_Build$Engine diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 22fd697..19b2a11 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -28,7 +28,7 @@ * SPDX-License-Identifier: BSD-2-Clause */ -package isabelle_dof +package isabelle.dof import isabelle._ import java.io.{File => JFile} diff --git a/src/scala/dof_mkroot.scala b/src/scala/dof_mkroot.scala index d37419f..6cf160f 100644 --- a/src/scala/dof_mkroot.scala +++ b/src/scala/dof_mkroot.scala @@ -34,7 +34,7 @@ Prepare session root directory for Isabelle/DOF. */ -package isabelle_dof +package isabelle.dof import isabelle._ diff --git a/src/scala/dof_tools.scala b/src/scala/dof_tools.scala index b21fee3..b298a73 100644 --- a/src/scala/dof_tools.scala +++ b/src/scala/dof_tools.scala @@ -29,7 +29,7 @@ */ -package isabelle_dof +package isabelle.dof import isabelle._ From 5ac41a72ac0909c260f504292bd84b03fc8b8a53 Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:58:10 +0200 Subject: [PATCH 07/13] More accurate treatment of sty files: do not just copy from all examples. --- src/scala/dof_document_build.scala | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 19b2a11..d70a10d 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -31,7 +31,6 @@ package isabelle.dof import isabelle._ -import java.io.{File => JFile} object DOF_Document_Build @@ -59,22 +58,22 @@ object DOF_Document_Build File.content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) .write(directory.doc_dir) } - val dof_home= Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME")); + val dof_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME")); // print(context.options.string("dof_url")); // copy Isabelle/DOF LaTeX templates - val template_dir = dof_home + Path.explode("src/document-templates/") + val template_dir = dof_home + Path.explode("src/document-templates") // TODO: error handling in case 1) template does not exist or 2) root.tex does already exist val template = regex.replaceAllIn(context.options.string("dof_template"),"") Isabelle_System.copy_file(template_dir + Path.explode("root-"+template+".tex"), directory.doc_dir+Path.explode("root.tex")) - // copy Isabelle/DOF LaTeX styles - val doc_jdir = new JFile(directory.doc_dir.implode) - val styles = File.find_files(new JFile(dof_home.implode),((f:JFile) => f.getName().endsWith(".sty")), true) - for (sty <- styles) { - Isabelle_System.copy_file(sty, doc_jdir) - } + // copy Isabelle/DOF LaTeX styles + List(Path.explode("src/DOF/latex"), Path.explode("src/ontologies")) + .flatMap(dir => + File.find_files((dof_home + dir).file, + file => file.getName.endsWith(".sty"), include_dirs = true)) + .foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file)) // create ontology.sty val ltx_styles = context.options.string("dof_ontologies").split(" +").map(s => regex.replaceAllIn(s,"")) From 516f5d2f79e94c2cffbaaac253820276f5a3f755 Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 22:11:30 +0200 Subject: [PATCH 08/13] Merely use session structure instead of component settings. --- src/scala/dof_document_build.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index d70a10d..31d8859 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -58,20 +58,20 @@ object DOF_Document_Build File.content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) .write(directory.doc_dir) } - val dof_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME")); + val isabelle_dof_dir = context.session_context.sessions_structure("Isabelle_DOF").dir // print(context.options.string("dof_url")); // copy Isabelle/DOF LaTeX templates - val template_dir = dof_home + Path.explode("src/document-templates") + val template_dir = isabelle_dof_dir + Path.explode("document-templates") // TODO: error handling in case 1) template does not exist or 2) root.tex does already exist val template = regex.replaceAllIn(context.options.string("dof_template"),"") Isabelle_System.copy_file(template_dir + Path.explode("root-"+template+".tex"), directory.doc_dir+Path.explode("root.tex")) // copy Isabelle/DOF LaTeX styles - List(Path.explode("src/DOF/latex"), Path.explode("src/ontologies")) + List(Path.explode("DOF/latex"), Path.explode("ontologies")) .flatMap(dir => - File.find_files((dof_home + dir).file, + File.find_files((isabelle_dof_dir + dir).file, file => file.getName.endsWith(".sty"), include_dirs = true)) .foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file)) From 82645c2e8e0154b3cda83123c3aa9a82e008eb32 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 30 Oct 2022 17:30:21 +0000 Subject: [PATCH 09/13] Update to Isabelle 2022. --- .woodpecker/build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.woodpecker/build.yml b/.woodpecker/build.yml index a19712a..a6d9d07 100644 --- a/.woodpecker/build.yml +++ b/.woodpecker/build.yml @@ -1,6 +1,6 @@ pipeline: build: - image: docker.io/logicalhacking/isabelle2021-1 + image: docker.io/logicalhacking/isabelle2022 commands: - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX - mkdir -p $ARTIFACT_DIR @@ -16,7 +16,7 @@ pipeline: - cd ../.. - ln -s * latest archive: - image: docker.io/logicalhacking/isabelle2021-1 + image: docker.io/logicalhacking/isabelle2022 commands: - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX - mkdir -p $ARTIFACT_DIR From 873151b4f3a28d205468b98d3bb1ee609e15a7b0 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 30 Oct 2022 17:56:15 +0000 Subject: [PATCH 10/13] Update to Isabelle 2022. --- .woodpecker/README.md | 2 +- CHANGELOG.md | 2 ++ README.md | 6 +++--- etc/options | 4 ++-- src/scala/dof_document_build.scala | 2 +- 5 files changed, 9 insertions(+), 7 deletions(-) diff --git a/.woodpecker/README.md b/.woodpecker/README.md index 049fb95..9e33d98 100644 --- a/.woodpecker/README.md +++ b/.woodpecker/README.md @@ -15,4 +15,4 @@ It may also contain additional tools and script that are useful for preparing a * pdflatex * [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/browser_info/Unsorted/) * [aux files](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/) -* [Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz) +* [Isabelle_DOF-Unreleased_Isabelle2022.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2022.tar.xz) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5f14e64..1eb853c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,8 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0. ### Changed +- Updated Isabelle version to Isabelle 2022 + ## [1.3.0] - 2022-07-08 ### Changed diff --git a/README.md b/README.md index 52ba084..336f908 100644 --- a/README.md +++ b/README.md @@ -9,10 +9,10 @@ online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF Isabelle/DOF has three major prerequisites: -* **Isabelle:** Isabelle/DOF requires [Isabelle 2021-1](http://isabelle.in.tum.de/website-Isabelle2021-1/). - Please download the Isabelle 2021-1 distribution for your operating +* **Isabelle:** Isabelle/DOF requires [Isabelle 2022](http://isabelle.in.tum.de/website-Isabelle2022/). + Please download the Isabelle 2022 distribution for your operating system from the [Isabelle - website](http://isabelle.in.tum.de/website-Isabelle2021-1/). + website](http://isabelle.in.tum.de/website-Isabelle2022/). * **AFP:** Isabelle/DOF requires two entries from the [Archive of Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the AFP following the instructions given at diff --git a/etc/options b/etc/options index 27aa370..0dc8e3a 100644 --- a/etc/options +++ b/etc/options @@ -12,8 +12,8 @@ option dof_version : string = "Unreleased" -- "Isabelle/DOF version" (* "Unreleased" for development, semantic version for releases *) -option dof_isabelle : string = "2021-1" -option dof_afp : string = "afp-2021-12-28" +option dof_isabelle : string = "2022" +option dof_afp : string = "afp-2022-10-27" option dof_latest_version : string = "1.3.0" option dof_latest_isabelle : string = "Isabelle2021-1" diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 31d8859..b1f1919 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -82,7 +82,7 @@ object DOF_Document_Build // create dof-config.sty File.write(directory.doc_dir+Path.explode("dof-config.sty"), """ -\newcommand{\isabelleurl}{https://isabelle.in.tum.de/website-Isabelle2021-1/""" + context.options.string("dof_isabelle") + """} +\newcommand{\isabelleurl}{https://isabelle.in.tum.de/website-Isabelle2022/""" + context.options.string("dof_isabelle") + """} \newcommand{\dofurl}{""" + context.options.string("dof_url") + """} \newcommand{\dof@isabelleversion}{""" + context.options.string("dof_isabelle") + """} \newcommand{\isabellefullversion}{""" + context.options.string("dof_isabelle") + """\xspace} From 4e47c388606c50163f3c1de8651571d95b9ea942 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 31 Oct 2022 19:20:34 +0000 Subject: [PATCH 11/13] Declared installation script as deprecated. --- README.md | 17 ++--------------- install-afp | 23 ++++++++++++++++++++++- 2 files changed, 24 insertions(+), 16 deletions(-) diff --git a/README.md b/README.md index 336f908..207dc85 100644 --- a/README.md +++ b/README.md @@ -14,22 +14,9 @@ Isabelle/DOF has three major prerequisites: system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2022/). * **AFP:** Isabelle/DOF requires two entries from the [Archive of - Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the + Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the AFP following the instructions given at - . For your convenience, we also - provide a script that only installs the two entries required by - Isabelle/DOF into the local Isabelle/DOF directory. First, Isabelle/DOF - needs to be registered as an Isabelle component: - - ```console - foo@bar:~$ isabelle components -u `pwd` - ``` - - Thereafter, the AFP entries can be installed as follows: - - ```console - foo@bar:~$ isabelle env ./install-afp - ``` + . * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least [TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied. diff --git a/install-afp b/install-afp index ff199a2..6945838 100755 --- a/install-afp +++ b/install-afp @@ -35,6 +35,8 @@ print_help() { echo "Usage: isabelle env ./install-afp [OPTION] " echo "" + echo "Warning: This tools is deprecated." + echo "" echo "Run ..." echo "" echo " --help, -h display this help message" @@ -44,11 +46,29 @@ print_help() exit_error() { echo "" - echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***" + echo " *** Local AFP installation FAILED, please check the README.md for help ***" echo "" exit 1 } +confirm_usage() { + echo "* From Isabelle2021-1 on, the recommended method for making the whole AFP " + echo " available to Isabelle is the isabelle components -u command." + echo " For doing so, please follow the instructions at: " + echo " https://www.isa-afp.org/help/" + echo "" + echo " Alternatively, you can continue, on your own risk, to install only" + echo " the AFP entries required to run Isabelle/DOF." + echo "" + read -p " Still continue (y/N)? " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]]; + then + echo " Continuing installation on your OWN risk." + else + exit_error + fi +} check_isabelle_version() { echo "* Checking Isabelle version:" if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then @@ -149,6 +169,7 @@ AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz" echo "" echo "Isabelle/DOF AFP Installation Utility" echo "=====================================" +confirm_usage check_isabelle_version check_afp_entries echo "* AFP Installation successful." From fc575a5be532df80b006a35993ada4fbdc7c5487 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 31 Oct 2022 21:33:26 +0000 Subject: [PATCH 12/13] Fixed mardown. --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index 207dc85..04e05ad 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,6 @@ Isabelle/DOF has three major prerequisites: Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the AFP following the instructions given at . - * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least [TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied. From ab1877ce8e927eb682402fa0c464e35dec95de6f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 1 Nov 2022 20:58:34 +0000 Subject: [PATCH 13/13] Linting. --- README.md | 92 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 47 insertions(+), 45 deletions(-) diff --git a/README.md b/README.md index 04e05ad..f8806a4 100644 --- a/README.md +++ b/README.md @@ -1,32 +1,32 @@ # [Isabelle/DOF](https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF): Document Preparation Setup Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. -Isabelle/DOF allows for both conventional typesetting as well as formal -development. The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available +Isabelle/DOF allows for both conventional typesetting and formal development. +The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf) ## Pre-requisites Isabelle/DOF has three major prerequisites: -* **Isabelle:** Isabelle/DOF requires [Isabelle 2022](http://isabelle.in.tum.de/website-Isabelle2022/). - Please download the Isabelle 2022 distribution for your operating - system from the [Isabelle +* **Isabelle:** Isabelle/DOF requires [Isabelle + 2022](http://isabelle.in.tum.de/website-Isabelle2022/). Please download the + Isabelle 2022 distribution for your operating system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2022/). -* **AFP:** Isabelle/DOF requires two entries from the [Archive of - Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the - AFP following the instructions given at - . +* **AFP:** Isabelle/DOF requires two entries from the [Archive of Formal Proofs + (AFP)](https://www.isa-afp.org/). Please install the AFP following the + instructions given at . * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least - [TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied. + [TeX Live 2022](https://www.tug.org/texlive/) with all available updates + applied. ## Installation Isabelle/DOF is provided as an Isabelle component. After installing the prerequisites, change into the directory containing Isabelle/DOF (this should be the directory containing this `README.md` file) and execute (if you executed -this command already during the installation of the pre-requisites, you -can skip it now): +this command already during the installation of the prerequisites, you can skip +it now): ```console foo@bar:~$ isabelle components -u `pwd` @@ -44,25 +44,24 @@ This will compile Isabelle/DOF and run the example suite. ### Opening an Example -If you want to work with or extend one of the examples, e.g., you can -open it similar to any standard Isabelle theory: +If you want to work with or extend one of the examples, e.g., you can open it +similar to any standard Isabelle theory: ```console isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy ``` -This will open an example of a scientific paper using the pre-compiled -session ``Isabelle_DOF``, i.e., you will not be able to edit the -ontology definitions. If you want to edit the ontology definition, -just open the theory file with the default HOL session: +This will open an example of a scientific paper using the pre-compiled session +``Isabelle_DOF``, i.e., you will not be able to edit the ontology definitions. +If you want to edit the ontology definition, just open the theory file with the +default HOL session: ```console isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy ``` While this gives you more flexibility, it might "clutter" your editing -experience, as a lot of internal theories are loaded into Isabelle's -editor. +experience, as a lot of internal theories are loaded into Isabelle's editor. ### Creating a New Project @@ -73,23 +72,22 @@ Isabelle projects that use DOF need to be created using foo@bar:~$ isabelle dof_mkroot ``` -The ``dof_mkroot`` command takes the same parameter as the standard -``mkroot`` command of Isabelle. Thereafter, the normal Isabelle -command for building documents can be used. +The ``dof_mkroot`` command takes the same parameter as the standard ``mkroot`` +command of Isabelle. Thereafter, the normal Isabelle command for building +documents can be used. -Using the ``-o`` option, different ontology setups can be -selected and using the ``-t`` option, different LaTeX setups -can be selected. For example, +Using the ``-o`` option, different ontology setups can be selected and using the +``-t`` option, different LaTeX setups can be selected. For example, ```console foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl ``` -creates a setup using the scholarly_paper ontology and the article -class from the KOMA-Script bundle. +creates a setup using the scholarly_paper ontology and the article class from +the KOMA-Script bundle. -The help (option ``-h``) show a list of all supported ontologies and -document templates: +The help (option ``-h``) show a list of all supported ontologies and document +templates: ```console foo@bar:~$ isabelle dof_mkroot -h @@ -114,7 +112,7 @@ are available: * [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz) * [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc) -### Older Releases +### Older Releases * Isabelle/DOF 1.2.0/Isabelle2021 * [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf) @@ -155,28 +153,32 @@ SPDX-License-Identifier: BSD-2-Clause ## Publications -* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart - Wolff. [Using The Isabelle Ontology Framework: Linking the Formal - with the Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf). - In Conference on Intelligent Computer Mathematics (CICM). Lecture - Notes in Computer Science (11006), Springer-Verlag, 2018. +* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff. + [Using The Isabelle Ontology Framework: Linking the Formal with the + Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf). + In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in + Computer Science (11006), Springer-Verlag, 2018. [doi:10.1007/978-3-319-96812-4_3](https://doi.org/10.1007/978-3-319-96812-4_3). * Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf). - In Software Engineering and Formal Methods (SEFM). Lecture Notes in - Computer Science (11724), Springer-Verlag, 2019. + In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer + Science (11724), Springer-Verlag, 2019. [doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15). -* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In - Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. +* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments + Targeting + Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). + In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). + Springer-Verlag 2019. [doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4) -* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development - Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document) - In ERTS 2018. +* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. + [Making Agile Development Processes fit for V-style Certification + Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document). In ERTS + 2018. ## Upstream Repository -The upstream git repository, i.e., the single source of truth, for this project is hosted -at . +The upstream git repository, i.e., the single source of truth, for this project +is hosted at .