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
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
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).
Yeah, that's another problem, Coq 8.9 has very limited support at this point.
in some sense, the problems with building on 8.9 led to the Coq mutation proving paper
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...
Thanks, I can't move from Coq 8.9 though because of a machine learning library that depends on it
And yeah it's work with Emily
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
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
ah, using names from 8.10 seems to work
This can be of use: https://github.com/coq/coq/blob/v8.9/META.coq.in
@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
Otherwise, you should be able to use the ocamlfind library
coq.kernel for example, but you need to install Coq
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
How do I get the patched version of Dune?
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)
ah thanks, using coq 0.2 doesn't work, but I'll try to revert to an older dune
(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
Here is the branch I'm trying to get working: https://github.com/uwplse/coq-plugin-lib/tree/dune
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
OK, it happens for every directory inside of my plugin, it can't find any of them at link-time :/
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