My impression is also that it is better to keep HOL-ODE-Numerics non-slow: Changes in HOL-Analysis often break HOL-ODE-Numerics, and I think it is better to get that feedback earlier (on Jenkins, isatest, or a private -a -X slow build)
Fabian Am 31. Mai 2018 23:24:50 MESZ schrieb Makarius <makar...@sketis.net>: >On 31/05/18 16:36, Makarius wrote: >> >> Anyway, with approx. 100min CPU time HOL-ODE-Numerics has become >> eligible for the "AFP slow" category: paradoxically this will make >the >> test much faster, but also less accurate in its timing information, >> because the test hardware and settings are quite different. > >Several sessions depend on HOL-ODE-Numerics: >HOL-ODE-Examples, Lorenz_Approximation, Lorenz_C0, Lorenz_C1 > >So it is better to keep it as non-slow: otherwise the whole tower needs >to be moved. > > > Makarius >_______________________________________________ >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
