Re: [isabelle-dev] AFP still broken (AList vs. Assoc_List)
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
Re: [isabelle-dev] Towards the Isabelle2015 release
If all goes well, there will be Isabelle2015-RC1 today in the evening. Until then there is still the opportunity to update NEWS and CONTRIBUTORS, which are also relevant for the website. The publication of Isabelle2015-RC1 does not yet mean a fork of the repository yet: there will be a few more days to sort out reported problems directly in the main Isabelle repository. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: [isabelle] Changing definition of finprod
This sounds like a good proposal to me. Do we have time before the fork? Larry > Begin forwarded message: > > From: "Thiemann, Rene" > Subject: [isabelle] Changing definition of finprod > Date: 17 April 2015 10:55:32 BST > To: Cl-isabelle Users > > Dear all, > > recently I started to formalize linear algebra results based on HOL-Algebra > (Matrices, Determinants, Eigenvalues, Gauss-Jordan-Elimination, …) > > while doing this I noticed a annoying difference between setprod and finprod > (or setsum and finsum): > the set-based variants define the sum or product of an infinite set as the > neutral element, whereas finsum and finprod take „undefined“. > > To have more similarity between the two operators I propose to change the > definition of finprod from „undefined“ to 1 (which entails 0 for finsum). > > Then a lot of lemmas for finprod and finsum can be simplified where often the > assumption „finite A“ is now obsolete (and they more closely relate to > corresponding setprod and setsum lemmas). > > If this change is appreciated, then can someone please include the following > patch? > It adapts all of HOL/Algebra to the change and also those entries of the AFP > which rely on HOL-Algebra still compile > (Free-Groups Jordan_Hoelder Koenigsberg_Friendship Lehmer Matrix > Perfect-Number-Thm Secondary_Sylow Tarskis_Geometry VectorSpace) > > I tested everything with Isabelle 8614f8f0fb4b and AFP 7c57eabaad4b. > > Best regards, > René > finprod.patch Description: Binary data > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: isabelle build -X
* The Isabelle tool "build" provides new options -X, -k, -x. This refers to Isabelle/e0d1d9203275. At the risk of using up all the alphabet for options eventually, there is now the possibility to exlude session groups systematically. This is particularly relevant for AFP/662e7aa68008, to save some hours of manual testing: isabelle build -d '$AFP' -a -X slow Here are the results for the slow group alone on my modest home machine (12 cores Xeon using -j4 and 6 ML threads): Finished JinjaThreads (0:38:02 elapsed time, 3:00:37 cpu time, factor 4.74) Finished ConcurrentGC (0:49:40 elapsed time, 2:26:41 cpu time, factor 2.95) Finished AODV (1:41:31 elapsed time, 8:46:49 cpu time, factor 5.18) About 10 years ago, tiny sessions like MicroJava required 45min elapsed time. We are a bit better than that today, but there is also a tendency of many people sticking to old hardware, and expecting that things are still fast. Moore's Law means that hardware is continously updated by cheaper and faster machines. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Changing definition of finprod
On Fri, 17 Apr 2015, Larry Paulson wrote: This sounds like a good proposal to me. Do we have time before the fork? Begin forwarded message: From: "Thiemann, Rene" Subject: [isabelle] Changing definition of finprod Date: 17 April 2015 10:55:32 BST To: Cl-isabelle Users I tested everything with Isabelle 8614f8f0fb4b and AFP 7c57eabaad4b. I will take care of that. We have yet another confusion of the mailing lists. The most simple syntactic check is this: if it is about particular changesets for particular repository versions it is for isabelle-dev; anything else about official releases or release candidates is for isabelle-users. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] AFP works
Just for the historical record: in Isabelle/caf2637a28a9 all of AFP/a44a0c9e17ef works. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On 04/17/2015 12:04 AM, Makarius wrote: On Tue, 7 Apr 2015, Christian Sternagel wrote: PS: I'm still waiting for isabelle build -n -a -d '$AFP' -k qualified to finish (but I guess proper checking, taking semantics into account, is just expensive). Oops, while writing this email I obtained: *** java.lang.OutOfMemoryError: Java heap space 0:03:32 elapsed time, 0:05:46 cpu time, factor 1.63 (Maybe because in parallel I am still waiting on isabelle build -v -n -a -d '$AFP' -k hidden -k private ? Which seems to "hangs" at "Session Pure/RAW" now for several minutes.) Maybe this is just the normal behaviour of the JVM under low-memory conditions. I routinely have local settings like this: ISABELLE_BUILD_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m" Thanks for the hint! This even worked with two "checks" running in parallel (each of which finished in less than 4 minutes). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the Isabelle2015 release
After the announcement of Isabelle2015-RC1 there are 48 more hours on the main Isabelle repository, before the critical fork to https://bitbucket.org/isabelle_project/isabelle-release happens. Then we will have several weeks of separate Isabelle repository development, and final convergence of the release branch, until everything is merged again at the end of May or start of June. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
