Email Gateway (Aug 19 2022 at 09:39): Email Gateway (Aug 19 2022 at 09:39):From: Walther Neuper <wneuper@ist.tugraz.at>
debugging a function definition with
:
using [[simp_trace_depth_limit=999]]
using [[simp_trace=true]]
by auto
'auto' is looping and the mass of data makes jEdit's Output panel unusable.
How can I redirect the output to a file?
(assuming that this is the best way to cope with the situation in jEdit)
Walther
PS: google tells me, that jEdit can redirect -- but I cannot find how
(and hope, there is somebody patient enough to tell me in a line ;-))
Email Gateway (Aug 19 2022 at 09:39):From: Lars Noschinski <noschinl@in.tum.de>
On 23.01.2013 15:29, Walther Neuper wrote:
debugging a function definition with
:
using [[simp_trace_depth_limit=999]]
using [[simp_trace=true]]
by auto'auto' is looping and the mass of data makes jEdit's Output panel unusable.
Probably the easiest solution is to use the upcoming Isabelle 2013,
which has a size limit for the traces in jEdit (and can dynamically
request a larger trace).
How can I redirect the output to a file?
(assuming that this is the best way to cope with the situation in jEdit)
I think with Isabelle 2012, your best bet is to click "Cancel" fast
enough in the System(?) view and then click on nothing in the editor buffer.
-- Lars
Email Gateway (Aug 19 2022 at 09:39):From: Walther Neuper <wneuper@ist.tugraz.at>
On 01/23/2013 03:43 PM, Lars Noschinski wrote:
Probably the easiest solution is to use the upcoming Isabelle 2013,
which has a size limit for the traces in jEdit (and can dynamically
request a larger trace).
... great to hear ! But we cannot wait:
How can I redirect the output to a file?
(assuming that this is the best way to cope with the situation in jEdit)I think with Isabelle 2012, your best bet is to click "Cancel" fast
enough in the System(?) view and then click on nothing in the editor
buffer.
... I'd guess to delete the respective code fast enough.
(supposing that "System(?) view" relates to emacs/Proof General)
-- Lars
Thank you for your help (with experiences hardly to be found in
documentation) !
Walther
Email Gateway (Aug 19 2022 at 09:40):From: Lars Noschinski <noschinl@in.tum.de>
I meant the "Prover Session" panel in jEdit.
Deleting the code will also delete the output. Tracing non-terminating
simplifier runs is not what the 2012 version shines at, unfortunately.
Thinks will be better in 2013 and there is currently a student working
on a completely new tracing facility.
-- Lars
Email Gateway (Aug 19 2022 at 09:40):From: Walther Neuper <wneuper@ist.tugraz.at>
On 01/24/2013 09:31 AM, Lars Noschinski wrote:
On 23.01.2013 16:44, Walther Neuper wrote:
I think with Isabelle 2012, your best bet is to click "Cancel" fast
enough in the System(?) view and then click on nothing in the editor
buffer.... I'd guess to delete the respective code fast enough.
(supposing that "System(?) view" relates to emacs/Proof General)I meant the "Prover Session" panel in jEdit.
Ah thanks, that's it !
(jEdit is becoming "intuitive" such that one might rely just an trying ;-)
Deleting the code will also delete the output. Tracing non-terminating
simplifier runs is not what the 2012 version shines at, unfortunately.
Thinks will be better in 2013 and there is currently a student working
on a completely new tracing facility.-- Lars
Looking forward to Isabelle2013, good luck for delivery !
Walther
Email Gateway (Aug 19 2022 at 09:41):From: Makarius <makarius@sketis.net>
You don't have to wait, but can start with
http://isabelle.in.tum.de/website-Isabelle2013-RC1/ right now.
There are unusually few incompatibilities wrt. Isabelle2012, and no new
ones are anticipated stepping from the release candidates to the final
release in mid-February.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC