[isabelle-dev] [isabelle] Status of HOL/Import

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110712/6cd6e02b/attachment.asc>