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? It would also be a nice proof of concept for the ever more emerging mira test infrastructure, particularly how to use subversion repositories – it does not seem that difficult, cf. http://mercurial.selenic.com/wiki/WorkingWithSubversion 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? 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? (for an impression how usability standards have evolved over the years, have a look at the second paragraph of http://isabelle.in.tum.de/reports/Isabelle/file/ab555029f583/CHANGES-92f.txt ;-) 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. I would be willing to work on these issues (although I cannot promise how much at moment), but this only makes sense of somebody seriously attempts the regression test issue. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann 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