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