Kleinigkeiten.
This commit is contained in:
parent
c0c92ac50c
commit
35a0a27c1d
|
|
@ -49,16 +49,23 @@
|
|||
\immediate\write\@auxout{\noexpand\addauthor{#1}}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{%
|
||||
\immediate\write\@auxout{\noexpand\title{\commandkey{#1}}}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubsectionHeader[label=,type=,examTitle=,examSubject=,date,timeAllowed][1]{%
|
||||
\immediate\write\@auxout{\noexpand\title{\commandkey{examTitle}}}%
|
||||
\newkeycommand\isaDofSectionHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{%
|
||||
\immediate\write\@auxout{\noexpand\title{\commandkey{#1}}}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubsectionHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{%
|
||||
\immediate\write\@auxout{\noexpand\title{\commandkey{#1}}}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextAnswerFormalStep[label=,type=,justification=,term=][1]{%
|
||||
#1
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextAnswerYesNo[label=,type=,step_label=, yes_no=][1]{%
|
||||
\newkeycommand\isaDofTextAnswerYesNo[label=,type=,step_label=,yes_no=][1]{%
|
||||
#1
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ begin
|
|||
|
||||
open_monitor*[exam::MathExam]
|
||||
|
||||
|
||||
(* currently rethinking on "deep ontologies" necessary ... Achim
|
||||
text*[idir::Author,affiliation="''LRI, CentraleSupelec''",
|
||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
|
@ -18,12 +18,11 @@ text*[keller::Author,affiliation="''LRI, Univ. Paris-Sud''",
|
|||
text{* This example is an excerpt from the french baccaleareat 2017.
|
||||
The textual explanations were kept in french.
|
||||
*}
|
||||
|
||||
text*[header::Header,examSubject= "[analysis,geometry]",
|
||||
examTitle="''BACCALAUREAT GENERAL MATHEMATIQUES''",
|
||||
date="''21-06-2017''",
|
||||
timeAllowed="240::int"]
|
||||
{*
|
||||
*)
|
||||
|
||||
text*[header::Header,examSubject="[analysis,geometry]", date="''21-06-2017''",
|
||||
timeAllowed="240::int"]{* BACCALAUREAT GENERAL MATHEMATIQUES *}
|
||||
text{*
|
||||
\begin{itemize}
|
||||
\item Les calculatrices électroniques de poche sont autorisées, conformément à la réglementation
|
||||
en vigueur.
|
||||
|
|
@ -38,8 +37,7 @@ text*[header::Header,examSubject= "[analysis,geometry]",
|
|||
|
||||
|
||||
text*[exo1 :: Exercise,
|
||||
Exercise.concerns= "{setter,student,checker,external_examiner}",
|
||||
Exercise.content="[q1::Task,q2,q3a]"]
|
||||
Exercise.concerns= "{setter,student,checker,externalExaminer}"]
|
||||
{* On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par :
|
||||
@{term "h(x) = x * exponent (-x)"}
|
||||
*}
|
||||
|
|
@ -52,21 +50,17 @@ text*[q1::Task, Task.concerns= "{setter,student}",
|
|||
level="oneStar", mark="1::int", type="formal"]
|
||||
{* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
|
||||
|
||||
text*[a1::Answer_Formal_Step]
|
||||
{* Fill in term and justification*}
|
||||
text*[a1::Answer_Formal_Step] {* Fill in term and justification*}
|
||||
|
||||
lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top"
|
||||
sorry
|
||||
lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top" sorry
|
||||
|
||||
text*[v1::Validation,
|
||||
proofs="[q1::thm]"]
|
||||
{* See lemma q1 *}
|
||||
text*[v1::Validation, proofs="[@{thm ''q1''}::thm]"] {* See lemma @{thm q1}. *}
|
||||
|
||||
|
||||
text*[q2::Task, Task.concerns= "{examiner,validator,student}",
|
||||
level="oneStar", mark="1::int", type="formal"]
|
||||
{* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et dresser son tableau
|
||||
de variation *}
|
||||
text*[q2::Task, Task.concerns= "{setter,checker,student}",
|
||||
level="oneStar", mark="1::int", type="formal"]
|
||||
{* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et
|
||||
dresser son tableau de variation *}
|
||||
|
||||
text*[a2::Answer_Formal_Step]
|
||||
{* Fill in term and justification*}
|
||||
|
|
@ -92,15 +86,14 @@ lemma q2_b : "0 \<le> x \<and> x \<le> y \<and> y \<le> 1 \<Longrightarrow> h x
|
|||
lemma q2_c : "1 \<le> x \<and> x \<le> y \<Longrightarrow> h x \<ge> h y"
|
||||
sorry
|
||||
|
||||
text*[v2::Validation,
|
||||
proofs="[q2_b::thm, q2_c]"]
|
||||
{* See lemmas q2_b and q2_c *}
|
||||
text*[v2::Validation, proofs="[@{thm ''q2_b''}, @{thm ''q2_c''}]"]
|
||||
{* See lemmas @{thm q2_b} and @{thm q2_c}. *}
|
||||
|
||||
|
||||
text*[q3a::Task, Task.concerns= "{examiner,validator,student}",
|
||||
text*[q3a::Task, Task.concerns= "{setter,checker,student}",
|
||||
level="oneStar", mark="1::int", type="formal"]
|
||||
{* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\<infinity>], on a :
|
||||
@term{h x = (exp (- x)) - (h' x)} *}
|
||||
@{term "h x = (exp (- x)) - (h' x)"}. *}
|
||||
|
||||
text*[a3a::Answer_Formal_Step]
|
||||
{* Fill in term and justification*}
|
||||
|
|
@ -108,17 +101,14 @@ text*[a3a::Answer_Formal_Step]
|
|||
lemma q3a : "h x = (exp (- x)) - (h' x)"
|
||||
by (simp add : h_def h'_def left_diff_distrib)
|
||||
|
||||
subsubsection*[v3a::Validation,
|
||||
proofs="[q3a::thm]"]
|
||||
{* See lemma q3a *}
|
||||
subsubsection*[v3a::Validation, proofs="[@{thm ''q3a''}::thm]"]
|
||||
{* See lemma @{thm q3a}. *}
|
||||
|
||||
|
||||
subsection*[sol1 :: Solution,
|
||||
Solution.content="[exo1::Exercise]",
|
||||
Solution.valids = "[v1::Validation,v2,v3a]"]
|
||||
{*
|
||||
See validations.
|
||||
*}
|
||||
{* See validations. *}
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -2,8 +2,12 @@ session "BAC2017" = "HOL" +
|
|||
options [document = pdf, document_output = "output",quick_and_dirty=true]
|
||||
theories [document = false]
|
||||
"../../../ontologies/mathex_onto"
|
||||
"Deriv"
|
||||
"Transcendental"
|
||||
theories
|
||||
BAC2017
|
||||
document_files
|
||||
"root.tex"
|
||||
"preamble.tex"
|
||||
"ontologies.tex"
|
||||
"build"
|
||||
|
|
|
|||
|
|
@ -12,3 +12,9 @@
|
|||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
||||
|
||||
%% This is a placeholder for user-specific configuration and packages.
|
||||
|
||||
\newkeycommand\isaDofTextExercise[label=,type=,Exercise.content=,concerns=,][1]{%
|
||||
\begin{Exercise}
|
||||
#1
|
||||
\end{Exercise}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,56 +1,71 @@
|
|||
\documentclass[11pt,a4paper]{article}
|
||||
\usepackage{isabelle,isabellesym}
|
||||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1
|
||||
|
||||
% further packages required for unusual symbols (see also
|
||||
% isabellesym.sty), use only when needed
|
||||
%% Warning: Do Not Edit!
|
||||
%% =====================
|
||||
%% This is the root file for the Isabelle/DOF.
|
||||
%% All customization and/or additional packages should be added to the file
|
||||
%% preamble.tex.
|
||||
|
||||
%\usepackage{amssymb}
|
||||
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
|
||||
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
|
||||
%\<triangleq>, \<yen>, \<lozenge>
|
||||
|
||||
%\usepackage{eurosym}
|
||||
%for \<euro>
|
||||
|
||||
%\usepackage[only,bigsqcap]{stmaryrd}
|
||||
%for \<Sqinter>
|
||||
|
||||
%\usepackage{eufrak}
|
||||
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
|
||||
|
||||
%\usepackage{textcomp}
|
||||
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
|
||||
%\<currency>
|
||||
|
||||
% this should be the last package used
|
||||
\usepackage{pdfsetup}
|
||||
|
||||
% urls in roman style, theory text in math-similar italics
|
||||
\RequirePackage{ifvtex}
|
||||
\documentclass[fontsize=11pt,DIV12,paper=a4]{scrartcl}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage{textcomp}
|
||||
\usepackage[english]{babel}
|
||||
\usepackage{isabelle}
|
||||
\input{ontologies}
|
||||
\usepackage{isabellesym}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
||||
\usepackage{hyperref}
|
||||
\setcounter{tocdepth}{3}
|
||||
\hypersetup{%
|
||||
bookmarksdepth=3
|
||||
,pdfpagelabels
|
||||
,pageanchor=true
|
||||
,bookmarksnumbered
|
||||
,plainpages=false
|
||||
} % more detailed digital TOC (aka bookmarks)
|
||||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
\urlstyle{rm}
|
||||
\isabellestyle{it}
|
||||
|
||||
% for uniform font size
|
||||
%\renewcommand{\isastyle}{\isastyleminor}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%% 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}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{BAC2017}
|
||||
\title{.}
|
||||
\author{By bu}
|
||||
\begin{document}
|
||||
\maketitle
|
||||
|
||||
\tableofcontents
|
||||
|
||||
% sane default for proof documents
|
||||
\parindent 0pt\parskip 0.5ex
|
||||
|
||||
% generated text of all theories
|
||||
\input{session}
|
||||
|
||||
% optional bibliography
|
||||
%\bibliographystyle{abbrv}
|
||||
%\bibliography{root}
|
||||
|
||||
\IfFileExists{root.bib}{%
|
||||
\bibliographystyle{abbrvnat}
|
||||
\bibliography{root}
|
||||
}{}
|
||||
\end{document}
|
||||
|
||||
%%% Local Variables:
|
||||
|
|
|
|||
|
|
@ -6,13 +6,10 @@ begin
|
|||
(*>*)
|
||||
open_monitor*[exam::MathExam]
|
||||
|
||||
section*[idir::Author, affiliation="''CentraleSupelec''",
|
||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
||||
subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1''",
|
||||
date="''02-05-2018''", timeAllowed="90::int"]
|
||||
{*
|
||||
section*[header::Header,examSubject= "[algebra]",
|
||||
date="''02-05-2018''", timeAllowed="90::int"] {* Exam number 1 *}
|
||||
text{*
|
||||
\begin{itemize}
|
||||
\item Use black ink or black ball-point pen.
|
||||
\item Draw diagrams in pencil.
|
||||
|
|
@ -20,6 +17,11 @@ subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1
|
|||
\end{itemize}
|
||||
*}
|
||||
|
||||
subsection*[idir::Author, affiliation="''CentraleSupelec''",
|
||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
||||
|
||||
(* should be in DOF-core
|
||||
|
||||
* causes crash on the LaTeX side:
|
||||
|
|
|
|||
|
|
@ -11,4 +11,4 @@ session "MathExam" = "HOL" +
|
|||
"ontologies.tex"
|
||||
"preamble.tex"
|
||||
"build"
|
||||
"document/figures/Polynomialdeg5.png"
|
||||
"figures/Polynomialdeg5.png"
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ where the author of the exam is not expected to be physically present.
|
|||
datatype ContentClass =
|
||||
setter -- \<open>the 'author' of the exam\<close>
|
||||
| checker -- \<open>the 'proof-reader' of the exam\<close>
|
||||
| external_examiner -- \<open>an external 'proof-reader' of the exam\<close>
|
||||
| externalExaminer -- \<open>an external 'proof-reader' of the exam\<close>
|
||||
| student -- \<open>the victim ;-) ... \<close>
|
||||
|
||||
|
||||
|
|
@ -40,7 +40,6 @@ datatype Grade =
|
|||
A1 | A2 | A3
|
||||
|
||||
doc_class Header =
|
||||
examTitle :: string
|
||||
examSubject :: "(Subject) list"
|
||||
date :: string
|
||||
timeAllowed :: int -- minutes
|
||||
|
|
@ -66,13 +65,13 @@ doc_class Task = Exam_item +
|
|||
level :: Level
|
||||
type :: Question_Type
|
||||
subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
|
||||
concerns :: "ContentClass set" <= "{setter,student,checker,external_examiner}"
|
||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
||||
mark :: int
|
||||
|
||||
|
||||
doc_class Exercise = Exam_item +
|
||||
content :: "(Task) list"
|
||||
concerns :: "ContentClass set" <= "{setter,student,checker,external_examiner}"
|
||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
||||
|
||||
|
||||
text{* In many institutions, it makes sense to have a rigorous process of validation
|
||||
|
|
@ -89,7 +88,7 @@ doc_class Validation =
|
|||
doc_class Solution = Exam_item +
|
||||
content :: "Exercise list"
|
||||
valids :: "Validation list"
|
||||
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
|
||||
concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}"
|
||||
|
||||
doc_class MathExam=
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
|
|
|
|||
Loading…
Reference in New Issue