Email Gateway (Aug 18 2022 at 15:00): Email Gateway (Aug 18 2022 at 15:00):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Users,
I'd like to ask you about an issue I have with Proof General (CVS
version) and see if someone has a quick work-around of any kind.
I've already filed a bug report, but as it's the only PG activity in the
last 90+ days, I don't know if anyone will get around to looking at it:
http://proofgeneral.inf.ed.ac.uk/trac/ticket/322
Basically, attempting to use the "tracing" function inside ML makes PG
choke, at least when it is done inside a proof method (which I use for
debugging when writing a new proof method). Here is an example:
theory SC imports Main
begin
ML {*
fun moo_tac ctxt (ct,i) = (
tracing ("Target: MOO!");
no_tac);
*}
method_setup moo = {*
Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (CSUBGOAL (moo_tac ctxt)))
*} "Some proof method reduced to a simple thing which fails."
(* don't match on different state vars *)
lemma "X ==> Y"
apply (moo)
At this point, PG stops with:
error in process filter: proof-shell-process-urgent-message: Wrong
number of arguments: #[(str) [...] [proof-trace-buffer str newline] 1
("/home/rafalk/repos/l4.verified/isabelle/contrib/ProofGeneral/generic/pg-response.elc"
. 12897)], 3
The [...] includes non-printable characters, hence omitted.
Has anyone seen anything similar?
Sincerely,
Rafal Kolanski.
Last updated: Apr 19 2024 at 12:27 UTC