[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Florian Haftmann]

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.haftmann at 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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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

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