diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 9564b19..065fa63 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -45,24 +45,18 @@ subsection*[installation::technical]\Installation\ text\ In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and \<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell). + + \<^isadof> requires Isabelle\<^bindex>\Isabelle\ (\isabellefullversion) with a recent \<^LaTeX>-distribution + (e.g., TexLive 2020 or later). + \<^isadof> uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version + 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. \ -subsubsection*[prerequisites::technical]\Pre-requisites\ +paragraph\Installing Isabelle.\ text\ - \<^isadof> has to major pre-requisites: - \<^item> \<^bold>\Isabelle\\<^bindex>\Isabelle\ (\isabellefullversion). - \<^isadof> uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version - 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\\ -\ - -paragraph\Installing Isabelle\ -text\ - Please download and install the Isabelle (version: \isabelleversion) distribution for your - operating system from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the + Please download and install Isabelle (version: \isabelleversion) 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 @@ -75,7 +69,7 @@ full qualified path, \<^eg>: ë\isabellefullversionë\} \ -paragraph\Installing \<^TeXLive>\ +paragraph\Installing \<^TeXLive>.\ 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 @@ -118,9 +112,11 @@ Isabelle/DOF Installer Trying to patch system .... Applied patch successfully, Isabelle/HOL will be rebuilt during the next start of Isabelle. -* Checking availability of AFP entries: - Warning: could not find AFP entry Regular-Sets. - Warning: could not find AFP entry Functional-Automata. +* Checking availability of AFP entries:\} + +@{boxed_bash [display] +\ëë Warning: could not find AFP entry Regular-Sets. + Warning: could not find AFP entry Functional-Automata. Trying to install AFP (this might take a few *minutes*) .... Registering Regular-Sets iëën /home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë @@ -143,54 +139,17 @@ Isabelle/DOF Installer Isabelle/DOF and all example documents by executing: /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \} -After the successful installation, you can now explore the examples (in the sub-directory +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>\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 . \} \ subsection*[first_project::technical]\Creating an \<^isadof> Project\ text\ \<^isadof> provides its own variant of Isabelle's - \<^boxed_bash>\mkroot\ tool, called \<^boxed_bash>\mkroot_DOF\:\index{mkroot\_DOF} - -@{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF -h - -Usage: isabelle mkroot_DOF [OPTIONS] [DIR] - - Options are: - -h print this hëëelp text and exëëit - -n NAME alternative session name (default: DIR base name) - -o ONTOLOGY (default: scholarly_paper) - Available ontologies: - * CENELEC_50128 - * math_exam - * scholarly_paper - * technical_report - -t TEMPLATE (default: scrartcl) - Available document templates: - * lncs - * scrartcl - * scrreprt-modern - * scrreprt - - Prepare session root DIR (default: current directory). \} - - 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\. - This is due to licensing restrictions). -\ -text\ - If you are happy with the defaults, \ie, using 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"}, you can create your first project - \<^boxed_bash>\myproject\ as follows: - + \<^boxed_bash>\mkroot\ tool, called \<^boxed_bash>\mkroot_DOF\\index{mkroot\_DOF}: @{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF myproject Preparing session "myproject" iëën "myproject" @@ -199,14 +158,15 @@ Preparing session "myproject" iëën "myproject" Now use the following coëëmmand line to build the session: isabelle build -D myproject \} - - This creates a directory \<^boxed_bash>\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 + 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\ + 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 \} -This will create the directory \<^boxed_bash>\myproject\: +The dictory \<^boxed_bash>\myproject\ contains the following files and directories: \begin{center} \begin{minipage}{.9\textwidth} \dirtree{% @@ -233,6 +193,43 @@ users are: \<^LaTeX>-packages or to add/modify \<^LaTeX>-commands. \ +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\. + 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 + 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: + + @{boxed_bash [display]\ë\prompt{}ë isabelle mkroot_DOF -h + +Usage: isabelle mkroot_DOF [OPTIONS] [DIR] + + Options are: + -h print this hëëelp text and exëëit + -n NAME alternative session name (default: DIR base name) + -o ONTOLOGY (default: scholarly_paper) + Available ontologies: + * CENELEC_50128 + * math_exam + * scholarly_paper + * technical_report + -t TEMPLATE (default: scrartcl) + Available document templates: + * lncs + * scrartcl + * scrreprt-modern + * scrreprt + + Prepare session root DIR (default: current directory). \} + +\ + section*[scholar_onto::example]\Writing Academic Publications in \<^boxed_theory_text>\scholarly_paper\\ subsection\Papers in freeform-style\ text\ @@ -267,7 +264,7 @@ text\ @{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 \}