Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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.

I need to be more specific:

  * Why is a plain "nightly build" done many times per day? (As
immediate reaction on repository pushes.)

  * Why are testboard policies intermixed with "nightly build" policies?

Add-on question:

  * Why is there a testboard at all, instead of plain ssh access?


None of this has been seriously discussed so far.


As far as I remember, the original Mira testboard was introduced in a
situation, where builds became so slow and unwieldy that the mental
model was changed to "batch-queue management" on a hypothetical
computing cluster. Luckily, David Matthews saved us from that, and made
everything small and fast again.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 easy to repair.

Finding latex errors is indeed a bit awkward, but that is just a matter
of brushing up document preparation a bit.

Such a small pending reform of how Isabelle latex invocation works
should not have any impact on the model of Isabelle testing.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 tested and maintained
> just as much, which requires (at least) the hardware resources that we
> provide; we cannot dedicate half of it to manual testing.

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. These resources are then missing for important tests, as
well as interactive sessions.

This can be easily changed by giving up these design decisions:

  * quasi real-time reactivity (of what is actually a 1.5h batch build)

  * exclusive "provisioning" of machines for Jenkins


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

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 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 tested and maintained just as 
much, which requires (at least) the hardware resources that we provide; we 
cannot dedicate half of it to manual testing.


Leaving the AFP entries broken actually increases the human resources required 
to fix them later.



A broken Isabelle repository is different: it means all wheels stand
still.


Both for the repository and the AFP, everything is selective. Most people do not 
suffer if HOL-Proofs does not build, for example. Just as many AFP entries are 
irrelevant to most of us. But in the end we want all of it to work.


Tobias


That can be easily avoided by spending about 20min with manual
tests before pushing -- on decent hardware.

When the Isabelle repository is broken, which happens about 2 times per
year, there are friendly mails on isabelle-dev about it, mostly
reminders of README_REPOSITORY. Can you point out a mail thread, where
anybody was seriously blamed for it?



Another improvement I can think of is
that it would be good to have a little more control over testing:
aborting tests when they are not necessary anymore, testing only the
repository (and not the AFP) etc. All of this we can talk about and find
a solution in time.


Yes. I read it as: ssh access to a proper test machine. That is the
traditional Isabelle development model.

When the Prover IDE learns to use remote machines eventually, that will
also use ssh for direct interaction with jobs.



The reality of it all is that our testing infrastructure was in shambles for
quite some time. Then Lars came along and put in a lot of effort to get
things up and running again. The main response on this mailing list were
vague insinuations that he does not understand how to do tests, or does
not care about doing it properly, which could hardly be farther removed
from the truth.


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.

The present situation is that we have no proper test environment after
isatest was shutdown prematurely. This is what I have called "flying
blind", because vital performance measurements are missing.

I need to improvise something for the coming release -- which is the
reason why I have been off-line for some days, and also postponed the
start of the hot phase for Isabelle2016-1.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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

On my own 2 * 6 core machine, I usually use this:

  isabelle build -j4 -a -o threads=6

and settings as follows:

  ML_OPTIONS="-H 1500 --gcthreads 6"


> If I know that my changes affect specific AFP entries, I run
> them manually.

I've also found myself doing the prediction in my head. Some tool
support for that would be nice, but I have no concrete ideas right now.


> A full test takes a couple of hours, and it is a pain.

What I often do is

  isabelle build -j4 -a -d '$AFP' -X slow

It takes approx. 1h, but is changing quickly recently, due to massive
inflow of new AFP entries (which is a very good thing).


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

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.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

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, it isn’t 
ideal.

Larry

> On 6 Oct 2016, at 13:00, Makarius  wrote:
> 
> Putting secrets into a repository is a bad idea -- they stay there
> forever, even if they are "deleted" in some versions. When it is clone
> eventually, secrets will leak.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

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, Makarius  wrote:
> 
> Larry, can you describe your own build/test process?
> 
> 
> 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.
> 
> Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
> think of the famous Stoiber speech here).
> 
> 
> I am doing manual Isabelle tests on my own machin in approx. 30min,
> which is already a bit painful. 20min is OK, 10min would be delightful.
> 
> At some point I need to convene with David Matthews again, to see if and
> how we manage another jump forward in general performance.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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, collisions were pretty
> much guaranteed.
> 
> There cannot be useful performance measurements unless the environment
> is controlled, i.e. free of other accesses.

The general policies are rather simple:

  * automated tests are run during the night

  * humans use the same hardware during the day

  * everybody understands the difference, and takes care to avoid conflicts


For the new hardware, it could be done slightly differently:

  * CPU 0 is exclusive for automated tests

  * CPU 1 is exclusive for manual tests

>From the hardware architecture, such a clear separation of the two CPU
sockets with their local memory modules could work, but it requires
proper physical experiments prove that.

Splitting a single CPU socket into logical parts (as done now) is likely
to cause conflicts via caches. It might be one of the reasons, why the
current Jenkins measurements are still quite erratic.

Moreover, enabling hyperthreading on the CPU for manual testing would
give another factor of 1.2.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> 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 test environment after
> isatest was shutdown prematurely. This is what I have called "flying
> blind", because vital performance measurements are missing.

This was already your criticism in 2014, because the performance
measurements weren't even that good when I took over. At some point, you
showed me the "/devel" graphs and explained to me that we need something
better for serious measurements. I fail to see how the situation is now
somehow worse than what we had with isatest.

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, collisions were pretty
much guaranteed.

There cannot be useful performance measurements unless the environment
is controlled, i.e. free of other accesses.

> I need to improvise something for the coming release -- which is the
> reason why I have been off-line for some days, and also postponed the
> start of the hot phase for Isabelle2016-1.

What exactly do you have to improvise?

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 a
> continually working state, because Jenkins also serves a "continuous
> delivery" purpose: The AFP statistics page, and also everything else on
>  (including documents) is being produced by
> Jenkins. Failure to produce a document in that sense is also a failure
> to present an entry.

"Continous delivery" seems to be one of the Jenkins defaults that
suddenly intrude the Isabelle development process.

The reasons, why generated PDFs for the Isabelle repository should not
be required:

  * It demands precious additional minutes in the main build (with its
target for 10-20min, but presently going slightly beyond 30min on my
machine).

  * A broken Latex document is easy to repair.

So if nobody tests PDFs seriously, that is a gain for everyone. There
could be a weekly or monthly test to point out latex problems automatically.


For AFP, with its focus on PDF articles, the situation is certainly
different. But AFP is not the Isabelle repository.

Many of the open problems are caused by putting everything in one pot:
Isabelle, AFP, testboard, nightly builds with serious measurements.


> In the long term, it could also make sense to present the official
> Isabelle documentation (i.e. everything in "~~/src/Doc") in a similar
> fashion. Currently users have to build documents themselves.

There is already "isabelle build_doc -a". It could be included in a
separate build job.

Even more, there could be a nightly job to run "Admin/Release/build" and
publish the resulting mini website, as a rplacement of
http://isabelle.in.tum.de/devel with its "Download".


>> The 1 thread test is the base of all other tests. Without that it
>> becomes very difficult to see anything concerning performance changes.
> 
> This is not a problem; I have it on my list anyway.
> 
> Makarius, last time we spoke I didn't get the impression that this is
> crucial for performance analysis, which is why I didn't prioritize it.

I pointed out the importance of the threads=1 test several times. A
proper test setup needs to provide a "mostly flat line" as reference for
anything else. That has been Isabelle standard for almost 10 years, and
was only recently lost.

Without that, performance tuning becomes very difficult. It is one of
the reasons, why no serious tuning has happened recently.


> As always, I first need to figure out how long this takes on our
> hardware and if necessary, provision an appropriate machine.

I don't like this idea of exclusive "provisioning" of machines for the
Jenkins monster. It is the main reason why test hardware is lacking.

It is a paradoxical situation of both wasting a lot of CPU resources,
and of scarcity and austerity.


> It would also be great if, as we discussed, there was a possibility to
control
> "ML_OPTIONS" via options instead of environment variables.

This is now addressed by the new Admin/build_history tool (presently
2c5039363ea3), but that is a different story for a different thread.


> Pull: Implement a loosely-coupled extension for hgweb to fetch
> information from Jenkins. All changesets and their statuses are recorded
> in there and can be retrieved from the API, not unlike the statistics
> page. This can be done with Javascript and implemented without changing
> anything in Jenkins.
> 
> Push: Embrace Bitbucket and use their "Build Status" API [2]. This
> information is displayed in the "Builds" column in the "Commits" view.
> Of course, this only works for repositories hosted on Bitbucket. This
> likely requires some Scala code to work (i.e. performing an
> authenticated HTTP request).
> 
> I'd be happy if someone other than me could take the lead on this.

I have already started to think about the problem of integrating test
data into Isabelle history myself.

Presently there are two main questions:

  * Is it feasible to have a standard database server hosted at TUM
(that can run the next 10 years), and be publicly accessible by some
standard protocol and standard authentication?

  * What are the prospects for generally available test hardware --
non-exclusive as in the past?


> In software engineering, this is known as "Not Invented Here" syndrome :-)
> 
>>   * How much efforts are required to make proper use of it? I.e. what is
>> the "payload" of it as a "carrier system" for an actual application.
> 
> The advantages, as outlined by Florian, by far outweigh the efforts.

Such discussions always need to true sources at hand. Where are the
Isabelle/Jenkins sources?


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> 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 sources in general, that's an easy question to answer:

  

And more specifically, the "remote machine" part:

  

There aren't any custom plugins running in our Jenkins instance.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> 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 possible.
The last three or so testboard runs didn't spend time waiting in the queue.

> Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
> think of the famous Stoiber speech here).
> 
> I am doing manual Isabelle tests on my own machin in approx. 30min,
> which is already a bit painful. 20min is OK, 10min would be delightful.

Here's my quick back-of-the-envelope calculation:

Our current testboard setup runs AFP with -j8 -o threads=2, that is, on
16 cores. It requires an elapsed time of 1:30 and 20:30 CPU hours.

Isabelle "build -a" runs with -j3 -o thread=2 (total 6 cores), with an
elapsed time of 1:20 and 6:45 CPU hours.

Let's just discount multithreading overhead for a bit here (it's two
threads per process anyway). We're getting a total of about 27 CPU
hours, give or take.

In order to process that full workload in 30 minutes, that would require
in the order of 50 cores with full load. We're close with a total of 44
cores. But for fairness, we're running the workload not on the full
number of cores, but rather just half.

In any case, I don't see how anything less than 30 minutes can be done
with reasonable hardware. And if at some point there are enough
improvements that it can be done on hardware, it's orthogonal to
Mira/Jenkins/whatever ...

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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

When we introduced Mercurial in 2008, this was one idea to aim at
eventually. Today, I would refrain from any automatic daemon producing
changesets.

Instead, it should be easy and painless for human users to do that
themselves. At some point, builds could be integrated nicely into the
Prover IDE, together with regular Mercurial repository operations.


> 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 prefer to have AFP working all the time, but that would require
much more resources, both hardware and humans.

A broken Isabelle repository is different: it means all wheels stand
still. That can be easily avoided by spending about 20min with manual
tests before pushing -- on decent hardware.

When the Isabelle repository is broken, which happens about 2 times per
year, there are friendly mails on isabelle-dev about it, mostly
reminders of README_REPOSITORY. Can you point out a mail thread, where
anybody was seriously blamed for it?


> Another improvement I can think of is
> that it would be good to have a little more control over testing:
> aborting tests when they are not necessary anymore, testing only the
> repository (and not the AFP) etc. All of this we can talk about and find
> a solution in time.

Yes. I read it as: ssh access to a proper test machine. That is the
traditional Isabelle development model.

When the Prover IDE learns to use remote machines eventually, that will
also use ssh for direct interaction with jobs.


> The reality of it all is that our testing infrastructure was in shambles for
> quite some time. Then Lars came along and put in a lot of effort to get
> things up and running again. The main response on this mailing list were
> vague insinuations that he does not understand how to do tests, or does
> not care about doing it properly, which could hardly be farther removed
> from the truth.

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.

The present situation is that we have no proper test environment after
isatest was shutdown prematurely. This is what I have called "flying
blind", because vital performance measurements are missing.

I need to improvise something for the coming release -- which is the
reason why I have been off-line for some days, and also postponed the
start of the hot phase for Isabelle2016-1.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 mechanism of the sort you 
> describe (provided it’s easy to use) would be ideal.

Larry, can you describe your own build/test process?


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.

Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
think of the famous Stoiber speech here).


I am doing manual Isabelle tests on my own machin in approx. 30min,
which is already a bit painful. 20min is OK, 10min would be delightful.

At some point I need to convene with David Matthews again, to see if and
how we manage another jump forward in general performance.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 cannot be public
> because they contain passwords and private keys. As for the public bits,
> you have already found and changed them.
> 
> Given the apparent "rhetoric" nature of this question I can no longer
> assume that you are arguing in good faith.

I have asked this question several times privately, and always got the
same answer.

Putting secrets into a repository is a bad idea -- they stay there
forever, even if they are "deleted" in some versions. When it is clone
eventually, secrets will leak.


The reasons why I am asking for public sources are manifold, including
general "open-source" reasons: work can be inspected, discussed, reused etc.

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.

Moreover, just empirically from what I have seen in the last 10-15
years: Isabelle infrastructure that is not easily accessible does not
survive very long. (Mira was an example for that.)


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

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 automatically be
> merged into the repository without an additional test. This avoids the
> current duplication of tests where one first pushes to the testboard,
> waits for everything to run through, and then pushes to the repository
> where everything is tested again.

This is definitely achievable; however, it needs broad developer
consensus first, because it's a change in the usual workflow. Consider
this a call for opinions.

Granted, the duplication of tests is an issue, but unfortunately, hard
to avoid under the current circumstances. By changing the workflow to
make breaking changes (except possibly AFP) "syntactically impossible",
many things can be simplified. Bitbucket, for example, has facilities to
enable such a workflow.

However, before we do that, we need to think carefully about formalising
the connection between Isabelle and the AFP. I'll let others take the
lead on this – Florian, maybe?

Also note that the status page now includes a load diagram. While the
interpolation is somewhat strange, it shows a clear trend: the
infrastructure is operating below 50% capacity.

> 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 a
continually working state, because Jenkins also serves a "continuous
delivery" purpose: The AFP statistics page, and also everything else on
 (including documents) is being produced by
Jenkins. Failure to produce a document in that sense is also a failure
to present an entry.

In the long term, it could also make sense to present the official
Isabelle documentation (i.e. everything in "~~/src/Doc") in a similar
fashion. Currently users have to build documents themselves.

> The 1 thread test is the base of all other tests. Without that it
> becomes very difficult to see anything concerning performance changes.

This is not a problem; I have it on my list anyway.

Makarius, last time we spoke I didn't get the impression that this is
crucial for performance analysis, which is why I didn't prioritize it.
As always, I first need to figure out how long this takes on our
hardware and if necessary, provision an appropriate machine. It would
also be great if, as we discussed, there was a possibility to control
"ML_OPTIONS" via options instead of environment variables.

> I am still hoping for October (which is actually now). I have explained
> many times privately, what the purpose of "platform tests" is: a
> portfolio of officially supported platforms -- some of them unusual for
> most isabelle-dev users -- need to be continuously tested (meaning once
> per day, or even once per week).

Together with Thomas Fritz I have already provisioned a native (i.e.
non-virtualized) El Capitan worker a week ago [0]. It runs a nightly
"build -a" job [1], 32 bit, 2 threads. It requires approx. 5 h for that.
It also doesn't send messages on failure (currently).

Makarius, if you'd like to be subscribed to build mails, please tell me.
Otherwise it'll stay silent.

> Mira was actually quite good in adjoining information to the repository
> history views of the two repositories. Over a few years, that was the
> main tool for me to figure out what works and what not, and to see when
> it stopped working etc. Right now, it requires much more clicking, and I
> am still unsure where the information is actually hidden.

The reason why it was "quite good" is that it was tightly coupled to the
Mercurial API; this is also the reason for its eventual demise.

There are two possible proper solutions for this, "push" and "pull".

Pull: Implement a loosely-coupled extension for hgweb to fetch
information from Jenkins. All changesets and their statuses are recorded
in there and can be retrieved from the API, not unlike the statistics
page. This can be done with Javascript and implemented without changing
anything in Jenkins.

Push: Embrace Bitbucket and use their "Build Status" API [2]. This
information is displayed in the "Builds" column in the "Commits" view.
Of course, this only works for repositories hosted on Bitbucket. This
likely requires some Scala code to work (i.e. performing an
authenticated HTTP request).

I'd be happy if someone other than me could take the lead on this.

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

I don't understand what that means. "Changeset identification" works
perfectly fine. 

Re: [isabelle-dev] Jenkins maintenance

[Manuel Eberl]

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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

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 to use) would be ideal.
Larry

> On 3 Oct 2016, at 16: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 additional test. This avoids the
> current duplication of tests where one first pushes to the testboard,
> waits for everything to run through, and then pushes to the repository
> where everything is tested again.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Manuel Eberl]

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 this
happen, and that's what Lars did – much of it, as I gather, in his free
time. I'm sure Lars does not object to others adapting this
infrastructure, and he has in fact already implemented a number of
suggestions for improvements.

>From what I have picked up, the new testing infrastructure we have now
is also a lot more adaptable and maintainable than anything we had
before. The words ‘industry standard’ may seem meaningless to you,
Makarius, but it cannot be denied that if /everyone/ does testing in a
certain way these days, then that is at least some evidence that it
might be a good idea to consider. Relying on the vague idea that things
never break because people never make mistakes does not seem like a
sensible approach to me – and once you accept that things /can/ break
because people /do/ make mistakes, prompt notification of /what/ broke
and /why/ is important.

No one is saying that the current state of affairs is optimal. I can
think of a number of possible improvements myself and have privately
communicated them to Lars, who seemed quite grateful for the feedback.

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 additional test. This avoids the
current duplication of tests where one first pushes to the testboard,
waits for everything to run through, and then pushes to the repository
where everything is tested again. 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) Another improvement I can think of is
that it would be good to have a little more control over testing:
aborting tests when they are not necessary anymore, testing only the
repository (and not the AFP) etc. All of this we can talk about and find
a solution in time.

It is important here to stress that none of us is working /against/
another – we all want the best possible infrastructure to do our work,
and I for one do not like the path this discussion has been taking. The
reality of it all is that our testing infrastructure was in shambles for
quite some time. Then Lars came along and put in a lot of effort to get
things up and running again. The main response on this mailing list were
vague insinuations that he does not understand how to do tests, or does
not care about doing it properly, which could hardly be farther removed
from the truth.

This email is getting a bit longer than I had planned, so let me
summarise my points once more for additional clarity:
– The current testing infrastructure is good, but not perfect, and we
should work together to make it better.
– The testboard, while also not perfect, has already become an
invaluable tool in my work on both Isabelle and the AFP.
– The tone of the discussion on this mailing list could occasionally do
with a little less passive-aggressiveness and fewer underhanded
insinuations.
– Lars deserves enormous gratitude from all of us for the work he put
into this so far. Of course, this does not mean that his decisions must
not be criticised, but when you work on something (mostly) alone in your
free time and the only public response you get is complaints, that's not
exactly uplifting.


Cheers and a happy Unification Day to all of you,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> 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 and private keys. As for the public bits,
you have already found and changed them.

Given the apparent "rhetoric" nature of this question I can no longer
assume that you are arguing in good faith.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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
> handling, proper daemonizing – it is surely easy to extend that list.
> The Jenkins universe, as fas as I can tell, embodies significant
> expertise in that area which you don't want to reimplement.

Using huge and complex things like Jenkins poses the usual questions:

  * How much efforts are required to make proper use of it? I.e. what is
the "payload" of it as a "carrier system" for an actual application.

  * Which policies and attitudes of the platform are forced on the
application? How easy (or difficult) is it to reshape it for our the
requirements.


So far, my impression is that Jenkins fares not too well in these
respects. What does it really deliver, for all the efforts?

And where are the public sources of Isabelle/Jenkins?


Makarius




signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Florian Haftmann]

> 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
following intentions:
a) provide a replacement for the isatest infrastructure with its
uncertain future at that time;
b) separate the »general idea« from the concrete application;
c) explore the design space for scheduling tests covering and combining
multiple histories.

The incentive to pursue c) led us to ignore Hudson/Jenkins entirely,
with the attitude »keep it simple, stupid«.

The following insights contributed to abandon the project:

1) Over time it became manifest that c) is too ambitious wrt. real
existing resources, hence the insight that pragmatically »tip testing«
is not so bad at all.

2) Further, »keep it simple, stupid« came to its limits with all the
involved technicalities: issues jobs on remote machines, exception
handling, proper daemonizing – it is surely easy to extend that list.
The Jenkins universe, as fas as I can tell, embodies significant
expertise in that area which you don't want to reimplement.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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
> repository with wide platform coverage, systematic collection of
> statistics etc.
> 
> In my perception the current Jenkins infrastructure has a slight bias
> towards b);  but I guess the framework is flexible enough to cover c)
> also, although I am not that involved to tell on the spot what would be
> missing here.

I guess there is no technical problem to do c) with Jenkins, only a lack
of understanding how important long-term testing over many platforms
with many parameters is.

Isabelle + AFP has grown a lot in the last 2-3 years, which can be seen
in the very nice overview https://devel.isa-afp.org/statistics.shtml

That growth will come to a grinding halt, if the continuous performance
tuning of the system can no longer be done properly, due to lack of
important test data.


Makarius




signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 the Jenkins API.
> The entire history is recorded and formally available (admittedly not in
> the repository).

Mira was actually quite good in adjoining information to the repository
history views of the two repositories. Over a few years, that was the
main tool for me to figure out what works and what not, and to see when
it stopped working etc. Right now, it requires much more clicking, and I
am still unsure where the information is actually hidden.

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.

Jenkins might have catched up a bit in recent years, but such huge tools
usually don't change substantially.


This means, any Isabelle tools built on top of Jenkins need to try hard
to do it the proper way, e.g. working over timeless / stateless
Mercurial history in a monotonic fashion. Views should make it easy to
see "into the history", without requiring a lot of clicking.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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#l282)
there is

  * a strict obligation to make a full build -a, before pushing anything
to the Isabelle repository (also after the merge)

  * no need to test pdf documents

  * no need to have AFP in a fully working state (although it would be
nice to sort problems out eventually)


> That is not entirely true. Currently we cover 2, 6, and 8 threads on
> Linux and both 32 and 64 bit.

The 1 thread test is the base of all other tests. Without that it
becomes very difficult to see anything concerning performance changes.


> Missing Mac tests are not the fault of the infrastructure itself, but a
> result of a difficult hardware situation, imposed by Apple. Still, I'm
> working on it, as I've already told you earlier this month. However,
> it's not a deal-breaker: Many Mac users routinely use the development
> version; system bootstrapping or integration problems will get detected
> very early even without automated testing. (That doesn't change the fact
> that automated testing on Mac is imminent, hopefully early October.)

I am still hoping for October (which is actually now). I have explained
many times privately, what the purpose of "platform tests" is: a
portfolio of officially supported platforms -- some of them unusual for
most isabelle-dev users -- need to be continuously tested (meaning once
per day, or even once per week).

That platform coverage is especially important when we approach a
release -- that is a phase when components tend to be updated.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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

Here are the meaningless buzzwords from that paragraphs:

  industry standard
  best practice
  outdated model

So far there were no explanations what the purpose of real-time
continuous integration for Isabelle really is. My questions were never
meant rethorically, but seriously.

There must be reasons behind this that can be explained, instead of
affirming "we want continuous integration".


We are heading towards an Isabelle release, which is a very delicate
process. For months the testing infrastructure is covering less than
half of the old isatest, which was already in a state of decline.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

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 reasons, not buzzwords.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

(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 Jenkins home
> page, too. In the unlikely event that something goes wrong with my
> deployment scripts and I have to roll back changes,

Maintenance period is now over. Here are the most prominent changes
affecting users.

~~~

- Previously, in occasions where Jenkins is under high load, subjob runs
(e.g. "isabelle-repo-afp") might have used a different Mercurial
revision than the parent job. This situation will not occur anymore.
Now: as soon as a job gets kicked off, the Isabelle revision is fixed.

  - 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 repository at some point and will monitor how much this
increases overall load.

  - This also means a potential increase in build notifications. To
alleviate this, I have changed the configuration such that all failure
mails will only be sent when the first failure in a job occurs. If it
keeps failing, no more emails. If it succeeds again and then fails
again, a new email.

- All "makeall" jobs now run in 64 bit mode to avoid spurious failures.
This is now uniform between "makeall" and "afp" jobs.

- The "isabelle-nightly-benchmark" job now runs more than just
"~~/src/HOL/Benchmarks", but also a variety of "critical" sessions to
obtain reliable timing information. It continues to run in 32 bit mode.

- The new job "isabelle-release-makeall" checks the Isabelle release
repository. This will become relevant after the fork point for
Isabelle2016-1. Currently, there is no job integrating that repository
and the AFP. I'm not sure yet how that should be organized.

- All builds now carry timestamp information in the console output.

- There are now four different views on the front page of Jenkins (these
are the newly-introduced tabs above the list of jobs).

  - "All": same as before; all jobs
  - "dashboard": graphical overview without testboard; this is like a
"mission control view"
  - "multijob": shows the hierarchical structure of the jobs*
  - "nightly": just the nightly jobs

I encourage all developers to try out the "dashboard" and "multijob"
views and give feedback:

  
  

One of them is eventually going to become the default view.

~~~

As always, feedback is appreciated. There are more changes planned (new
jobs), but they can proceed without downtime.

Cheers
Lars




* The "multijob" plugin experienced some breaking changes recently. This
lead to nasty exceptions being displayed by Jenkins. I have now deployed
an unreleased, patched version which I believe is stable. If you see any
JVM stack traces or exceptions, please report them to me privately.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> 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 now executing the bulk of the jobs on new
hardware (44 cores!) with the following layout:

- AFP: -j 8 -o threads=2
- makeall: -j 3 -o threads=2
- slow: -j 1 -o threads=8

For developers, nothing changed. URLs and repositories stay the same.

Note that the domain "ci.isabelle.systems" already points to the new
server, but DNS propagation might take a while. So it might very well be
that you receive mails with links that don't work until tomorrow, 23th
July 16:00 UTC.

Thanks for your patience!

Cheers
Lars

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Dmitriy Traytel]

> 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 space is not hardwired. Any "component" can add 
> new tool directories by augmenting ISABELLE_TOOLS.
> 
> So there could be a "testboard" component to abstract whatever needs to be 
> abstracted.

I see. Then I am in favor of a “non-main” component that provides a tool which 
starts a new test job (either via plain push -f as before, or something 
complicated involving new repositories but also supporting mq-patches).

Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Makarius]

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 directories by augmenting ISABELLE_TOOLS.


So there could be a "testboard" component to abstract whatever needs to be 
abstracted.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Dmitriy Traytel]

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 would need to use the 
-f for testing mq-patches.

Overall, I don’t see a too big problem with force-pushing. Florian showed how 
to do it properly on the client's side [1]. If everybody would just use this 
setup, we would not be talking here.

Dmitriy

[1] 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-February/002258.html


> On 16 Feb 2016, at 10:44, Lars Hupel  wrote:
> 
>> 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 happens once every five years or so, maybe it's not
>> so great an issue that the workflow needs to be changed.
> 
> As I said, I'm not blaming anybody. Any workflow which requires
> force-pushing on a regular basis is broken. In particular, I wouldn't
> want to encourage contributors to make their own scripts.
> 
> To that end I'm suggesting an official "Isabelle tool" which schedules
> testboard builds. Ideally this would push to some fresh repository,
> schedule a build, and delete the repository again. Users would write
> "isabelle testboard" and be done with it. I'll sit down on the weekend
> and try to come up with a proof of concept.
> 
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Lars Hupel]

> 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 happens once every five years or so, maybe it's not
> so great an issue that the workflow needs to be changed.

As I said, I'm not blaming anybody. Any workflow which requires
force-pushing on a regular basis is broken. In particular, I wouldn't
want to encourage contributors to make their own scripts.

To that end I'm suggesting an official "Isabelle tool" which schedules
testboard builds. Ideally this would push to some fresh repository,
schedule a build, and delete the repository again. Users would write
"isabelle testboard" and be done with it. I'll sit down on the weekend
and try to come up with a proof of concept.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Jasmin Blanchette]

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 workflow of force-pushing into some "dumping ground" repository.
> Any ideas?

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 happens once every five 
years or so, maybe it's not so great an issue that the workflow needs to be 
changed.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Gerwin Klein]

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 not yet sent to the mailing list, neither is there a benchmark
> job. The reason follows.
>
>
> There was some weirdness wrt to the testboard. New jobs would suddenly
> complain about 'bin/isabelle not found' or similar. My suspicion was
> that either Jenkins, Mercurial or both got confused about the meaning of
> the "default" branch (possibly an ancient revision which reappeared?),
> so I nuked and re-create all testboard jobs, resulting in the loss of
> old builds (those weren't of much value anyway).
>
> 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 workflow of force-pushing into some "dumping ground" repository.
> Any ideas?
>
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev