forked from Isabelle_DOF/Isabelle_DOF
9bc493250f
By default invariants checking generates warnings.
if invariants_strict_checking theory option is enabled,
the checking generates errors.
Errors to resolve:
- Option type in invariant:
See src/ontologies/scholarly_paper/scholarly_paper.thy:133
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
status :: status <= "description"
formal_results :: "thm list"
invariant L1 :: "the (level σ) > 0"
The attribute L1 uses "the" to project the level value
but the default value is None:
See src/ontologies/scholarly_paper/scholarly_paper.thy:69
doc_class text_section = text_element +
main_author :: "author option" <= None
fixme_list :: "string list" <= "[]"
level :: "int option" <= "None"
It generates an error in src/ontologies/CENELEC_50128/CENELEC_50128.thy
for the Definition* commands, for which the level is not defined.
It triggers an error because "the None" triggers an error.
Get rid of the option type?
The value None is used in the check function
in examples/scholarly_paper/2020-iFM-CSP/paper.thy to check
that a subsequent instance of the same class has a level >= than
the previous instance of the same class.
Update this function?
- What to do with the checking done in scholarly_paper (see check function)
which use low level invariant to check the attributes?
Migrate to High level invariant?
If we change the default value of the level attribute in the text_lement
class from "None" to "Some 0" then check function in scholarly_paper
is triggered in examples/scholarly_paper/2020-iFM-CSP/paper.thy
for the introduction instance "introtext" line 55 and generates
a checking error.
It comes from the fact that the previous instance introheader line 54
is a section*, and then has a default value level of 1.
Then, if the default value of the level attribute in the text_element
is put to Some 0, the low level checking invariant function "check" in
scholarly_paper triggers an error, because the "check" function
checks that the instances in a sequence of the same class
have a growing level.
for a sequence: [("scholarly_paper.introduction", "introheader")
, ("scholarly_paper.introduction", "introtext")]
introtext must have a level >= than introheader.
Same issue with
the examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
theory.
- Bypass checking of high-level invariants
when the class default_cid = "text",
the top (default) document class.
We want the class default_cid to stay abstract
and not have the capability to be defined with attribute,
invariants, etc.
Hence this bypass handles docitem without a class associated,
for example when you just want a document element to be referenceable
without using the burden of ontology classes.
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
The functions get_doc_class_global and get_doc_class_local trigger
an error when the class is "text" (default_cid),
then the functions like check_invariants which use it will fail
if the checking is enabled by default for all the theories.
A quick and dirty fix is proposed to pass the compilation, but must be revised.
See the diff.
|
||
|---|---|---|
| .. | ||
| CC_ISO15408/PikeOS_study | ||
| CENELEC_50128 | ||
| cytology | ||
| scholarly_paper | ||
| technical_report | ||
| README.md | ||
| ROOTS | ||
README.md
Examples
Scholarly (Academic) Papers
The examples in the directory scholarly_paper
are examples of typical conference papers (usually, in computer science).
Technical Reports
The examples in the directory technical_report
are examples of typical technical reports. This includes also the
Isabelle/DOF User and Implementation Manual.