Hi Andreas, > In Isabelle2014, processing this datatype declaration takes about one minute. > So what has happened in between? (The Isabelle2014 timing panel is also way > off with 8 seconds.)
Thanks for your report. What happened in between is that we generate more theorems. I suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the number of constructors. As for the timing panel, I suspect it does not take into consideration the time spent in tactics with multithreading on, but I’m not an expert there. We’ll look into this. You could try “quick_and_dirty” around that particular datatype to make things more tolerable in the meantime. Cheers, Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
