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
