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:

lemma P
 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))
›

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)
›

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.