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] The HOL Light library

And now that I have managed to prove “invariance of domain”, a significant if not especially famous result. Larry > On 6 Oct 2016, at 14:08, Makarius wrote: > > Definitely. It is probably worth a line to the ANNOUNCE file for > Isabelle2016-1.

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

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

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

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

> 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

> 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] The HOL Light library

On 03/10/16 15:16, Lawrence Paulson wrote: > I’ve just added a lot more advanced material from HOL Light. There isn't much > about this in the NEWS file; unfortunately there is no headline result to > mention or even a dominant theme. Nor can we say that the entire library has > been ported.

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

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

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

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