FS#58203 - [coq] library packaging

Attached to Project: Community Packages
Opened by Andres (andreser) - Wednesday, 11 April 2018, 17:13 GMT
Last edited by Baptiste (zorun) - Thursday, 03 May 2018, 07:22 GMT
Task Type Bug Report
Category Packages
Status Closed
Assigned To Baptiste (zorun)
Architecture All
Severity Medium
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 0
Private No

Details

The libraries installed with package coq are not registered with ocamlfind, making them essentially unusable for most software that build-depends on coq. It seems that registering libraries with ocamlfind is also recommended practice (https://wiki.archlinux.org/index.php/OCaml_package_guidelines#Libraries).

Steps to reproduce:

$ pacman -Si coq | grep -i version :(
Version : 8.7.2-1
$ pacman -Ql coq | grep -q META || printf "not META\n"
not META
$ ocamlfind list | grep -i coq || printf "not found\n"
not found
$ git clone https://github.com/ejgallego/coq-serapi.git
$ cd coq-serapi
$ make 2>&1 > /dev/null
$ ocamlbuild -use-ocamlfind -j 4 sertop/sertop.native
+ ocamlfind ocamldep -package cmdliner -package coq.intf,coq.stm,sexplib -modules sertop/sertop.ml > sertop/sertop.ml.depends
ocamlfind: Package `coq.intf' not found
Command exited with code 2.
Compilation unsuccessful after building 1 target (0 cached) in 00:00:00.
This task depends upon

Closed by  Baptiste (zorun)
Thursday, 03 May 2018, 07:22 GMT
Reason for closing:  Fixed
Additional comments about closing:  coq 8.8.0-2
Comment by Baptiste (zorun) - Wednesday, 18 April 2018, 13:52 GMT
This looks like an upstream issue, I have opened a ticket: https://github.com/coq/coq/issues/7296
Comment by Baptiste (zorun) - Wednesday, 18 April 2018, 14:57 GMT
It was a packaging issue after all, introduced with the coq/coqide split. Fixed in 8.8.0-1.
Comment by Andres (andreser) - Thursday, 03 May 2018, 01:53 GMT
  • Field changed: Percent Complete (100% → 0%)
In example in the original post, ocamlfind still fails to locate coq libraries. The following workaround seems to fix it, though:

/usr/lib/ocaml/coq: symbolic link to /usr/lib/coq
Comment by Baptiste (zorun) - Thursday, 03 May 2018, 07:21 GMT
Ok, I've added the workaround.

Upstream bug report is at https://github.com/coq/coq/issues/7411

Loading...