[isabelle-dev] Towards the release

[Makarius]

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

[Makarius]

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

[Makarius]

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

[Makarius]

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

[Gerwin.Klein]

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

[Makarius]

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

[Makarius]

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

[Lawrence Paulson]

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

[Gerwin.Klein]

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

[Makarius]

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

[Makarius]

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

[Jasmin Blanchette]

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

[Simon Cruanes]

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

[Makarius]

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

[Jasmin Blanchette]

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

[Makarius]

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

[Lawrence Paulson]

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

[Manuel Eberl]

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

[Florian Haftmann]

> 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

[Makarius]

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

[Makarius]

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

[Makarius]

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

[Makarius]

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

[Makarius]

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

[Makarius]

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

[Manuel Eberl]

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

[Johannes Hölzl]

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

[Manuel Eberl]

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

[Manuel Eberl]

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

[Makarius]

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

[Lawrence Paulson]

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 -- Bitbucket

[Makarius]

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

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 STIXGeneral as fall
back, which is somehow hardwired into Proof General 4.1

  * (proof-full-annotation nil) for improved stability and performance.

  * (proof-strict-read-only t) for improved stability.

There is a remaining issue with preferences 
http://proofgeneral.inf.ed.ac.uk/trac/ticket/387 which is a show-stopper 
for the Isabelle2011 release.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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: instead of IsabelleText refer to STIXGeneral as fall
   back, which is somehow hardwired into Proof General 4.1

 * (proof-full-annotation nil) for improved stability and performance.

 * (proof-strict-read-only t) for improved stability.

There is a remaining issue with preferences 
http://proofgeneral.inf.ed.ac.uk/trac/ticket/387 which is a show-stopper 
for the Isabelle2011 release.


This is one more update of 
http://www4.in.tum.de/~wenzelm/test/isa2011-test3/


The only difference to above is ProofGeneral-4.1pre101216 instead of 
ProofGeneral-4.1pre110112 as basis for our patches, so the problem of 
ticket/387 is absent.



After one more round of looking closely at the distribution, we have a 
chance for the final Isabelle2011 snapshot on Sunday or Monday.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 robust Isabelle/Scala document processing, especially
on systems with few cores, and on x86_64

  * last-minute fixes for HOL-SPARK

  * ProofGeneral-4.1pre110112: option -f FONT can be used
e.g. with IsabelleText to get proper Unicode symbols

  * Mac OS X app bundle is back to GNU Emacs 23.2.x (no-nonsense),
default font configuration for IsabelleText font

This is another chance to see if everything works. I hope that we manage 
the final release before the end of the months, which is now very close.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Lucas Dixon]

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 error window saying 
something like:


2011-01-25 11:42:54.894 Emacs[7555:623] ns_raise_fr
2011-01-25 11:42:58.407 Emacs[7555:623] notification
2011-01-25 11:43:01.187 Emacs[7555:623] ns_raise_fr
2011-01-25 11:43:02.788 Emacs[7555:623] notification
2011-01-25 11:43:31.366 Emacs[7555:623] notification

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 don't get a 
dialogue-box telling me about the active processes; instead, I get the 
typical emacs mini-buffer message. When I say yes there, it quits 
without any strange error messages.


best,
lucas

On 24/01/2011 15:12, Makarius wrote:

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 been
resolved.

Some notable changes:

* contrib/spass-3.7: make it actually work on x86-darwin (Leopard)
(avoiding really weird crashes and strange error messages with
Sledgehammer)

* contrib/cvc3-2.2: make it actually work on darwin without Mac Ports

* contrib/z3: make it actually work on x86_64-linux; still not working
on Windows/Cygwin (?) unavailable on Mac OS X (!)

* Cygwin: Back to old ProofGeneral-3.7.1.1 with ancient XEmacs, because
PG 4.x with GNU Emacs 23 is very slow here.

* ProofGeneral-4.1pre110112: deleted .elc files on Linux to improve
compatibility with GNU Emacs 23.1.x instead of 23.2.1

In the Mac OS X app/dmg I have also exchanged GNU Emacs 23.2.x (no
nonsense version) with Aquamacs 2.1, although it looks again like this
is the choice between Scylla and Charybdis.

It is also unclear when exactly PG 4.1-final will be released this week.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 don't get a dialogue-box telling me 
about the active processes; instead, I get the typical emacs mini-buffer 
message. When I say yes there, it quits without any strange error 
messages.


The dialogue-box is part of the Isabelle.app bundle, it merely shows all 
results from stdout/stderr after the process has terminated. I reckon that 
the Aquamacs.app merely absorbs such traces, whereever they might come 
from.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 Isabelle2011 release until 
the dust on the PG 4.1-final development has settled.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 been 
resolved.


Some notable changes:

  * contrib/spass-3.7: make it actually work on x86-darwin (Leopard)
(avoiding really weird crashes and strange error messages with
Sledgehammer)

  * contrib/cvc3-2.2: make it actually work on darwin without Mac Ports

  * contrib/z3: make it actually work on x86_64-linux; still not working
on Windows/Cygwin (?) unavailable on Mac OS X (!)

  * Cygwin: Back to old ProofGeneral-3.7.1.1 with ancient XEmacs, because
PG 4.x with GNU Emacs 23 is very slow here.

  * ProofGeneral-4.1pre110112: deleted .elc files on Linux to improve
compatibility with GNU Emacs 23.1.x instead of 23.2.1

In the Mac OS X app/dmg I have also exchanged GNU Emacs 23.2.x (no 
nonsense version) with Aquamacs 2.1, although it looks again like this is 
the choice between Scylla and Charybdis.


It is also unclear when exactly PG 4.1-final will be released this week.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 
evening (GMT).  So this is the very last chance for small amendments on 
the main Isabelle repository.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 sent to me via 
email, as clean changesets without any merges inside.


  * Changes for isabelle-release should *not* be pushed to the main 
Isabelle repository, but they will come there after the release is shipped 
and the isabelle-release clone merged back.


  * isatest refers to isabelle-release

  * AFP morally refers to isabelle-release as well. (There are still some 
broken theories on AFP, probably due to some last minute changes in main 
HOL.)



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2011 release

[Makarius]

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 http://isabelle.in.tum.de/repos/isabelle is again 
open for submissions for the post-release development cycle (cf. 
c78b786fe060).


The only limitation is that big HOL library changes on the Isabelle 
development branch should be postponed, until AFP for Isabelle2011 is 
officially released.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev