[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 the repository fork and Isabelle2018-RC2. At least that is the plan right now. There are still many details to be sorted out. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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: * https://bitbucket.org/isabelle_project/isabelle-release/ is where the final release preparations happen before roll-out in a few weeks. The starting point is https://bitbucket.org/isabelle_project/isabelle-release/commits/73859eb8d1fe * http://isabelle.in.tum.de/repos/isabelle is back in post-release mode right now (changeset 2bafda87b524). Anything pushed there is for the next release after Isabelle2016-1. * AFP needs to be understood wrt. isabelle-release at the moment. Gerwin will explain when and how a fork of afp-devel (presently at 022d752f6426) vs. afp-2016-1 happens. * http://isabelle.in.tum.de/devel follows the isabelle-release repository -- I plan to make a bit more generated website content soon. * isabelle-users is the place to discuss Isabelle2016-1-RC versions. * isabelle-dev is the place to discuss ongoing post-release development. The isabelle-release repository has no public push access. Any changes that are relevant for the release need to be sent to me via email (produced by "hg export" or "hg bundle"). Changesets need to be prepared from a current state of isabelle-release, not the ongoing post-release development, and applied to only one of the two repository branches. Changes to the actual code base should be limited to really important things. During the forked state of the two repositories, big upheaveals on the isabelle repository should be avoided, so that the isabelle-release branch can be merged back cleanly after several weeks; but it is better to publish changes now than to stockpile them for a long time. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 to make sure that material meant for this release is not pushed at the wrong time in the wrong place. The isabelle-dev post-release state will look again like this: http://isabelle.in.tum.de/repos/isabelle/rev/5fb86150a579 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 isabelle-dev repository, >> to simplify immediate reactions on suggestions and observations by testers. >> >> The repository fork to isabelle-release will happen after RC1. > > We are more or less on schedule. Isabelle2016-1-RC1 is anticipated > towards the end of the week (around 28-Oct-2016). The isabelle-rev > repository will remain open a few days afterwards to facilitate > immediate reactions by early adopters. That is today. I will prepare Isabelle2016-1-RC1 in the evening of Friday 28-Oct-2016. The isabelle-dev repository will remain open until Monday 31-Oct-2016, and then fork to https://bitbucket.org/isabelle_project/isabelle-release Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 change a running system, especially macbroy2, which is very >> important for the Isabelle administration and release process. >> >> After the release, we can probably discontinue Mountain Lion, and update >> macbroy30 to El Capitan or Sierra. Both macbroy30 and macbroy31 are >> MacBookPro6,2 from Mid 2010, so it looks like Sierra still works, but >> that might be also the latest possible version. > > I have had a chat with the system administration at TUM. We can keep up > the status quo with some minor updates, but not much more. > > So the present plan is this: > > * After the release of Isabelle2016-1 (December 2016) we discontinue > support for 10.8 Mountain Lion and update macbroy30 to 10.12 Sierra > (probably the ultimate version that is possible on this hardware). > > * After one more release cycle by Apple (2017?) we discontinue support > for 10.9 Mavericks and update macbroy2 to 10.11 El Capitan (definitely > the ultimate version that is possible on this hardware). > > > This means we hold up the standard of approx. 4 versions of Apple's OS, > whatever its name might be next year. > > > Makarius > > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 process. > > After the release, we can probably discontinue Mountain Lion, and update > macbroy30 to El Capitan or Sierra. Both macbroy30 and macbroy31 are > MacBookPro6,2 from Mid 2010, so it looks like Sierra still works, but > that might be also the latest possible version. I have had a chat with the system administration at TUM. We can keep up the status quo with some minor updates, but not much more. So the present plan is this: * After the release of Isabelle2016-1 (December 2016) we discontinue support for 10.8 Mountain Lion and update macbroy30 to 10.12 Sierra (probably the ultimate version that is possible on this hardware). * After one more release cycle by Apple (2017?) we discontinue support for 10.9 Mavericks and update macbroy2 to 10.11 El Capitan (definitely the ultimate version that is possible on this hardware). This means we hold up the standard of approx. 4 versions of Apple's OS, whatever its name might be next year. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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: >> Generally, the reference systems according to Isabelle/Admin/PLATFORMS >> are required for three main purposes: >> >> * Compilation of Isabelle components (via ssh) -- on the *oldest* >> supported version. >> >> * Routine batch-builds of Isabelle + add-on tools -- on *all* >> supported versions. This is usually done by the administrative cronjob. >> >> * Occasional interactive tests (via Screen Sharing), to figure out GUI >> portability problems, to test the Isabelle.app integration etc. Before we introduced these reference systems, platform support was less systematic, and generally less ambitious. That was before 2007/2008. Makarius ___ 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 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 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 still >> supported). > > The PLATFORMS file documents the current situation for Isabelle support > of certain Mac OS X versions, see > http://isabelle.in.tum.de/repos/isabelle/file/4f0acbd97491/Admin/PLATFORMS#l25 > > 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 process. > > After the release, we can probably discontinue Mountain Lion, and update > macbroy30 to El Capitan or Sierra. Both macbroy30 and macbroy31 are > MacBookPro6,2 from Mid 2010, so it looks like Sierra still works, but > that might be also the latest possible version. > > Note that in the long run, it is more important to have reference system > installations for older Mac OS versions that for newer ones: the newer > ones are more likely to be installed by current users, although that is > not really a systematic test. > > > Generally, the reference systems according to Isabelle/Admin/PLATFORMS > are required for three main purposes: > > * Compilation of Isabelle components (via ssh) -- on the *oldest* > supported version. > > * Routine batch-builds of Isabelle + add-on tools -- on *all* > supported versions. This is usually done by the administrative cronjob. > > * Occasional interactive tests (via Screen Sharing), to figure out GUI > portability problems, to test the Isabelle.app integration etc. > > > We have come quite far in the Isabelle platform support, not just on Mac > OS X (or mac OS). It would be sad to loose that for no particular reasons. > > > 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] 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 still supported). Cheers, Gerwin > On 26.10.2016, at 04:39, Makarius wrote: > > 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. Nonetheless, Nunchaku >> will remain labeled as "experimental", for a variety of reasons, and will >> not be properly documented. > > Great. > > Note that the updated Isabelle PLATFORMS file is here: > http://isabelle.in.tum.de/repos/isabelle/file/3f4a86c9d2b5/Admin/PLATFORMS#l25 > > I have bumped the Linux baseline to Ubuntu 12.04 recently. Cygwin is > also updated to 2.6 -- last time I somehow missed the change of the > numbering scheme, so we were lagging behind. > > > 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] 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 sense to switch them over to 10.11 and 10.12 (if the hardware is still > supported). The PLATFORMS file documents the current situation for Isabelle support of certain Mac OS X versions, see http://isabelle.in.tum.de/repos/isabelle/file/4f0acbd97491/Admin/PLATFORMS#l25 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 process. After the release, we can probably discontinue Mountain Lion, and update macbroy30 to El Capitan or Sierra. Both macbroy30 and macbroy31 are MacBookPro6,2 from Mid 2010, so it looks like Sierra still works, but that might be also the latest possible version. Note that in the long run, it is more important to have reference system installations for older Mac OS versions that for newer ones: the newer ones are more likely to be installed by current users, although that is not really a systematic test. Generally, the reference systems according to Isabelle/Admin/PLATFORMS are required for three main purposes: * Compilation of Isabelle components (via ssh) -- on the *oldest* supported version. * Routine batch-builds of Isabelle + add-on tools -- on *all* supported versions. This is usually done by the administrative cronjob. * Occasional interactive tests (via Screen Sharing), to figure out GUI portability problems, to test the Isabelle.app integration etc. We have come quite far in the Isabelle platform support, not just on Mac OS X (or mac OS). It would be sad to loose that for no particular reasons. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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. Nonetheless, Nunchaku > will remain labeled as "experimental", for a variety of reasons, and will not > be properly documented. Great. Note that the updated Isabelle PLATFORMS file is here: http://isabelle.in.tum.de/repos/isabelle/file/3f4a86c9d2b5/Admin/PLATFORMS#l25 I have bumped the Linux baseline to Ubuntu 12.04 recently. Cygwin is also updated to 2.6 -- last time I somehow missed the change of the numbering scheme, so we were lagging behind. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 "experimental", for a variety of reasons, and will not be properly documented. This will come with the (expected) Isabelle2017 release. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 https://github.com/alainfrisch/flexdll/releases/tag/0.35 > The Windows platform is a bit strange, but there are usually many ways > to get things through eventually. > > > > Would it make sense to push the source code only, with no binary component, > > for Isabelle2016-1? It's about 2000 lines of code and could go to > > "Library". Or would a Linux/Mac-only binary component be acceptable for > > such a (for the moment, experimental) tool? Otherwise, we can wait for the > > next release. > -- Simon Cruanes http://weusepgp.info/ key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3 7D8D 4AC0 1D08 49AA 62B6 signature.asc Description: PGP signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 on Windows. 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? The Windows platform is a bit strange, but there are usually many ways to get things through eventually. > Would it make sense to push the source code only, with no binary component, > for Isabelle2016-1? It's about 2000 lines of code and could go to "Library". > Or would a Linux/Mac-only binary component be acceptable for such a (for the > moment, experimental) tool? Otherwise, we can wait for the next release. I don't know. It is ultimately up to you. In principle, the Isabelle distribution promises equal rights for citizens of Linux, Windows, Mac OS X, but in practice there are a few drop-outs in odd cases. We could also proceed now, and use protesting crowds of Windows users to accelerate a pending ocamlbuild tracker item somewhere. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 the source code only, with no binary component, for Isabelle2016-1? It's about 2000 lines of code and could go to "Library". Or would a Linux/Mac-only binary component be acceptable for such a (for the moment, experimental) tool? Otherwise, we can wait for the next release. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 immediate reactions on suggestions and observations by testers. > > The repository fork to isabelle-release will happen after RC1. We are more or less on schedule. Isabelle2016-1-RC1 is anticipated towards the end of the week (around 28-Oct-2016). The isabelle-rev repository will remain open a few days afterwards to facilitate immediate reactions by early adopters. A bit later there will be the usual fork to https://bitbucket.org/isabelle_project/isabelle-release and further changes need to be really important (and sent to me via email). > Are there any non-trivial chunks still in the commit/push pipeline that > need special considerations? There have been various smaller and bigger pushes in the meantime. Please make sure that NEWS and CONTRIBUTORS are updated as well. Anything else still left in the pipeline? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 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 ___ 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 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 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 immediate reactions on suggestions and observations by testers. > > The repository fork to isabelle-release will happen after RC1. > > > I am presently still stuck updating the Admin area. > > Are there any non-trivial chunks still in the commit/push pipeline that > need special considerations? > > > 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] 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: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[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 by testers. The repository fork to isabelle-release will happen after RC1. I am presently still stuck updating the Admin area. Are there any non-trivial chunks still in the commit/push pipeline that need special considerations? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/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/ is where the final release preparations happen before roll-out in a few weeks. The starting point is https://bitbucket.org/isabelle_project/isabelle-release/commits/e208fa77beb1 * http://isabelle.in.tum.de/repos/isabelle is back in post-release mode right now (changeset 5fb86150a579). Anything pushed there is for the next release after Isabelle2016. * AFP needs to be understood wrt. isabelle-release at the moment. Gerwin needs to say when and how a fork of afp-devel vs. afp-2016 happens. * isatest continues testing isabelle-release * isabelle-users is the place to discuss Isabelle2016-RC versions * isabelle-dev is the place to discuss ongoing post-release development The isabelle-release repository has no public push access. Any changes that are relevant for the release need to be sent to me via email (produced by "hg export" or "hg bundle"). Changesets need to be prepared from a current state of isabelle-release, not the ongoing post-release development, and applied to only one of the two repository branches. Changes to the actual code base should be limited to really important things. During the forked state of the two repositories, big upheaveals on the isabelle repository should be avoided, so that the isabelle-release branch can be merged back cleanly after several weeks; but it is better to publish changes now than to stockpile them for a long time. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 repository. The fork will happen in 50min. The last changeset that I see is: changeset: 62209:009c6e0b44bb tag: tip user:blanchet date:Wed Jan 20 18:04:41 2016 +0100 files: NEWS description: fixed NEWS w.r.t. multisets If there is anything else, please tell me via email just in time, that we avoid race conditions on the two repositories. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 repository. Afterwards, changesets for the release need to be sent by mail to me. In is important to keep in mind what goes where, i.e. what is meant for post-release development and what for polishing of Isabelle2016. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the release
This is an update on the situation: after the informal Isabelle2016-RC0 and many additions and clarifications, we are moving towards the first formal Isabelle2016-RC1. This will happen in a few days on the main isabelle-dev repository, without a fork yet. Thus it is easier to finish remaining details and react on initial feedback by users testing that version. A bit later next week, presumably after the Java 8 update of Oracle, there will be the fork of isabelle-dev versus isabelle-release on Bitbucket. In the coming days it is important to keep Isabelle + AFP in a clean working state. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 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] Towards the release
This is certainly a must! Thanks! Larry > On 4 Jan 2016, at 19:48, Johannes Hölzl wrote: > > 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. ___ 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'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 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] 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 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 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
[isabelle-dev] Towards the release
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] 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 testing the test for the packaging, which was not a proper release candidate yet. So I need to hurry up. Last December we have had a lot of NFS problems at TUM, so I would like to experiment a bit with viable alternatives, and Bitbucket seems to be the main player for Mercurial. Various side-repositories that are required for the release will be hosted there (e.g. the website). See also https://bitbucket.org/isabelle_project/isabelle-release/wiki/Home for the main entry point for the actual release. I have activated the tracker, too, to see if a few more reports are coming in the critical weeks before actual lift-off. (For Isabelle2012 we've had about 3 people testing before the release, and about 5 testing afterwards.) I recommend to register at Bitbucket already, choosing a good account name. It is a very easy and generous server. As someone with academic mail address you immediately get a free upgrade to "unlimited users" for private repositories. Public repositories are always unlimited. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
