[isabelle-dev] AFP still broken (AList vs. Assoc_List)

[Tobias Nipkow]

Thanks for alerting me. I just fixed it.

Tobias

On 16/04/2015 22:49, Makarius wrote:
> In Isabelle/f5c4b49c8c9a and AFP/420dac7d9446 from today the situation of
> various AFP sessions is as bad as some days ago:
>
> Promela FAILED
> (see also /home/makarius/.isabelle/heaps/polyml-5.5.3_x86-linux/log/Promela)
>
> *** At command "by" (line 1082 of
> "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy")
> *** Failed to finish proof (line 1083 of
> "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy"):
> *** goal (1 subgoal):
> ***  1. [| lsl = Assoc_List.impl_of ls;
> ***        delete_aux k (update_with_aux v k (%_. v) (Assoc_List.impl_of ls)) =
> ***        Assoc_List.impl_of ls |]
> ***     ==> Assoc_List
> ***          (AList.delete_aux k
> ***            (AList.update_with_aux v k (%_. v) (Assoc_List.impl_of ls))) =
> ***         ls
> *** At command "by" (line 1083 of
> "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy")
> *** Failed to finish proof (line 1061 of
> "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy"):
> *** goal (1 subgoal):
> ***  1. [| lsl = Assoc_List.impl_of ls;
> ***        update_with_aux v k (%_. v) (Assoc_List.impl_of ls) =
> ***        Assoc_List.impl_of ls |]
> ***     ==> Assoc_List
> ***          (AList.update_with_aux v k (%_. v) (Assoc_List.impl_of ls)) =
> ***         ls
> *** At command "by" (line 1061 of
> "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy")
>
>
> I am desparately trying to find a locally stable point to make Isabelle2015-RC1
> -- the official start for several weeks of testing towards Isabelle2015 (May
> 2015), but it is likely to become June 2015 instead.
>
>
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150417/dee74339/attachment.bin>