[isabelle-dev] Fwd: status (AFP)

[Gerwin Klein]

On 18/09/2011, at 10:37 PM, Florian Haftmann wrote:

>> *** Undeclared constant: "semilattice_sup_class.sup"
>> *** At command "definition" (line 20 of "/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
>> val it = (): unit
>> Exception- TOPLEVEL_ERROR raised
>> *** ML error
>> 
>> It looks like something in the class setup changed slightly. Could somebody who is more up-to-date in this area have a look, please?
> 
> Done.

Thanks. I've set the JinjaThreads test to run every day now, at least until the release.


>> After not running in the test for quite some time, JinjaThreads now
> comes back failing
> 
> This is one of the principal problems we have with JinjaThreads and
> FlyspeckTame that they don't run (more exactly, don't terminate)

JinjaThreads does terminate ;-), it just runs out of memory.

Flyspeck has always taken very long, but it terminates eventually.


> on our
> reference machines (macbroyXY, Apple IMac) since one year.  Somehow we
> must come to a solution for this, or at least figure out why this
> happends.  The mere size or massive computations alone cannot be the
> only reason for this.

It would certainly be nice to figure out where the memory is going in these computations and maybe even speed them up.

I have yet to pick up similar investigations for our seL4 proofs again. At least with the current polyml svn version, you can get more precise numbers on memory than before.

Cheers,
Gerwin