Re: [isabelle-dev] Maintenance work on Jenkins VM

[Lars Hupel]

Hi Dmitriy,

> What about having an additional afp_testboard repository where one 
> could also push -f changes. I am particularly interested in “slow” 
> sessions there.

for now I've created a job which runs everything but the slow sessions
(so not quite what you wanted). The repository is:

  

Same rules as for the Isabelle testboard apply.

The corresponding job is:

  

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