[isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> 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
> seconds.

A compromise could be to let just the 2 min recdef stand and migrate the
others…

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150607/e7721e0a/attachment.sig>