Re: [isabelle-dev] Jenkins maintenance

> Also note that the Mira architects were actually looking at Jenkins at > that time, and pointed out that it was a bit old-fashioned in focusing > on "latest" versions by default and lacking proper changeset identification. The story behind is actually more delicate: mira was started with the

[isabelle-dev] Fwd: You have been unsubscribed from the Isabelle-ci mailing list

Forwarded Message Subject: You have been unsubscribed from the Isabelle-ci mailing list Date: Sat, 01 Oct 2016 20:44:59 +0200 From: isabelle-ci-boun...@mail46.informatik.tu-muenchen.de No more Jenkins SPAM. Makarius ___

[isabelle-dev] Notes on isabelle build -a

The art of manual isabelle build -a seems to have been forgotten, so here are some basic notes in accordance to README_REPOSITORY (e.g. Isabelle/4effb93c2a09). In contrast to the batch-queue model of testboard, manual builds are incremental to some extent: the full build happens in the context of

Re: [isabelle-dev] Jenkins maintenance

On 27/09/16 11:43, Lars Hupel wrote: > Finding out the latest status is as easy as visiting > , which includes the Mercurial > IDs, the build time, the build cause and the link to the full build log. > > Even more information is available, as usual, through

Re: [isabelle-dev] Jenkins maintenance

On 27/09/16 11:43, Lars Hupel wrote: > There are a lot of different issues in this thread, so let's unpack them > separately. > >> Technical decisions need real reasons, not buzzwords. > > What's the buzzword? On 24/09/16 17:47, Lars Hupel wrote: > > This is hardly a new concept – it's not >

Re: [isabelle-dev] Jenkins maintenance

On 01/10/16 10:44, Florian Haftmann wrote: > > c) Sustainable system governance > > After a push to the main repository, there might still be undiscovered > issues, e.g. document production, platform-specific drop-outs, worse > resource usage etc. Hence the regular regression test of the main >

Re: [isabelle-dev] NEWS: new proof method "argo"

On 29/09/16 21:44, Sascha Boehme wrote: > *** HOL *** > > * New proof method "argo" using the built-in Argo solver based on SMT > technology. > The method can be used to prove goals of quantifier-free propositional logic, > goals based on a combination of quantifier-free propositional logic with

Re: [isabelle-dev] Jenkins maintenance

On 27/09/16 11:43, Lars Hupel wrote: > > In an ideal world everyone would run "isabelle build -D $AFP -a -o > document=pdf" before pushing, but clearly that is impractical. According to the official README_REPOSITORY

Re: [isabelle-dev] NEWS: new proof method "argo"

Hi Makarius, Compared to „argo“ the „smt“ method is more powerful since it supports quantifiers as well as linear natural and integer arithmetic. For the moment, argo is not capable of proving problems that require both equality reasoning and linear real arithmetic. This combination of

Re: [isabelle-dev] Jenkins maintenance

> And where are the public sources of Isabelle/Jenkins? I feel like the other readers on this thread should know that you have asked me exactly the same question when you last visited Garching. I explained to you that some parts of the infrastructure cannot be public because they contain

Re: [isabelle-dev] Jenkins maintenance

On 01/10/16 19:05, Florian Haftmann wrote: > > The story behind is actually more delicate > > The following insights contributed to abandon the project: > > 2) Further, »keep it simple, stupid« came to its limits with all the > involved technicalities: issues jobs on remote machines, exception