since approximately Isabelle/e0cd57aeb60c (~1 week):
*** Malformed global fact
"Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict"
*** Illegal fixed variable: "s1"
*** At command "primrec" (line 164 of
"~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy")
Hi Lars,
Thanks for the heads-up. Makarius's change e0cd57aeb60c is clearly the
immediate source of the problem, but the more profound cause seems to be some
nonstandard handling of variables. The "illegal fixed variable" in question,
"s1", seems to originate from line 397 in "bnf_fp_n2m.ML":
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
The session HOL-ODE-Numerics has become much slower recently
(Isabelle/3a7f257dcac7:23e12da0866c and AFP/4b06a8701616:cf739ca5383b),
but it seems be just a consequence of removing HOL-ODE-Refinement:
lxcisa0 threads=1
ML_PLATFORM="x86_64-linux"
