Re: [isabelle] Redundant trace with jEdit



This has nothing to do with jedit. Simplification is an interative process that
may traverse the proof state multiple times. Hence the same premise may be
inserted into the context multiple times, and each time you are notified. We
apologize for any inconvenience this may cause.

Tobias

Am 30/07/2012 20:02, schrieb Yannick Duchêne (Hibou57):
> Hi all the people,
> 
> The title mention jEdit, while I'm not sure that's jEdit specific. Read: at
> least with jEdit.
> 
> If ever I create a redundant lemma, Isabelle warns me all the time, even when I
> feel it helps readability. But it seems it don't applies the same to it‑self:
> whenever I do “using [[simp_trace=true]]” and enable trace in the output pan, I
> often get redundant entries starting with
> 
>   “[1]Adding rewrite rule "??.unknown":”
> 
> For a concrete case I just had, there were multiple
> 
>   [1]Adding rewrite rule "??.unknown":
>   r x y ≡ True
> 
> When repeated multiple times for multiple rewrite rules, this make the trace
> encumbered and less readable.
> 
> Is there a known way to filter it out automatically? If possible, I would like
> to have only one trace message for each added rewrite rule. A quick search using
> https://lists.cam.ac.uk/mailman/mmsearch/cl-isabelle-users returned nothing on
> that topic.
> 
> 
> Have an happy time
> 





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