Re: [isabelle] "show" taking very long with goals with many hypothesis



On Tue, 11 Jun 2013, Joachim Breitner wrote:

I have an inductive proof where the induction rule has a lot of very
similar assumptions, due to the Nominal machinery

This thread is already quite old, but the performance problems "due to the Nominal machinery" are still there.

The question here is why Nominal2 needs to produce such large amounts of side-conditions that are structurally almost equal. None of the usual "could unify" shortcuts will work, and the system is bogged down as was observed here, not just for 'show' in Isar, but many other situations.

Nominal2 could and should be smarter in organizing this in a more compact and structured manner.


On Tue, 11 Jun 2013, Joachim Breitner wrote:

the real code is, for example, here: http://afp.sourceforge.net/browser_info/current/HOL/HOLCF/Nominal2/Launchbury/LaunchburyStacked.h$ (Lemma reds_fresh', case DApplication, first "thus").

Apart from that publicly visible application, Larry has shown me his private project which is all very huge and slow due to Nominal2. There are Simplifier invocations that take minutes due to all these small Nominal2 freshness particles.

We should probably move over this thread over to isabelle-dev, to sort out both the performance issues of Nominal2 and the question if it manages become part of the next Isabelle release, which will happen quite soon after the summer. (I am myself not an active participant of the nominal mailing list.)


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.