Re: Bug#876533: hol-light FTBFS with OCaml 4.05.0
Hendrik Tews:
>
>> Hi Hendrik, any progress on this? I notice in the ocaml transition tracker:
>
> I really spend more than 4 weeks in discussions with upstream
> about license and copyright clarifications. Now it is finished. I
> uploaded a new hol-light version to DOM git yesterday. Please
> review and upload.
>
Ouch, well here are some comments:
dpkg-gencontrol: warning: package hol-light: unused substitution variable ${ocaml:Provides}
dpkg-gencontrol: warning: package hol-light: unused substitution variable ${perl:Depends}
These are quite important, you should never ignore them. You need to add an extra Provides: ${ocaml:Provides}, and add ${perl: Depends} to the already-existing Depends field.
(I actually don't know why dpkg-gencontrol doesn't just fail the build instead of emitting a warning. Perhaps for backwards-compat or something.)
The rest of the package looks fine, except that I am not sure about installing everything in /usr/share/hol-light.
If hol-light allows itself to be used as an importable ocaml library for other programs and code, then it should be installed in /usr/lib/ocaml/hol-light - AFAIU extrapolating the (out-of-date) Debian Ocaml packaging policy. I am not sure our Debian ocaml toolchain will pick up libraries installed into /usr/share - and you will have to move it into /usr/lib anyway if the project eventually provides native shared libs, since /usr/share must only contain architecture-independent files.
It would be good if someone else from the team less new than me, could explain this issue properly and/or confirm what I'm suspecting here.
If there are good reasons for installing it in /usr/share/hol-light (which seems to be inconsistent with the packaging policy, as I mentioned) please describe them in debian/README.Debian. For example, I can see that upstream does not have a proper "make install" target for this stuff, and you specify /usr/share yourself in d/rules. So perhaps it is not supposed to be used by other ocaml code, and you include stuff in /usr/share merely "for reference". If that is correct, please add this explanation to the README.
X
--
GPG: ed25519/56034877E1F87C35
GPG: rsa4096/1318EFAC5FBBDBCE
https://github.com/infinity0/pubkeys.git
Reply to: