Re: [isabelle-dev] Towards the release
I'm currently cleaning up the Central Limit Theorem, and I want to it entirely to HOL-Probability. I hope to finish this in 1 week, to get it into Isabelle 2016. - Johannes Am Freitag, den 01.01.2016, 20:24 +0100 schrieb Makarius: > Isabelle2016-RC0 is published, but we are still in normal incremental > change mode on the isabelle-dev repository. > > This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, > and the > website. > > > Are there bigger changes still in the pipeline? Larry are you > finished > with the ports from HOL Light, as far as Isabelle2016 is concerned? > > Depending on that, the fork point for the release will be a bit > sooner or > later. Lets say in about 2 weeks. Hopefully, Oracle manages to > deliver > the next Java 8 update in 3 weeks, as scheduled. > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the release
I completed the merge I mentioned in my previous email. Everything went into Multivariate_Analysis, apart form Nonpos_Ints and Periodic_Fun, which went into Library. I'm running tests overnight to make sure I did not break anything. Manuel On 01/01/16 20:50, Manuel Eberl wrote: I still have a few thousand lines of stuff to merge into the distribution, most notably the definition of the radius of convergence of a series and a number of convergence tests. This would be nice to have in the distribution because two results of mathematical importance rest upon it: the Gamma function and the Generalised Binomial Theorem. The work itself is already, all that remains is to merge it into the distribution. I put the files in this repository if anyone wants to look at them: https://github.com/3of8/isabelle_summation The only files that require any real merging (as opposed to just copying the file into the distribution) are Summation.thy, Extended_Real_Lemma_Bucket.thy, and Liminf_Limsup_Lemma_Bucket.thy. The file "Concave.thy" is not required by the rest and does not need to be merged. None of this really has to end up in Isabelle2016; I can also wait for the next release. My plan was to meet with Johannes and Fabian after the holidays and ask them for their opinions on this material. Cheers, Manuel On 01/01/16 20:24, Makarius wrote: Isabelle2016-RC0 is published, but we are still in normal incremental change mode on the isabelle-dev repository. This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, and the website. Are there bigger changes still in the pipeline? Larry are you finished with the ports from HOL Light, as far as Isabelle2016 is concerned? Depending on that, the fork point for the release will be a bit sooner or later. Lets say in about 2 weeks. Hopefully, Oracle manages to deliver the next Java 8 update in 3 weeks, as scheduled. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] CoreC++ broken
I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know what exactly went wrong or what caused the failure. The problem seems to be related to some change in theory imports. It seems as if code_pred cannot retrieve the specification of a constant under certain import orders, but I am not familiar enough with these Isabelle internals to pinpoint the problem. Andreas On 30/12/15 00:20, Makarius wrote: AFP/CoreC++ is broken (already quite some time). The current situation: Isabelle/a70b89a3e02e AFP/a2c981ab8d39 CoreC++ FAILED *** Failed to load theory "CoreC++" (unresolved "Execute") *** No such predicate: "SubObj.path_via" *** At command "code_pred" (line 214 of "~/isabelle/afp-devel/thys/CoreC++/Execute.thy") Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
