Can you minimize the test-case into a minimal program that still segfaults? This might be tricky with the unsafeCoerces around, since deleting instructions probably will be break any invariants your coerces are relying on. Maybe you can reduce the Coq itself, or make the test case smaller.
It seems pretty plausible that there might be a bug in the actual extraction code (after all, you can't actually formalize that.) Can you (perhaps manually) eliminate as many unsafe coercions as possible? Edward Excerpts from Adam Megacz's message of Wed Apr 20 15:04:42 -0400 2011: > > So, I have a situation where my modified GHC is segfaulting. All > compilation is done with -O0. I'm sort of hoping for suggestions on how > to continue figuring this out. > > I've tried all of the suggestions on these pages, short of using gdb: > > http://hackage.haskell.org/trac/ghc/wiki/Debugging > http://hackage.haskell.org/trac/ghc/wiki/Debugging/CompiledCode > > The code which segfaults is a Haskell extraction of a Coq program. Now, > this is a tricky situation because: > > 1. In theory, Coq extractions should never segfault, since they've > been type-checked by Coq. To my understanding, the correctness > proof for the extraction is based on type-erased dynamic semantics > (i.e. proves type-ignorant reduction never gets stuck) rather than > any sort of reduction to the static semantics of Haskell (which > probably isn't possible). > > 2. Coq extractions use unsafeCoerce, since Haskell doesn't have > full-spectrum dependent types. Using unsafeCoerce is sort of a > "all bets are off" situation. > > The really strange part is this: if I modify the extraction machinery > and wrap every subexpression "e" as "(trace e)" where trace is: > > trace x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x > > Everything works perfectly (though very slowly)! I stumbled upon this > solution in the process of inserting tracing code. I guess this makes > it a Heisenbug. > > Perhaps the "trace" calls are defeating some GHC optimization (which is > enabled even at -O0), and that optimization indirectly relies on the > fact that there are no value-indexed types in Haskell? > > FWIW, the segfault happens even in ghc-stage1, built using 6.12, so this > isn't a behavior introduced by GHC7. > > Thanks in advance for any hints, no matter how vague. I'm anxious to > get rid of the nasty hack above. > > - a > _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
