Custom Query (361 matches)

[Report from Lucas Dixon]

seems that Proof General is sometimes dieing on the ML error output from Isabelle.

Anyway, PG leaves the processed theory header red, and doesn't show an error - but it doesn't completely lock up, although it gets slow for a while - presumably lots of processing/parsing.

In Emacs (Carbon emacs GNU Emacs 22.3.1 (i386-apple-darwin9.6.0, Carbon Version 1.6.0)

of 2009-01-03 on seijiz.local; ProofGeneral is the latest dev snapshot taken yesterday evening - but happens on 3.7.1 too), I'm getting a lot of messages like:

[Isabelle] Theory loader: removing "BasicIsaP"
error in process filter: if: Lisp nesting exceeds `max-lisp-eval-depth'
error in process filter: Lisp nesting exceeds `max-lisp-eval-depth'
[Isabelle] Theory loader: removing "BasicIsaP"
error in process filter: if: Lisp nesting exceeds `max-lisp-eval-depth'
error in process filter: Lisp nesting exceeds `max-lisp-eval-depth'
[Isabelle] Theory loader: removing "BasicIsaP"
error in process filter: if: Lisp nesting exceeds `max-lisp-eval-depth'
error in process filter: Lisp nesting exceeds `max-lisp-eval-depth'
bufhist-erase-buffer: Buffer is read-only: #<buffer *response*>

This happens in Isabelle 2009 - also recent dev snapshots. the output from the *isabelle* buffer is:

*** signature DTAC =
*** sig val print : Context.proof -> T -> unit
*** val pretty : T -> Context.proof -> Pretty.T val mks : string * gtac -> T
*** val mk_from_isa_tac_s : string * tactic -> T
*** val mk_from_isa_tac_local_s : string * tactic -> T
*** val mk_from_isa_tac_local : (Context.proof -> Pretty.T) * tactic -> T
*** val mk_from_isa_tac : (Context.proof -> Pretty.T) * tactic -> T
*** val mk : (Context.proof -> Pretty.T) * gtac -> T val gtac : T -> gtac
*** val compose_local_result_th :
***    Prf.gname -> Prf.T -> thm -> (Prf.gname list * Prf.T) Seq.seq
*** val compose : (Prf.gname * Prf.gname) list -> Prf.T -> Prf.T Seq.seq
*** exception bug_exp of string * (Prf.gname * Prf.T * thm)
*** val apply_localasms_tac :
***    (Context.proof -> Pretty.T) * (thm -> thm Seq.seq) ->
***    Prf.gname -> Prf.T -> (Prf.gname list * Prf.T) Seq.seq
*** val apply_allasms_tac :
***    (Context.proof -> Pretty.T) * (thm -> thm Seq.seq) ->
***    Prf.gname -> Prf.T -> (Prf.gname list * Prf.T) Seq.seq
*** type T end
*** structure DB_DTac :
*** sig val thin_all : int -> thm -> thm val print : T -> Context.proof -> unit
*** val pretty : T -> Context.proof -> Pretty.T val mks : string * gtac -> T
*** val mk_from_isa_tac_s : string * (thm -> thm Seq.seq) -> T
*** val mk_from_isa_tac_local_s : string * (thm -> thm Seq.seq) -> T
*** val mk_from_isa_tac_local :
***    (Context.proof -> Pretty.T) * (thm -> thm Seq.seq) -> T
*** val mk_from_isa_tac :
***    (Context.proof -> Pretty.T) * (thm -> thm Seq.seq) -> T
*** val mk : (Context.proof -> Pretty.T) * gtac -> T val gtac : T -> gtac
*** val compose_local_result_th :
***    string -> Prf.T -> thm -> (Prf.gname list * Prf.T) Seq.seq
*** val compose_all_result_th :
***    string -> Prf.T -> thm -> (Prf.gname list * Prf.T) Seq.seq
*** val compose : (Goaln.NSet.name * Prf.gname) list -> Prf.T -> Prf.T Seq.seq
*** exception bug_exp of string * (Prf.gname * Prf.T * thm)
*** val apply_localasms_tac :
***    (Context.proof -> Pretty.T) * (thm -> thm Seq.seq) ->
***    Prf.gname -> Prf.T -> (Prf.gname list * Prf.T) Seq.seq
*** val apply_allasms_tac :
***    (Context.proof -> Pretty.T) * (thm -> thm Seq.seq) ->
***    Prf.gname -> Prf.T -> (Prf.gname list * Prf.T) Seq.seq
*** datatype T = DPrfTac of {p: Context.proof -> Pretty.T, gtac: gtac} end
*** Error: Structure does not match signature.
***    Signature: val print: Context.proof -> T -> unit
***    Structure: val print: DB_DTac.T -> Context.proof -> unit
***    Reason:
***       Can't match DB_DTac.T to Context.proof = Context.proof
***          (Different type constructors) (line 217 of "/Users/ldixon/work/IsaP-trunk/IsaPlanner/src/rtechn/basic/dtac.ML")
*** Exception- ERROR of "Static Errors" raised
*** At command "theory" (line 1 of "/Users/ldixon/work/IsaP-trunk/IsaPlanner/src/build/BasicIsaP.thy").
*** At command "theory".

When I go to the Isabelle dir, and hit return, the error messages do then get shown in the response buffer.

Editing document sets the parse edit offset, the position from which parsing begins next time.

The code for adjusting this had faulty logic in earlier versions. It was fixed but seems to have broken again, perhaps with parser adjustments. This causes bad breakage because it gets difficult to edit text.

Editing text doesn't always change the document model underlying. Then sending the next command sends the old text.