I believe Gerwin already reported this in some email, and I can confirm it: the afp test hangs even on my own laptop. The trace:
lapbroy100:AFP nipkow$ isabelle afp_build -A Building Jinja ... Finished Jinja (0:05:06 elapsed time, 0:15:28 cpu time, factor 3.03) Building LatticeProperties ... Finished LatticeProperties (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.69) Building HOL-Probability ... Finished HOL-Probability (0:01:47 elapsed time, 0:05:10 cpu time, factor 2.89) Building Group-Ring-Module ... Finished Group-Ring-Module (0:02:50 elapsed time, 0:08:24 cpu time, factor 2.96) Building Simpl ... Finished Simpl (0:02:05 elapsed time, 0:05:35 cpu time, factor 2.68) Building Collections ... Finished Collections (0:04:51 elapsed time, 0:11:08 cpu time, factor 2.29) Building Refine_Monadic ... And this is where it ends. No more activity: CPU usage: 0.23% user Can anybody still build the AFP on some machine? Tobias Am 03/12/2012 06:38, schrieb 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 <[email protected]> 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 >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
