[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

On packaging coq plugins



Hi,

I'm starting to package my first Coq plugin, so I'm a bit unsure how to
proceed: there doesn't seem to be that many examples.

There are two libraries (src:coq-float and src:ssreflect) -- but they
provide coq theories, so they look like coq-theories (from src:coq): a
big number of .v, .vo, .vos and .glob files and html documentation.

This is a coq plugin: there are also .v, .vo and .glob files, but there
are also:
-rw-r--r-- root/root  10065791 2021-10-27 18:11 ./usr/lib/coq/user-
contrib/elpi/elpi_plugin.cma
-rw-r--r-- root/root     78275 2021-10-27 18:11 ./usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmi
-rw-r--r-- root/root   3552765 2021-10-27 18:11 ./usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmo
-rw-r--r-- root/root     85056 2021-10-27 18:11 ./usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmx
-rw-r--r-- root/root     11470 2021-10-27 18:11 ./usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmxa
-rw-r--r-- root/root   4366784 2021-10-27 18:11 ./usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmxs

and of course, that makes lintian very unhappy:
E: libelpi-coq: ocaml-dangling-cmx usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmx
E: libelpi-coq: ocaml-dangling-cmxa usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmxa
W: libelpi-coq: shared-library-lacks-prerequisites usr/lib/coq/user-
contrib/elpi/elpi_plugin.cmxs
I: libelpi-coq: ocaml-stray-cmo usr/lib/coq/user-
contrib/elpi/elpi_plugin.cma
P: libelpi-coq: ocaml-dev-file-in-nondev-package 3 files in
usr/lib/coq/user-contrib/elpi


Cheers,

J.Puydt


Reply to: