Stream: SerAPI

Topic: Loading SerAPI in a plugin


view this post on Zulip Talia Ringer (Sep 08 2021 at 00:46):

Hi all, I just emailed coq-club, but basically, I need SerAPI in a plugin, and I've tried both with a standard _CoqProject (this is Coq 8.9 which I'm stuck on because of a dependency) and also with Dune. In the former case, I get a linking error; in the later case, I can't even get the project to build with Dune before I use SerAPI. This is a really big blocker for me and a student, so I'd really love some help

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2021 at 08:20):

Hi @Talia Ringer , @Emily First had the same question, the answer is a bit tricky, now that I'm back from holidays will try to provide an answer

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:25):

from memory, SerAPI for 8.10 could be considered the first not-completely-experimental release (could (de)serialize huge real-world projects which 8.9 SerAPI broke down on).

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2021 at 08:28):

Yeah, that's another problem, Coq 8.9 has very limited support at this point.

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:29):

in some sense, the problems with building on 8.9 led to the Coq mutation proving paper

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2021 at 08:32):

Also it depends on what you wanna do with SerAPI, for example if the idea is make Replica data machine-readable you wanna do some further tweaks, etc...

view this post on Zulip Talia Ringer (Sep 08 2021 at 16:28):

Thanks, I can't move from Coq 8.9 though because of a machine learning library that depends on it

view this post on Zulip Talia Ringer (Sep 08 2021 at 16:28):

And yeah it's work with Emily

view this post on Zulip Talia Ringer (Sep 08 2021 at 16:29):

I'm trying to use Dune with 8.9, and I can't even figure out the names of Coq libraries to depend on to get it building _without_ SerAPI

view this post on Zulip Talia Ringer (Sep 08 2021 at 16:30):

Is this listed somewhere? Like if I want access to Constr and Environ, what do I put in the Dune dependency? I tried looking at the Dune files but the 8.9 release on Github doesn't include them

view this post on Zulip Talia Ringer (Sep 08 2021 at 16:34):

ah, using names from 8.10 seems to work

view this post on Zulip Théo Zimmermann (Sep 08 2021 at 16:43):

This can be of use: https://github.com/coq/coq/blob/v8.9/META.coq.in

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2021 at 16:58):

@Talia Ringer , if you are planning to use a compositional build, I'm afraid that only 8.10 includes that support, you would have to backport the dune files to 8.9 if you wanted

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2021 at 16:58):

Otherwise, you should be able to use the ocamlfind library coq.kernel for example, but you need to install Coq

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:12):

Still working on building with just Dune (before SerAPI). It mostly works until I get this error: https://github.com/ocaml/dune/issues/4142 . And I'm not sure what to do about it

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:13):

How do I get the patched version of Dune?

view this post on Zulip Karl Palmskog (Sep 08 2021 at 18:15):

based on the issue, the solution is either to set (using coq 0.2) in dune-project, or to downgrade to a Dune version below 2.8 (all Dune versions are in opam)

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:20):

ah thanks, using coq 0.2 doesn't work, but I'll try to revert to an older dune

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:28):

(Still on dune with nothing fancier like SerAPI yet.) Now I get:

File "./theories/Plib.v", line 1, characters 0-25:
Error:
while loading /home/talia/coq-plugin-lib/_build/default/src/plib.cmxs:
error loading shared library: /home/talia/coq-plugin-lib/_build/default/src/plib.cmxs: undefined symbol: camlDecompiler

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:29):

Not sure if that's my symbol it can't find or something else, but I do have a file decompiler.ml

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:31):

Here is the branch I'm trying to get working: https://github.com/uwplse/coq-plugin-lib/tree/dune

view this post on Zulip Talia Ringer (Sep 08 2021 at 18:42):

Yeah it's the first symbol the .ml4 file tries to import. Not sure why it's looking for camlDecompiler and not the actual file I've included and built with Dune

view this post on Zulip Talia Ringer (Sep 08 2021 at 19:45):

OK, it happens for every directory inside of my plugin, it can't find any of them at link-time :/

view this post on Zulip Talia Ringer (Sep 08 2021 at 20:31):

I loaded every directory separately into the .v file, and now I just get a bunch of warnings saying that "declared ML module termutils has not been found!" and so on


Last updated: Feb 06 2023 at 05:03 UTC