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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)