Hi Florian, On Wed, Jul 13, 2011 at 6:15 AM, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> wrote: > Of course there is a lot one could clean up. In my eyes there are some > issues which prevent an understanding of HOL-Import »in the large«, and > maybe your experience could answer the following questions: > > a) HOL-Import seems to import both HOL4 and HOL Light, but the ROOT.ML > file > http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/ROOT.ML > only mentions HOL4Compat and HOL4Syntax as imported theories. Where > does HOL Light come in?
The setup is indeed confusing and it would be great to change it. Currently IsaMakefile allows for two targets: HOL-Generate-HOL and HOL-Generate-HOLLight (They cannot be called together, so the 'generate' target in the makefile does not make sense). Generate-HOL refers to the ROOT.ML you mentioned. HOLLight refers to a ROOT.ML in a subdirectory: http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/Generate-HOLLight/ROOT.ML Which refers to the HOLLight generation script which uses some of the files from the main Import directory. > b) There seems to be no README or generated document which explains at > least rudimentary how to actually use the importer. Is there any > reference for that? There is a README in HOL-Light source code that explains how to get the recorded proofs: http://hol-light.googlecode.com/svn/trunk/Proofrecording/README With the files generated this way, it is enough to set the HOL4PROOFS environment variable and one can import the generated file or run 'isabelle make HOL-Generate-HOLLight' to regenerate it. This is all I have used. > There is also space for structural improvements; one is mentioned in > the at least parly outdated > http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/HOL/README > it is confusing that files *from* which files are generated are placed > in a directory named »Generate…« and not the other way round. > One could also ask whether generated files must be part of the versioning > anyway. Renaming the files and splitting them into the directories: HOL4, HOLLight, Common and Generated would be a great idea. I would however keep the generated "thy" files in the distribution. It is a collection of 1300 lemmas. without proofs (so they do not take up too much space), that do not exist in Isabelle in this form elsewhere and (as the README says) could be used without getting HOLLight running, exporting the proofs etc. Cheers, Cezary _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev