Re: [isabelle-dev] New HOL/Import
On 03/28/2012 11:33 PM, Cezary Kaliszyk wrote: We have been working on a modernized reimplementation of HOL/Import, for HOL Light. We think we are at a point where it could be pushed to the main Isabelle repository replacing the old one. This has happened now, cf. 4c7548e7df86. A component with a proof bundle exported from HOL Light (and postprocessed further) is available at http://isabelle.in.tum.de/devel/components/hol-light-bundle-0.5-126.tar.gz It contains HOL-Light's equivalent of Main, i.e., the lemmas that you get when you use hol.ml in HOL Light. When this component is available, it will be imported as part of the HOL-Import session. You'll know that it happens when that session takes 30 seconds to run instead of 3 (on my laptop). Of course, this is not the whole story, as we are actually targeting flyspeck :-) Further refinements will happen at some point: we'll be looking at parallelization, and also try to track down remaining bottlenecks. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New HOL/Import
On Wed, 28 Mar 2012, Cezary Kaliszyk wrote: - The code is shorter and cleaner. For those that would like to inspect the code it is at: http://cl-informatik.uibk.ac.at/~cek/import.tgz Wow, I am impressed by the brevity of it. You should mention the secret http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be uncompressed, before it can be used with import_file in the example. You are no longer using any XML/YXML now. Is the format somehow related to OpenTheory by Joe Hurd? - Is anyone using the old HOL/Import? In principle you could ask on isabelle-users as well, although I would be surprised to hear about anybody using the old relic. It has sucked up maintenance resources for many years, without tangible results. - Does anyone have opinions about the HOL4 code that has been long dead? Which HOL4 code do you mean exactly? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New HOL/Import
On Thu, Mar 29, 2012 at 8:04 PM, Makarius makar...@sketis.net wrote: Wow, I am impressed by the brevity of it. You should mention the secret http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be uncompressed, before it can be used with import_file in the example. That's the preprocessed proof image for importing basic hol-light. You are no longer using any XML/YXML now. Is the format somehow related to OpenTheory by Joe Hurd? No; the information stored is similar to the old format, but more brief and easier to parse: every line contains a next typ/term/thm to read, with arguments space separated and last uses of an object marked with a minus. It could be converted (possibly automatically) to OpenTheory; however the sharing is done at a different level so it would be hard to recover additional sharing and without it, Opentheory would be at least an order of magnitude bigger. - Does anyone have opinions about the HOL4 code that has been long dead? Which HOL4 code do you mean exactly? The code currently in isabelle repository is in 3 places: Import, Import/HOL_Light and Import/HOL4 The Import/HOL_Light is functional but the proposed code replaces it. The Import/HOL4 has not been functional for a while, (I have not been able to use it even with proofs from 2004); should it still stay in the repository? Regards, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
