Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

I have been very busy, but I will find time to work on it. Viorel On 11/23/2017 6:46 PM, Lawrence Paulson wrote: Whatever happened with this? The new release has been out for a while, and it would make sense to integrate your work now, well before any thought of a new release. Larry On 27

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

Whatever happened with this? The new release has been out for a while, and it would make sense to integrate your work now, well before any thought of a new release. Larry > On 27 Aug 2017, at 15:59, Viorel Preoteasa wrote: > > I managed to integrate the new complete

Re: [isabelle-dev] Towards the Isabelle2017 release

This is a brief summary of the current situation: * The current RC version is http://isabelle.in.tum.de/website-Isabelle2017-RC3 and http://isabelle.in.tum.de/website-Isabelle2017 is an alias for that. * http://isabelle.in.tum.de/repos/isabelle/rev/ebb97a834338 is a preliminary merge of the

Re: [isabelle-dev] Towards the Isabelle2017 release

> My plan would be to fork the AFP 2017 release branch tomorrow (around > midnight CET from Mon to Tue). > > There still seems to be quite a bit of ongoing activity - if there is > anything that needs to go into the afp-2017 release, please let me know. One more thing that is of interest to

Re: [isabelle-dev] Towards the Isabelle2017 release

My plan would be to fork the AFP 2017 release branch tomorrow (around midnight CET from Mon to Tue). There still seems to be quite a bit of ongoing activity - if there is anything that needs to go into the afp-2017 release, please let me know. Cheers, Gerwin > On 9 Sep 2017, at 04:30,

Re: [isabelle-dev] Towards the Isabelle2017 release

We are now past the fork point for the Isabelle2017 release. 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

Re: [isabelle-dev] Towards the Isabelle2017 release

On 08/09/17 11:13, Makarius wrote: > The all-important release fork will happen today in the evening. That is now! Within the next hour there should not be any pushes to http://isabelle.in.tum.de/repos/isabelle in order to avoid confusion about the two branches. I will come back a bit later

Re: [isabelle-dev] Towards the Isabelle2017 release

On 03/09/17 12:06, Makarius wrote: > > The isabelle-dev repository remains open for 3 more days. Afterwards it > forks to https://bitbucket.org/isabelle_project/isabelle-release and > further changes (really important ones!) need to be sent to me via email. There were some delays, but we are now

Re: [isabelle-dev] Towards the Isabelle2017 release

Dear Florian, thanks for the explanation and the hint on style. The below pattern works perfectly in our formalization. Cheers, René > Am 31.08.2017 um 14:03 schrieb Florian Haftmann > : > > Note that the pattern above is avoided nowadays by an

Re: [isabelle-dev] Towards the Isabelle2017 release

On 21/08/17 20:24, Makarius wrote: > > The first official release candidate Isabelle2017-RC1 is anticipated for > 2/3-Sep-2017, that is a bit less than 2 weeks from now. > > That is also the deadline for any significant additions. That is today. I will publish Isabelle2017-RC1 within a few

Re: [isabelle-dev] Towards the Isabelle2017 release

Hi Rene, > = > locale foo = fixes f :: "nat => nat" > assumes f_mono[termination_simp]: "f x <= x" > begin > > fun bar :: "nat => nat" where > "bar 0 = 0" > | "bar (Suc x) = Suc (bar (f x))" > > end > > definition com where > [code del]: "com = foo.bar id" > > interpretation foo id

Re: [isabelle-dev] Towards the Isabelle2017 release

On 24/08/17 09:38, Thiemann, Rene wrote: > > - Most changes have been caused by integrating session-qualified theory > imports. > This will also require a reform of the splitting of sessions, which > previously > was structured towards a fast build-process, but now should be structured >

Re: [isabelle-dev] Towards the Isabelle2017 release

On 24/08/17 17:40, Florian Haftmann wrote: > > Hence that change should be fine if someone is willing to undertake it > before the RC stabilization phase. We are already in stabilization phase for some weeks. There are a few days left until Isabelle2017-RC1 (presumably on 03-Sep-2017) to make

Re: [isabelle-dev] Towards the Isabelle2017 release

Dear Florian, >> - There have been some changes w.r.t. code-generation which now lead >> to runtime exception in the generated code. For instance, now >> I get code like >> “f x = Code.abort …” >> whereas in 2016-1 there was a proper code like >> “f x = some ordinary right-hand side” >> We

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

On 8/27/2017 6:11 PM, Lawrence Paulson wrote: In the AFP, grep picks up these: ~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r . ./Coinductive/Examples/CCPO_Topology.thy ./Concurrent_Ref_Alg/Refinement_Lattice.thy ./DataRefinementIBP/Diagram.thy ./DataRefinementIBP/Hoare.thy

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

Hi Viorel, it's probably easiest to send a patch containing your changes to this mailing list. (Alternatively, a copy of all the files you changed.) Some Isabelle committer can then push this to the testboard which will run the whole AFP. Cheers Lars On 27 August 2017 16:59:44 CEST, Viorel

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

In the AFP, grep picks up these: ~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r . ./Coinductive/Examples/CCPO_Topology.thy ./Concurrent_Ref_Alg/Refinement_Lattice.thy ./DataRefinementIBP/Diagram.thy ./DataRefinementIBP/Hoare.thy ./DataRefinementIBP/Statements.thy

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

I managed to integrate the new complete distributive lattice into HOL library. The changes are these: Complete_Lattice.thy - replaced the complete_distrib_lattice with the new stronger version. - moved some proofs about complete_distrib_lattice and some instantiations to Hilbert_Choice

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

> On 25 Aug 2017, at 20:14, Viorel Preoteasa wrote: > > One possible solution: > > Add the new class in Complete_Lattice.thy, replacing the existing class > > Prove the instantiations and the complete_linearord subclass later > in Hilbert_Choice. > > On the other

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

I have investigated the possibility of replacing the existing complete_distrib_lattice with the stronger version. Here are the problems: 1. The new class needs Hilbert choice in few places: proving the dual of the distributivity property, proving the set and fun instantiations, and proving

Re: [isabelle-dev] Towards the Isabelle2017 release

On 2017-08-24 23:25, Manuel Eberl wrote: Purely out of interest: Does this also hold for filters? Manuel Do filters form a complete lattice? It seems that a filter of a lattice should be nonempty. I think that this condition would prevent the set of filters to be a lattice. If empty set

Re: [isabelle-dev] Towards the Isabelle2017 release

Am 24.08.2017 um 22:39 schrieb Manuel Eberl: > On 2017-08-24 17:34, Florian Haftmann wrote: >> I would still appreciate if someone would take the comment »Deviates >> from the definition given in the library in number theory« as a starting >> point to reconcile that definition with

Re: [isabelle-dev] Towards the Isabelle2017 release

For the final record: > \phi is the result of a simple typo accident see http://isabelle.in.tum.de/repos/isabelle/rev/ba94aeb02fbc > Concerning \mu and \nu, I am currently investigating whether an import > swap could re-establish the situation known from Isabelle2016-1 see

Re: [isabelle-dev] Towards the Isabelle2017 release

On 2017-08-24 17:34, Florian Haftmann wrote: > I would still appreciate if someone would take the comment »Deviates > from the definition given in the library in number theory« as a starting > point to reconcile that definition with src/HOL/Number_Theory/Totient.thy. Oh actually I fixed that a

Re: [isabelle-dev] Towards the Isabelle2017 release

Purely out of interest: Does this also hold for filters? Manuel On 2017-08-24 20:54, Viorel Preoteasa wrote: > I have now a file with the new class, and all necessary proofs > (both distributivity equalities, bool, set, fun interpretations, > proofs of the old distributivity properties). > > I

Re: [isabelle-dev] Towards the Isabelle2017 release

Hi Rene, > - In the NEWS I read about freeing short constant names like the > “Renamed ii to imaginary_unit in order to free up ii as a variable”. > I definitely support this kind of change, but at the same time found > quite the opposite in HOL-Algebra: > If one imports

Re: [isabelle-dev] Towards the Isabelle2017 release

Dear all, let me share my opinions after porting IsaFoR to yesterdays development version: - In total the transition from our 2016-1 source went quite smooth (~ 14 hours for whole of IsaFoR) - Most changes have been caused by integrating session-qualified theory imports. This will also

Re: [isabelle-dev] Towards the Isabelle2017 release

Sounds good to me. Can anybody think of an objection? Larry > On 23 Aug 2017, at 15:17, Viorel Preoteasa wrote: > > Hello, > > I am not sure if this is the right place to post this message, but it is > related to the upcoming release as I am prosing adding something

Re: [isabelle-dev] Towards the Isabelle2017 release

Hello, I am not sure if this is the right place to post this message, but it is related to the upcoming release as I am prosing adding something to the Isabelle library. While working with complete distributive lattices, I noticed that the Isabelle class complete_distrib_lattice is weaker

[isabelle-dev] Towards the Isabelle2017 release

Dear Isabelle contributors, we are now definitely heading towards the Isabelle2017 release. The first official release candidate Isabelle2017-RC1 is anticipated for 2/3-Sep-2017, that is a bit less than 2 weeks from now. That is also the deadline for any significant additions. I have already