Email Gateway (Aug 19 2022 at 15:30): Email Gateway (Aug 19 2022 at 15:30):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
in some cases, duplicate annotations occur in terms in proof_methods.
Consider the theory:
lemma P
apply (simp add: exI[of _ 1])
and hover over the 1, which now has a duplicate set of annotations.
Duplicate annotations also occur in locale expressions:
locale A = fixes x
locale B = A z for z + assumes False
Here, the "z" has a duplicate set of annotations from Syntax.check_term
(but only a single one from Syntax.read_term).
I tried to dig into what triggers this behaviour:
For proof methods, this is related to the introduction of a method
closure (which executes every proof method twice). The use of e.g. the
Args.term parser is fine; but if one uses Args.name_inner_syntax and
Syntax.read_term later, annotations are duplicated:
method_setup foo1 = ‹
Args.term >> (fn _ => fn _ => SIMPLE_METHOD' (K all_tac))
›
vs.
method_setup foo2 = ‹
Scan.peek (fn ctxt => Args.name_inner_syntax >> Syntax.read_term
(Context.proof_of ctxt)) >>
(fn _ => fn _ => SIMPLE_METHOD' (K all_tac))
›
except if the method errors out unconditionally (and hence is called
only once):
method_setup foo3 = ‹
Args.term -- Scan.peek (fn ctxt => Args.name_inner_syntax >>
Syntax.read_term (Context.proof_of ctxt)) >>
(fn _ => raise Match)
›
-- Lars
Email Gateway (Aug 19 2022 at 15:33):From: Makarius <makarius@sketis.net>
This is a careful analysis of this particular situation in
Isabelle2014-RC1, which was the result of spending several weeks this year
to make refinements over Isabelle2013-2.
Here is another example:
lemma "x = x" "x = x" "x = x" by (rule refl [of x])+
If you C-hover over the fact "refl" and the variable "x" in either
Isabelle version, you see how often the system traverses that spot to make
a PIDE markup report.
It is the very concept of PIDE that markup is produced as a trace from
internal aspects of the prover. It is then left as an exercise to rework
the prover that this information makes sense to the user. Attendants of
the UITP2014 workshop in Vienna may remember the brief discussion we've
had about that for Coq PIDE in particular.
In the example above, the rule method is already in a pretty good state:
its main argument outline is processed exactly once in its "static phase",
before actually applying it to the goal state. The attribute "of"
notoriously suffers from dynamic evaluation, though, and causes redundant
multiplication of markup.
The static closure of proof methods has made progress in Isabelle2014-RC1,
but it is not fully finished yet. Even in that partial stage, I can
foresee complaints by proof tool authors about that sanitation. See also
the NEWS:
* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax. Method arguments should be
processed in the original proof context as far as possible, before
operating on the goal state. In any case, the standard discipline for
subgoal-addressing needs to be observed: no subgoals or a subgoal
number that is out of range produces an empty result sequence, not an
exception. Potential INCOMPATIBILITY for non-conformant tactical
proof tools.
The requirements for tactics or Isar proof methods are described in the
"implementation" manual, as usual.
The relative silence in that respect of "potential incompatibility" is
probably a proof that only few people have tested their own tools with
Isabelle2014-RC1 so far.
Makarius
Email Gateway (Aug 19 2022 at 15:43):From: Lars Noschinski <noschinl@in.tum.de>
On 01.08.2014 21:19, Makarius wrote:
Here is another example:
In the example above, the rule method is already in a pretty good
state: its main argument outline is processed exactly once in its
"static phase", before actually applying it to the goal state. The
attribute "of" notoriously suffers from dynamic evaluation, though,
and causes redundant multiplication of markup.The static closure of proof methods has made progress in
Isabelle2014-RC1, but it is not fully finished yet. Even in that
partial stage, I can foresee complaints by proof tool authors about
that sanitation. See also the NEWS:* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax. Method arguments should be
processed in the original proof context as far as possible, before
operating on the goal state. In any case, the standard discipline for
subgoal-addressing needs to be observed: no subgoals or a subgoal
number that is out of range produces an empty result sequence, not an
exception. Potential INCOMPATIBILITY for non-conformant tactical
proof tools.
After looking carefully at args.ML I know now how e.g. Args.term
prevents a term from being parsed twice.
I am in a more complicated situation: I have a parser which read_term-s
the terms in a different order than they appear in the source and
modifies the context (by fixing some of the term variables), so I need
to use Parse.term instead of Args.term. It is static in the sense that
the interpretation of the terms does not depend on the goal state.
Some questions arise from that and my new understanding of
static/dynamic phase separation:
* Does it make sense at this point to mimic the Token.assign machinery
used in Args? Or is it likely that the need to do this manually will
go away with say 2014+1?
If yes:
* Is it ok for a context_parser to modify the context? (probably not,
since most of the parser will be short-circuited after the static phase)
The relative silence in that respect of "potential incompatibility" is
probably a proof that only few people have tested their own tools with
Isabelle2014-RC1 so far.
I had to convert a few methods already; mostly by wrapping them into
SUBGOAL.
Last updated: Nov 21 2024 at 12:39 UTC