I said yesterday that these instructions work --- they give me a poly driver which I can use OK with old heap images, but unfortunately compiling a new Isabelle image crashes (just my luck, during proof_general.ML). Also with "use" at the command line I get immediate exits on some files.
- D.
signature PROOF_GENERAL = sig val full_proofs : bool -> unit val help : unit -> unit val inform_file_processed : string -> unit val inform_file_retracted : string -> unit val init : bool -> unit val init_pgip : bool -> unit val isa_restart : unit -> unit val isarcmd : string -> unit val kill_goal : unit -> unit val preferences : (string * (string * (string * (string * ... * ...))) list) list ref val process_pgip : string -> unit val repeat_undo : int -> unit val setup : (Theory.theory -> Theory.theory) list val show_context : unit -> Theory.theory val thms_containing : string list -> unit val try_update_thy_only : string -> unit val update_thy_only : string -> unit val write_keywords : string -> unit val xmls_of_str : string -> string list end catchSEGV; &context = 0x809a5e8, in_run_time_system=1, context.trapno=14
Martin Ellis wrote:
This page suggests that you might be able to get away with just rebuilding the 'driver' directory from the development sources if you want to run (reliably) with a recent kernel: http://www.polyml.org/linuxsegfault.html
David M. pointed me at this a couple of days ago, but I haven't managed to check this yet.