[isabelle-dev] Remaining uses of defer_recdef?
florian.haftmann at informatik.tu-muenchen.de
Sun Jun 7 21:34:30 CEST 2015
> I could not believe that recdef could not be replaced by fun, so here is
> the patch that removes usages of recdef from Decision_Procs. The proof
> rules that come out of the function package are fine (one just needs a
> few split_format (complete) attributes in a few places).
> I'm not sure if this is something for the repository though, since it
> has a factor of >2 impact on the build-time:
> recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu
> time, factor 3.45)
> fun : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu
> time, factor 3.35)
> On the other hand 8 minutes is still not much. The longest fun
> invocation (numadd in MIR) takes about 2 minutes, other are all below 20
A compromise could be to let just the 2 min recdef stand and migrate the
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev