Re: [isabelle-dev] Jenkins maintenance

On 06/10/2016 17:11, Makarius wrote: 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 t

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 broken Latex document is

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 Signature

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 te

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 pre

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 experiment

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. Still

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, Makar

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, c

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 sourc

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 poss

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 mech

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 c

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 a

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 h

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 t

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 passwords

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 fo

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 (http://isabelle.in.tum.de/repos/isabelle/file/ec0fb01c6d50/README_REPOSITORY#l2

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 > jus

Re: [isabelle-dev] Jenkins maintenance

Dear all, let my add my perspective on testing an general as I perceive it; maybe this helps to clarify the discussion. I personally distinguish the following use cases, with decreasing distance to production: a) Iterative evaluation of changes to the system You change something, and run build

Re: [isabelle-dev] Jenkins maintenance

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? > It happens to very few people, only every 1-2 years. Such incidents are > not a problem and need not be taken into account of techni

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 rea

Re: [isabelle-dev] Jenkins maintenance

On 24/09/16 17:47, Lars Hupel wrote: >> This reminds me of a still open question: Why is there this "continuous >> integration" on every push anyway? > > This question is not open; it has been answered quite often in the past. > > For the repositories, it serves as a reminder to not push "broken"

Re: [isabelle-dev] Jenkins maintenance

> This reminds me of a still open question: Why is there this "continuous > integration" on every push anyway? This question is not open; it has been answered quite often in the past. For the repositories, it serves as a reminder to not push "broken" changes. (Or at least repair problems when the

Re: [isabelle-dev] Jenkins maintenance

On 24/09/16 16:55, Lars Hupel wrote: > > Note that worker allocation is "first come first serve". We currently > have bandwidth for two AFP and two distribution builds at the same time, > each taking approx. 80-90 minutes; everything else gets queued. Please > push responsibly. This reminds me of

Re: [isabelle-dev] Jenkins maintenance

> - This means that we're getting close to be able to run concurrent > jobs. Currently, some pushes don't get built: when a job is already > running and more than one push happens in the meantime (only the last > push is built). Soon, all pushes will get built. I will enable this for > the AFP re

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 is

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 Isabelle tool name spac

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 directorie

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 happen

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 > this

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 again. > > Mails are no

Re: [isabelle-dev] Jenkins maintenance window

> 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 again. Mails are not yet sent to the mailing list, neither is there a benchmark job. The reason follows. There was some weirdness wrt t