[isabelle-dev] AFP devel broken

[Gerwin Klein]

After looking at this over the weekend, the problem still escapes me.

On macbroy2 when using the installation in ~/afp/isadist/Isabelle (basically the last built development snapshot), the session HOL-Probability with a high probability just hangs. This can be confirmed interactively:

macbroy2:Probability isatest$ pwd
/home/isatest/afp/isadist/Isabelle/src/HOL/Probability
macbroy2:Probability isatest$ ~/afp/isadist/Isabelle/bin/isabelle tty -l HOL-Multivariate_Analysis
> val it = (): unit
val commit = fn: unit -> bool
Unofficial version of Isabelle/HOL-Multivariate_Analysis (Isabelle repository snapshot 38870ee59311 02-Dec-2012)
> use_thy "Probability";

just hangs (also doesn't react to Ctrl-C). Copying the isadist directory to my laptop and linking it with the corresponding contrib directory built that session just fine in under 2 min.

Any ideas anyone?

I'm tempted to move the whole AFP test to a different machine just to get things going again, it's been quite a while since we've had any solid test results.

Gerwin


On 29/11/2012, at 11:47 PM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote:

> On 11/09/2012 12:26 AM, Christian Sternagel wrote:
>> Just follow the "Browse theories" link of any devel entry, e.g.,
>> http://afp.sourceforge.net/browser_info/devel/HOL/Bondy/index.html
> As far as I can tell the problem still remains. Is it known in the meantime what the problem is?
> 
> cheers
> 
> chris
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>