Talia Ringer (Sep 08 2021 at 00:46): 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
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
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).
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.
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
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...
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
Talia Ringer (Sep 08 2021 at 16:28):And yeah it's work with Emily
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
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
Talia Ringer (Sep 08 2021 at 16:34):ah, using names from 8.10 seems to work
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
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
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
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
Talia Ringer (Sep 08 2021 at 18:13):How do I get the patched version of Dune?
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)
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
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
Not sure if that's my symbol it can't find or something else, but I do have a file decompiler.ml
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
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
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 :/
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: Jun 01 2023 at 12:01 UTC