Email Gateway (Aug 22 2022 at 14:42): Email Gateway (Aug 22 2022 at 14:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now 7705926ee595.
The reason was the generalization of prime from nat to a generic
algebraic structure, including int. If you run the example in
Isabelle2016 changing int to nat, you run into the same performance
bottleneck.
Again, the overall problem is that simp rules for computing concrete
values are often not apt for abstract reasoning and vice versa.
Nevertheless in this particular case it is surely better to have that
simp rule removed.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 14:50):From: Stefan Berghofer <berghofe@in.tum.de>
Dear all,
while updating some of my theories to Isabelle2016-1, I noticed that simplification of some goals
involving numerals is extremely slow when the "Primes" theory is imported. In the attachment, you
can find a small theory containing two applications of "simp". When the Primes theory is loaded,
the first application takes about a minute to complete, whereas the second one returns almost
immediately. When importing Main instead of Primes, both invocations of simp are equally fast.
I did not observe this behaviour with Isabelle2016. Does anyone have an idea what is going wrong?
Perhaps the simpset got messed up during the recent update of the number theory library?
Greetings,
Stefan
Slow.thy
Email Gateway (Aug 22 2022 at 14:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
after a short chat with Manuel I was able to pin down the offending simp
rule.
But I have to check first whether this causes any breakdown in the distro.
Cheers,
Florian
dangerous_simp
signature.asc
Email Gateway (Aug 22 2022 at 14:50):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Florian and Manuel,
thanks for looking into this. I can confirm that locally deleting the prime_dvd_mult_iff rule
solves the problem with my theory.
Greetings,
Stefan
Email Gateway (Aug 22 2022 at 14:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Next round of refinement…
dangerous_simp
signature.asc
Email Gateway (Aug 22 2022 at 14:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Last round of refinement…
I am still at a loss to explain why this obviously somehow evil simp
rule did not result in such a mess in earlier releases and hence I am
uncertain whether we should really attempt to resolved this now.
Cheers,
Florian
dangerous_simp
dangerous_simp
signature.asc
Email Gateway (Aug 22 2022 at 14:51):From: Lawrence Paulson <lp15@cam.ac.uk>
The evidence may be clear that removing this simprule corrects the problem, but there is nothing obviously wrong with the rule. The problem may be due to an interaction with some other rule. Is this one really the underlying cause?
Larry Paulson
Email Gateway (Aug 22 2022 at 14:51):From: Makarius <makarius@sketis.net>
How is the situation concerning the Isabelle2016-1 release? The original
plan was to make the final snapshot on Monday. If another change is
coming, we need to respin, i.e. make a new release candidate.
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 14:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
At the moment I am inclined to leave things as they are and have a close
look after the release.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 14:51):From: Makarius <makarius@sketis.net>
OK, so I will make the final Isabelle2016-1 release snapshot tomorrow
(in approx. 24h).
Makarius
signature.asc
Last updated: Apr 18 2024 at 08:19 UTC