On Tuesday 23 Nov 2004 11:45, you wrote:

Can you give me some more information about this? I've just downloaded the source for 2.6.9-1.6_FC2 and built a kernel from that. Poly/ML runs fine using either the development version or the 4.1.3 RPM from polyml.org . Are you using a pre-built kernel and if so which one? Run uname -r if you're not sure.

It's a custom build from the kernel source distributed by Debian.

I'm guessing Brent is probably running a kernel with similar patch set, given his email address.

Martin

Another warning --- at least for people who use FC3 and automatically upgrade with e.g. yum or up2date: I've just upgraded to kernel 2.6.11-1.14_FC3 and now get segmentation faults on PolyML startup. (The previous kernel 2.6.10-1.770_FC3 still works.) This is the first (pre-built) kernel distributed with Fedora Core to have had this problem and it should be easy to reproduce.

[phil@pclayton phil]$ poly Poly/ML RTS version I386-4.1.3 (14:28:57 Sep 30 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Segmentation fault [phil@pclayton phil]$ uname -a Linux pclayton.eris.qinetiq.com 2.6.11-1.14_FC3 #1 Thu Apr 7 19:23:49 EDT 2005 i686 i686 i386 GNU/Linux

Phil

David Matthews wrote:

Martin Ellis wrote:

...

Lest anyone be planning an upgrade, I get segmentation faults on PolyML startup using Linux 2.6.9 (using PolyML as distributed with Isabelle). Maybe it's just me though.

2.6.8.1 seems fine though.

Can you give me some more information about this? I've just downloaded the source for 2.6.9-1.6_FC2 and built a kernel from that. Poly/ML runs fine using either the development version or the 4.1.3 RPM from polyml.org . Are you using a pre-built kernel and if so which one? Run uname -r if you're not sure.

David. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

On Wednesday 13 Apr 2005 19:03, David Aspinall wrote:

Philip Clayton wrote:

...

This is the first (pre-built) kernel distributed with Fedora Core to have had this problem and it should be easy to reproduce.

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.

Yes, I'm also seeing it, on both my FC3 machines. A nuisance, as I have been planning to make a LiveCD with Isabelle on it next month, based on the latest FC release.

You know about this? Or you want FC3 specifically? http://www.brucker.ch/projects/isamorph/index.en.html

Martin

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.