diff --git a/examples/cenelec/mini_odo/ROOT b/examples/cenelec/mini_odo/ROOT new file mode 100644 index 0000000..00c8f67 --- /dev/null +++ b/examples/cenelec/mini_odo/ROOT @@ -0,0 +1,11 @@ +session "mini_odo" = "Isabelle_DOF" + + options [document = pdf, document_output = "output"] + theories [document = false] + (* Foo *) + (* Bar *) + theories + "mini_odo" + document_files + "isadof.cfg" + "preamble.tex" + "build" diff --git a/examples/cenelec/mini_odo/document/build b/examples/cenelec/mini_odo/document/build new file mode 100755 index 0000000..c4a05ab --- /dev/null +++ b/examples/cenelec/mini_odo/document/build @@ -0,0 +1,46 @@ +#!/usr/bin/env bash +# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved. +# 2018 The University of Paris-Sud. All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in +# the documentation and/or other materials provided with the +# distribution. +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +# POSSIBILITY OF SUCH DAMAGE. +# +# SPDX-License-Identifier: BSD-2-Clause + +set -e +if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then + echo "" + echo "Error: Isabelle/DOF not installed" + echo "=====" + echo "This is a Isabelle/DOF project. The document preparation requires" + echo "the Isabelle/DOF framework. Please obtain the framework by cloning" + echo "the Isabelle/DOF git repository, i.e.: " + echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" + echo "You can install the framework as follows:" + echo " cd Isabelle_DOF/document-generator" + echo " ./install" + echo "" + exit 1 +fi + +cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh . +source build_lib.sh diff --git a/examples/cenelec/mini_odo/document/isadof.cfg b/examples/cenelec/mini_odo/document/isadof.cfg new file mode 100644 index 0000000..7ee5f29 --- /dev/null +++ b/examples/cenelec/mini_odo/document/isadof.cfg @@ -0,0 +1,3 @@ +Template: scrartcl +Ontology: scholarly_paper +Ontology: cenelec_50128 diff --git a/examples/cenelec/mini_odo/document/preamble.tex b/examples/cenelec/mini_odo/document/preamble.tex new file mode 100644 index 0000000..6c4b5fd --- /dev/null +++ b/examples/cenelec/mini_odo/document/preamble.tex @@ -0,0 +1,3 @@ +%% This is a placeholder for user-specific configuration and packages. +\title{mini-odo}{}{}{}{}{}{} +\author{By brucker}{}{}{}{}{} diff --git a/examples/cenelec/mini_odo/mini_odo.thy b/examples/cenelec/mini_odo/mini_odo.thy new file mode 100644 index 0000000..d2a6759 --- /dev/null +++ b/examples/cenelec/mini_odo/mini_odo.thy @@ -0,0 +1,90 @@ + +theory mini_odo + imports "Isabelle_DOF.CENELEC_50128" + "Isabelle_DOF.scholarly_paper" +begin + +section\ Some examples of Isabelle's standard antiquotations. \ +(* some show-off of standard anti-quotations: *) +text \THIS IS A TEXT\ + +text\ @{thm refl} of name @{thm [source] refl} + @{thm[mode=Rule] conjI} + @{file "mini_odo.thy"} + @{value "3+4::int"} + @{const hd} + @{theory List} + @{term "3"} + @{type bool} + @{term [show_types] "f x = a + x"} \ + + + + +section\ Core Examples for stating text-elements as doc-items.\ + +text\An "anonymous" text-item, automatically coerced into the top-class "text".\ +text*[tralala] \ Brexit means Brexit \ + +text\Examples for declaration of typed doc-items "assumption" and "hypothesis", + concepts defined in the underlying ontology @{theory "CENELEC_50128"}. \ +text*[ass1::assumption] \ The subsystem Y is safe. \ +text*[hyp1::hypothesis] \ P not equal NP \ + +text\A real example fragment from a larger project, declaring a text-element as a + "safety-related application condition", a concept defined in the @{theory "CENELEC_50128"} + ontology:\ + +text*[new_ass::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ + +text*[ass122::srac] \ The overall sampling frequence of the odometer +subsystem is therefore 14 khz, which includes sampling, computing and +result communication times... \ + +text*[t10::test_result] \ This is a meta-test. This could be an ML-command +that governs the external test-execution via, eg., a makefile or specific calls +to a test-environment or test-engine \ + + +section\ References to doc-items.\ +text\Finally some examples of references to doc-items, i.e. text-elements with declared + meta-information and status. \ +text \ As established by @{docref (unchecked) \t10\}, + @{docref (define) \t10\} \ +text \ the @{docref \t10\} + as well as the @{docref \ass122\}\ +text \ represent a justification of the safety related applicability + condition @{srac \ass122\} aka exported constraint @{ec \ass122\}.\ + + + + +section\ Some Tests for Ontology Framework and its CENELEC Instance \ + +declare_reference* [lalala::requirement, alpha="main", beta=42] +declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] + + + + + +section*[h::example]\ Some global inspection commands for the status of docitem and doc-class tables ... \ + + + +section*[i::example]\ Text Antiquotation Infrastructure ... \ + +text\ @{docitem \lalala\} -- produces warning. \ +text\ @{docitem (unchecked) \lalala\} -- produces no warning. \ + +text\ @{docitem \ass122\} -- global reference to a text-item in another file. \ + +text\ @{ec \ass122\} -- global reference to a exported constraint in another file. + Note that the link is actually a srac, which, according to + the ontology, happens to be an "ec". \ + + + +end + +