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
