From a66e90cf253a99459c5995b0d703a4c372788f4b Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 17 Mar 2022 08:48:25 +0000 Subject: [PATCH 1/6] Switchted to notion of upstream repository. --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index b24d8a36..f085da04 100755 --- a/README.md +++ b/README.md @@ -192,7 +192,7 @@ SPDX-License-Identifier: BSD-2-Clause Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document) In ERTS 2018. -## Main Repository +## Upstream Repository -The main git repository, i.e., the single source of truth, for this project is hosted +The upstream git repository, i.e., the single source of truth, for this project is hosted at . From f6e9e39a582d0b9ccb12d8271d519a242c974fbf Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 17 Mar 2022 08:51:37 +0000 Subject: [PATCH 2/6] Removed reference to lncs as a special case, as llncs.cls finally arrived on CTAN. --- .../technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 876f5c02..f06f9a48 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -195,8 +195,8 @@ text\ Creating a new document setup requires two decisions: \<^item> which ontologies (\<^eg>, scholarly\_paper) are required and \<^item> which document template (layout)\index{document template} should be used - (\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually - obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \<^boxed_bash>\llncs.cls\. + (\<^eg>, scrartcl\index{scrartcl}). Some templates require that the users manually + obtains and adds the necessary \<^LaTeX> class file. This is due to licensing restrictions).\ text\ This can be configured by using the command-line options of of \<^boxed_bash>\mkroot_DOF\. In From e4195a68a27190b8faa4d8b518555187471e9845 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 17 Mar 2022 17:14:20 +0100 Subject: [PATCH 3/6] Update DOF manual, chapters 02-03 - Use antiquotations when possible to reference classes and attributes in text (typ and const antiquotations) - Update some isar code examples - Fix typos --- .../Isabelle_DOF-Manual/02_Background.thy | 14 +- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 151 +++++++++--------- 2 files changed, 81 insertions(+), 84 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index fce573bc..12a8a4aa 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -26,7 +26,7 @@ figure*[architecture::figure,relative_width="95",src="''figures/isabelle-archite the IDE (right-hand side). \ text*[bg::introduction]\ -While Isabelle @{cite "nipkow.ea:isabelle:2002"} is widely perceived as an interactive theorem +While Isabelle is widely perceived as an interactive theorem prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize the view that Isabelle is far more than that: it is the \<^emph>\Eclipse of Formal Methods Tools\. This refers to the ``\<^emph>\generic system framework of Isabelle/Isar underlying recent versions of Isabelle. @@ -37,7 +37,7 @@ with explicit infrastructure for building derivative systems.\''~@{cite " The current system framework offers moreover the following features: \<^item> a build management grouping components into to pre-compiled sessions, -\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends +\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends, \<^item> documentation-generation, \<^item> code generators for various target languages, \<^item> an extensible front-end language Isabelle/Isar, and, @@ -70,13 +70,13 @@ declare_reference*["fig:dependency"::text_section] text\ - The Isabelle Framework is based on a \<^emph>\document-centric view\ bindex>\document-centric view\ of + The Isabelle Framework is based on a \<^emph>\document-centric view\\<^bindex>\document-centric view\ of a document, treating the input in its integrality as set of (user-programmable) \<^emph>\document element\ that may mutually depend and link to each other; A \<^emph>\document\ in our sense is what is configured in a set of \<^verbatim>\ROOT\- and \<^verbatim>\ROOTS\-files. Isabelle assumes a hierarchical document model\<^index>\document model\, \<^ie>, an \<^emph>\integrated\ document - consist of a hierarchy \<^emph>\sub-documents\ (files); dependencies are restricted to be + consist of a hierarchy of \<^emph>\sub-documents\ (files); dependencies are restricted to be acyclic at this level. Sub-documents can have different document types in order to capture documentations consisting of documentation, models, proofs, code of various forms and other technical artifacts. We call the @@ -104,7 +104,7 @@ text\ A text-element \<^index>\text-element\ may look like th text\ According to the \<^emph>\reflexivity\ axiom @{thm refl}, we obtain in \ for @{term "fac 5"} the result @{value "fac 5"}.\\} ... so it is a command \<^theory_text>\text\ followed by an argument (here in \\ ... \\ paranthesis) which -contains characters and and a special notation for semantic macros \<^bindex>\semantic macros\ +contains characters and a special notation for semantic macros \<^bindex>\semantic macros\ (here \<^theory_text>\@{term "fac 5"}).\ \ @@ -122,7 +122,7 @@ value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\\(formal) text-contexts\,\<^index>\formal text-contexts\ \<^emph>\(ML) code-contexts\\<^index>\code-contexts\ and \<^emph>\term-contexts\\<^index>\term-contexts\ if we refer to sub-elements inside the \\...\\ cartouches of these command families. Note that the Isabelle -framework allows for nesting cartouches that permits to support to switch into a different +framework allows for nesting cartouches that permits to support switching into a different context. In general, this has also the effect that the evaluation of antiquotations changes. \<^footnote>\In the literature, this concept has been referred to \Cascade-Syntax\ and was used in the Centaur-system and is existing in some limited form in some Emacs-implementations these days. \ @@ -188,7 +188,7 @@ text\ Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits. Besides UTF8-support for characters used in text-elements, Isabelle offers built-in already a - mechanism user-programmable antiquotations \<^index>\antiquotations\ which we use to implement + mechanism for user-programmable antiquotations \<^index>\antiquotations\ which we use to implement semantic macros \<^index>\semantic macros\ in \<^isadof> (We will actually use these two terms as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index f06f9a48..50b7395c 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -24,13 +24,13 @@ begin chapter*[isadof_tour::text_section]\\<^isadof>: A Guided Tour\ text\ - In this chapter, we will give a introduction into using \<^isadof> for users that want to create and + In this chapter, we will give an introduction into using \<^isadof> for users that want to create and maintain documents following an existing document ontology. \ section*[getting_started::technical]\Getting Started\ text\ -As an alternative to installing \<^isadof>{} locally, the latest official release \<^isadof> is also +As an alternative to installing \<^isadof>{} locally, the latest official release of \<^isadof> is also available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus, if you have \href{https://www.docker.com}{Docker} installed and your installation of Docker supports X11 application, you can start \<^isadof> as follows: @@ -85,7 +85,7 @@ text\ We start by extracting the \<^isadof> archive: @{boxed_bash [display]\ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\} This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution. -Next, we need to invoke the \<^boxed_bash>\install\ script. If necessary, the installations +Next, we need to invoke the \<^boxed_bash>\install\ script. If necessary, the installation automatically downloads additional dependencies from the AFP (\<^url>\https://www.isa-afp.org\), namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a @@ -138,7 +138,7 @@ Isabelle/DOF Installer /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \} After the successful installation, you can explore the examples (in the sub-directory -\<^boxed_bash>\examples\ or create your own project. On the first start, the session +\<^boxed_bash>\examples\) or create your own project. On the first start, the session \<^boxed_bash>\Isabelle_DOF\ will be built automatically. If you want to pre-build this session and all example documents, execute: @{boxed_bash [display]\ë\prompt{\isadofdirn}ë isabelle build -D . \} @@ -158,13 +158,13 @@ Now use the following coëëmmand line to build the session: isabelle build -D myproject \} The created project uses the default configuration (the ontology for writing academic papers (scholarly\_paper) using a report layout based on the article class (\<^boxed_latex>\scrartcl\) of - the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}. The directory \<^boxed_bash>\myproject\ + the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}). The directory \<^boxed_bash>\myproject\ contains the \<^isadof>-setup for your new document. To check the document formally, including the generation of the document in PDF, you only need to execute -@{boxed_bash [display]\ë\prompt{}ë isabelle build -d . myproject \} +@{boxed_bash [display]\ë\prompt{myproject}ë isabelle build -d . myproject \} -The dictory \<^boxed_bash>\myproject\ contains the following files and directories: +The directory \<^boxed_bash>\myproject\ contains the following files and directories: \begin{center} \begin{minipage}{.9\textwidth} \dirtree{% @@ -172,7 +172,7 @@ The dictory \<^boxed_bash>\myproject\ contains the following files .2 myproject. .3 document. .4 build\DTcomment{Build Script}. -.4 isadof.cfg\DTcomment{\<^isadof> configuraiton}. +.4 isadof.cfg\DTcomment{\<^isadof> configuration}. .4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}. .3 ROOT\DTcomment{Isabelle build-configuration}. } @@ -193,14 +193,14 @@ users are: text\ Creating a new document setup requires two decisions: - \<^item> which ontologies (\<^eg>, scholarly\_paper) are required and + \<^item> which ontologies (\<^eg>, scholarly\_paper) are required, and \<^item> which document template (layout)\index{document template} should be used (\<^eg>, scrartcl\index{scrartcl}). Some templates require that the users manually obtains and adds the necessary \<^LaTeX> class file. This is due to licensing restrictions).\ text\ - This can be configured by using the command-line options of of \<^boxed_bash>\mkroot_DOF\. In - Particular, \<^boxed_bash>\-o\ allows selecting the ontology and \<^boxed_bash>\-t\ allows to selecting + This can be configured by using the command-line options of \<^boxed_bash>\mkroot_DOF\. In + Particular, \<^boxed_bash>\-o\ allows selecting the ontology and \<^boxed_bash>\-t\ allows selecting the document template. The built-in help (using \<^boxed_bash>\-h\) shows all available options as well as a complete list of the available document templates and ontologies: @@ -233,31 +233,31 @@ subsection\Writing Academic Papers\ text\ The ontology \<^boxed_theory_text>\scholarly_paper\ \<^index>\ontology!scholarly\_paper\ is an ontology modeling - academic/scientific papers, with a slight bias to texts in the domain of mathematics and engineering. - We explain first the principles of its underlying ontology, and then we present two ''real'' + academic/scientific papers, with a slight bias towards texts in the domain of mathematics and engineering. + We explain first the principles of its underlying ontology, and then we present two ``real'' examples from our own publication practice. \ text\ \<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text, heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing - between statements, definitions and proofs which is ontologically tracked. However, wrt. + between statements, definitions and proofs which are ontologically tracked. However, wrt. the possible linking between the underlying formal theory and this mathematical presentation, it follows a pragmatic path without any ``deep'' linking to types, terms and theorems, deliberately not exploiting \<^isadof> 's full potential with this regard. \<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately - refrain from integrating references to formal content in order demonstrate that \<^isadof> is not + refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not a framework from Isabelle users to Isabelle users only, but people just avoiding as much as possible \<^LaTeX> notation. The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\scholarly_paper\ in the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/} or - \nolinkurl{examples/scholarly_paper/2020-ifm-csp-applications/}. + \nolinkurl{examples/scholarly_paper/2020-iFM-CSP}. You can inspect/edit the example in Isabelle's IDE, by either - \<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the + \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the Isabelle-Icon provided by the Isabelle installation) and loading the file - \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}. - \<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling: + \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}, + \<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling: @{boxed_bash [display]\ë\prompt{\isadofdirn}ë isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \} @@ -270,7 +270,7 @@ text\ You can build the PDF-document at the command line by calling: subsection*[sss::technical]\A Bluffers Guide to the \<^verbatim>\scholarly_paper\ Ontology\ text\ In this section we give a minimal overview of the ontology formalized in - @{theory \Isabelle_DOF.scholarly_paper\}.\ + \<^theory>\Isabelle_DOF.scholarly_paper\.\ text\ We start by modeling the usual text-elements of an academic paper: the title and author information, abstract, and text section: @@ -292,18 +292,18 @@ doc_class abstract = principal_theorems :: "thm list"\} \ -text\Note \short_title\ and \abbrev\ are optional and have the default \None\ (no value). -Note further, that abstracts may have a \principal_theorems\ list, where the built-in \<^isadof> type -\thm list\ which contain references to formally proven theorems that must exist in the logical -context of this document; this is a decisive feature of \<^isadof> that conventional ontological -languages lack.\ - -text\We continue by the introduction of a main class: the text-element \text_section\ (in contrast -to \figure\ or \table\ or similar). Note that -the \main_author\ is typed with the class \author\, a HOL type that is automatically derived from -the document class definition \author\ shown above. It is used to express which author currently -``owns'' this \text_section\, an information that can give rise to presentational or even -access-control features in a suitably adapted front-end. +text\Note \<^const>\short_title\ and \<^const>\abbrev\ are optional and have the default\<^const>\None\ +(no value). Note further, that \<^typ>\abstract\s may have a \<^const>\principal_theorems\ list, where +the built-in \<^isadof> type \<^typ>\thm list\ contains references to formally proven theorems that must +exist in the logical context of this document; this is a decisive feature of \<^isadof> that +conventional ontological languages lack.\ +find_consts name:"level" +text\We continue by the introduction of a main class: the text-element \<^typ>\text_section\ +(in contrast to \<^typ>\figure\ or \table\ or similar). Note that +the \<^const>\main_author\ is typed with the class \<^typ>\author\, a HOL type that is automatically +derived from the document class definition \<^typ>\author\ shown above. It is used to express which +author currently ``owns'' this \<^typ>\text_section\, an information that can give rise to +presentational or even access-control features in a suitably adapted front-end. @{boxed_theory_text [display] \ doc_class text_section = text_element + @@ -312,16 +312,16 @@ doc_class text_section = text_element + level :: "int option" <= "None" \} -The \level\-attibute \<^index>\level\ enables doc-notation support for headers, chapters, sections, and -subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at. -The values are interpreted accordingly to the \<^LaTeX> standard. The correspondance between the levels +The \<^const>\Isa_COL.text_element.level\-attibute \<^index>\level\ enables doc-notation support for +headers, chapters, sections, and subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at. +The values are interpreted accordingly to the \<^LaTeX> standard. The correspondence between the levels and the structural entities is summarized as follows: - \<^item> part \<^index>\part\ \<^bigskip>\<^bigskip> \Some -1\ \vspace{-1cm} - \<^item> chapter \<^index>\chapter\ \<^bigskip>\<^bigskip> \Some 0\ \vspace{-1cm} - \<^item> section \<^index>\section\ \<^bigskip>\<^bigskip> \Some 1\ \vspace{-1cm} - \<^item> subsection \<^index>\subsection\ \<^bigskip>\<^bigskip> \Some 2\ \vspace{-1cm} - \<^item> subsubsection \<^index>\subsubsection\ \<^bigskip>\<^bigskip> \Some 3\ \vspace{-0.1cm} + \<^item> part \<^index>\part\ \Some -1\ \vspace{-0.3cm} + \<^item> chapter \<^index>\chapter\ \Some 0\ \vspace{-0.3cm} + \<^item> section \<^index>\section\ \Some 1\ \vspace{-0.3cm} + \<^item> subsection \<^index>\subsection\ \Some 2\ \vspace{-0.3cm} + \<^item> subsubsection \<^index>\subsubsection\ \Some 3\ \vspace{-0.1cm} Additional means assure that the following invariant is maintained in a document conforming to \<^verbatim>\scholarly_paper\: @@ -329,11 +329,11 @@ conforming to \<^verbatim>\scholarly_paper\: \center {\level > 0\} \ -text\ The rest of the ontology introduces concepts for \introductions\, \conclusion\, \related_work\, -\bibliography\ etc. More details can be found in \<^verbatim>\scholarly_paper\ contained ion the -theory @{theory \Isabelle_DOF.scholarly_paper\}. \ +text\ The rest of the ontology introduces concepts for \<^typ>\introduction\, \<^typ>\conclusion\, +\<^typ>\related_work\, \<^typ>\bibliography\ etc. More details can be found in \<^verbatim>\scholarly_paper\ +contained ion the theory \<^theory>\Isabelle_DOF.scholarly_paper\. \ -subsection\Writing Academic Publications I : A Freeform Mathematics Text \ +subsection\Writing Academic Publications: A Freeform Mathematics Text \ text*[csp_paper_synthesis::technical, main_author = "Some bu"]\We present a typical mathematical paper focussing on its form, not refering in any sense to its content which is out of scope here. As mentioned before, we chose the paper~@{cite "taha.ea:philosophers:2020"} for this purpose, @@ -345,9 +345,9 @@ figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/head \ A mathematics paper as integrated document source ... \ figure*[fig0B::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_pdf.png''"] - \ \ldots and as corresponding \<^pdf>-output. \ + \ ... and as corresponding \<^pdf>-output. \ -text\The integrated source of this paper-except is shown in \<^figure>\fig0\, while the +text\The integrated source of this paper-excerpt is shown in \<^figure>\fig0\, while the document build process converts this to the corresponding \<^pdf>-output shown in \<^figure>\fig0B\.\ @@ -358,16 +358,16 @@ The other text-elements provide the authors and the abstract as specified by the to the \<^theory_text>\doc_class\es of \<^verbatim>\scholarly_paper\; we say that these text elements are \<^emph>\instances\ \<^bindex>\instance\ of the \<^theory_text>\doc_class\es \<^bindex>\doc\_class\ of the underlying ontology. \ -text\\vspace{1,5cm} The paper proceeds by providing instances for introduction, technical sections, +text\The paper proceeds by providing instances for introduction, technical sections, examples, \<^etc>. We would like to concentrate on one --- mathematical paper oriented --- detail in the ontology \<^verbatim>\scholarly_paper\: @{boxed_theory_text [display] -\doc_class technical = text_section + . . . +\doc_class technical = text_section + ... type_synonym tc = technical (* technical content *) -datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ... +datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ... doc_class math_content = tc + ... @@ -380,25 +380,25 @@ doc_class "theorem" = math_content + text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical -"technical content" in mathematical or engineering papers: code, definitions, theorems, +``technical content" in mathematical or engineering papers: code, definitions, theorems, lemmas, examples. From this class, the more stricter class of @{typ \math_content\} is derived, which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these class definitions are omitted here). Note, however, that class identifiers can be abbreviated by standard \<^theory_text>\type_synonym\s for convenience and enumeration types can be defined by the standard inductive \<^theory_text>\datatype\ definition mechanism in Isabelle, since any HOL type is admitted -for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type +for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type definition. \ figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"] \ A screenshot of the integrated source with definitions ...\ -text\An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as -\"definition"\s in terms of the \<^verbatim>\scholarly_paper\-ontology and their type-conform referencing +text\An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as +\<^typ>\definition\s in terms of the \<^verbatim>\scholarly_paper\-ontology and their type-conform referencing later is shown in \<^figure>\fig01\ in its presentation as the integrated source. Note that the use in the ontology-generated antiquotation \<^theory_text>\@{definition X4}\ is type-checked; referencing \<^verbatim>\X4\ as \<^theory_text>\theorem\ would be a type-error and be reported directly by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing -hierarchy makes \<^verbatim>\X4\ \<^emph>\navigable\ in Isabelle/jedit; a click will cause the IDE to present the +hierarchy makes \<^verbatim>\X4\ \<^emph>\navigable\ in Isabelle/jEdit; a click will cause the IDE to present the defining occurrence of this text-element in the integrated source. % TODO: @@ -407,14 +407,13 @@ defining occurrence of this text-element in the integrated source. Note, further, how \<^isadof>-commands like \<^theory_text>\text*\ interact with standard Isabelle document antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail. -We refrain ourselves here to briefly describe three freeform antiquotations used her in this text: +We refrain ourselves here to briefly describe three freeform antiquotations used in this text: \<^item> the freeform term antiquotation, also called \<^emph>\cartouche\, written by - \@{cartouche [style-parms] \. . .\\ or just by \\...\\ if the list of style parameters + \@{cartouche [style-parms] \...\}\ or just by \\...\\ if the list of style parameters is empty, -\<^item> the freeform antiquotation for theory fragments written \@{theory_text [style-parms] \...\\ - or just \<^verbatim>\\<^theory_text> \...\\ if the list of style parameters - is empty, +\<^item> the freeform antiquotation for theory fragments written \@{theory_text [style-parms] \...\}\ + or just \<^verbatim>\\<^theory_text>\\\...\\ if the list of style parameters is empty, \<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements. \ @@ -423,9 +422,10 @@ figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/def text\ \<^isadof> text-elements such as \<^theory_text>\text*\ allow to have such standard term-antiquotations inside their -text, permitting to give the whole text entity a formal, referentiable status with typed meta- -information attached to it that may be used for presentation issues, search, or other technical -purposes. The corresponding output of this snippet in the integrated source is shown in \<^figure>\fig02\. +text, permitting to give the whole text entity a formal, referentiable status with typed +meta-information attached to it that may be used for presentation issues, search, +or other technical purposes. +The corresponding output of this snippet in the integrated source is shown in \<^figure>\fig02\. \ @@ -443,10 +443,10 @@ doc_class figure = text_section + \} \ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"] - \ Declaring figures in the integrated source \ldots \ + \ Declaring figures in the integrated source.\ text\ - The document class \<^boxed_theory_text>\figure\ (supported by the \<^isadof> command abbreviation + The document class \<^typ>\figure\ (supported by the \<^isadof> command abbreviation \<^boxed_theory_text>\figure*\) makes it possible to express the pictures and diagrams as shown in \<^figure>\fig_figures\, which presents its own representation in the integrated source as screenshot.\ @@ -459,14 +459,11 @@ text\ doc_class article = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" - where "(title ~~ \subtitle\ ~~ \author\$^+$+ ~~ abstract ~~ - introduction ~~ \technical || example\$^+$ ~~ conclusion ~~ - bibliography)" + accepts "(title ~~ \subtitle\ ~~ \author\\<^sup>+ ~~ abstract ~~ \introduction\\<^sup>+ + ~~ \background\\<^sup>* ~~ \technical || example \\<^sup>+ ~~ \conclusion\\<^sup>+ + ~~ bibliography ~~ \annex\\<^sup>* )" \}\ - (* % TODO: - % Update to the new implementation. - % where is deprecated and the new implementation uses accepts and rejects. *) text\ In a integrated document source, the body of the content can be paranthesized into: @@ -478,7 +475,7 @@ text\ which signals to \<^isadof> begin and end of the part of the integrated source in which the text-elements instances are expected to appear in the textual ordering -defined by \<^theory_text>\article\. +defined by \<^typ>\article\. \ @@ -493,10 +490,10 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV- caption="''Hyperlink to class-definition.''",relative_width="48", src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''", caption2="''Exploring an attribute.''",relative_width2="47", - src2="''figures/Dogfood-III-bgnd-text_section''"]\Navigation via generated hyperlinks.\ + src2="''figures/Dogfood-V-attribute''"]\Navigation via generated hyperlinks.\ text\ From these class definitions, \<^isadof> also automatically generated editing - support for Isabelle/jedit. In \autoref{fig-Dogfood-II-bgnd1} and + support for Isabelle/jEdit. In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how hovering over links permits to explore its meta-information. Clicking on a document class identifier permits to hyperlink into the corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an @@ -509,7 +506,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood- text\ An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the -ontology-dependant antiquotation \<^boxed_theory_text>\@ {example ...}\ refers to the corresponding +ontology-dependant antiquotation \<^boxed_theory_text>\@{example ...}\ refers to the corresponding text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the link does not exist or has a non-compatible type, the text is not validated,\<^ie>, Isabelle/jEdit will respond with an error.\ @@ -522,10 +519,10 @@ text\ The \<^isadof> distribution contains a small example using the ontology ``CENELEC\_50128'' in the directory \nolinkurl{examples/CENELEC_50128/mini_odo/}. You can inspect/edit the integrated source example by either - \<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the + \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the Isabelle-Icon provided by the Isabelle installation) and loading the file \nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}. - \<^item> starting Isabelle/jedit from the command line by calling: + \<^item> starting Isabelle/jEdit from the command line by calling: @{boxed_bash [display]\ë\prompt{\isadofdirn}ë isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy \} @@ -738,7 +735,7 @@ of ontologies and document templates (see @{docitem (unchecked) \isadof_on Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can -ensure that a document that does not generate any error messages in Isabelle/jedit also generated +ensure that a document that does not generate any error messages in Isabelle/jEdit also generated a PDF document. Second, future version of \<^isadof> might support different targets for the document generation (\<^eg>, HTML) which, naturally, are only available to documents not using too complex native \<^LaTeX>-commands. From b7d701542335520ea16bf57a39ab80b51ec14bd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 17 Mar 2022 17:28:40 +0100 Subject: [PATCH 4/6] Cleanup Manual chapter 03 --- examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 50b7395c..2915610f 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -297,7 +297,7 @@ text\Note \<^const>\short_title\ and \<^const>\abbrev\< the built-in \<^isadof> type \<^typ>\thm list\ contains references to formally proven theorems that must exist in the logical context of this document; this is a decisive feature of \<^isadof> that conventional ontological languages lack.\ -find_consts name:"level" + text\We continue by the introduction of a main class: the text-element \<^typ>\text_section\ (in contrast to \<^typ>\figure\ or \table\ or similar). Note that the \<^const>\main_author\ is typed with the class \<^typ>\author\, a HOL type that is automatically From 6c74a2e0f5245db5e0e871a39db5c2b791e208e5 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 17 Mar 2022 22:28:31 +0000 Subject: [PATCH 5/6] Basic Woodpecker setup (migration from Jenkins). --- {.ci => .woodpecker}/Jenkinsfile | 0 .woodpecker/build.yml | 7 +++++++ {.ci => .woodpecker}/isabelle4isadof/Dockerfile | 0 {.ci => .woodpecker}/mk_release | 2 +- 4 files changed, 8 insertions(+), 1 deletion(-) rename {.ci => .woodpecker}/Jenkinsfile (100%) create mode 100644 .woodpecker/build.yml rename {.ci => .woodpecker}/isabelle4isadof/Dockerfile (100%) rename {.ci => .woodpecker}/mk_release (98%) diff --git a/.ci/Jenkinsfile b/.woodpecker/Jenkinsfile similarity index 100% rename from .ci/Jenkinsfile rename to .woodpecker/Jenkinsfile diff --git a/.woodpecker/build.yml b/.woodpecker/build.yml new file mode 100644 index 00000000..57131b09 --- /dev/null +++ b/.woodpecker/build.yml @@ -0,0 +1,7 @@ +pipeline: + generate_nn: + image: docker.io/logicalhacking/isabelle2021 + commands: + - ./install + - isabelle build -D . + diff --git a/.ci/isabelle4isadof/Dockerfile b/.woodpecker/isabelle4isadof/Dockerfile similarity index 100% rename from .ci/isabelle4isadof/Dockerfile rename to .woodpecker/isabelle4isadof/Dockerfile diff --git a/.ci/mk_release b/.woodpecker/mk_release similarity index 98% rename from .ci/mk_release rename to .woodpecker/mk_release index 4cc93469..63157fe1 100755 --- a/.ci/mk_release +++ b/.woodpecker/mk_release @@ -107,7 +107,7 @@ build_and_install_manuals() echo " 2018-cicm-isabelle_dof-applications Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true - rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.ci $ISADOF_WORK_DIR/.afp + rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp if [ -f $ROOTS.backup ]; then mv $ROOTS.backup $ROOTS fi From 2886f7df99ca0f4bf9e5a7f4734b35c86e351b29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 18 Mar 2022 17:00:06 +0100 Subject: [PATCH 6/6] Update CENELEC_50128 theory An application condition should be an assumption --- src/ontologies/CENELEC_50128/CENELEC_50128.thy | 10 ++++++---- src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty | 2 ++ 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 02fe9fdf..a90d3f36 100755 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -373,10 +373,6 @@ doc_class FnI = requirement + is_concerned :: "role set" <= "UNIV" type_synonym functions_and_interfaces = FnI -doc_class AC = requirement + - is_concerned :: "role set" <= "UNIV" - -type_synonym application_conditions = AC text\The category \<^emph>\assumption\ is used for domain-specific assumptions. It has formal, semi-formal and informal sub-categories. They have to be tracked and discharged by appropriate @@ -387,6 +383,12 @@ datatype ass_kind = informal | semiformal | formal doc_class assumption = requirement + assumption_kind :: ass_kind <= informal +doc_class AC = assumption + + is_concerned :: "role set" <= "UNIV" + +type_synonym application_conditions = AC + + text\ The category \<^emph>\exported constraint\ (or \<^emph>\EC\ for short) is used for formal application conditions; They represent in particular \<^emph>\derived constraints\, i.e. constraints that arrive as side-conditions during refinement proofs or implementation decisions and must be tracked.\ diff --git a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty index 5fc62f1f..2c55fd0c 100755 --- a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty +++ b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty @@ -71,6 +71,7 @@ ,CENELEC_50128.SRAC.formal_repr=% ,CENELEC_50128.SRAC.assumption_kind=% ,CENELEC_50128.EC.assumption_kind=% +,CENELEC_50128.assumption.assumption_kind=% ][1]{% \begin{isamarkuptext}% \ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{% @@ -123,6 +124,7 @@ ,CENELEC_50128.SRAC.formal_repr=% ,CENELEC_50128.SRAC.assumption_kind=% ,CENELEC_50128.EC.assumption_kind=% +,CENELEC_50128.assumption.assumption_kind=% ][1]{% \begin{isamarkuptext}% \ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%