Re: [isabelle-dev] [isabelle] Status of HOL/Import
Hi Florian, On Sun, Mar 04, 2012 at 10:15:38AM +0100, Florian Haftmann wrote: I've been working on the Importer stuff, not very deeply, but separating HOL4 and HOL Light contents, stripping generic parts of any name reference to HOL4, etc. [...] Great! There could be done a lot more on the ML stuff to introduce basic coding practice there, of course, but for the moment I will leave that aside. As I mentioned to you privately, we (w Alex) are trying to write a new better import. So before working on the old one too much, lets first see which parts are reused and which will not. Two questions: a) There is a README; maybe you would like to update it according to your current expertise? b) After the pred/set issue, the generated HOL Light theories must be regenerated. Do you have time to accomplish this? Alternatively, I could follow the README instructions as soon as available. There are two issues; first: This is not as straightforward as it seems; apparently some of the constant maps have types that are not valid anymore (for example INSERT), so it is not going to work immediately. One can update it with most of the constant maps removed immediately; but I would suggest waiting a week or two for the new import and trying to get the maps correct there. But more importantly, the concept of generating these files and then replaying them with 'sorrys' is very strange in an LCF approach. Having built the session once, one can checkpoint the image and this is much nicer than the generated sources. The only thing this needs instead is some way to generate documentation. Makarius once suggested an antiquotation, that does something like 'print_theorems'. I have not investigated how to implement one? Cheers, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
but I would suggest waiting a week or two for the new import and trying to get the maps correct there. Ack. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
On Sun, 4 Mar 2012, Cezary Kaliszyk wrote: Makarius once suggested an antiquotation, that does something like 'print_theorems'. I have not investigated how to implement one? Pretty printing into latex source is not a big deal, if you are satisfied with regular multiline output in the display style of the document preparation system. If you are more ambitious, say you want some tabular stuff in Latex, then some experts on LatexSugar and Christian Urban can help. Alternatively, the pretty printing can be done in plain HTML. Yet more alternatively, you can just make an interactive print command, say like 'print_theory'. In Isabelle/jEdit the target will be HTML anyway. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
On 07/12/2011 11:15 PM, Florian Haftmann wrote: Hi Cezary (et al), first, thanks a lot for your efforts, this is a valuable contribution! There are a number of obvious things that could be done with it, like you mention Isabelle settings but also proper use of local theories (this would avoid the Stale theory errors), split conjunction theorems and look them up separately, etc. However I am not sure there is enough interest. The interest, I guess, is there, only the degree of suffering so far has always been below the critical line. I totally agree with Makarius that improvements will fall into disrepair as long as there is no regression test for the imports. Maybe one of the TUM guys would be willing to invest some time and effort to this? This doesn't seem so hard once we know how to build all this. I just tried to redo this to see how it works $ svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light $ cd hol_light/Proofrecording/hol_light $ make and it failed with [...] convert type.ml ... convert update_database.ml ... convert wf.ml ... warning: ignoring 'lemma1' in wf.ml warning: ignoring 'pth' in wf.ml warning: ignoring 'pth' in wf.ml done. 1622 named proofs found. make: Warning: File `pa_j_3.04.ml' has modification time 0.015 s in the future \ if test `ocamlc -version | cut -c3` = 0 ; \ then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \ else cp pa_j_3.1x_`camlp5 -v 21 | cut -f3 -d' ' | cut -c1`.xx.ml pa_j.ml; \ fi if test `ocamlc -version | cut -c1-4` = 3.10 -o `ocamlc -version | cut -c1-4` = 3.11 ; \ then ocamlc -c -pp camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I +camlp5 pa_j.ml; \ else ocamlc -c -pp camlp4r pa_extend.cmo q_MLast.cmo -I +camlp4 pa_j.ml; \ fi File pa_j.ml, line 104, characters 10-13: Parse error: :: or ] expected after [sem_expr_for_list] (in [expr]) File pa_j.ml, line 1, characters 0-1: Error: Preprocessor error make: *** [pa_j.cmo] Error 2 Any hints? Also, what is the HOL Light release policy? Is everybody really just using the svn head? Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss kra...@in.tum.de wrote: On 07/12/2011 11:15 PM, Florian Haftmann wrote: I just tried to redo this to see how it works $ svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light $ cd hol_light/Proofrecording/hol_light $ make and it failed with [...] The issue is with versions of OCaml. The HOL Light distribution includes a number of versions of the parser (files pa_j_XXX.ml) that are supposed to work with particular versions of OCaml. I am using an old version of OCaml for HOL Light (3.10.2) however the distribution includes some pa_j_ files for versions 3.11.XXX. Also make sure that camlp5 has the same version as ocaml; as this is not the case for example on macbroys. One more suggestions, try to run 'make' in the top directory of hol light first; after this works you can copy pa_j.ml and pa_j.cm* to ProofRecodring/hollight. Also, what is the HOL Light release policy? Is everybody really just using the svn head? Last named release (2.20) was in 2005, since then John Harrison sometimes packs versions considered more stable. Otherwise it is the SVN. Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
