[isabelle-dev] Towards the release

We are slowly moving towards the release. Tomorrow, I will publish an informal snapshot Isabelle2018-RC0 on isabelle-users. Approx. 4 weeks later, there will be Isabelle2018-RC1, still on the isabelle-dev repository. >From 8..15-Jul-2018 I will be at FLoC / Oxford, UK. Afterwards, there will be

Re: [isabelle-dev] Towards the release

We are now definitely past the fork point for the Isabelle2016-1 release. One informal and one formal release candidate have already been published; some more will be coming soon. Here is a summary of the status of the Isabelle development process: *

Re: [isabelle-dev] Towards the release

On 28/10/16 00:10, Makarius wrote: > > The isabelle-dev repository will remain open until Monday 31-Oct-2016, > and then fork to https://bitbucket.org/isabelle_project/isabelle-release The fork will happen in approx. 4h. Afterwards, changes need to be sent by email to me. It is also important

Re: [isabelle-dev] Towards the release

On 23/10/16 18:18, Makarius wrote: > On 12/10/16 11:36, Makarius wrote: >> After the public appearance of Isabelle2016-1-RC0 some days ago, we are >> still in consolidation mode for the Isabelle repository -- lets say at >> least 2 more weeks. >> >> Isabelle2016-1-RC1 will still be based on the

Re: [isabelle-dev] Towards the release

That makes sense. Cheers, Gerwin > On 27 Oct 2016, at 00:25, Makarius wrote: > > On 26/10/16 11:58, Makarius wrote: > >> In the past we've had particularly enthusiastic Mac system >> administration at TUM, but I don't see that at the moment. So I am >> reluctant to

Re: [isabelle-dev] Towards the release

On 26/10/16 11:58, Makarius wrote: > In the past we've had particularly enthusiastic Mac system > administration at TUM, but I don't see that at the moment. So I am > reluctant to change a running system, especially macbroy2, which is very > important for the Isabelle administration and release

Re: [isabelle-dev] Towards the release

On 26/10/16 12:39, Lawrence Paulson wrote: > I see no need for a (?) next to El Capitan. I’ve been using it on multiple > machines for nearly a year. The question mark means that there is no reference system as a proof for platform support. This is required for the following reasons: >>

Re: [isabelle-dev] Towards the release

I see no need for a (?) next to El Capitan. I’ve been using it on multiple machines for nearly a year. Larry > On 26 Oct 2016, at 10:58, Makarius wrote: > > On 26/10/16 00:05, gerwin.kl...@data61.csiro.au wrote: >> I’m planning to switch over to Sierra this week, and can

Re: [isabelle-dev] Towards the release

I’m planning to switch over to Sierra this week, and can hopefully report back next week on any issues with our l4v proofs, AFP, and isabelle itself. Do we know who is administering macbroy30 and macbroy2? It think it would make sense to switch them over to 10.11 and 10.12 (if the hardware is

Re: [isabelle-dev] Towards the release

On 26/10/16 00:05, gerwin.kl...@data61.csiro.au wrote: > I’m planning to switch over to Sierra this week, and can hopefully report > back next week on any issues with our l4v proofs, AFP, and isabelle itself. > > Do we know who is administering macbroy30 and macbroy2? It think it would > make

Re: [isabelle-dev] Towards the release

On 25/10/16 14:29, Jasmin Blanchette wrote: > >> The Windows platform is a bit strange, but there are usually many ways >> to get things through eventually. > > Simon has found a way to avoid "ocamlbuild". It looks like we'll be able to > have the three binaries in place before the branch.

Re: [isabelle-dev] Towards the release

Hi Makarius, > The Windows platform is a bit strange, but there are usually many ways > to get things through eventually. Simon has found a way to avoid "ocamlbuild". It looks like we'll be able to have the three binaries in place before the branch. Nonetheless, Nunchaku will remain labeled as

Re: [isabelle-dev] Towards the release

Le Mon, 24 Oct 2016, Makarius a écrit : > Maybe we can sort out these problems now, within the next few weeks. Is > there a tracker item or other place to see this ocamlbuild isse? https://github.com/ocaml/ocamlbuild/issues/104 and the corresponding flexdll release

Re: [isabelle-dev] Towards the release

On 24/10/16 19:19, Jasmin Blanchette wrote: > >> Are there any non-trivial chunks still in the commit/push pipeline that >> need special considerations? > > I was hoping to push Nunchaku into Isabelle (source code + binary component) > before the release, but we have some issues with ocamlbuild

Re: [isabelle-dev] Towards the release

Hi Makarius, > Are there any non-trivial chunks still in the commit/push pipeline that > need special considerations? I was hoping to push Nunchaku into Isabelle (source code + binary component) before the release, but we have some issues with ocamlbuild on Windows. Would it make sense to push

Re: [isabelle-dev] Towards the release

On 12/10/16 11:36, Makarius wrote: > After the public appearance of Isabelle2016-1-RC0 some days ago, we are > still in consolidation mode for the Isabelle repository -- lets say at > least 2 more weeks. > > Isabelle2016-1-RC1 will still be based on the isabelle-dev repository, > to simplify

Re: [isabelle-dev] Towards the release

That would be great! I believe that Gauss’s law of quadratic reciprocity and Wilson’s theorem were never ported To Number_Theory. Larry > On 13 Oct 2016, at 17:36, Manuel Eberl wrote: > > I for one am hoping to be able to get rid of the Old Number Theory > before the

Re: [isabelle-dev] Towards the release

I for one am hoping to be able to get rid of the Old Number Theory before the release. All that is left to do is actually to adapt some theories of the ported theories to my recent changes concerning prime numbers, so I think I should be able to take care of that next week. Cheers, Manuel On

Re: [isabelle-dev] Towards the release

> Are there any non-trivial chunks still in the commit/push pipeline that > need special considerations? I have some matter on euclidean division in the pipeline which I hope to be able to finish before my vacation starting at end of October. Florian -- PGP available:

[isabelle-dev] Towards the release

After the public appearance of Isabelle2016-1-RC0 some days ago, we are still in consolidation mode for the Isabelle repository -- lets say at least 2 more weeks. Isabelle2016-1-RC1 will still be based on the isabelle-dev repository, to simplify immediate reactions on suggestions and observations

Re: [isabelle-dev] Towards the release

On Wed, 20 Jan 2016, Makarius wrote: Around 19:00 GMT 20-Jan-2016 the fork of isabelle-dev versus isabelle-release will happen (see (https://bitbucket.org/isabelle_project/isabelle-release) There are a few hours left to push refinements and clarifications on the regular isabelle-dev

Re: [isabelle-dev] Towards the release

We are now past the fork point for the Isabelle2016 release. One informal and one formal release candidate have already been published; more will be coming soon. Here is a summary of the status of the Isabelle development process: * https://bitbucket.org/isabelle_project/isabelle-release/

Re: [isabelle-dev] Towards the release

Important update of the situation: Around 19:00 GMT 20-Jan-2016 the fork of isabelle-dev versus isabelle-release will happen (see (https://bitbucket.org/isabelle_project/isabelle-release) There are a few hours left to push refinements and clarifications on the regular isabelle-dev

Re: [isabelle-dev] Towards the release

Current Isabelle/9ca00b65d36c and AFP/2c322507b8a6 appears to be a fairly stable state, so I will take this as starting point for Isabelle2016-RC1 later today. The main isabelle-dev remains open a few more days for fine-tuning and consolidation. Makarius

Re: [isabelle-dev] Towards the release

On Mon, 4 Jan 2016, Manuel Eberl wrote: I completed the merge I mentioned in my previous email. Fine. This is Isabelle/b0f941e207cf. Do you want to write an entry for NEWS and CONTRIBUTORS? Makarius ___ isabelle-dev mailing list

Re: [isabelle-dev] Towards the release

Ah yes, I completely forgot about that. Will do. On 05/01/16 14:27, Makarius wrote: On Mon, 4 Jan 2016, Manuel Eberl wrote: I completed the merge I mentioned in my previous email. Fine. This is Isabelle/b0f941e207cf. Do you want to write an entry for NEWS and CONTRIBUTORS? Makarius

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

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

Re: [isabelle-dev] Towards the release

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

Re: [isabelle-dev] Towards the release

On Fri, 1 Jan 2016, Lawrence Paulson wrote: I'm still working on a major theorem. It would be nice to include it if possible. Do you have a time estimate for that? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Towards the release

I'm still working on a major theorem. It would be nice to include it if possible. However, I have no major changes on the order of the real vs of_nat rationalisation. Larry > On 1 Jan 2016, at 19:24, Makarius wrote: > > Isabelle2016-RC0 is published, but we are still in

[isabelle-dev] Towards the release -- Bitbucket

Dear all, this week is left for finalizing the regular Isabelle repository for the release. Then the usual fork to the isabelle-release repository will happen, and release candidates appear for public testing on isabelle-users like last time. Some very quick guys have already started

Re: [isabelle-dev] Towards Isabelle2011 release

On Thu, 27 Jan 2011, Makarius wrote: Yet another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ There is now an update of the same isa2011-test3 with a patched version of ProofGeneral-4.1pre110112 as follows: * Mac OS X fonts: instead of IsabelleText refer to

Re: [isabelle-dev] Towards Isabelle2011 release

On Fri, 28 Jan 2011, Makarius wrote: On Thu, 27 Jan 2011, Makarius wrote: Yet another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ There is now an update of the same isa2011-test3 with a patched version of ProofGeneral-4.1pre110112 as follows: * Mac OS X fonts:

Re: [isabelle-dev] Towards Isabelle2011 release

Yet another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ Some odd problems have shown up and addressed as follows: * contrib/z3: make native Windows executables actually work on x86-cygwin * quickcheck/codegen: eliminated serious race condition * slightly more

Re: [isabelle-dev] Towards Isabelle2011 release

I get a (minor) error when running this version (MacOS 10.6, double-clicking on isa2011-test2.app icon): if I have theory file being processed, and I quit Isabelle/Aquamacs, I get a dialogue box telling me that I have active processes, and do I want to kill them. If I say yes, then I get a

Re: [isabelle-dev] Towards Isabelle2011 release

On Tue, 25 Jan 2011, Lucas Dixon wrote: Seems to be coming from the Isabelle application wrapper: Scenario 2: I start-up by Aquamacs directly - not via the Isabelle icon, using my emacs settings which starts PG using the load-file command, then when I quit (by command-Q). In this case, I

Re: [isabelle-dev] Towards Isabelle2011 release

On Mon, 24 Jan 2011, Makarius wrote: * ProofGeneral-4.1pre110112: deleted .elc files on Linux to improve compatibility with GNU Emacs 23.1.x instead of 23.2.1 It is also unclear when exactly PG 4.1-final will be released this week. We stick with ProofGeneral-4.1pre110112 for the

Re: [isabelle-dev] Towards Isabelle2011 release

Here is another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test2/ while the main Isabelle code base seems to be in good shape, there are various issues with the overall integration of external tools on the different platforms that we support officially. Some of them have

[isabelle-dev] Towards Isabelle2011 release

On Sat, 15 Jan 2011, Makarius wrote: The actual test branch for Isabelle2011 will probably start within the next few days -- on a separate repository clone where submission of changesets works via email or pull only. It looks like the point zero will be today, either in the afternoon or

Re: [isabelle-dev] Towards Isabelle2011 release

On Mon, 17 Jan 2011, Makarius wrote: It looks like the point zero will be today, either in the afternoon or evening (GMT). As of version 54a4512e29a6 the release branch continues at http://isabelle.in.tum.de/repos/isabelle-release * Any urgent changes that need to go onto that need to be

Re: [isabelle-dev] Towards Isabelle2011 release

On Mon, 17 Jan 2011, Makarius wrote: On Mon, 17 Jan 2011, Makarius wrote: It looks like the point zero will be today, either in the afternoon or evening (GMT). As of version 54a4512e29a6 the release branch continues at http://isabelle.in.tum.de/repos/isabelle-release This also means that