Re: [isabelle-dev] Jenkins maintenance

On 06/10/16 17:03, Tobias Nipkow wrote: > Sorry, I don't consider them useless. > > Tobias > > On 06/10/2016 17:00, Makarius wrote: >> This is actually my main point of criticism for the present situation: >> the Jenkins setup uses a lot of hardware resources, by doing too many >> useless tests.

Re: [isabelle-dev] Jenkins maintenance

On 06/10/16 15:36, Lawrence Paulson wrote: > I don’t agree with this point at all. Fixing the errors is easy but locating > them certainly isn’t. I’m happy as long as somebody else is willing to do > that. > Larry > >> On 6 Oct 2016, at 14:02, Makarius wrote: >> >> * A

Re: [isabelle-dev] Jenkins maintenance

Sorry, I don't consider them useless. Tobias On 06/10/2016 17:00, Makarius wrote: This is actually my main point of criticism for the present situation: the Jenkins setup uses a lot of hardware resources, by doing too many useless tests. smime.p7s Description: S/MIME Cryptographic

Re: [isabelle-dev] Jenkins maintenance

On 06/10/16 16:44, Tobias Nipkow wrote: > >> I also prefer to have AFP working all the time, but that would require >> much more resources, both hardware and humans. > > For a growing number of Isabelle users, the AFP is just as important as > the Isabelle repository. Hence the AFP needs to be

Re: [isabelle-dev] Jenkins maintenance

On 06/10/2016 14:34, Makarius wrote: On 03/10/16 17:12, Manuel Eberl wrote: It would also be an effective safeguard against breaking the repository (and possibly even the AFP), which /does/ happen quite frequently. (cf. the current situation where things have been broken for days) I also

Re: [isabelle-dev] Jenkins maintenance

On 06/10/16 15:22, Lawrence Paulson wrote: > I have a Mac Pro, and I just use “isabelle build -a”. Maybe I could use > multithreading more (the machine supports 12 cores). There is a certain art to combine build options -j N and -o threads=M, depending on the hardware (based on manual

Re: [isabelle-dev] Jenkins maintenance

I don’t agree with this point at all. Fixing the errors is easy but locating them certainly isn’t. I’m happy as long as somebody else is willing to do that. Larry > On 6 Oct 2016, at 14:02, Makarius wrote: > > * A broken Latex document is easy to repair.

Re: [isabelle-dev] Jenkins maintenance

I have wanted to keep out of this rather fraught discussion, but I agree on this issue. How dangerous it is depends on how critical those secrets are. And I’m perfectly aware that key management can be difficult and maybe there is little point if only one instance of this thing is running.

Re: [isabelle-dev] Jenkins maintenance

I have a Mac Pro, and I just use “isabelle build -a”. If I know that my changes affect specific AFP entries, I run them manually. A full test takes a couple of hours, and it is a pain. Maybe I could use multithreading more (the machine supports 12 cores). Larry > On 6 Oct 2016, at 13:05,

Re: [isabelle-dev] Jenkins maintenance

On 06/10/16 15:07, Lars Hupel wrote: > In fact, the situation was even worse back then: Various Isabelle > developers have told me that they're using "macbroy2" which would > otherwise be used for isatest/afptest for private experiments. Since a > full test run would sometimes take some 10 hours,

Re: [isabelle-dev] Jenkins maintenance

> I had many private discussions with Lars in the past few months. I even > pointed out important requirements before the start of the Jenkins project. I am aware of that (I keep notes), and also of the relevant email threads dating back to 2014. > The present situation is that we have no proper

Re: [isabelle-dev] Jenkins maintenance

On 05/10/16 18:07, Lars Hupel wrote: >> According to the official README_REPOSITORY >> (http://isabelle.in.tum.de/repos/isabelle/file/ec0fb01c6d50/README_REPOSITORY#l282) >> there is >> >> * no need to test pdf documents > > This is arguable. In fact, it is very convenient to have documents in

Re: [isabelle-dev] Jenkins maintenance

> I have often wondered how certain details are done by Jenkins, e.g. > logging into a remote machine, controlling the job and getting its results. Your use of the term "Isabelle/Jenkins" led me to believe that you're interested in the Ansible scripts. If you're instead interested in Jenkins

Re: [isabelle-dev] Jenkins maintenance

> I have just used the new Jenkins testboard for the first time, and was a > bit disappointed by the very long runtimes: about 1.5h each for Isabelle > and AFP. This is slightly misleading, because the total time spent waiting for both is typically 1:30 hours; Jenkins runs them in parallel if

Re: [isabelle-dev] Jenkins maintenance

On 03/10/16 17:12, Manuel Eberl wrote: > > I for one think that a big improvement would be a system where no one > pushes to the repository directly: every push goes to a testing server, > and if the test is successful, the changes can then automatically be > merged into the repository without an

Re: [isabelle-dev] Jenkins maintenance

On 03/10/16 17:31, Lawrence Paulson wrote: > I’d be happy with this, if it’s achievable. > > I’ve only tried the testboard once or twice; I find it too easy to do the > wrong thing when you have a choice of targets to push to, and I have a > powerful machine so I prefer to test there. But a

Re: [isabelle-dev] Jenkins maintenance

On 01/10/16 22:38, Lars Hupel wrote: >> 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

Re: [isabelle-dev] Jenkins maintenance

Thank you for bringing the discussion back on track. Let me try to address the remaining points. > I for one think that a big improvement would be a system where no one > pushes to the repository directly: every push goes to a testing server, > and if the test is successful, the changes can then

Re: [isabelle-dev] Jenkins maintenance

This, too, is an industry standard. Of course, I am not the expert, but I'm pretty sure this is achievable with the system we have – if there is a consensus that this is what we want, that is. Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Jenkins maintenance

I’d be happy with this, if it’s achievable. I’ve only tried the testboard once or twice; I find it too easy to do the wrong thing when you have a choice of targets to push to, and I have a powerful machine so I prefer to test there. But a mechanism of the sort you describe (provided it’s easy

Re: [isabelle-dev] Jenkins maintenance

I have decided to add my own opinions to this debate. My knowledge of the old testing system is limited, but I hope my perspective will still hold some interest. First of all, a usable testing infrastructure does not grow overnight by itself. Someone has to put in a lot of time and effort to make

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

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

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] 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: > > 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] 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 24/09/16 17:47, Lars Hupel wrote: > > This is hardly a new concept – it's not > just industry standard, but even best practice (the term "Continuous > integration" itself traces back to 1991). There is no point in going > back to an outdated development model. Technical decisions need real

Re: [isabelle-dev] Jenkins maintenance

(Please read carefully!) > over the weekend, there will be – once again – a scheduled maintenance > on the build infrastructure. I will add some more jobs (which are > running nightly) to test a wider variety of side conditions (mainly > -j/-o threads). I will take this opportunity to tidy up the

Re: [isabelle-dev] Jenkins maintenance

> over the weekend, there will be a scheduled maintenance on the build > infrastructure. As announced earlier, jobs will be migrated to a new > machine, but also the Jenkins server itself will move. It took longer than anticipated, but on the plus side, I didn't have to cancel anything. Jenkins

Re: [isabelle-dev] Jenkins maintenance window

> On 16 Feb 2016, at 11:30, Makarius wrote: > > On Tue, 16 Feb 2016, Dmitriy Traytel wrote: > >> I am unsure if an Isabelle tool is the right level of abstraction for an >> operation, only members of the isabelle (UNIX) group at TUM can/should >> execute. > > BTW, the

Re: [isabelle-dev] Jenkins maintenance window

On Tue, 16 Feb 2016, Dmitriy Traytel wrote: I am unsure if an Isabelle tool is the right level of abstraction for an operation, only members of the isabelle (UNIX) group at TUM can/should execute. BTW, the Isabelle tool name space is not hardwired. Any "component" can add new tool

Re: [isabelle-dev] Jenkins maintenance window

Hi Lars, I am unsure if an Isabelle tool is the right level of abstraction for an operation, only members of the isabelle (UNIX) group at TUM can/should execute. Also, wouldn’t a push to a fresh repository take quite long. (OK, negligible compared to the actual build, but still.) And one still

Re: [isabelle-dev] Jenkins maintenance window

> Was it me? I think I saw a warning to that effect, but with "-f" > (which is necessary since we're creating new heads) it's too late > once the warning is shown. I can easily change the trusty old script > I use to push to testboard to make sure I do it from my Isabelle > repository. If it

Re: [isabelle-dev] Jenkins maintenance window

Hi Lars, > However, turns out that the actual problem was that somebody pushed > something completely unrelated (maybe a different repository?) into > testboard. This also generated a gargantuan changelog in Jenkins. I > don't blame that person, it could happen to anyone. But we need to fix >

Re: [isabelle-dev] Jenkins maintenance window

How about pushing feature branches instead? Cheers, Gerwin > On 16 Feb 2016, at 09:25, Lars Hupel wrote: > >> tonight between 20:00 UTC and 22:00 UTC there will be a maintenance >> window for the Jenkins instance. > > Maintenance period is over now. All builds are running