Re: [isabelle] 2014-RC1 issues: Duplicate annotations
On Fri, 1 Aug 2014, Lars Noschinski wrote:
in some cases, duplicate annotations occur in terms in proof_methods.
Consider the theory:
apply (simp add: exI[of _ 1])
and hover over the 1, which now has a duplicate set of annotations.
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))
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
method_setup foo3 = ‹
Args.term -- Scan.peek (fn ctxt => Args.name_inner_syntax >>
Syntax.read_term (Context.proof_of ctxt)) >>
(fn _ => raise Match)
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
* 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and