[isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

[Manuel Eberl]

Is it intentional that the "Computational_Algebra" theory does not
import "Polynomial_Factorial"?

Manuel

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Makarius]

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
small additions and do some fine tuning.

After the Isabelle2017-RC1 there will be the usual 4-6 weeks to sort out
genuine problems only, notably ones that have been newly introduced
since the last release.


Makarius



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] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Clemens Ballarin]

On 2017-08-24 09:38, Thiemann, Rene wrote:


  If one imports HOL-Algebra.Multiplicative_Group (which we actually do
  via some transitive import), then \mu (LFP), \nu (GFP) and
  \phi (Euler’s totient function) become constants.


Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.

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

Re: [isabelle-dev] Complete Distributive Lattice

[Viorel Preoteasa]

OK, I understand, what is the time frame for going back to normal? I did 
spent some time on this and I would like to see it finished.


As I mentioned earlier, I added finite lattices to simplify the proofs
in Enum.thy that finite_n are distributive complete lattices. However,
searching for dependencies on complete_distrib_lattice, I found a very 
similar class of finite lattices in Library. How should this be handled?


Viorel

On 8/28/2017 5:26 PM, Lawrence Paulson wrote:
For sure. The work is very welcome, but too drastic to undertake at this 
precise moment.

Larry

On 28 Aug 2017, at 13:08, Makarius > wrote:


Nothing of this is relevant for the Isabelle2017 release. When the "RC"
versions show up, it is time to finish and not to start new things.



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

Re: [isabelle-dev] Complete Distributive Lattice

[Makarius]

On 28/08/17 20:26, Viorel Preoteasa wrote:
> OK, I understand, what is the time frame for going back to normal?

This is hard to say, since official Isabelle2017-RC1 is not even there
yet, but it is planned for Sun 03-Sep-2017.

The final lift off will probably take 6 weeks from Isabelle2017-RC1, but
it also depends a lot on the participation of users testing the RC chain.


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

Re: [isabelle-dev] Complete Distributive Lattice

[Lawrence Paulson]

For sure. The work is very welcome, but too drastic to undertake at this 
precise moment.
Larry

> On 28 Aug 2017, at 13:08, Makarius  wrote:
> 
> Nothing of this is relevant for the Isabelle2017 release. When the "RC"
> versions show up, it is time to finish and not to start new things.

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

Re: [isabelle-dev] Complete Distributive Lattice

[Makarius]

On 27/08/17 16:59, Viorel Preoteasa wrote:
> I managed to integrate the new complete distributive lattice into HOL
> library.
> 
> The changes are these:
> 
> Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s
> GC time, factor 1.83)
> Finished HOL (0:04:26 elapsed time)
> 
> Finished at Sun Aug 27 17:41:30 GMT+3 2017
> 0:04:37 elapsed time
> 
> But I don't now how to go from here to have these changes into Isabelle.

Someone who understands Isabelle library maintenance needs to pick it up
and apply it in the proper way. This usually takes quite some time, and
exposes many unexpected problems. Main HOL is not easily changed on the
spot.


> There is also AFP.

This usually takes 2-3 more rounds of exploration.


Nothing of this is relevant for the Isabelle2017 release. When the "RC"
versions show up, it is time to finish and not to start new things.


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