diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index e1916f1..ff8b79c 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay + * 2019-2021 The University of Exeter + * 2018-2021 The University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -35,12 +35,10 @@ available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus \href{https://www.docker.com}{Docker} installed and your installation of Docker supports X11 application, you can start \<^isadof> as follows: -@{boxed_bash [display] -\ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \ +@{boxed_bash [display] \ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \ -v /tmp/.X11-unix:/tmp/.X11-unix \ logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \ - isabelle jedit -\} + isabelle jedit\} \ subsection*[installation::technical]\Installation\ @@ -57,41 +55,24 @@ text\ of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle. Thus, the same version of \<^isadof> might be available for different versions of Isabelle. \<^item> \<^bold>\\<^TeXLive> 2020\\<^bindex>\TexLive@\<^TeXLive>\ (or any other modern \<^LaTeX>-distribution where - \<^pdftex> supports the \<^boxed_latex>\\expanded\ primitive). - \<^footnote>\see \<^url>\https://www.texdev.net/2018/12/06/a-new-primitive-expanded\\ + \<^pdftex> supports the \<^boxed_latex>\\expanded\ + primitive).\<^footnote>\see \<^url>\https://www.texdev.net/2018/12/06/a-new-primitive-expanded\\ \ paragraph\Installing Isabelle\ text\ -%\enlargethispage{\baselineskip} - Please download and install the Isabelle \isabelleversion distribution for your operating system - from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the successful - installation of Isabelle, you should be able to call the \<^boxed_bash>\isabelle\ tool on the - command line: - -\begin{bash} -ë\prompt{}ë isabelle version -ë\isabellefullversionë -\end{bash} -% bu : do not know why this does not work here ... -%@ {boxed_bash [display]\ -%ë\prompt{}ë isabelle version -%ë\isabellefullversionë -%\} + Please download and install the Isabelle (version: \isabelleversion) distribution for your + operating system from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the + successful installation of Isabelle, you should be able to call the \<^boxed_bash>\isabelle\ + tool on the command line: +@{boxed_bash [display]\ë\prompt{}ë isabelle version +ë\isabellefullversionë\} Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\bin\ directory in your \<^boxed_bash>\PATH\, you will need to invoke \<^boxed_bash>\isabelle\ using its full qualified path, \<^eg>: - -\begin{bash} -ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version -ë\isabellefullversionë -\end{bash} - -%@ {boxed_bash [display]\ -%ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version -%ë\isabellefullversionë -%\} +@{boxed_bash [display]\ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version +ë\isabellefullversionë\} \ paragraph\Installing \<^TeXLive>\ @@ -99,13 +80,7 @@ text\ Modern Linux distribution will allow you to install \<^TeXLive> using their respective package managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command should install all required \<^LaTeX> packages: - -\begin{bash} -ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra -\end{bash} -%@ {boxed_bash [display]\ -%ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra -%\} +@{boxed_bash [display]\ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra\} \ subsubsection*[isadof::technical]\Installing \<^isadof>\ @@ -114,10 +89,7 @@ text\ (\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for installing are extracting the \<^isadof> distribution and calling its \inlinebash|install| script. We start by extracting the \<^isadof> archive: - -\begin{bash} -ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë -\end{bash} +@{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 automatically downloads additional dependencies from the AFP (\<^url>\https://www.isa-afp.org\), @@ -132,8 +104,7 @@ If the \<^boxed_bash>\isabelle\ tool is not in your \<^boxed_bash> path of the \<^boxed_bash>\isabelle\ tool ( \<^boxed_bash>\install --help\ gives you an overview of all available configuration options): -\begin{bash} -ë\prompt{}ë cd ë\isadofdirnë +@{boxed_bash [display]\ë\prompt{}ë cd ë\isadofdirnë ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë Isabelle/DOF Installer @@ -170,17 +141,14 @@ Isabelle/DOF Installer /home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë * Installation successful. Enjoy Isabelle/DOF, you can build the session Isabelle/DOF and all example documents by executing: - /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . -\end{bash} + /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \} After the successful installation, you can now explore the examples (in the sub-directory \inlinebash|examples| or create your own project. On the first start, the session \inlinebash|Isabelle_DOF| will be built automatically. If you want to pre-build this session and all example documents, execute: -\begin{bash} -ë\prompt{\isadofdirn}ë isabelle build -D . -\end{bash} +@{boxed_bash [display]\ë\prompt{\isadofdirn}ë isabelle build -D . \} \ subsection*[first_project::technical]\Creating an \<^isadof> Project\ @@ -188,8 +156,7 @@ text\ \<^isadof> provides its own variant of Isabelle's \inlinebash|mkroot| tool, called \inlinebash|mkroot_DOF|:\index{mkroot\_DOF} -\begin{bash} -ë\prompt{}ë isabelle mkroot_DOF -h +@{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF -h Usage: isabelle mkroot_DOF [OPTIONS] [DIR] @@ -209,8 +176,7 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR] * scrreprt-modern * scrreprt - Prepare session root DIR (default: current directory). -\end{bash} + Prepare session root DIR (default: current directory). \} Creating a new document setup requires two decisions: \<^item> which ontologies (\<^eg>, scholarly\_paper) are required and @@ -225,24 +191,20 @@ text\ the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}, you can create your first project \inlinebash|myproject| as follows: -\begin{bash} -ë\prompt{}ë isabelle mkroot_DOF myproject +@{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF myproject Preparing session "myproject" iëën "myproject" creating "myproject/ROOT" creating "myproject/document/root.tex" Now use the following coëëmmand line to build the session: - isabelle build -D myproject -\end{bash} + isabelle build -D myproject \} This creates a directory \inlinebash|myproject| containing 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 -\begin{bash} -ë\prompt{}ë isabelle build -d . myproject -\end{bash} +@{boxed_bash [display]\ë\prompt{}ë isabelle build -d . myproject \} This will create the directory \inlinebash|myproject|: \begin{center} @@ -302,17 +264,13 @@ text\ \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}. \<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling: - \begin{bash} -ë\prompt{\isadofdirn}ë - isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy -\end{bash} +@{boxed_bash [display]\ë\prompt{\isadofdirn}ë + isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \} \ (* We should discuss if we shouldn't put the iFM paper more in the foreground *) text\ You can build the PDF-document at the command line by calling: - -@{boxed_bash [display] -\ë\prompt{}ë isabelle build -d . 2020-iFM-csp \} +@{boxed_bash [display] \ë\prompt{}ë isabelle build -d . 2020-iFM-csp \} \ subsection*[sss::technical]\A Bluffers Guide to the \<^verbatim>\scholarly_paper\ Ontology\ @@ -631,16 +589,12 @@ text\ \nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}. \<^item> starting Isabelle/jedit from the command line by calling: - \begin{bash} -ë\prompt{\isadofdirn}ë - isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy -\end{bash} +@{boxed_bash [display]\ë\prompt{\isadofdirn}ë + isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy \} \ text\\<^noindent> Finally, you \<^item> can build the PDF-document by calling: - \begin{bash} -ë\prompt{}ë isabelle build mini_odo -\end{bash} +@{boxed_bash [display]\ë\prompt{}ë isabelle build mini_odo \} \ subsection\Modeling CENELEC 50128\ @@ -776,18 +730,12 @@ text\ Isabelle-Icon provided by the Isabelle installation) and loading the file \nolinkurl{examples/math_exam/MathExam/MathExam.thy}. \<^item> starting Isabelle/jedit from the command line by calling: - - \begin{bash} -ë\prompt{\isadofdirn}ë - isabelle jedit examples/math_exam/MathExam/MathExam.thy -\end{bash} +@{boxed_bash [display]\ë\prompt{\isadofdirn}ë + isabelle jedit examples/math_exam/MathExam/MathExam.thy \} \ text\ You can build the PDF-document by calling: - - \begin{bash} -ë\prompt{}ë isabelle build MathExam -\end{bash} +@{boxed_bash [display]\ë\prompt{}ë isabelle build MathExam\} \ subsection\Modeling Exams\