Re: [isabelle-dev] HOL-IMP very slow
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice of
names in Skolemization, that has been entirely redone in the past few years.
I imagine it is now something like this:
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =
EVERY1 [skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt'])
ctxt 1]) i st
(I found this in meson.ML.)
The original version made little use of contexts, as I recall.
I was a bit confused when I wrote about skolemization being the culprit. The
problem is that fixed variables occurring in the conjecture end up keeping
their names (modulo some slight alterations). After all, such variables are for
all practical purposes just like constants. By fixed variables, I mean among
other things the parameters of the goal (those entites which rename_tac
works on).
That metis performance is affected by the naming of constants is not
surprising to anybody who knows a thing or two about automated reasoning, but
it is surprising that even the goal parameter naming affects it.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
I know it was a problem for machine learning that a free variable in a goal (x
say) might appear with multiple types in a problem set. This is connected with
the issue you’re describing now. I assume that that was solved somehow.
Larry
On 13 Feb 2014, at 12:31, Jasmin Blanchette jasmin.blanche...@gmail.com wrote:
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice of
names in Skolemization, that has been entirely redone in the past few years.
I imagine it is now something like this:
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =
EVERY1 [skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt'])
ctxt 1]) i st
(I found this in meson.ML.)
The original version made little use of contexts, as I recall.
I was a bit confused when I wrote about skolemization being the culprit.
The problem is that fixed variables occurring in the conjecture end up
keeping their names (modulo some slight alterations). After all, such
variables are for all practical purposes just like constants. By fixed
variables, I mean among other things the parameters of the goal (those
entites which rename_tac works on).
That metis performance is affected by the naming of constants is not
surprising to anybody who knows a thing or two about automated reasoning, but
it is surprising that even the goal parameter naming affects it.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
On Thu, 13 Feb 2014, Jasmin Blanchette wrote:
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice
of names in Skolemization, that has been entirely redone in the past
few years. I imagine it is now something like this:
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =
EVERY1 [skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt
1]) i st
I was a bit confused when I wrote about skolemization being the
culprit. The problem is that fixed variables occurring in the conjecture
end up keeping their names (modulo some slight alterations). After all,
such variables are for all practical purposes just like constants. By
fixed variables, I mean among other things the parameters of the
goal (those entites which rename_tac works on).
That metis performance is affected by the naming of constants is not
surprising to anybody who knows a thing or two about automated
reasoning, but it is surprising that even the goal parameter naming
affects it.
The Subgoal.FOCUS combinator turns goal parameters into local fixes of the
context, re-using the accidental comment fields in the Abs nodes, in the
traditional way as they are printed (this is a well-known insider joke).
What I have explained before about the reasons to use Variable.next_bound
in the Simplifier seems to apply here as well. So I should probably try
the same in these structured proof combinators, but the formerly adhoc
bounds of the Simplifier need a few more reforms first, to make them
actual fixes.
In any case, such a change of internal names is likely to break existing
proofs and proof tools, but this needs concrete empirical exploration
instead of speculation.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
Tests about slowness take long, but here is a presumably good point in the published history: Isabelle/db691cc79289 Finished Pure (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.20) Finished HOL (0:02:13 elapsed time, 0:05:56 cpu time, factor 2.67) Finished HOL-IMP (0:01:58 elapsed time, 0:07:28 cpu time, factor 3.79) It probably corresponds to AFP/08874371d79e. This might help someone to detach for a few hours or days, until the public history is back to normal and in a testable state. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
Should be fine again (or at least better) with b445c39cc7e9. Thanks for the notification. Dmitriy Am 12.02.2014 16:28, schrieb Makarius: Tests about slowness take long, but here is a presumably good point in the published history: Isabelle/db691cc79289 Finished Pure (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.20) Finished HOL (0:02:13 elapsed time, 0:05:56 cpu time, factor 2.67) Finished HOL-IMP (0:01:58 elapsed time, 0:07:28 cpu time, factor 3.79) It probably corresponds to AFP/08874371d79e. This might help someone to detach for a few hours or days, until the public history is back to normal and in a testable state. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel tray...@in.tum.de: Should be fine again (or at least better) with b445c39cc7e9. Thanks for the notification. For the record: The goal state before and after had different variable names in it. These become Skolem constants to Metis (in the FO logic sense, not in the Isabelle sense). The Metis prover, like most if not all ATPs, is sensitive to the (relative order of the) names of the symbols -- e.g. it may apply different rules in a different order. It would be possible, and indeed a good idea, to insulate ourselves from this by having the metis proof method name Skolems serially (sk1, sk2, etc.) before invoking the Metis prover [*]. This would probably trigger a couple of bad cases like we saw today, but as a result we would be immune from the disease. I'll think about this. Jasmin [*] Subtle terminology point: Metis is a FO ATP developed by Hurd. metis is a higher-order proof method (and tactic) that translates HOL to FOL (like Sledgehammer does), developed by Paulson Susanto. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
Am 12.02.2014 um 16:03 schrieb Makarius makar...@sketis.net: I see a lot of incoming changes (and many hg queue accidents) just before that, The accidents were that I experimented with qfold for the first time. The command merges two patches together. The patches themselves were all as I intended them to be, and the extra pass I applied to reorder and merge the patches was well worth it. What I didn't notice until it was too late was that after merging, the messages were merged as well (with * * * and in a multiline style). I had expected only the description of the parent patch (the one that's merged into) to appear. The one-line format used for displaying descriptions encouraged my misbelief. To those who use queues and don't know about hg qpush --move and hg qfold (which didn't exist some years ago): Those are very useful tools, when used correctly. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
On Wed, 12 Feb 2014, Jasmin Blanchette wrote: Metis is a FO ATP developed by Hurd. metis is a higher-order proof method (and tactic) that translates HOL to FOL (like Sledgehammer does), developed by Paulson Susanto. Do you understand yourself how that works? Does that refer to Metis or metis? I've never looked much under Metis's hood except to tweak its options. For metis, the answer is a qualified yes. Mainly the proof reconstruction on the Isabelle side, especially the question of type variables. See also 568b2cd65d50: the long comment in the source after the change looks like the recently introduced reform of Thm.bicompose (0fa3b456a267) might help here, but it didn't. Or maybe I was just confused about 8 different modes of that function. (One of the booleans is only required for this particular instance, IIRC.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-IMP very slow
Am 12.02.2014 um 20:40 schrieb Makarius makar...@sketis.net: Mainly the proof reconstruction on the Isabelle side, especially the question of type variables. I can't help much there. Perhaps Larry knows more. All I can recall is that Metis sometimes suggests type instantiations (since types are encoded as terms, and type variables as term variables), but that in metis these are ignored for some reason, sometimes leading to more polymorphic theorems on the Isabelle side of things than on the Metis side. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
