For the record:
> Running on host lxbroy10
> isabelle: fc53fbf9fe01 tip
> afp: 835c7e115feb tip
> Running ConcurrentGC ...
> Finished ConcurrentGC (1:08:48 elapsed time, 5:15:14 cpu time, factor 4.58)
> 1:21:59 elapsed time, 5:53:13 cpu time, factor 4.30
This seems to be fine now.
Thanks to all who have invested time and energy to work on those issues.
Nevertheless I have the impression that in the last time there have have
been lots of movements in the distribution being speculative in the
sense that no systematic testing including the AFP had taken place.
What is the
Hi Florian,
> What is the reason for this? No access to suitable computing machines?
currently, the "new" testboard only performs "makeall" on the
distribution. As I wrote in my mail from yesterday, I'm working on it. I
expect to be able to make a recommendation on how to reinstate regular
I am partly to blame. The changes involving the “real” function caused a lot of
disruption. I needed a week to get all of Isabelle/HOL working again, and
thought it a more practical option to tackle the AFP failures after they
occurred. Most of them were only out of action for a day.
Larry
>
Am Sonntag, den 15.11.2015, 11:43 +0100 schrieb Andreas Lochbihler:
> Vickey_Clarke_Groves looks related to the changes to "real", but I
> have not tried to fix this.
This should be fixed now in AFP e6d87060e398.
- Johannes
___
isabelle-dev mailing
isabelle: f1b257607981 tip
afp: 1a688183b05a tip
Any idea what is going on here?
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Running ConcurrentGC ...
Running MonoBoolTranAlgebra ...
Running
MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal
of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but
just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016.
Presburger-Automata had a looping
