[isabelle-dev] HOL-ODE-Numerics vs. HOL-ODE-Refinement

[Fabian Immler]

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 <makarius at 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-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180601/727d409c/attachment.html>