> The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc > measures to get meaningful interactive tests, without wasting too much > time. It probably makes sense to imitate that for "testboard" setups.
The idea is to distribute the build load over multiple machines, since that isn't supported by "isabelle build". This is generally helpful – even if we get better hardware – because distributing jobs is trivial with Jenkins and there's no reason we shouldn't. The shorter the build time, the better. > For regular batch tests in the style of "isatest", the main purpose is > to accumulate accurate timing information, and preserve that in a simple > format over a long time. This has been forgotten in recent years, since > measurements have become more and more messed up. So performance-wise, we > are flying blind, especially for AFP. I can't yet say with confidence that we now have a setup with reliable performance numbers. In a couple of days I will look at the numbers to get an idea of their variance. > A related question is what to do with SML/NJ and the ML_SYSTEM_POLYML > variable. For the Isabelle2016 release, I've tried to build everything > with SML/NJ as usual, but many sessions failed, even just HOL-Library. > > We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session > for SML/NJ. > > Or we could discontinue SML/NJ altogether. I proposed that the last > time 10 years ago. Building with SML/NJ configuration is trivial. It would be "just another job" in Jenkins. I'd just need to know about what to build precisely. Can you explain to me what the ML_SYSTEM_POLYML variable means? Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev