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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
