Re: [isabelle] Redundant trace with jEdit



Hi Tobias,

You don't have to apologize. Isabelle as a proof assistant, largely overweight that kind of issue :-P I just wanted to know, not really complaining.

Le Mon, 30 Jul 2012 21:48:58 +0200, Tobias Nipkow <nipkow at in.tum.de> a écrit:

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





--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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