Re: [isabelle-dev] Jenkins reconfiguration

2018-06-29 Thread Makarius
On 28/06/18 11:41, Lars Hupel wrote: > Dear Isabelle developers, > > you may have already noticed that some Jenkins jobs got reconfigured. > > The following changes are relevant for developers: > > - The new job "isabelle-all" runs Isabelle+AFP together, incrementally. > This should improve

Re: [isabelle-dev] Jenkins reconfiguration

2018-06-29 Thread Lars Hupel
Does it mean that the great new hardware is now locked up and exclusively available for Jenkins? That assessment is accurate. ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] a question about regulations

2018-06-29 Thread José Manuel Rodriguez Caballero
Hi Makarius and Gerwin, Thank you by the information. I sorry if this mailing list was not the best to ask this legal question, I did not find another one more appropriated for this subject. With respect to Makarius worries with open source, I'm the first who enjoys open source. Kind Regards,

Re: [isabelle-dev] Jenkins reconfiguration

2018-06-29 Thread Lars Hupel
> - The "testboard" job will also be replaced to run Isabelle+AFP > together. Historic builds will be deleted, as they are not relevant for > the official history. I have implemented this now. I'm currently monitoring the situation, but so far, it seems like this sped up the process overall.

Re: [isabelle-dev] a question about regulations

2018-06-29 Thread Makarius
On 29/06/18 08:08, José Manuel Rodriguez Caballero wrote: >   Thank you by the information. I sorry if this mailing list was not the > best to ask this legal question, I did not find another one more > appropriated for this subject. By default you can post everything on isabelle-users, unless it

Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

2018-06-29 Thread Lawrence Paulson
Okay, I have replaced it by Complex_Main. In fact derivatives are only needed in a couple of places. Larry > On 28 Jun 2018, at 17:03, Florian Haftmann > wrote: > >> Is it right for this theory to base itself on HOL.Deriv rather than >> Complex_Main? >> >> Larry >> >> section ‹Polynomials