AKCL malloc on HP 700 ?

[hall@leopard.cs.uidaho.edu (Kelly Hall)]

Hello,

I've been running into problems with the HOL proof assistant on our HP 730,
and I think my problem might be related to the malloc used by AKCL.

On large proofs, the 730's load goes very high, becomes excrutiatingly
slow, and generally becomes useless.  When we run 'top' to see what's
taking up so much time, we find that the hol process is at around 2%, all
other user processes are virtually stopped, and very little system work is
happening.  Our guess is that some resource is getting scarce, and
everything is waiting for that resource.

Our system disk still has lots of room, and there's lots of swap space
remaining.  I regret I don't know if the system disk was thrashing when the
machine slowed down.

These symptoms seem to point to a ill-behaved malloc, at least in my mind.
My question is, is there an easy way to comment out the GNU malloc and
related code and use the standard HPUX malloc?  This might not fix our
problem, but it would verify that AKCL wasn't the problem.

BTW, this isn't the problem we get when compiling large (AKCL made) C files
with the HPUX C compiler.

Thanks for any advice or insight,
Kelly
--
Kelly Hall == hall@leopard.cs.uidaho.edu
no disclaimer, no cute quotes