Re: [isabelle] 2014-RC1 issues: Duplicate annotations



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.



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