[isabelle-dev] Fwd: status (AFP)

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Sep 18 14:37:38 CEST 2011


> *** 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.


> 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) 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.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110918/0dd59deb/attachment.sig>


More information about the isabelle-dev mailing list