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.
Florian
Am 16.11.2015 um 17:17 schrieb Peter Gammie:
> For:
>
> isabelle: e6784939d645
> afp: e6d87060e398
>
> the attached patch makes ConcurrentGC go through under Isabelle/JEdit. I
> waited ~ 4 CPU hours for the batch build before killing it. I cannot read the
> log files that Isabelle generates now, so I do not know what proof I
> interrupted. Sorry about that. I’ve attached the log in case it has value to
> someone. The log from isatest also does not have enough useful context.
>
> It seems that the simplifier got smarter about the option datatype.
>
> cheers,
> peter
>
>
>
>
>
>> On 15 Nov 2015, at 16:38, Florian Haftmann
>> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>>
>> 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
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
