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

[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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ConcurrentGC.patch
Type: application/octet-stream
Size: 1774 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151116/2bec1ba5/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ConcurrentGC.gz
Type: application/x-gzip
Size: 224330 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151116/2bec1ba5/attachment-0002.bin>
-------------- next part --------------


> 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

-- 
http://peteg.org/