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
