Add SerAPI to the Coq Platform

[palmskog]

SerAPI is an OCaml project which contains:

1. a library and a set of tools for large-scale (de)serialization of Coq code to and from JSON and S-expressions, and
2. a structured protocol for machine-to-machine communication with Coq.

SerAPI provides unique functionality to Coq tool developers, which, e.g., obviates writing their own lexer and parser for Coq code. It has been used for implementing mutation analysis of Coq code and machine learning on Coq code. SerAPI has had consistent releases for major Coq versions since Coq 8.9. It is packaged directly in the OCaml opam repository.

For the benefit of tool developers and experimental use by end Coq users, I propose that SerAPI is included in the Coq Platform.

I am one of the maintainers of SerAPI, but as the main author, @ejgallego should have ultimate veto over inclusion into the platform.

[Zimmi48]

This will also likely be a dependency for other candidates for inclusion in the platform.

[ejgallego]

Thanks for taking care of this @palmskog , indeed I see now problem; tho the current 8.12 candidate has still a few bugs so I'm not sure it will make it to the first platform release.

[ejgallego]

Hi folks, I have had a few requests to include SerAPI in the platforms so let's go for it; it seems the number of users is an order of magnitude more than I knew.

[trirpi]

Very nice that this is picked up this quickly! I will close Issue #105 since this issue should solve it.

Me and some colleagues would also like to help solve the issues which currently make SerAPI incompatible with the Coq platform. Since we're not too knowledgeable about the build process, it would take a bit longer for us to figure out stuff. So if you can fix this quickly, it might be unnecessary. But we'd like to help, to this can be done because it is rather urgent for our team.

Could you let us know what's the best way to help. In addition, do you have any idea on how quickly we can get this done?

[Zimmi48]

Very nice that this is picked up this quickly! I will close Issue #105 since this issue should solve it.

@trirpi Don't get your hopes too high. This is just the maintainer of SerAPI approving inclusion in the platform. It could take some time before the platform is actually extended with more packages including this one.

And thanks for proposing your help!

[ejgallego]

I think we can fix the build problem quick enough.

[trirpi]

I did some more exploring. Creating the serapi installer using the create_windows_installer.sh and then installing it in the same folder as the developer is a hack around the build issue described earlier.

Doing this, only some dependency issues need to be resolved. The (absence of the) following packages caused problems:

• ppx_deriving
• base
• threads
• sexplib0
• result

I think, this is normally solved in the create installer script somewhere. I did not manage to edit the installer script. But I did manage to solve them as follows:

1. Copying ppx_deriving, base, sexplib0, result library folders from the 'developer installation folder' to the users installation folder.
2. Editing the META file in the threads library folder. Specifically the following lines

type_of_threads = "posix"
requires(mt,mt_posix) = "threads.posix"

were changed to

type_of_threads = "none"
#requires(mt,mt_posix) = "threads.posix"

This does, probably, disable threading, so this is suboptimal.

After this the SerAPI worked.

[trirpi]

I commented out the following lines in the create_windows_installer.sh file to alleviate the package issues:

OPAM_FILE_WHITELIST[base]='.^' # ocaml stdlib
OPAM_FILE_WHITELIST[sexplib0]='.^'
OPAM_FILE_WHITELIST[result]='.^'
OPAM_FILE_WHITELIST[ppx_deriving]='.^' # linked in elpi

In addition, the editing of the META file in the threads lib folder can be done before creating the installer. Note that this causes a (modified since) to appear when running opam show --list-files $1 and an error that the files (modified and since) cannot be found will be displayed. Removing line 276 can be done to ignore the issue.

In this way a fully working installer is made except for the hardcoded path issue.

Currently, it requires that the installation is into path C:\cygwin64_coq_platform\home\trist\.opam\_coq-platform_.2021.02.1.
I might look into automatically creating some symlinks as another hack to solve this issue.

[MSoegtropIMC]

I had a look at this request.

One issue I see is that installing the opam package requests a few downgrades which affects other packages:

  - downgrade ppxlib                  0.23.0 to 0.15.0 [required by ppx_deriving_yojson, ppx_deriving, ppx_sexp_conv]
  - downgrade ppx_deriving            5.2.1 to 5.1     [required by coq-serapi]
  - recompile elpi                    1.13.7           [uses ppx_deriving]
  - recompile coq-elpi                1.9.7            [uses elpi]
  - recompile coq-hierarchy-builder   1.1.0            [uses coq-elpi]

Is this a real requirement or outdated opam information?

As far as I understand this is still beta, so I would suggest we put it into the "extended" level.

Can someone please summarize the Windows issues? The installer generator should handle all dependencies declared in opam automatically - if it doesn't it is a bug.

Is there some easy way to test if the installation was properly done?

[palmskog]

Here is one smoke test that could be done after installation, from the command line:

sercomp --input=vernac --mode=sexp --exn_on_opaque tests/genarg/specialize.v > example.sexp
sercomp --input=sexp --mode=check example.sexp

This is based on using this file as input.

[ejgallego]

Is this a real requirement or outdated opam information?

Unfortunately that's a real requirement, there is an ongoing migration on the ppx ecosystem, and ppx_import is still gonna take a bit. That could be a problem for the platform indeed.

Can someone please summarize the Windows issues?

Indeed, there should not be packaging issues in windows as far as I know [tho, serapi requires findlib to be properly configured, I guess it is the only package in the platform that stresses this]

Is there some easy way to test if the installation was properly done?

What Karl says, of we could implement the with-test opam field so you could use opam -t to run the tests.

[MSoegtropIMC]

@ejgallego , @palmskog , @gares : what shall we do about the ppxlib downgrade? My helicopter view gut feeling decision would be to not include serapi in the platform until it is compatible with a current version of ppxlib. But as it looks @gares is the only other user of this, so if he agrees I find it acceptable to include serapi and use the older version ppxlib.

[Zimmi48]

How is a downgrade of ppxlib a problem exactly?

[gares]

elpi does nothing fancy with ppxlib, if it compiles it is ok.

[MSoegtropIMC]

@Zimmi48 : it is not a problem, it is a potential problem. It is not unreasonable to expect that some time in the future we will have packages which require a later version of ppxlib - assuming new features are there for a reason. If we then have one package which requires ppxlib <= 0.15.0 and one package which requires ppxlib > 0.15.0, these packages are incompatible.

So at a minimum we should have the statement from other users (@gares) that they don't plan to use later features from ppxlib soon - we have this now.

I am still not super happy about this, but more on a project management theoretical background than for a tangible reason.

[Zimmi48]

Indeed, you have a good point. That being said, the reason of these version constraints has to do with the OCaml ppx ecosystem, which is slowly undergoing a migration to be more compatible with future OCaml versions at a lower maintenance cost. So it is expected that eventually everything will work fine with the latest ppxlib version. But it is also beyond our expertise to make this happen.

[MSoegtropIMC]

Since SerAPI is of some importance, I would say it is fine to add it to the "extended" set. In case we are facing issues around the ppxlib version in the future, I count on that we can sort these out in the time frame the Coq Platform schedule gives us.

FTR: it does work fine to install it together with coq-elpi.

I wonder if I should leave a note on this in the package file, so that users are aware.

[ejgallego]

Indeed, if there is a solution package set for the required Elpi and SerAPI version I think we should be good for this time.

But yeah, the more and more complex packages we have in the platform, the harder will usually be to find a consistent package set; several approaches to this problem have been studied, but indeed, in the Coq and OCaml it is not easy to solve due to the lack of ABI for example.

[MSoegtropIMC]

OK, it will be added soon (with PR #144) to the extended set of 2021.09 8.13. I plan to also add it to 8.14 beta.