forked from Isabelle_DOF/Isabelle_DOF
Improved documentation and fixed width-bug of figure* macro.
This commit is contained in:
parent
d0cd28a45c
commit
641bea4a58
|
|
@ -1,6 +1,6 @@
|
|||
%% Copyright (C) 2019 University of Exeter, UK
|
||||
%% 2018 The University of Sheffield, UK
|
||||
%% 2018 The University of Paris-Saclay, France
|
||||
%% Copyright (C) University of Exeter, UK
|
||||
%% The University of Sheffield, UK
|
||||
%% The University of Paris-Saclay, France
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
|
|
@ -39,8 +39,8 @@
|
|||
\pagestyle{headings}
|
||||
|
||||
\uppertitleback{
|
||||
Copyright \copyright{} 2019--2022 University of Exeter, UK\\
|
||||
\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
|
||||
Copyright \copyright{} 2019--2023 University of Exeter, UK\\
|
||||
\phantom{Copyright \copyright{}} 2018--2023 Universit\'e Paris-Saclay, France\\
|
||||
\phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
|
||||
|
||||
\smallskip
|
||||
|
|
@ -74,14 +74,11 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|||
}
|
||||
|
||||
\lowertitleback{%
|
||||
This manual describes \isadof version \isadofversion. The latest official
|
||||
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}).
|
||||
The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest
|
||||
release. The latest development version as well as official releases are available at
|
||||
This manual describes \isadof as available in the Archive of Formal Proofs (AFP). The latest development version as well as releases that can be installed as Isabelle component are available at
|
||||
\url{\dofurl}.
|
||||
|
||||
\paragraph*{Contributors.} We would like to thank the following contributors to \isadof
|
||||
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
|
||||
(in alphabetical order): Idir Ait-Sadoune and Paolo Crisafulli.
|
||||
|
||||
\paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay,
|
||||
France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
|
||||
|
|
|
|||
|
|
@ -337,6 +337,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) =
|
|||
val ht_s= if relative_height = 100 then ""
|
||||
else "height="^Real.toString((Real.fromInt relative_height)
|
||||
/ (Real.fromInt 100)) ^"\\textheight"
|
||||
val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s])
|
||||
val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s])
|
||||
val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
|
||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||
|
|
@ -344,7 +345,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) =
|
|||
in if Input.string_of(caption) = "" then
|
||||
file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|
||||
|> (XML.enclose ("\\includegraphics"^arg_single^"{") "}")
|
||||
else
|
||||
file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|
|
@ -401,12 +402,13 @@ fun float_command (name, pos) descr cid =
|
|||
{is_inline = true}
|
||||
{define = true} oid pos (set_default_class cid_pos) doc_attrs
|
||||
val opts = {markdown = false, body = true}
|
||||
fun parse_and_tex opts (margs, text) ctxt = (fig_content ctxt
|
||||
fun parse_and_tex _ (margs, text) ctxt = (fig_content ctxt
|
||||
(convert_meta_args margs o upd_caption Input.empty,
|
||||
convert_src_from_margs margs))
|
||||
|> (fn X => (Latex.macro0 "centering"
|
||||
@ X
|
||||
@ Latex.macro "caption" (generate_caption ctxt text)))
|
||||
(* TODO: add label *)
|
||||
|> (Latex.environment ("figure") )
|
||||
in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex
|
||||
end
|
||||
|
|
|
|||
|
|
@ -150,12 +150,6 @@ text\<open>
|
|||
\<^url>\<open>https://doi.org/10.1007/978-3-030-34968-4_4\<close>.
|
||||
\end{quote}
|
||||
\<close>
|
||||
subsubsection\<open>Availability\<close>
|
||||
text\<open>
|
||||
The implementation of the framework is available at
|
||||
\url{\<^dofurl>}. The website also provides links to the latest releases. \<^isadof> is licensed
|
||||
under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -51,10 +51,9 @@ foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in
|
|||
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
|
||||
ancestor-list as well as typed, user-defined state for plugins such as \<^isadof>.
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
support for higher specification constructs were built.
|
||||
\<^footnote>\<open>We use the term \<^emph>\<open>plugin\<close> for a collection of HOL-definitions, SML and Scala code in order
|
||||
to distinguish it from the official Isabelle term \<^emph>\<open>component\<close> which implies a particular
|
||||
format and support by the Isabelle build system.\<close>
|
||||
support for higher specification constructs were built.\<^footnote>\<open>We use the term \<^emph>\<open>plugin\<close> for a collection
|
||||
of HOL-definitions, SML and Scala code in order to distinguish it from the official Isabelle
|
||||
term \<^emph>\<open>component\<close> which implies a particular format and support by the Isabelle build system.\<close>
|
||||
\<close>
|
||||
|
||||
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
|
||||
|
|
@ -87,7 +86,7 @@ text\<open>
|
|||
main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files. A theory file\<^bindex>\<open>theory!file\<close>
|
||||
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
||||
consisting of a sequence of document elements called
|
||||
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "docModGenConcr"}(left)). Even
|
||||
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "docModGenConcr"} (left-hand side)). Even
|
||||
the header consists of a sequence of commands used for introductory text elements not depending on
|
||||
any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a
|
||||
\<^boxed_theory_text>\<open>keyword\<close> section, for example:
|
||||
|
|
@ -113,7 +112,7 @@ text\<open>The body of a theory file consists of a sequence of \<^emph>\<open>co
|
|||
by a command keyword such as \<^boxed_theory_text>\<open>requirement\<close> above. Command keywords may mark
|
||||
the the begin of a text that is parsed by a command-specific parser; the end of the
|
||||
command-span is defined by the next keyword. Commands were used to define definitions, lemmas,
|
||||
code and text-elements (see @{float "docModGenConcr"}(right)). \<close>
|
||||
code and text-elements (see @{float "docModGenConcr"} (right-hand side)). \<close>
|
||||
|
||||
text\<open> A simple text-element \<^index>\<open>text-element\<close> may look like this:
|
||||
|
||||
|
|
@ -148,8 +147,8 @@ Its Its general syntactic format reads as follows:
|
|||
|
||||
The sub-context may be different from the surrounding one; therefore, it is possible
|
||||
to switch from a text-context to a term-context, for example. Therefore, antiquotations allow
|
||||
the nesting of cartouches, albeit not all combinations are actually supported.
|
||||
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
|
||||
the nesting of cartouches, albeit not all combinations are actually supported.\<^footnote>\<open>In the
|
||||
literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
|
||||
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
|
||||
Isabelle comes with a number of built-in antiquotations for text- and code-contexts;
|
||||
a detailed overview can be found in @{cite "wenzel:isabelle-isar:2020"}. \<^dof> reuses this general
|
||||
|
|
|
|||
|
|
@ -70,7 +70,7 @@ text\<open>
|
|||
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
|
||||
text\<open>
|
||||
By installing the AFP in the previous steps, you already installed \<^isadof>. In fact, \<^isadof>
|
||||
is currently consisting out of two AFP entries:
|
||||
is currently consisting out of three AFP entries:
|
||||
|
||||
\<^item> \<^verbatim>\<open>Isabelle_DOF\<close>: This entry
|
||||
contains the \<^isadof> system itself, including the \<^isadof> manual.
|
||||
|
|
@ -87,15 +87,6 @@ is currently consisting out of two AFP entries:
|
|||
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, and therefore does deliberately not exploit \<^isadof> 's full potential.
|
||||
\<^item> \<^verbatim>\<open>Isabelle_DOF-Examples-Extra\<close>: This sessen contains a collection of other examples;
|
||||
but is only accessible at the developer git
|
||||
\<^url>\<open>https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/main/Isabelle_DOF-Examples-Extra\<close>.
|
||||
|
||||
|
||||
% The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\<open>scholarly_paper\<close> in
|
||||
% the directory \<^nolinkurl>\<open>examples/scholarly_paper/2018-cicm-isabelle_dof-applications/\<close> or
|
||||
% \<^nolinkurl>\<open>examples/scholarly_paper/2020-iFM-CSP\<close>.
|
||||
|
||||
|
||||
It is recommended to follow the structure these examples.\<close>
|
||||
|
||||
|
|
@ -236,32 +227,21 @@ subsection\<open>Editing Major Examples\<close>
|
|||
text\<open>
|
||||
The ontology \<^verbatim>\<open>scholarly_paper\<close> \<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
|
||||
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, for examples
|
||||
using these ontologies we refer to the example sessions described in \<^technical>\<open>isadof\<close>.
|
||||
engineering.
|
||||
|
||||
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
|
||||
Isabelle-Icon provided by the Isabelle installation) and loading the file
|
||||
\<^nolinkurl>\<open>Isabelle_DOF-Example-I/IsaDofApplications.thy"\<close>
|
||||
\<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling:
|
||||
|
||||
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
|
||||
isabelle jedit -d . Isabelle_DOF-Example-II/paper.thy \<close>}
|
||||
|
||||
% bu assumes a particular organisation of Isabelle_DOF, Isabelle_DOF-Example-I, ... and an according ROOTS here ...
|
||||
\<close>
|
||||
|
||||
|
||||
text\<open> You can build the \<^pdf>-document at the command line by calling:
|
||||
@{boxed_bash [display] \<open>ë\prompt{}ë isabelle build -d . IsaDofApplications \<close>}
|
||||
\<close>
|
||||
text\<open> You can build the \<^pdf>-document at the command line by calling:
|
||||
@{boxed_bash [display] \<open>ë\prompt{}ë isabelle build Isabelle_DOF-Example-I\<close>}
|
||||
\<close>
|
||||
|
||||
subsection*[sss::technical]\<open>A Bluffers Guide to the \<^verbatim>\<open>scholarly_paper\<close> Ontology\<close>
|
||||
text\<open> In this section we give a minimal overview of the ontology formalized in
|
||||
\<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>.\<close>
|
||||
|
||||
text\<open> We start by modeling the usual text-elements of an academic paper: the title and author
|
||||
information, abstract, and text section:
|
||||
text\<open> In this section we give a minimal overview of the ontology formalized in
|
||||
\<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. We start by modeling the usual text-elements of an
|
||||
academic paper: the title and author information, abstract, and text section:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>doc_class title =
|
||||
short_title :: "string option" <= "None"
|
||||
|
|
@ -313,13 +293,9 @@ as follows:
|
|||
\<^item> subsubsection \<^index>\<open>subsubsection\<close> \<open>Some 3\<close> \<^vs>\<open>-0.3cm\<close>
|
||||
|
||||
Additional means assure that the following invariant is maintained in a document
|
||||
conforming to \<^verbatim>\<open>scholarly_paper\<close>:
|
||||
|
||||
\<^center>\<open>\<open>level > 0\<close>\<close>
|
||||
conforming to \<^verbatim>\<open>scholarly_paper\<close>: \<open>level > 0\<close>.
|
||||
\<close>
|
||||
|
||||
text\<open>\<^vs>\<open>1.0cm\<close>\<close>
|
||||
|
||||
text\<open> The rest of the ontology introduces concepts for \<^typ>\<open>introduction\<close>, \<^typ>\<open>conclusion\<close>,
|
||||
\<^typ>\<open>related_work\<close>, \<^typ>\<open>bibliography\<close> etc. More details can be found in \<^verbatim>\<open>scholarly_paper\<close>
|
||||
contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. \<close>
|
||||
|
|
|
|||
|
|
@ -2,8 +2,6 @@
|
|||
|
||||
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
|
||||
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
|
||||
|
||||
|
|
@ -31,13 +29,16 @@ distribution for your operating system from the [Isabelle
|
|||
website](https://isabelle.in.tum.de/). Furthermore, please install the AFP
|
||||
following the instructions given at <https://www.isa-afp.org/help.html>.
|
||||
|
||||
Isabelle/DOF is currently consisting out of two AFP entries:
|
||||
Isabelle/DOF is currently consisting out of three AFP entries:
|
||||
|
||||
* [Isabelle_DOF:](https://www.isa-afp.org/entries/Isabelle_DOF.html) This entry
|
||||
contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.
|
||||
* [Isabelle_DOF-Example-I:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-I.html)
|
||||
This entry contains an example of an academic paper written using the
|
||||
Isabelle/DOF system.
|
||||
* [Isabelle_DOF-Example-II:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-II.html)
|
||||
This entry contains an example of an academic paper written using the
|
||||
Isabelle/DOF system.
|
||||
|
||||
-->
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue