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
