Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Redundant trace with jEdit


view this post on Zulip Email Gateway (Aug 19 2022 at 08:01):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:02):

From: Tobias Nipkow <nipkow@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:02):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.


Last updated: Mar 28 2024 at 16:17 UTC