Extremely poor GC performance in SML/NJ >= 110.41

[Christopher Richards]

A query for the SML/NJ hackers reading the group:

When the GC leak was fixed in 110.41, my application's performance
degraded by an order of magnitude. (I'm using Frank Pfenning's Twelf
system to type/proof-check several megabytes of LF terms.)

For Twelf running on a ~10 MB data set, the timings look like this:

110.40: 70.93s real 54.78s user 3.64s system
110.42: 686.71s real 540.85s user 139.23s system

As a consequence, versions >= 110.41 are completely unusable for me
and several others here.

Is there a way to fix the GC leak without this significant slowdown?

--
Chris

[Matthias Blume]

We are generally aware of this problem and intend to fix it. (It
hasn't happened yet due to various time constraints.)

Please, notice that some important SML/NJ developers do not read any
netnews, so posting bug reports here is less useful than you might
think. The preferred way is to send a bug report to the SML/NJ
development mailing list.

We are currently moving that list to a new home, so take a note:

ten tod egrofecruos tod stsil ta tsil hsad ved hsad jnlms

[Reverse this line and put in proper punctuation (at->'@', dot->'.',
dash->'-'). I scrambled the address to thwart spammers.]

Matthias

Christopher Richards <richard...@CS.Princeton.EDU> writes:

--
-Matthias

[Rob Arthan]

Christopher Richards wrote:

Using Poly/ML rather than SML/NJ might help. My experience with ProofPower
and the experience of many others with Isabelle indicates that Poly/ML is
much faster and much leaner than SML/NJ for type-checking and
theorem-proving applications. Sadly, when I tried it, it looked like
there's some work to do to twelf to make it compile under Poly/ML.

Rob Arthan (r...@lemma-one.com)