Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)

On 13/09/12 22:23, David Matthews wrote:
On 13/09/2012 02:34, Rafal Kolanski wrote:
Yes, we ended up doing that, and now we're back to PolyML segfaulting
with -q 2. David seems to be applying quite a few fixes to the GC
though, so we have high hopes of getting it working soon.

I have fixed all the segfaults I am aware of with the GC and I'm on the
point of releasing SVN 1594 as Poly/ML 5.5.  If you have an example that
consistently fails I will investigate.  However, I need as much detail
as possible and if at all possible a script that I can run to reproduce
it.  Bear in mind that I know absolutely nothing about using Isabelle so
it needs to be foolproof.

I will be testing that as my third task for today, so fingers crossed. It's unlikely if anything goes wrong I'll be able to give you a reproducible script though. The errors I've seen so far are always of the kind "PolyML segfaults sometimes when building large images" :/

I really wish that there was some way to get exception traces again when working interactively in Isabelle. You have already said you don't know much about using Isabelle, but perhaps someone here knows a trick? There already is a nice debugging interface built into PolyML, I just don't know how to use it while working with a theorem prover.


Rafal Kolanski.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.