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
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/is
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
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 isa
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, es
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 pr
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:
>> General
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
>> ba
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 st
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 se
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. Nonet
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
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/f
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
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
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 immed
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
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
> 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.i
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
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/
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 repositor
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
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
___
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
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
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-
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
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.
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 inc
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 Gam
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://mailm
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 chan
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 H
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 testin
35 matches
Mail list logo