search

ejgallego / coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Other
128 stars 39 forks source link

Is sercomp broken in v8.16? #286

Closed artagnon closed 1 year ago

artagnon commented 1 year ago

Hi,

The build succeeds, but the sercomp binary seems to be broken.

~/src/coq-serapi v8.16 ❯ _build/install/default/bin/sercomp --mode=sexp ~/src/bonak/theories/NType/NType.v
[sertop] Couldn't find the SerAPI plugin coq-serapi.serlib.firstorder
 please check `ocamlfind list` does include SerAPI's plugin libraries.
Error:
       Findlib error: coq-serapi.serlib.firstorder not found in:
       /Users/artagnon/.opam/default/lib
artagnon commented 1 year ago

Invoking it directly from the build tree is problematic due to findlib not finding the shared libraries.

dune exec -- sercomp works.

ejgallego commented 1 year ago

Let me know if you think we can document this better.