Stream: CertiCoq

Topic: Install or build CertiCoq


view this post on Zulip Anders Larsson (Apr 02 2022 at 07:20):

I tried to follow the instructions on: https://github.com/CertiCoq/certicoq/blob/master/INSTALL.md from top to bottom and got stuck for some reason. (I'm new to this ecosystem so I may have missed something obvious).

Any suggestions?

[certicoq]$ opam install coq-certicoq

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-certicoq.~dev] no changes from git+file:///tmp/certicoq#master

Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting
[certicoq]$ pwd
/tmp/certicoq

[certicoq]$ opam install coq-certicoq --deps-only

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-certicoq.~dev] no changes from git+file:///tmp/certicoq#master

Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:26):

Can you show the output of opam repo list and opam list?

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:26):

You can also try installing the dependencies in https://github.com/CertiCoq/certicoq/blob/ea52e6f93adb90c3d2a6badd63e677a5f4c27572/coq-certicoq.opam by hand.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:27):

Or rather, try simulating their installation with --dry-run.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:28):

My guess? Those instructions aren't complete, and they assume that you (1) installed opam (which you did) (2) added the coq-released repository (opam repo list would tell us)

view this post on Zulip Anders Larsson (Apr 02 2022 at 07:33):

Sure:

$ opam repo list
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.

<><> Repository configuration for switch default ><><><><><><><><><><><><><><><>
 1 coq-extra-dev https://coq.inria.fr/opam/extra-dev
 2 coq-released  https://coq.inria.fr/opam/released
 3 default       https://opam.ocaml.org

view this post on Zulip Anders Larsson (Apr 02 2022 at 07:34):

$ opam list
# Packages matching: installed
# Name                  # Installed # Synopsis
alt-ergo                2.4.1       The Alt-Ergo SMT prover
alt-ergo-lib            2.4.1       The Alt-Ergo SMT prover library
alt-ergo-parsers        2.4.1       The Alt-Ergo SMT prover parser library
base-bigarray           base
base-threads            base
base-unix               base
biniou                  1.2.1       Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
bitstring               4.1.0       Bitstrings and bitstring matching for OCaml
cairo2                  0.6.2       Binding to Cairo, a 2D Vector Graphics Library
camlp5                  7.14        Preprocessor-pretty-printer of OCaml
camlzip                 1.11        Accessing compressed files in ZIP, GZIP and JAR format
cmdliner                1.0.4       Declarative definition of command line interfaces for OCaml
conf-adwaita-icon-theme 2           Virtual package relying on adwaita-icon-theme
conf-autoconf           0.1         Virtual package relying on autoconf installation
conf-cairo              1           Virtual package relying on a Cairo system installation
conf-findutils          1           Virtual package relying on findutils
conf-gmp                4           Virtual package relying on a GMP lib system installation
conf-graphviz           0.1         Virtual package relying on graphviz installation
conf-gtk3               18          Virtual package relying on GTK+ 3
conf-gtksourceview3     0+2         Virtual package relying on a GtkSourceView-3 system installation
conf-perl               2           Virtual package relying on perl
conf-pkg-config         2           Check if pkg-config is installed and create an opam switch local pkgconfig folder
conf-which              1           Virtual package relying on which
conf-zlib               1           Virtual package relying on zlib
coq                     8.13.2      Formal proof management system
coq-elpi                1.11.1      Elpi extension language for Coq
coq-hierarchy-builder   1.2.1       High level commands to declare and evolve a hierarchy based on packed classes
coq-mathcomp-algebra    1.14.0      Mathematical Components Library on Algebra
coq-mathcomp-analysis   0.3.13      An analysis library for mathematical components
coq-mathcomp-bigenough  1.0.1       A small library to do epsilon - N reasoning
coq-mathcomp-field      1.14.0      Mathematical Components Library on Fields
coq-mathcomp-fingroup   1.14.0      Mathematical Components Library on finite groups
coq-mathcomp-finmap     1.5.1       Finite sets, finite maps, finitely supported functions
coq-mathcomp-solvable   1.14.0      Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect  1.14.0      Small Scale Reflection
coq-of-ocaml            2.5.1       Compile a subset of OCaml to Coq
coqide                  8.13.2      IDE of the Coq formal proof management system
cppo                    1.6.8       Code preprocessor like cpp for OCaml
csexp                   1.5.1       Parsing and printing of S-expressions in Canonical form
depext                  transition  opam-depext transition package
dune                    2.9.2       Fast, portable, and opinionated build system
dune-configurator       2.9.1       Helper library for gathering system configuration
easy-format             1.3.2       High-level and functional interface to the Format module of the OCaml standard library
elpi                    1.13.8      ELPI - Embeddable λProlog Interpreter
lablgtk3                3.1.2       OCaml interface to GTK+3
lablgtk3-sourceview3    3.1.2       OCaml interface to GTK+ gtksourceview library
menhir                  20211128    An LR(1) parser generator
menhirLib               20211128    Runtime support library for parsers generated by Menhir
menhirSdk               20211128    Compile-time library for auxiliary tools related to Menhir
num                     1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                   4.12.0      The OCaml compiler (virtual package)
ocaml-base-compiler     4.12.0      Official release 4.12.0
ocaml-compiler-libs     v0.12.4     OCaml compiler libraries repackaged
ocaml-config            2           OCaml Switch Configuration
ocaml-options-vanilla   1           Ensure that OCaml is compiled with no special options enabled
ocamlfind               1.9.3       A library manager for OCaml
ocamlgraph              2.0.0       A generic graph library for OCaml
ocplib-simplex          0.4         A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizing linear objective functions
opam-depext             1.2.1       Install OS distribution packages
ppx_derivers            1.2.1       Shared [@@deriving] plugin registry
ppx_deriving            5.2.1       Type-driven code generation for OCaml
ppxlib                  0.24.0      Standard library for ppx rewriters
psmt2-frontend          0.4.0       The psmt2-frontend project
re                      1.10.3      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.07.
sexplib0                v0.14.0     Library containing the definition of S-expressions and some base converters
smart-print             0.3.0       A pretty-printing library in OCaml
stdlib-shims            0.3.0       Backport some of the new stdlib features to older compiler
why3                    1.4.0       Why3 environment for deductive program verification
why3-coq                1.4.0       Why3 environment for deductive program verification
why3-ide                1.4.0       Why3 environment for deductive program verification
yojson                  1.7.0       Yojson is an optimized parsing and printing library for the JSON format
zarith                  1.12        Implements arithmetic and logical operations over arbitrary-precision integers

view this post on Zulip Anders Larsson (Apr 02 2022 at 07:43):

I'll start with installing coq-equations - it looked like it was missing.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:46):

You have a different coq version there

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:49):

you could upgrade coq, but creating a new opam switch is likely safer

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:51):

sorry, nevermind, there might be something wrong with coq-certicoq…

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:52):

http://coq.io/opam/coq-compcert.3.9.html depends on Coq < 8.14, but https://github.com/CertiCoq/certicoq/blob/master/coq-certicoq.opam#L29-L33 depends on compcert 3.9 and Coq 8.14.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 07:55):

coq-certicoq’s CI seems to use this combination (https://github.com/CertiCoq/certicoq/blob/master/.github/workflows/build.yml#L21), but they must be using a different package for compcert?

view this post on Zulip Anders Larsson (Apr 02 2022 at 07:58):

opam switch sounds like a good idea.

I had Coq 8.13.2 installed on one system and 8.15.1 on another.

Maybe reading up on opam switch and trying with 8.14 could be a good idea.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 08:01):

IIUC @Tim Carstens set up that Docker image?

view this post on Zulip Karl Palmskog (Apr 02 2022 at 09:21):

CompCert 3.9 has been patched to support Coq 8.9 to 8.15 8.14 in the opam repo. It looks pretty clear from the name of this Docker image what the versions should be to build the current CertiCoq: 'tcarstens/coq-vst:8.14.1-ocaml-4.12.0-flambda--compcert-3.9--vst-2.8'

So I'd recommend trying:

... all installed from the Coq opam released archive (avoid extra-dev in the switch)

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 11:06):

@Karl Palmskog that patch is not there AFAICT: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-compcert/coq-compcert.3.9/opam

view this post on Zulip Karl Palmskog (Apr 02 2022 at 11:08):

I meant, patched to support 8.9 to 8.14, which this was about. The "patch" in this case was "-ignore-coq-version"

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 11:10):

Sorry, nevermind! Now I was just confused. coq.io seems out of date but I'll double check later

view this post on Zulip Anders Larsson (Apr 02 2022 at 11:34):

I'm trying the build instructions in a container ('tcarstens/coq-vst:8.14.1-ocaml-4.12.0-flambda--compcert-3.9--vst-2.8')

Then I got past my trouble with: opam install coq-certicoq .

(I just wanted to test run the certicoq tool).

view this post on Zulip Notification Bot (Apr 02 2022 at 11:35):

Anders Larsson has marked this topic as resolved.

view this post on Zulip Tim Carstens (Apr 02 2022 at 16:09):

Thank you for checking out CertiCoq! Sorry about the installation trouble. I will update the instructions to make the experience smoother. (Things are in flux as we prep for a new release, so please let me know if you run into any other issues)

view this post on Zulip Anders Larsson (Apr 02 2022 at 18:29):

OK. Here is what confuses me now (the solution is probably to read up on the toolchain and opam):

I try to build (install) in a container from:

tcarstens/coq-vst                                  8.14.1-ocaml-4.12.0-flambda--compcert-3.9--vst-2.8

And I get what looks like a trivial programming error:

theories/utils/canonicaltries/String2pos.v
# COQC theories/utils/canonicaltries/CanonicalTries.v
# COQC theories/utils/ByteCompare.v
# File "./theories/utils/ByteCompare.v", line 4, characters 9-18:
# Error: The reference Byte.to_N was not found in the current environment.
#
# make[3]: *** [Makefile.coq:763: theories/utils/ByteCompare.vo] Error 1
# make[2]: *** [Makefile.coq:386: all] Error 2
# make[2]: Leaving directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13/template-coq'
# make[1]: *** [Makefile:6: coq] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13/template-coq'
# make: *** [Makefile:55: template-coq] Error 2

But 1) That is odd as the CI system compiles it fine. And 2) The .opam tries very hard to download from github anyway .

If I just run coqtop on utils/ByteCompare.v, then I can fix the issue by replacing:

From Coq Require Import Byte NArith.BinNat.

with

From Coq Require Import Strings.Byte NArith.BinNat.

But that is really nonobvious to implement as coq-metacoq-translations.opam points to
dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" .

view this post on Zulip Karl Palmskog (Apr 02 2022 at 18:39):

dev-repo is not used during opam package installation in any way

view this post on Zulip Karl Palmskog (Apr 02 2022 at 18:44):

I'd recommend creating a fresh opam switch instead of using the container, since easier to debug

view this post on Zulip Anders Larsson (Apr 02 2022 at 19:21):

The issue with that (I'm running Fedora 34 by the way) is that opam refuses to install
the same tools that is already available inside the Docker container.

$ opam repo
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.

<><> Repository configuration for switch 4.12.0+flambda+nnpchecker ><><><><><><>
 1 coq-released https://coq.inria.fr/opam/released
 2 default      https://opam.ocaml.org
$
$ opam list
# Packages matching: installed
# Name                  # Installed    # Synopsis
base-bigarray           base
base-threads            base
base-unix               base
ocaml                   4.12.0         The OCaml compiler (virtual package)
ocaml-config            2              OCaml Switch Configuration
ocaml-option-flambda    1              Set OCaml to be compiled with flambda activated
ocaml-option-nnpchecker 1              Set OCaml to be compiled with --enable-naked-pointers-checker
ocaml-variants          4.12.0+options Official release of OCaml 4.12.0
$ opam pin
coq.8.14.1           (uninstalled)  version  8.14.1
coq-compcert.3.9     (uninstalled)  version  3.9
coq-compcert-32.3.9  (uninstalled)  version  3.9
$ opam install coq-compcert
Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting
$

view this post on Zulip Karl Palmskog (Apr 02 2022 at 19:46):

you can't use the nnpchecker option with Coq, the Coq package has this:

conflicts:    "base-nnp" "ocaml-option-nnpchecker"

view this post on Zulip Karl Palmskog (Apr 02 2022 at 19:47):

you'll have to recreate a switch with only 4.12.0+flambda, i.e., without nnpchecker. Maybe easiest to do something like: opam switch create 4.11.2+flambda (the option handling was easier for 4.11.2)

view this post on Zulip Notification Bot (Apr 02 2022 at 19:48):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Karl Palmskog (Apr 02 2022 at 19:50):

I also really recommend installing all versions explicitly, for example:

opam install coq.8.14.1 coq-compcert.3.9 coq-vst.2.8

view this post on Zulip Anders Larsson (Apr 02 2022 at 19:50):

I'll try that.

view this post on Zulip Anders Larsson (Apr 02 2022 at 20:48):

This time the switch setup worked and produces the same result as the Docker image.

#=== ERROR while compiling coq-metacoq-template.1.0~beta2+8.13 ================#
# context     2.0.8 | linux/x86_64 | ocaml-variants.4.11.2+flambda | pinned(git+file:///tmp/certicoq/submodules/metacoq#HEAD#3d6f8edb)
# path        ~/.opam-coq.8.14.eval/4.11.2+flambda/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13
# command     ~/.opam-coq.8.14.eval/opam-init/hooks/sandbox.sh build make -j 7 template-coq
# exit-code   2
# env-file    ~/.opam-coq.8.14.eval/log/coq-metacoq-template-2330996-57f057.env
# output-file ~/.opam-coq.8.14.eval/log/coq-metacoq-template-2330996-57f057.out
### output ###
# [...]
# COQC theories/utils/MCProd.v
# COQC theories/utils/MCSquash.v
# File "./theories/utils/ByteCompare.v", line 4, characters 9-18:
# Error: The reference Byte.to_N was not found in the current environment.
#
# make[3]: *** [Makefile.coq:763: theories/utils/ByteCompare.vo] Error 1
# make[3]: *** Waiting for unfinished jobs....
# make[2]: *** [Makefile.coq:386: all] Error 2
# make[2]: Leaving directory '/home/andla/.opam-coq.8.14.eval/4.11.2+flambda/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13/template-coq'
# make[1]: *** [Makefile:6: coq] Error 2
# make[1]: Leaving directory '/home/andla/.opam-coq.8.14.eval/4.11.2+flambda/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13/template-coq'
# make: *** [Makefile:55: template-coq] Error 2

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 21:55):

The version number would suggest that metacoq package is for Coq 8.13... I guess this package was patched as well somewhere?

view this post on Zulip Karl Palmskog (Apr 02 2022 at 21:57):

they use a git submodule for MetaCoq. It [the content of the submodule] has to be opam-pinned in a very particular way to be sanely installed

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:00):

(the basic problem in my view is that MetaCoq did not do releases for 8.14 and 8.15, but they have commits/branches that work just fine with those Coq versions...)

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:03):

Right, I've used the 8.15 branch too…

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:03):

so for example:

git submodule update --init
cd submodules/metacoq
opam pin add coq-metacoq-template -k path .
opam pin add coq-metacoq-pcuic -k path .
opam pin add coq-metacoq-erasure -k path .

The gets the required package coq-metacoq-erasure.1.0~beta2+8.13 to install on 8.14

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:04):

IIUC, this will just install the sources — the version number used by opam is somewhat arbitrary

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:05):

IIRC you can pick another one when pinning

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:05):

in this case, I think it takes after the latest released version

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:06):

even though the -k path forces local

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:06):

separately, I wonder why opam is giving uninformative error messages, maybe it depends on the solver that is enabled

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:07):

really shaky to have this version name (1.0~beta2+8.13) in the opam file in the repo (coq-certicoq.opam), in my view. I would have just said "coq-metacoq-erasure" without version constraints, when it's some git commit anyway...

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:07):

the official opam binaries produce much better messages

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:07):

By two lines of guessing I managed to compile/install. I'm running the benchmark now.

diff --git a/template-coq/theories/utils/ByteCompare.v b/template-coq/theories/utils/ByteCompare.v
index 2a3582bd..1e892ef6 100644
--- a/template-coq/theories/utils/ByteCompare.v
+++ b/template-coq/theories/utils/ByteCompare.v
@@ -1,7 +1,7 @@
-From Coq Require Import Byte NArith.BinNat.
+From Coq Require Import Strings.Byte NArith.BinNat.

-Definition eqb (x y : byte) :=
+Definition eqb (x y : byte) :=
   N.eqb (Byte.to_N x) (Byte.to_N y).

-Definition compare (x y : byte) :=
+Definition compare (x y : byte) :=
   N.compare (Byte.to_N x) (Byte.to_N y).
diff --git a/template-coq/theories/utils/ByteCompareSpec.v b/template-coq/theories/utils/ByteCompareSpec.v
index 1159c5e6..f93ed1de 100644
--- a/template-coq/theories/utils/ByteCompareSpec.v
+++ b/template-coq/theories/utils/ByteCompareSpec.v
@@ -1,4 +1,4 @@
-From Coq Require Import Byte NArith.
+From Coq Require Import Strings.Byte NArith.
 From MetaCoq.Template Require Import ReflectEq ByteCompare.
 From Equations Require Import Equations.

@@ -36,7 +36,7 @@ Lemma compare_equiv x y : compare x y = N.compare (Byte.to_N x) (Byte.to_N y).
 Proof.
   reflexivity.

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:08):

that compilation problem [with Byte] will likely not happen when you use the MetaCoq from the CertiCoq repo submodule

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:09):

the original import seems genuinely ambiguous since it might refer to Coq.Init.Byte. And IIRC the resolution logic was rewritten in Coq 8.15 to have better semantics here…

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:10):

actually, let me check the pinned hash…

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:11):

that compilation problem [with Byte] will likely not happen when you use the MetaCoq from the CertiCoq repo submodule

I'm not that familiar with submodules in Git, but I thought git submodule update --init should have fixed that.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:12):

@Anders Larsson and you followed the certicoq instructions using their opam pin command, right?

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:12):

are you using the opam pin add coq-metacoq-* -k path . commands?

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:12):

I should stop doing this from an iPad, but going from https://github.com/CertiCoq/certicoq/tree/master/submodules I find https://github.com/MetaCoq/metacoq/blob/3d6f8edbdf43bf0b5b45f6493a25ae6cfb087040/template-coq/theories/utils/ByteCompare.v#L1 which does have the ambiguous require…

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:13):

I'm looking here: https://github.com/CertiCoq/certicoq/runs/5590356861?check_suite_focus=true#step:4:243

and I don't see ambiguity problems in the output

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:13):

@Paolo Giarrusso - yes, I tried my best to follow the install instruction (but failed a couple of times, so my comments above are OK but not perfect).

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:13):

the Certicoq README recommends opam pin -n -y submodules/metacoq, but it’s reasonable it’d work as well

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:14):

@Karl Palmskog but that’s the point: the code has undefined behavior, and Coq until 8.14 does something bad — and (I fear) filesystem-dependent. Coq 8.15 will just reject this code.

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:15):

and regardless of what Coq does, should From Coq Require Byte find Strings.Byte or Init.Byte?

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:15):

Big thanks for all the comments. I think I got through now . :-)

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:16):

if all they need is MetaCoq-erasure, then it seems like a waste to pin+install all MetaCoq packages

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:18):

ah, I guess the only redundant one is translations, in the end

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:20):

are you using the opam pin add coq-metacoq-* -k path . commands?
No. Just:

$ opam pin -n -y submodules/metacoq
$ opam pin -n -y .

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:22):

the whole thing with pinning a whole directory of .opam files in one command seems shaky

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:23):

That's a good point, but I've never found a good way to install all pinned packages later, when pinning with -n... Do you know one?

view this post on Zulip Paolo Giarrusso (Apr 02 2022 at 22:24):

@Anders Larsson out of curiosity, which filesystem are you building on?

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:25):

the only time I pin with -n is in CI to install dependencies separately

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:28):

out of curiosity, which filesystem are you building on?

What an embarrassing question... :-)

tmpfs 16368348 300576 16067772 2% /tmp

(I scripted the installation instructions to speed up things, that's why).

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:30):

how often is Coq really IO bound? I think the consensus is that it's mostly memory bound

view this post on Zulip Anders Larsson (Apr 02 2022 at 22:30):

But I got the same result when the source code was inside Docker (which I think counts as it's own file system in this context).

view this post on Zulip Tim Carstens (Apr 03 2022 at 06:41):

I’ve confirmed that the MetaCoq issue reproduces on my end 😭 There’s definitely some work to be done here, sorry for the trouble.

Sounds like:

  1. The opam files shouldn’t be naming specific MetaCoq versions
  2. The MetaCoq branch isn’t working (but somehow works in the CI???)
  3. The install instructions need to provide steps for adding the Coq opam repo
  4. The install instructions should use more precise pins

Anything else so far?

view this post on Zulip Karl Palmskog (Apr 03 2022 at 07:26):

building/installation of CertiCoq works fine once one does the pinning of the MetaCoq packages in the submodule

view this post on Zulip Karl Palmskog (Apr 03 2022 at 07:28):

the counterintuitive part is that the MetaCoq packages will get assigned strange version numbers when pinned. The MetaCoq people should add clauses like the following in their in-repo opam packages:

version: "8.14.dev"

view this post on Zulip Paolo Giarrusso (Apr 03 2022 at 08:46):

re “building works fine after pinning”: the requires in question are not entitled to work, so “works in CI but not locally” seems plausible; IIUC, Require results could depend on filesystem traversal order before, but @Hugo Herbelin would know better

view this post on Zulip Karl Palmskog (Apr 03 2022 at 09:54):

OK, I can at least say that: "the error-free CI build of latest CertiCoq was replicated locally [by me]"

view this post on Zulip Karl Palmskog (Apr 03 2022 at 10:06):

@Tim Carstens I can submit a CertiCoq PR with how I think the CI pinning/installing of dependencies should be done (or I can give code here if you prefer). However, the best CI idiom is probably not the best one to replicate a build locally (although it should work).

view this post on Zulip Karl Palmskog (Apr 03 2022 at 10:07):

to solve the MetaCoq issues more definitely, we need to discuss with MetaCoq people on a sensible opam versioning scheme that extends across beta releases into the opam files in the git repo.

view this post on Zulip Karl Palmskog (Apr 03 2022 at 10:08):

the whole thing with 1.0~betaX+8.YZ for releases is difficult to reconcile with git branches - maybe 1.0~betaX+8.YZ.dev?

view this post on Zulip Michael Soegtrop (Apr 04 2022 at 05:49):

Btw.: fell free to request to add it to the Coq Platform - IMHO it is a quite important project and might be stable (from an API change point of view) enough at least for the "extended" level.

view this post on Zulip Paolo Giarrusso (Apr 04 2022 at 06:16):

You mean certicoq or metacoq? But :+1:

view this post on Zulip Michael Soegtrop (Apr 04 2022 at 07:11):

I meant CertiCoq, but since it depends on MetaCoq (afaik), this would include MetaCoq.

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 08:16):

Hi, we hope to release actual working (and somewhat complete) versions of both MetaCoq and CertiCoq soonish. For sure we'll submit them to the platform when they're ready

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:21):

@Matthieu Sozeau any thoughts on released version numbering scheme vs. in-repo numbering scheme? If you switch to 1.0 without the beta part, this would make things a lot simpler

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:23):

for example, 1.0+8.XY vs. 1.0+8.XY.dev

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 08:23):

I guess we should have tags in the git repo corresponding to each release, wouldn't that be enough?

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 08:24):

Do you mean we can confuse the versioning logic of opam when we use +?

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:24):

tags are great, but I wanted to solve the problem with CertiCoq pinning a version of MetaCoq that will be misleading, like 1.0~beta2+8.13 from the MetaCoq repo, which actually only works with Coq 8.14

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:25):

for example, many plugins have the following scheme:

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:26):

this ensures that 8.15.dev is always greater than any 8.15.0/8.15.1 package version to opam

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 08:27):

Right, I see that

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:29):

the problem right now is that MetaCoq in-repo opam packages do not give a version: declaration, which makes it almost nondeterministic what version you get when pinning in the MetaCoq repo

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 08:29):

Hopefully we can come to a point where CertiCoq and MetaCoq are decoupled enough so that submodules becomes unnecessary.

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 08:29):

You mean this could be fixed by regularly updating the version: in metacoq's .opam files?

view this post on Zulip Karl Palmskog (Apr 04 2022 at 08:30):

in my view, you only need to update version: when you branch. For example, here is what version looks like in AAC Tactics branch v8.14: https://github.com/coq-community/aac-tactics/blob/v8.14/coq-aac-tactics.opam#L6

version: "8.14.dev"

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 09:52):

Ok, that sounds easy enough :)

view this post on Zulip Anders Larsson (Apr 04 2022 at 10:27):

the problem right now is that MetaCoq in-repo opam packages do not give a version: declaration,

Maybe it's time to assign a 0.0.1 version numer and update the last figure when the dependencies change?
Neither packages are in early stage development any more.

view this post on Zulip Karl Palmskog (Apr 04 2022 at 10:28):

0.0.1 can't be used since it would be sorted before the last beta, 1.0~beta2

view this post on Zulip Anders Larsson (Apr 04 2022 at 10:36):

OK.
But were any non beta versions ever assigned? I didn't look like that in the repository.

view this post on Zulip Matthieu Sozeau (Apr 04 2022 at 12:43):

Nope, there was no non-beta releases yet


Last updated: Feb 06 2023 at 07:03 UTC