Avoid reporting for meta arguments attributes of isabelle_DOF
commands and for text input of text*
The last reporting duplication not resolved comes
from the document_command command in Isa_DOF,
which parses the meta arguments twice,
one time for the creation of the docitem
with create_and_check_docitem which will add reporting
for the attributes value
(see conv_attrs whichs calls Syntax.read_term_global,
which iwill add reporting)
and the other for the document output
with document_output which also adds reporting
(see meta_args_2_latex which calls
(Syntax.check_term ctxt o Syntax.parse_term ctxt) with
ltx_of_markup and Syntax.parse_term also adds reporting)
- Make optional meta arguments completely optional
- Make meta arguments context of ML* available in its ML context
- Make meta arguments of ML* mandatory to mimic text*.
Without meta arguments, its behavior is already captured by
the ML command
ci/woodpecker/push/build Pipeline was successfulDetails
Support invariants on attributes of classes atttributes.
Example:
doc_class inv_test1 =
a :: int
doc_class inv_test2 =
b :: "inv_test1"
c:: int
invariant inv_test2 :: "c σ = 1"
invariant inv_test2' :: "a (b σ) = 2"
doc_class inv_test3 = inv_test1 +
b :: "inv_test1"
c:: int
invariant inv_test3 :: "a σ = 1"
invariant inv_test3' :: "a (b σ) = 2"
To support invariant on attributes in attributes
and invariant on attributes of the superclasses,
we check that the type of the attribute of the subclass is ground:›
ML‹
val Type(st, [ty]) = \<^typ>‹inv_test1›
val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme›
val t = ty = \<^typ>‹unit›
›
ci/woodpecker/push/build Pipeline was successfulDetails
- The current implementation triggers a warning when
rejected classes are find in the monitor,
and an error if monitor_strict_checking is enable.
It follows these rules:
Inside the scope of a monitor,
all instances of classes mentioned in its accepts_clause
(the ∗‹accept-set›) have to appear in the order specified
by the regular expression.
Instances not covered by an accept-set may freely occur.
Monitors may additionally contain a rejects_clause
with a list of class-ids (the reject-list).
This allows specifying ranges of
admissible instances along the class hierarchy:
- a superclass in the reject-list and a subclass in the
accept-expression forbids instances superior to the subclass, and
- a subclass S in the reject-list and a superclass T in the
accept-list allows instances of superclasses of T to occur freely,
instances of T to occur in the specified order and forbids
instances of S.
- No message is triggered for the free classes,
but two theory options, free_class_in_monitor_checking
and free_class_in_monitor_strict_checking,
are added and can be used if we want to trigger warnings or errors,
in the case we do not want free classes inside a monitor.
- Fix the checking warning when defining a monitor,
as the monitor was added to the monitor table and then
the instance of the monitor was added to the theory.
So a monitor had the bad behavior to check itself.
ci/woodpecker/push/build Pipeline was successfulDetails
By default invariants checking generates warnings.
If invariants_strict_checking theory option is enabled,
the checking generates errors.
- Update 2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
and 2020-iFM-CSP/paper.thy to pass the checking of
the low level invariant checking function "check"
in scholarly_paper.thy,
which checks that the instances in a sequence of the same class
have a growing level.
For a sequence:
section*[intro::introduction]‹ Introduction ›
text*[introtext::introduction, level = "Some 1"]‹...›
introtext must have a level >= than intro.
- Bypass the 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.
Nicolas Méric
Achim D. Brucker
Burkhart Wolff
Makarius Wenzel