Opam packages for hol2dk with all dependencies (including patched HOL-Light)

[MSoegtropIMC]

Looking at the install instructions, I wonder if you would like to create opam packages for hol2dk including the patched HOL-Light and whatever else is needed. As maintainer of Coq Platform I might be able to support you with this, say by supplying a set of working packages for the current version, but I would prefer if Deducteam would maintain this then.

[fblanqui]

Hi Michael. I already have an opam package for a part of translated theories: https://github.com/Deducteam/coq-hol-light. I don't think that this is very useful to include hol-light itself in it. Noe also that the proofs are too big to be added in opam. And, to be useful, we need to align hol-light definitions with coq definitions. I did it for natural numbers and a number of arithmetic functions. It now needs to be extended to lists, reals, etc.

[MSoegtropIMC]

Hi Fréderic, I meant a set of dependent opam packages, including a separate opam package for a patched HOL light. The installation instructions are IMHO too complicated to encourage people to try it.

For me it might already be useful if just nat and Z translate reasonably well.

[fblanqui]

Right, it is a little bit complicated to use at the moment. I keep improving this. But hol-light itself is not on opam and not easy to use either. I will think about your idea of having an opam package for the (patched) hol-light.
As for the translation itself, it already works very well for nat! Actually, we can translate all of HOL-Light already. But to get something readily usable for Coq users, we need to align HOL-Light definitions with Coq definitions. Anthony Bordg is working on extending the alignment to lists.

[MSoegtropIMC]

If I can support you with the opam part, please let me know.

Anthony Bordg is working on extending the alignment to lists.

Lists are indeed also needed.

Is there research on automating such tasks? I would expect that for types with similar structure this does work. There is some research in the ATP/SMT area to find similarities between functions.