Max lisp nesting exceeded on large error outputs

[David Aspinall]

[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.

[David Aspinall]

A first attempt to reproduce with this way of generating an 80,000 line error message:

ML {* Output.error_msg (cat_lines (List.tabulate (80000,K "This is a big error message"))); *}

does not trigger the max eval depth problem on Linux Emacs 22.2.1 or 23.0.91.1 (Ubuntu snapshot), either when processed interactively or in a required theory file.

Maybe it is the combination of the large error message and the message asking PG to retract a file that triggers the problem. Really need a small test case for this.

[Lucas Dixon]

here's a way to get it to happen - assuming you're on AFS...

isabelle emacs /afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/IsaP.thy

try to process the theory header in emacs/PG.

tested with install of Isabelle/emacs/PG at: /afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/

using versions:

GNU Emacs 23.0.93.1 (i686-pc-linux-gnu, GTK+ Version 2.10.4) of 2009-05-06 on haggis.inf.ed.ac.uk

ProofGeneral 4.0pre090817;

Isabelle 32399:4dc441c71cce date: Mon Aug 24 13:59:08 2009 +0200

[David Aspinall]

First you need Lucas's paths setup too:

cd /afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev
source source_me.sh
isabelle emacs /afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/IsaP.thy

and then the bug triggers, contents of *isabelle* uploaded next.

[David Aspinall]

attachments seem to be disabled. Below is final segment of output:

Theory loader: removing "HOL_IsaP", "IsaCoSy", "IsaScheme"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/HOL_IsaP.thy"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/gproof/prf/subst.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/critics/metavar_lib.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/basic/res.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/basic/rtechn_env.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/cinfos/counterex_cinfo.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/wrulesdb.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/basic/isa_dtacs.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/induct/induct_dtac.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/induct_HOL.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/basic/dtac_rtechn.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/induct/induct_rtechn.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/isar_attr.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/split/split_rtechn.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/conj/conj_stack_cinfo.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/conj/conjecturedb_lib.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/conj/conjdb_cinfo.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/conj/lemma_conj_lib.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/lemma_conj_HOL_data.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/conj/conj_rtechn.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/quickcheck_auto.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/induct_and_simp.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/wrules_gctxt.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/critics/middleout_rw.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/critics/lemma_speculation.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/basic_cinfo.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/basic_rtechn.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/midout_cinfo.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/casesplit.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/casesplit_calc.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/postripple_casesplit.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/lemcalc.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/rtechn/rippling/lemspec.ML"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/IsaCoSy.thy"
Proof General, you can unlock the file "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/IsaScheme.thy"
### Unknown theory "IsaCoSy"
### Unknown theory "IsaScheme"
*** Theory loader: failed to load "IsaScheme" (unresolved "IsaCoSy")
*** Theory loader: failed to load "IsaCoSy" (unresolved "HOL_IsaP")
*** Error: Type error in function application. Function: Pretty.block : Pretty.T list -> Pretty.T
***    Argument: "a" : string
***    Reason:
***    Can't unify Pretty.T list (*In Basis*) with string (*In Basis*) (Different type constructors) (line 133 of "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/interface/interface.ML")
*** Exception- ERROR of "Static Errors" raised
*** At command "theory" (line 1 of "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/HOL_IsaP.thy").
*** At command "theory" (line 1 of "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/IsaP.thy").
> 

[David Aspinall]

The backtrace reveals the bug is in `isar-remove-line' which recurses indefinitely. The code is due to Makarius, I'll ask him to investigate.

Debugger entered--Lisp error: (error "Lisp nesting exceeds `max-lisp-eval-depth'")
  (if (not files) nil (let* (... ... ...) (if same ... ...)))
  isar-remove-file("/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/HOL_IsaP.thy" ("/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/Names.thy" "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/EmbeddingNotation.thy" "/afs/inf.ed.ac.uk/group/dreamers/public/software/IsaDev/IsaP-trunk-test/IsaPlanner/src/build/IsaPHOLUtils.thy") nil)
  (cons file (isar-remove-file name rest cmp-base))
  (if same (isar-remove-file name rest cmp-base) (cons file (isar-remove-file name rest cmp-base)))
  (let* ((file ...) (rest ...) (same ...)) (if same (isar-remove-file name rest cmp-base) (cons file ...)))
  (if (not files) nil (let* (... ... ...) (if same ... ...)))
  isar-remove-file("/afs/inf.ed.ac.uk/group/dreamers/public/software

[David Aspinall]

I've fixed, `isar-remove-line' was not recursing indefinitely, but was exhausting the Emacs lisp evaluation depth. Tail recursive version repairs that.