On 10.08.2014, at 11:13 pm, Makarius wrote:
> Note that isatest and AFP are still hooked on Isabelle2014-RC, until Gerwin
> points out the schedule for the correlated AFP release fork.
We’ll do the inverse of the usual process: we’ll fork afp very soon.
Since the Isabelle2014-RC's are looking
On Thu, 7 Aug 2014, Makarius wrote:
This is an update on the ongoing release / testing process:
* The next release candidate (Isabelle2014-RC3) will probably appear at
the 1 week distance that we've had so far, i.e. next Sunday or Monday.
* I will merge back the isabelle-release reposi
This is an update on the ongoing release / testing process:
* The next release candidate (Isabelle2014-RC3) will probably appear at
the 1 week distance that we've had so far, i.e. next Sunday or Monday.
* I will merge back the isabelle-release repository at the same time, so
that ong
We are now past the fork point for the Isabelle2014 release. This means:
* https://bitbucket.org/isabelle_project/isabelle-release/ is where the
final release preparations happen before roll-out in approx. 3 weeks.
The starting point is
https://bitbucket.org/isabelle_project/
On Mon, 21 Jul 2014, Makarius wrote:
This means the main Isabelle repository needs to converge for the release
fork, presumably on Sunday 27-Jul-2014.
The situation looks good at the moment (5b652fd305d4). The fork to the
release repository is planned for Sunday afternoon.
Makariu
On Tue, 22 Jul 2014, Lars Noschinski wrote:
While working on bringing a larger library (AutoCorres) to 2014-rc0, I
relatively often run into prover hiccups (processing theories stops for
a while). This might be seconds, minutes or "too long, restarted the
prover instead".
If this is a "PIDE gr
Being back from VSL 2014 (after the middle ITP week with adjacent
workshops), I have started to pick up this important thread again.
Isabelle2014-RC0 was meant as early-access quasi release-candidate for VSL
presentations. That event finishes at the end of this week. At the same
time the reg
Am 07.07.2014 um 11:38 schrieb Makarius :
> You probably mean the defaults for the "Provers" in the Sledgehammer panel.
> It is now a bit simpler in only providing some static default, which is made
> persistent on the editor side if you change that.
>
> Adding "smt" there includes that prover
On Mon, 7 Jul 2014, Mamoun FILALI-AMINE wrote:
I have downloaded the Isabelle2014-RC0, the smt solver is not anymore
implicitely in the window of solvers and when we put it it gives up
systematically, please is there some setting to do?
(I am bouncing this back on the mailing list, since I am
On Sat, 5 Jul 2014, Makarius wrote:
On Fri, 4 Jul 2014, Makarius wrote:
On Tue, 1 Jul 2014, Makarius wrote:
> I am about to update the website, such that Isabelle2014-RC0 can be
> published with an approximation of the one for the coming release.
I will tag Isabelle2014-RC0 today or to
>> I will tag Isabelle2014-RC0 today or tomorrow, shooting blindly at the
>> repository.
>
> There were some delays, but I will definitely make a blind shot today,
> within the next few hours.
Btw. http://isabelle.in.tum.de/reports/Isabelle/rev/9e5f47e83629 is my
last proactive contribution to th
On Fri, 4 Jul 2014, Makarius wrote:
On Tue, 1 Jul 2014, Makarius wrote:
I am about to update the website, such that Isabelle2014-RC0 can be
published with an approximation of the one for the coming release.
I will tag Isabelle2014-RC0 today or tomorrow, shooting blindly at the
repository.
On Tue, 1 Jul 2014, Makarius wrote:
I am about to update the website, such that Isabelle2014-RC0 can be
published with an approximation of the one for the coming release.
I will tag Isabelle2014-RC0 today or tomorrow, shooting blindly at the
repository. This is not a regular release candidat
Good point. Tom, if you send me the text I will update the two files.
Cheers,
Gerwin
On 3 Jul 2014, at 10:30 pm, Makarius wrote:
> On Thu, 3 Jul 2014, Gerwin Klein wrote:
>
>> Applied cleanly and is now pushed.
>>
>> On 3 Jul 2014, at 9:55 am, Thomas Sewell wrote:
>>
>>> On 02/07/14 06:49, Ger
On Thu, 3 Jul 2014, Gerwin Klein wrote:
Applied cleanly and is now pushed.
On 3 Jul 2014, at 9:55 am, Thomas Sewell wrote:
On 02/07/14 06:49, Gerwin Klein wrote:
http://isabelle.in.tum.de/testboard/Isabelle/rev/d765be00b181
For the release we also need the canonical NEWS and CONTRIBUTORS
e in though.
>
> Thomas.
>
>
> From: Makarius [makar...@sketis.net]
> Sent: Monday, June 30, 2014 9:56 PM
> To: Gerwin Klein; Thomas Sewell
> Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] Towards the I
Isabelle/ecad2a53755a has a first round of updates of the important files
for the "Release notes", notably NEWS, CONTRIBUTORS, ANNOUNCE.
Now is a good time to check that it is all up-to-date.
As usual the ANNOUNCE file is an extract of the NEWS, but importants
things might be still missing. P
__
From: Makarius [makar...@sketis.net]
Sent: Monday, June 30, 2014 9:56 PM
To: Gerwin Klein; Thomas Sewell
Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Towards the Isabelle2014 release
On Wed, 11 Jun 2014, Gerwin Klein wrote:
> On 11.06.2014, at 2
On Wed, 11 Jun 2014, Gerwin Klein wrote:
On 11.06.2014, at 2:56 pm, Thomas Sewell wrote:
Gerwin will push the isabelle hypsubst change to the testboard now (assuming he
can remember how).
He could and did.
Has that change been landed? Which changeset IDs are relevant?
I don't have any
This is a tremendous achievement, thanks!
Some of those proofs are unbearably messy… I’m impressed that you were able to
do this in such a short time!
Larry
On 11 Jun 2014, at 05:56, Thomas Sewell wrote:
> OK, I've finished the needed adjustments the AFP proofs which were affected
> by the h
On 11.06.2014 06:56, Thomas Sewell wrote:
> OK, I've finished the needed adjustments the AFP proofs which were
> affected by the hypsubst change.
>
> The result is fairly encouraging: the AFP is *huge* and the diffstat
> of the required changes is:
> 63 files changed, 134 insertions(+), 81 deletio
On 11.06.2014, at 2:56 pm, Thomas Sewell wrote:
> Gerwin will push the isabelle hypsubst change to the testboard now (assuming
> he can remember how).
He could and did.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal
> The summer is getting close, and we need to start thinking about the
> coming release.
I have two or three cleanup tasks in the pipeline which I hope to get
ready during June.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_
I certainly agree with your point of view, but I would immediately insert the
local context around any proof that causes problems rather than waste time
trying to fix it.
Maybe we could then invite the maintainers of the entries to update their
proofs if they wish.
Larry
On 5 Jun 2014, at 04:4
On 05.06.2014 05:44, Thomas Sewell wrote:
> In particular, I want to avoid ever changing the setting globally. I've
> had some bad experiences in the past with theories with differing global
> configurations, which means that the location of a tactic and the
> include graphs of theories start havin
Indeed, there is a backward compatibility mode declaration. In fixing
things, I've been trying to use it as little as possible and as locally
as possible. Perhaps I should be bolder.
I'm aesthetically against using the compatibility mode all over the
place, since I feel that it's just mysterio
Didn’t we agree that a “backward compatibility mode” declaration (restoring the
former behaviour) would have to be available? That should make repairing legacy
proofs trivial. Naturally we would like to gradually port some of these
developments to do things the new way, but only some of them, an
I had hoped to have the change I was making to hypothesis-substitution
ready for the coming release.
I've got it working for all of HOL and the library, and begun looking at
the AFP and at the l4.verified proofs. The HOL+library changes were easy
enough, but the l4.verified changes are somewha
28 matches
Mail list logo
