On 27/09/16 11:43, Lars Hupel wrote: > > In an ideal world everyone would run "isabelle build -D $AFP -a -o > document=pdf" before pushing, but clearly that is impractical.
According to the official README_REPOSITORY (http://isabelle.in.tum.de/repos/isabelle/file/ec0fb01c6d50/README_REPOSITORY#l282) there is * a strict obligation to make a full build -a, before pushing anything to the Isabelle repository (also after the merge) * no need to test pdf documents * no need to have AFP in a fully working state (although it would be nice to sort problems out eventually) > That is not entirely true. Currently we cover 2, 6, and 8 threads on > Linux and both 32 and 64 bit. The 1 thread test is the base of all other tests. Without that it becomes very difficult to see anything concerning performance changes. > 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.) I am still hoping for October (which is actually now). I have explained many times privately, what the purpose of "platform tests" is: a portfolio of officially supported platforms -- some of them unusual for most isabelle-dev users -- need to be continuously tested (meaning once per day, or even once per week). That platform coverage is especially important when we approach a release -- that is a phase when components tend to be updated. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
