Coq-Elpi (& hierarchy-builder)

[gares]

I'd like Coq-Elpi and hierarchy-builder to be in. They are already in the Coq installer for windows.

I have a question. Context: I'd like to release, this week probably, a version of Coq-Elpi that takes advantage of a few new features of Coq 8.12, version 1.5.0. Should we pick it? Can we pick it for the platform?

The one shipped with the installer is almost identical to the released version 1.4.1 which works on Coq 8.11. I think this would be ideal for the platform, since it has almost no incompatibility with the previous version. But there is no platform for 8.11, and no Coq-Elpi in the windows installer for 8.11 either. So I'm considering the idea, better to break compatibility now than later.

But, I don't know if, on Windows, the platform has to agree with the installer or not. If it has to agree then we have to stay with 1.4.1, but if has not to agree then I'll invest energy this week to make a 1.5.0 release (and adjust hierarchy-builder to it).

[Zimmi48]

IMHO the platform should be viewed as an object that is fully independent of the current Windows installer (even if it should eventually, hopefully as soon as 8.13, supersede it). So I would say 1.5.0 is a good pick for the first platform release. The platform will still officially be in an experimental state for the first release anyway, so the constraints are somehow more relaxed.

[MSoegtropIMC]

@gares : Can you please recommend a tag for Coq-elpi and hierarchy builder for the Coq platform 8.11.2 (I plan to release one as well) and Coq platform 8.12.0? A plain build of coq-elpi from opam does not seem to work even on 8.11.2 - it starts building and successfully installs quite a few prerequisites put the build of coq-elpi itself fails for 8.11.2.

[gares]

Are you building on a memory constrained machine? The version for 8.11 (1.4.x iirc, I'm on vac) runs a test that needs 2+GB. For 8.12 we don't have yet a HB release, only a coq-elpi one (1.5.1).

I should be able to be more precise next week.

[MSoegtropIMC]

No, I have tested this with 32 and 128 GB. Maybe the opam files or not up to date.

[gares]

Both 1.4.1 and 1.5.0 should work on 8.11. There is no HB tag using 1.5.0 yet.

Would you mind posting the error? I don't have a laptop to try it out myself.

[gares]

We do have a tag now, 0.10. we may still lack an open package. cc @CohenCyril

[MSoegtropIMC]

Thanks - I will do some test runs over the weekend. Missing opam packages are no issue - the Coq platform comes with its own opam patch repo.

[gares]

We now have an opam package as well, and as per coq/coq#12391 Coq 8.12.1 is likely to get these versions as well.

[MSoegtropIMC]

Very well - I will test it this week. The platform alpha3 release was still mostly technical and I didn't put much effort into package completeness. Now I will focus on this.

[MSoegtropIMC]

@gares : I tried simple "opam install coq-elpi" on the 8.11.2 platform and I get this error:

dune build -p elpi -j 15 @all ; RC=$?; \
	( cp -r _build/default/src/.ppcache src/ 2>/dev/null || true ); \
	( echo "FLG -ppx './merlinppx.exe --as-ppx --cookie '\''elpi_trace=\"true\"'\'''" >> src/.merlin );\
	exit $RC
ppxfindcache_deriving_std src/API.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/API.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/API.pp.ml
ppxfindcache_deriving_std src/compiler.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/compiler.mli --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/compiler.pp.mli
ppxfindcache_deriving_std src/ast.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/ast.mli --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/ast.pp.mli
ppxfindcache_deriving_std src/API.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/API.mli --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/API.pp.mli
ppxfindcache_deriving_std src/data.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/data.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/data.pp.ml
ppxfindcache_deriving_std src/compiler.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/compiler.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/compiler.pp.ml
ppxfindcache_deriving_std src/ast.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/ast.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/ast.pp.ml
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.ml --ppx-opt --cookie --ppx-opt 'elpi_trace="true"' --cache-file src/.ppcache/runtime_trace_on.ml --cache-file src/.ppcache/runtime_trace_on.mli) > _build/default/src/runtime_trace_on.pp.ml
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.mli --ppx-opt --cookie --ppx-opt 'elpi_trace="false"' --cache-file src/.ppcache/runtime_trace_off.ml --cache-file src/.ppcache/runtime_trace_off.mli) > _build/default/src/runtime_trace_off.pp.mli
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.mli --ppx-opt --cookie --ppx-opt 'elpi_trace="true"' --cache-file src/.ppcache/runtime_trace_on.ml --cache-file src/.ppcache/runtime_trace_on.mli) > _build/default/src/runtime_trace_on.pp.mli
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.ml --ppx-opt --cookie --ppx-opt 'elpi_trace="false"' --cache-file src/.ppcache/runtime_trace_off.ml --cache-file src/.ppcache/runtime_trace_off.mli) > _build/default/src/runtime_trace_off.pp.ml

My opam package version list is:

base-bigarray            base
base-threads             base
base-unix                base
cairo2                   0.6.1            Binding to Cairo, a 2D Vector Graphics Library
camlp5                   7.12             Preprocessor-pretty-printer of OCaml
conf-autoconf            0.1              Virtual package relying on autoconf installation
conf-boost               1                Virtual package relying on boost
conf-cairo               1                Virtual package relying on a Cairo system installation
conf-findutils           1                Virtual package relying on findutils
conf-g++                 1.0              Virtual package relying on the g++ compiler (for C++)
conf-gmp                 1                Virtual package relying on a GMP lib system installation
conf-gnome-icon-theme3   0                Virtual package relying on gnome-icon-theme
conf-gtk3                18               Virtual package relying on GTK+ 3
conf-gtksourceview3      0+2              Virtual package relying on a GtkSourceView-3 system installation
conf-m4                  1                Virtual package relying on m4
conf-mpfr                2                Virtual package relying on library MPFR installation
conf-pkg-config          1.3              Virtual package relying on pkg-config installation
conf-which               1                Virtual package relying on which
coq                      8.11.2           pinned to version 8.11.2
coq-aac-tactics          8.11.0           This Coq plugin provides tactics for rewriting universally quantified equa
coq-bignums              8.11.0           Bignums, the Coq library of arbitrary large numbers
coq-compcert             3.7~coq-platform The CompCert C compiler (using coq-platform supplied version of Flocq)
coq-coquelicot           3.1.0            A Coq formalization of real analysis compatible with the standard library
coq-equations            1.2.3+8.11       A function definition package for Coq
coq-ext-lib              0.11.2           A library of Coq definitions, theorems, and tactics
coq-flocq                3.3.1            A formalization of floating-point arithmetic for the Coq system
coq-gappa                1.4.4            A Coq tactic for discharging goals about floating-point arithmetic and rou
coq-interval             4.0.0            A Coq tactic for proving bounds on real-valued expressions automatically
coq-mathcomp-algebra     1.11.0           Mathematical Components Library on Algebra
coq-mathcomp-bigenough   1.0.0            A small library to do epsilon - N reasonning
coq-mathcomp-character   1.11.0           Mathematical Components Library on character theory
coq-mathcomp-field       1.11.0           Mathematical Components Library on Fields
coq-mathcomp-fingroup    1.11.0           Mathematical Components Library on finite groups
coq-mathcomp-finmap      1.5.0            Finite sets, finite maps, finitely supported functions, orders
coq-mathcomp-real-closed 1.1.1            Mathematical Components Library on real closed fields
coq-mathcomp-solvable    1.11.0           Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect   1.11.0           pinned to version 1.11.0
coq-menhirlib            20190924         A support library for verified Coq parsers produced by Menhir
coq-mtac2                1.1+8.11         Mtac2: Typed Tactics for Coq
coq-quickchick           1.3.2            Randomized Property-Based Testing Plugin for Coq
coq-simple-io            1.3.0            IO monad for Coq
coq-unicoq               1.3+8.11         An enhanced unification algorithm for Coq
coq-vst                  2.6              Verified Software Toolchain
coqide                   8.11.2           IDE of the Coq formal proof management system
cppo                     1.6.6            Code preprocessor like cpp for OCaml
depext                   transition       opam-depext transition package
dune                     2.6.2            Fast, portable, and opinionated build system
dune-configurator        2.6.2            Helper library for gathering system configuration
dune-private-libs        2.6.2            Private libraries of Dune
gappa                    1.3.5            Tool intended for formally proving properties on numerical programs dealin
lablgtk3                 3.0.beta5        pinned to version 3.0.beta5
lablgtk3-sourceview3     3.0.beta6        OCaml interface to GTK+ gtksourceview library
menhir                   20190924         An LR(1) parser generator
num                      1.3              The legacy Num library for arbitrary-precision integer and rational arithm
ocaml                    4.07.1           The OCaml compiler (virtual package)
ocaml-base-compiler      4.07.1           Official release 4.07.1
ocaml-compiler-libs      v0.12.1          OCaml compiler libraries repackaged
ocaml-config             1                OCaml Switch Configuration
ocaml-migrate-parsetree  1.7.3            Convert OCaml parsetrees between different versions
ocamlbuild               0.14.0           OCamlbuild is a build system with builtin rules to easily build most OCaml
ocamlfind                1.8.1            A library manager for OCaml
opam-depext              1.1.3            Query and install external dependencies of OPAM packages
ppx_derivers             1.2.1            Shared [@@deriving] plugin registry
ppx_deriving             4.5              Type-driven code generation for OCaml >=4.02.2
ppx_tools                5.1+4.06.0       Tools for authors of ppx rewriters and other syntactic tools
ppxfind                  1.4              Tool combining ocamlfind and ppx
ppxlib                   0.15.0           Standard library for ppx rewriters
re                       1.9.0            RE is a regular expression library for OCaml
result                   1.5              Compatibility Result module
seq                      base             Compatibility package for OCaml's standard iterator type starting from 4.0
sexplib0                 v0.14.0          Library containing the definition of S-expressions and some base converter
stdlib-shims             0.1.0            Backport some of the new stdlib features to older compiler

[MSoegtropIMC]

On the Coq platform 8.12 it is the same. Maybe the OCaml version I use (4.07.1)?

Can you please try the coq platform 8.11 and 8.12 alpha3 scripts - they should run on pretty much any platform with a posix shell now.

The scripts create new opam switches for the coq platform with these names:

 _coq-platform_.8.11.2.alpha3
 _coq-platform_.8.12.0.alpha3

so they shouldn't change anything in your existing setup.

[MSoegtropIMC]

Another test didn't work either:

opam switch create elpi-test ocaml-system.4.08.1
eval $(opam env)
opam repo add coq-released "https://coq.inria.fr/opam/released"
opam install coq-elpi
The following actions will be performed:
  - install seq                     base    [required by re]
  - install dune                    2.6.2   [required by elpi]
  - install conf-findutils          1       [required by coq]
  - install conf-m4                 1       [required by ocamlfind]
  - install camlp5                  7.12    [required by elpi]
  - install stdlib-shims            0.1.0   [required by ppxlib]
  - install sexplib0                v0.14.0 [required by ppxlib]
  - install result                  1.5     [required by ocaml-migrate-parsetree, ppx_deriving]
  - install re                      1.9.0   [required by elpi]
  - install ppx_tools               6.2     [required by ppx_deriving]
  - install ppx_derivers            1.2.1   [required by ppx_deriving, ocaml-migrate-parsetree, ppxlib]
  - install ocaml-compiler-libs     v0.12.1 [required by ppxlib]
  - install cppo                    1.6.6   [required by ppx_deriving]
  - install ocamlfind               1.8.1   [required by coq]
  - install ocaml-migrate-parsetree 1.7.3   [required by elpi]
  - install num                     1.3     [required by coq]
  - install ppxlib                  0.15.0  [required by elpi]
  - install ppxfind                 1.4     [required by ppx_deriving]
  - install coq                     8.12.0  [required by coq-elpi]
  - install ppx_deriving            4.5     [required by elpi]
  - install elpi                    1.11.2  [required by coq-elpi]
  - install coq-elpi                1.5.1
===== 22 to install =====
Do you want to continue? [Y/n] Y
:
[ERROR] The compilation of elpi failed at "/Users/msoegtrop/.opam/opam-init/hooks/sandbox.sh build make build
        DUNE_OPTS=-p elpi -j 15".

The detailed error messages are as above. I tested this on macOS - in case you think this is a Mac specific sandboxing issue (not unheard of), I can also try it on Linux and Windows - the errors look to unspecific to me to judge this.

[MSoegtropIMC]

P.S.: I also tried to disable sandboxing on Mac - this doesn't work either.

[MSoegtropIMC]

OK, now some good news: on Linux (Ubuntu 18.04) and Windows it does work both for 8.11.2 and 8.12.0. Any idea what the Mac issue could be? There is not really an error message - it just says "exit 1". Maybe we can have a remote debug session on my Mac.

[MSoegtropIMC]

@gares : I debugged this and found that elpi is using "sha1sum". This is not available on mac by default, but can be installed using Macports and homebrew (package name is in both cases md5sha1sum so one of these commands should work (I tried with MacPorts and it fixes the elpi issue):

sudo port install md5sha1sum
brew install md5sha1sum

How shall we fix this? The options I see are

• create an opam conf package for md5sha1sum with depext support for Mac (on Ubuntu and cygwin it is already installed)
• use something more up to date, say shasum or openssl dgst. I will check what is available on plain Ubuntu, plain Mac and my coq platform cygwin installation
• use an OCaml library for this - I am sure something like this must be available

[MSoegtropIMC]

I tested that shasum is available on the Mac, Linux (Ubuntu 18.04) and Cygwin and it should be functionally identical to sha1sum. I created a PR (LPCIC/elpi#82).

Of cause we can still go with the opam conf option if you want to avoid new tags.

[gares]

Sorry I was one vac and I had no time to read this. Your fix is great!

[MSoegtropIMC]

@gares : I have one more issue: CoqElpi does not work in CoqIDE 8.11.2 - I guess you know that since someone fixed it in 8.12.0. My plan is to also publish a Coq platform for Coq 8.11.2 (at the same time as for 8.12.0). Any suggestions what I should do with Elpi:

• not include it in Coq platform 8.11.2
• patch CoqIDE
• put a disclaimer somewhere

In case you are not aware: the following piece of code works in VSCoq 8.11.2 but not in CoqIDE 8.11.2:

From elpi Require Import elpi.

Goal True.

Elpi Tactic show.
Elpi Accumulate lp:{{

  solve _ [goal Ctx Proof Type _] _ :-
    coq.say "Goal:" Ctx "|-" Proof ":" Type.
}}.
Elpi Typecheck.
elpi show.

[gares]

Hum, is it the parsing of lp:{{ .... }} that fails?
You can always do Elpi Accumulate " some code " but then you need to escape "Goal:" for example, using Coq's string escaping.

I think that at some point I tried to fix CoqIDE (it pre-chops the text looking for . and this does not work anymore) and failed, so the patch was reverted. I don't recall exactly what fixed it in 8.12.

[gares]

FTR, elpi 1.11.4 which includes your sha1sum fix is released

[MSoegtropIMC]

@gares: I added it to the v8.12 branch - you can try it there. Please note that this branch does a full parallel build which requires a bit more than 13 GB of RAM, so you should have at least 16 GB physical (I will add a sequential build option later).

For 8.11 I will add a note displayed after install if CoqIDE and coq-elpi are installed, that CoqIDE does not work with Coq-elpi and that it does work in 8.12.

[MSoegtropIMC]

This is fixed meanwhile.

coq-elpi is included in 8.12.2 and 2021.02.0.

I will delay creating of Platforms for older versions of Coq (something which is useful for fighting package bit rot). If I include coq-elpi in such older releases we can see then.