Added: simple test setup.

This commit is contained in:
Achim D. Brucker 2018-03-06 09:44:07 +00:00
parent e72addeca8
commit b1d39bd9ec
5 changed files with 176 additions and 0 deletions

1
.gitignore vendored
View File

@ -1 +1,2 @@
document-generator/converter/bin/*.jar
output

View File

@ -0,0 +1,63 @@
theory DOF_example
imports "../../CENELEC_50126"
begin
section{* Some show-off's of general antiquotations. *}
(* some show-off of standard anti-quotations: *)
text{* @{thm refl}
@{file "../../Isa_DOF.thy"}
@{value "3+4::int"}
@{const hd}
@{theory List}
@{term "3"}
@{type bool}
@{term [show_types] "f x = a + x"} *}
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
declare_reference [lalala::requirement, alpha="main", beta=42]
(*
declare_reference [lalala::quod] (* shouldn't work *)
*)
declare_reference [blablabla::cid, alpha=beta, beta=gamma]
paragraph*[sdf]{* just a paragraph *}
(*
subsection*[sdf]{* shouldn't work, multiple ref. *}
*)
section*[sedf::requirement]{* works again. One can hover over the class constraint and
jump to its definition. *}
text\<open>\label{sedf}\<close> (* Hack to make the LaTeX-ing running. Should disappear. *)
section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting,
but wrong doc_class constraint. *}
section{* Text Antiquotation Infrastructure ... *}
text{* @{docref \<open>lalala\<close>} -- produces warning. *}
text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
text{* @{ec \<open>ass122\<close>} -- 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". *}
(*
text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". *}
*)
text{* Here is a reference to @{docref \<open>sedf\<close>} *}
(* works currently only in connection with the above label-hack.
Try to hover over the sedf - link and activate it !!! *)
end

View File

@ -0,0 +1,10 @@
session "DOF_example" = "HOL" +
options [document = pdf, document_output = "output"]
theories [document = false]
(* Foo *)
(* Bar *)
theories
DOF_example
document_files
"root.tex"
"build"

View File

@ -0,0 +1,47 @@
#!/usr/bin/env bash
# Copyright (c) 2018 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
OUTFORMAT=${1:-pdf}
NAME=${2:-root}
set -e
ROOT_NAME="root_$NAME"
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar .
cp $ISABELLE_HOME_USER/DOF/latex/DOF.sty .
$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex"

View File

@ -0,0 +1,55 @@
\RequirePackage{ifvtex}
\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage{fixltx2e}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}
\usepackage{DOF}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=false
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{DOF-example}
\author{By brucker}
\begin{document}
\maketitle
\tableofcontents
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
\bibliographystyle{abbrvnat}
\bibliography{root}
}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: