added basic Exercise ontology
This commit is contained in:
Burkhart Wolff
parent
5096d1ecaa
commit
91fd6c1f25
@ -0,0 +1,67 @@
|
||||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2026 The University of Exeter
|
||||
* 2026 The University of Paris-Saclay
|
||||
*
|
||||
* License:
|
||||
* This program can be redistributed and/or modified under the terms
|
||||
* of the 2-clause BSD-style license.
|
||||
*
|
||||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
chapter \<open>An Outline of an Exercise Ontology\<close>
|
||||
|
||||
text\<open> \<close>
|
||||
|
||||
(*<<*)
|
||||
theory Exercise
|
||||
imports
|
||||
"Isabelle_DOF.scholarly_paper"
|
||||
begin
|
||||
|
||||
(*
|
||||
define_ontology "exercise.sty" "Exercise"
|
||||
*)
|
||||
|
||||
text\<open>The Exercise ontology is distantly oriented towards the exercise.sty offerred by the
|
||||
TeXLife distribution. A documentation can be found here
|
||||
\url\<open>https://ctan.tetaneutral.net/macros/latex/contrib/exercise/exercise.pdf\<close>.\<close>
|
||||
|
||||
doc_class "exercise" = text_section + \<comment> \<open> equivalent 'ExerciseList' in exercise.sty\<close>
|
||||
title :: string
|
||||
difficulty :: int
|
||||
origin :: string
|
||||
name :: string
|
||||
counter :: int
|
||||
\<comment> \<open>The body of the exercise class is used to give context information or background material.\<close>
|
||||
|
||||
doc_class task = text_section + \<comment> \<open> equivalent 'Exercise' in exercise.sty\<close>
|
||||
header :: \<open>string option\<close>
|
||||
number :: \<open>int option\<close>
|
||||
difficulty :: int
|
||||
\<comment> \<open>The body of the task class is used formulate the question.\<close>
|
||||
|
||||
|
||||
doc_class solution = text_section + \<comment> \<open> equivalent 'Answer' in exercise.sty\<close>
|
||||
header :: \<open>string option\<close>
|
||||
refers_to :: \<open>string list\<close> \<comment> \<open>references to CMs and TDs and beyond.\<close>
|
||||
\<comment> \<open>The body of the task class is used to give context information or background.\<close>
|
||||
|
||||
|
||||
datatype category = TD | TP | CM | Exam
|
||||
|
||||
doc_class exercise_sheet =
|
||||
status :: status <= semiformal
|
||||
authors :: \<open>author list\<close>
|
||||
reviewers :: \<open>author list\<close>
|
||||
institution :: \<open>string\<close>
|
||||
cat :: category
|
||||
course :: string
|
||||
year :: int
|
||||
month :: int
|
||||
\<comment> \<open>The body of the task class may be used to give context information general hints.\<close>
|
||||
accepts "\<lbrace> exercise ~~ \<lbrace>task ~~ solution \<rbrace>\<^sup>+ \<rbrace>\<^sup>+"
|
||||
|
||||
|
||||
end
|
||||
@ -0,0 +1,81 @@
|
||||
% Package exercise, v. 0.4e (20/03/2007).
|
||||
% Claude Marché (marche@lri.fr), Ralf Treinen (treinen@lri.fr),
|
||||
% Cas Cremers (cas.cremers@gmail.com).
|
||||
% Defines environments "exercise" (for exercises) and "solution"
|
||||
% (for solutions). "exercise" is a theorem-like environment. The effect
|
||||
% of a "solution" environment depends on the options passed to the
|
||||
% package:
|
||||
% - without any option, the text inside this environment is printed
|
||||
% in an appropriate layout, the command "\showsolutions" has no effect;
|
||||
% - with the "none" option, the environement with its contents is completely
|
||||
% ignored, the command "\showsolutions" has no effect;
|
||||
% - with the "end" option, the corrections are saved. The command
|
||||
% "\showsolutions" prints all corrections gathered so far.
|
||||
% The heading of this section can be redefined by renewcommanding
|
||||
% the command "\makesolutionsheading".
|
||||
% Package is actually in English now.
|
||||
%
|
||||
% With the option "bychpater", exercises get numbered by chapter.
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}
|
||||
\ProvidesPackage{exercise}[2007/03/20]
|
||||
|
||||
\RequirePackage{theorem}
|
||||
|
||||
% we use internally three cases:
|
||||
% 0 (no option), 1 (option none), 2 (option end)
|
||||
\def\corcase{0}
|
||||
\newif\if@bychapter\@bychapterfalse
|
||||
\DeclareOption{none}{\def\corcase{1}}
|
||||
\DeclareOption{end}{\def\corcase{2}}
|
||||
\DeclareOption{bychapter}{\@bychaptertrue}
|
||||
|
||||
\ProcessOptions
|
||||
|
||||
\newcommand{\makesolutionsheading}{\section*{Solutions to the exercises}}
|
||||
|
||||
{
|
||||
\theoremstyle{break}
|
||||
\theorembodyfont{\rmfamily}
|
||||
\if@bychapter
|
||||
\newtheorem{exercise}{Exercice}[chapter]
|
||||
\else
|
||||
\newtheorem{exercise}{Exercice}
|
||||
\fi
|
||||
}
|
||||
|
||||
\expandafter\ifcase\corcase % no option
|
||||
\newenvironment{solution}%
|
||||
{\par\noindent\begin{small}\slshape\textbf{Solution :}}%
|
||||
{\end{small}\par\smallskip}
|
||||
\let\showsolutions\relax
|
||||
\or % none option
|
||||
\RequirePackage{verbatim}
|
||||
\let\solution\comment
|
||||
\let\endsolution\endcomment
|
||||
\let\showsolutions\relax
|
||||
\or % end option
|
||||
\RequirePackage{verbatim}
|
||||
\newwrite\solution@out%
|
||||
\immediate\openout\solution@out\jobname.cor
|
||||
\newenvironment{solution}
|
||||
{\let\do\@makeother\dospecials\catcode`\^^M\active
|
||||
\immediate\write\solution@out{%
|
||||
\noexpand\begin{showsolution}{\theexercise}}
|
||||
\def\verbatim@processline{%
|
||||
\immediate\write\solution@out{\the\verbatim@line}}%
|
||||
\verbatim@start}
|
||||
{\immediate\write\solution@out{\noexpand\end{showsolution}}}
|
||||
|
||||
\newenvironment{showsolution}[1]
|
||||
{\par\noindent\textbf{Exercice #1:}\par}
|
||||
{\par}
|
||||
|
||||
\newcommand{\showsolutions}{%
|
||||
\immediate\closeout\solution@out
|
||||
\makesolutionsheading
|
||||
\@input{\jobname.cor}
|
||||
\immediate\openout\solution@out\jobname.cor
|
||||
}
|
||||
\fi
|
||||
@ -0,0 +1,26 @@
|
||||
session "Isabelle_DOF-Ontologies" = "Isabelle_DOF" +
|
||||
options [document = pdf, document_output = "output", document_build = dof]
|
||||
|
||||
directories
|
||||
"CC_v3_1_R5"
|
||||
"Exercise"
|
||||
"Conceptual"
|
||||
"small_math"
|
||||
"CENELEC_50128"
|
||||
theories
|
||||
"document_setup"
|
||||
"document_templates"
|
||||
"CC_v3_1_R5/CC_v3_1_R5"
|
||||
"CC_v3_1_R5/CC_terminology"
|
||||
"Exercise/Exercise"
|
||||
"Conceptual/Conceptual"
|
||||
"small_math/small_math"
|
||||
"CENELEC_50128/CENELEC_50128"
|
||||
"CENELEC_50128/CENELEC_50128_Documentation"
|
||||
document_files
|
||||
"root.bib"
|
||||
"lstisadof-manual.sty"
|
||||
"preamble.tex"
|
||||
"figures/antiquotations-PIDE.png"
|
||||
"figures/srac-as-es-application.png"
|
||||
"figures/srac-definition.png"
|
||||
@ -1,65 +0,0 @@
|
||||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2026 The University of Exeter
|
||||
* 2026 The University of Paris-Saclay
|
||||
*
|
||||
* License:
|
||||
* This program can be redistributed and/or modified under the terms
|
||||
* of the 2-clause BSD-style license.
|
||||
*
|
||||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
chapter \<open>An Outline of an Exercise Ontology\<close>
|
||||
|
||||
text\<open> \<close>
|
||||
|
||||
(*<<*)
|
||||
theory Exercise
|
||||
imports
|
||||
"Isabelle_DOF.scholarly_paper"
|
||||
begin
|
||||
|
||||
|
||||
define_ontology "exercise.sty" "Exercise"
|
||||
|
||||
|
||||
text\<open>\<close>
|
||||
|
||||
datatype category = TD | TP | CM
|
||||
|
||||
doc_class exercise_sheet =
|
||||
status :: status <= "semiformal"
|
||||
authors :: "author list"
|
||||
reviewers :: "author list"
|
||||
institution :: "string"
|
||||
course :: string
|
||||
year :: int
|
||||
month :: int
|
||||
|
||||
doc_class exercise =
|
||||
dfgd :: string
|
||||
label::string
|
||||
title::string
|
||||
difficulty::int
|
||||
origin::string
|
||||
name::string
|
||||
counter::int
|
||||
number::string
|
||||
exam::string
|
||||
year::string
|
||||
|
||||
doc_class description = sdf:: int
|
||||
|
||||
doc_class task =
|
||||
dfgd :: string
|
||||
|
||||
|
||||
doc_class solution =
|
||||
dfgd :: string
|
||||
|
||||
doc_class anwer =
|
||||
dfgd :: string
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user