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? > It happens to very few people, only every 1-2 years. Such incidents are > not a problem and need not be taken into account of technical engineering. The build history paints a different picture. In an ideal world everyone would run "isabelle build -D $AFP -a -o document=pdf" before pushing, but clearly that is impractical. The alternative, giving developers direct access to the build machines to test out manually before pushing, is slightly less impractical overall, but it is not the preferred way by developers and it creates significant administrative overhead. > It wastes CPU resources that are missing for important tests: coverage > of thread parameters and other platform options is presently at 10-20% > of what the last isatest setup was doing (which was already in a state > of decline). We are flying mostly blind for a long time. That is not entirely true. Currently we cover 2, 6, and 8 threads on Linux and both 32 and 64 bit. All other tools (GHC, OCaml, ...) are uniformly available on all build machines and participate in regular testing. 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.) Missing Windows tests are not a new problem and require some engineering effort to automate due to more difficult administration and security concerns. Admittedly, the management of ML_OPTIONS as an environment variable is not ideal currently, but I think we came to an agreement about this earlier this month. > We have also lost the correlation of Isabelle vs. AFP. > > In the past, there was usually an accidental pairing of both repository > snapshots, because tests were started at a fixed time after midnight > when nobody was pushing. > > By recording the two repository ids together with the nightly build > status, it is usually easy to find a working state of particular AFP > entries, based on a suitable Isabelle version. This is not true at all. The correlation between Isabelle and AFP has never been better. Finding out the latest status is as easy as visiting <https://devel.isa-afp.org/status.shtml>, 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). The only caveat is that the "slow" sessions don't participate here; but even so, they break extremely rarely and their pairing to the Isabelle repository is also available through Jenkins. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev