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