Add dependencies to opam file

[intoverflow]

The issue

The opam file provided by the repo does not document the project's dependencies. This makes the installation process slightly harder than necessary.

Reproduction steps

Clone the repository and activate a fresh opam switch. Pin the repo directory and confirm that you would like to install the packages.

What's expected

opam detects that various dependencies are missing. It fetches them before attempting to build & install WasmCert-Coq.

What happens

[tcarstens@sigma WasmCert-Coq]$ opam pin -y .
This will pin the following packages: Wasm, wasm_interpreter. Continue? [Y/n] y
Package Wasm does not exist, create as a NEW package? [Y/n] y
Wasm is now pinned to git+file:///home/tcarstens/appliedfm/WasmCert-Coq#master (version ~dev)
Package wasm_interpreter does not exist, create as a NEW package? [Y/n] y
wasm_interpreter is now pinned to git+file:///home/tcarstens/appliedfm/WasmCert-Coq#master (version ~dev)

The following actions will be performed:
  ∗ install Wasm             ~dev*
  ∗ install wasm_interpreter ~dev*
===== ∗ 2 =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved wasm_interpreter.~dev  (no changes)
⬇ retrieved Wasm.~dev  (no changes)
∗ installed Wasm.~dev
[ERROR] The compilation of wasm_interpreter.~dev failed at "dune build -p wasm_interpreter -j 79 --promote-install-files=false @install".

#=== ERROR while compiling wasm_interpreter.~dev ==============================#
# context     2.1.1 | linux/x86_64 | ocaml-base-compiler.4.13.1 | pinned(git+file:///home/tcarstens/appliedfm/WasmCert-Coq#master#e7d6bb78)
# path        ~/.opam/coq-8.14/.opam-switch/build/wasm_interpreter.~dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p wasm_interpreter -j 79 --promote-install-files=false @install
# exit-code   1
# env-file    ~/.opam/log/wasm_interpreter-544242-cdae42.env
# output-file ~/.opam/log/wasm_interpreter-544242-cdae42.out
### output ###
# <> and prefix parseque.
# [...]
# (cd _build/default && /home/tcarstens/.opam/coq-8.14/bin/coqc -w -notation-overridden -w -abstract-large-number -w -extraction-reserved-identifier -R theories Wasm theories/list_extra.v)
# File "./theories/list_extra.v", line 117, characters 19-24:
# Error: Cannot find a physical path bound to logical path matching suffix
# <> and prefix ITree.
# 
#         coqc theories/.pickability.aux,theories/pickability.{glob,vo} (exit 1)
# (cd _build/default && /home/tcarstens/.opam/coq-8.14/bin/coqc -w -notation-overridden -w -abstract-large-number -w -extraction-reserved-identifier -R theories Wasm theories/pickability.v)
# File "./theories/pickability.v", line 4, characters 29-38:
# Error: Cannot find a physical path bound to logical path matching suffix
# <> and prefix mathcomp.
# 

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build wasm_interpreter ~dev
└─ 
┌─ The following changes have been performed
│ ∗ install Wasm ~dev
└─ 
[NOTE] Pinning command successful, but your installed packages may be out of sync.

The former state can be restored with:
    /usr/bin/opam switch import "/home/tcarstens/.opam/coq-8.14/.opam-switch/backup/state-20220226050557.export"
Or you can retry to install your package selection with:
    /usr/bin/opam install --restore
[tcarstens@sigma WasmCert-Coq]$

[intoverflow]

On further investigation, it appears that WasmCert-Coq is using esy, dune, and opam in some way to do a highly customized build.

Is this necessary? It would be nice if I could use this in my current opam workflow without adopting esy.

[Mbodin]

Indeed, it is based on esy. At some point, we got some reproducibility issues and I suggested using esy, that forces our dependencies to be as close as possible. But it might work outside esy… just that we have a lot of dependencies, some of which coming with heavy constraints (CompCert is for instance relying on a lot of low-level Makefile commands to install itself): esy seemed a good solution to avoid issues whilst providing some reproducibility guarantees.

Although esy pins most versions by a commit-hash, I would expect up-to-date versions of most packages to still work fine. You can ignore all the "resolutions" installation procedures: these are just there to install the dependencies in a separate place (rather than putting them next to coqc).

Do tell me if I can help on this ☺

[intoverflow]

Thank you for the quick reply @Mbodin ~ I'll give it another go and report back here

[Mbodin]

I would be happy to help if I can.

I do agree that it’s misleading that we left the Opam packages generated by dune on the repo as these do not include the Coq dependencies specified in packages.json. Maybe we should remove them?

[intoverflow]

Your project is very exciting and I think it has the potential to be tremendously useful in the broader Coq ecosystem.

Build systems & packaging are always a bit of a challenge to get right. On the one hand, the build has to serve the needs of the project contributors & maintainers. On the other hand, users always show up out of nowhere with new packaging requests 😇

In my case, there are two use cases I have in mind:

• Eventual inclusion in the Coq Platform releases
• Integration with other packages that seek to emit WASM

The Coq Platform is based on opam, as are the other projects I'm currently working with, so naturally I'm here to advocate for opam 😅

For this project, opam support might require a few obnoxious tasks. For instance, at a glance it appears that the parser combinator library doesn't have an opam package. There might be other upstream dependencies that are also lacking opam files.

In other words, this issue might take a bit of work to resolve. But the payoff is that it would make the project easier for others to use.

I'll investigate further on my end to get a better sense of the scope of effort required. If we can plot a course, I'd be happy to help drive the effort.

[womeier]

Quick update on this issue:

The parseque library is now available in the opam coq archive (name: coq-parseque, thanks @jeromesimeon) meaning StrongInduction is the only dependency not available via opam. Is it strictly required? It seems to be just a single theorem, that maybe could be inlined?

I've been using my fork that uses an opam build for half a year now, I have not seen reproducibility issues. Could you maybe give some more detail on the issues you had, @Mbodin ? Is there a way for you to test if they are still present?

(I'm only using the mechanization, not the interpreter.)

[Mbodin]

Indeed, StrongInduction would be easy to inline.

Unfortunately my configurations changed, so I can't reproduce my reproducibility issue ☺ Basically the project was compiling in a computer but not at another despite having synchronised the git project. Upon inspection, it was due to a slight difference of version in one package, but I don't remember which (and as usual with Coq, a slight difference in version can lead to large changes). I agree that having an Opam package would be a good thing for this project.

[raoxiaojia]

Packaging for an Opam package is something that I've been having in mind as well for many reasons (especially after a previous incident where esy updated their overrides which messed up with compilation), but I haven't had the time to look into it for quite long. I might spend some time on this so that we can provide two methods of installation!

[womeier]

It would help me quite a bit, if it was available via opam.

I have a compiling version of the following:

• only the Wasm library
• removed the interpreter for now (I don't know dune very well. Couldn't make the extraction work yet)
• inlined stronginduction
• updated to Coq 8.14
• removed esy files, as it doesn't compile anymore with the versions fixed in your setup (due to the update to Coq 8.14)
• gh actions config

Would you be interested in a PR? (not to master yet, because of the broken esy setup) but another branch maybe, so it could be released in the opam-coq-archive?

Thanks!

[Mbodin]

I think that I can make the interpreter part work: I would be interested in your PR.

The issue with it was due to a bug in the Coq extraction ( https://github.com/coq/coq/issues/12813 ) that has been fixed in between: it is possible that I just have to remove the hack we had to add to fix Coq's output.

[raoxiaojia]

This is now marked as resolved as part of merging #24 and #26.