> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
