Opened 15 years ago
Closed 15 years ago
#274 closed defect (fixed)
Max lisp nesting exceeded on large error outputs
Reported by: | David Aspinall | Owned by: | Makarius |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.0 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
[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.
Change History (6)
comment:1 Changed 15 years ago by
Status: | new → accepted |
---|
comment:2 Changed 15 years ago by
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
comment:3 Changed 15 years ago by
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.
comment:4 Changed 15 years ago by
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"). >
comment:5 Changed 15 years ago by
Owner: | changed from David Aspinall to Makarius |
---|---|
Status: | accepted → assigned |
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
comment:6 Changed 15 years ago by
Resolution: | → fixed |
---|---|
Status: | assigned → closed |
I've fixed, `isar-remove-line' was not recursing indefinitely, but was exhausting the Emacs lisp evaluation depth. Tail recursive version repairs that.
A first attempt to reproduce with this way of generating an 80,000 line 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.