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).
[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
Can you show the output of
opam repo list and
You can also try installing the dependencies in https://github.com/CertiCoq/certicoq/blob/ea52e6f93adb90c3d2a6badd63e677a5f4c27572/coq-certicoq.opam by hand.
Or rather, try simulating their installation with --dry-run.
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)
$ 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
$ 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
I'll start with installing coq-equations - it looked like it was missing.
You have a different coq version there
you could upgrade coq, but creating a new opam switch is likely safer
sorry, nevermind, there might be something wrong with coq-certicoq…
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.
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?
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.
IIUC @Tim Carstens set up that Docker image?
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:
So I'd recommend trying:
... all installed from the Coq opam
released archive (avoid
extra-dev in the switch)
@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
I meant, patched to support 8.9 to 8.14, which this was about. The "patch" in this case was
Sorry, nevermind! Now I was just confused. coq.io seems out of date but I'll double check later
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).
Anders Larsson has marked this topic as resolved.
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)
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:
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: *** [Makefile.coq:763: theories/utils/ByteCompare.vo] Error 1 # make: *** [Makefile.coq:386: all] Error 2 # make: Leaving directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13/template-coq' # make: *** [Makefile:6: coq] Error 2 # make: 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.
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" .
dev-repo is not used during opam package installation in any way
I'd recommend creating a fresh opam switch instead of using the container, since easier to debug
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 $
you can't use the
nnpchecker option with Coq, the Coq package has this:
conflicts: "base-nnp" "ocaml-option-nnpchecker"
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)
Karl Palmskog has marked this topic as unresolved.
I also really recommend installing all versions explicitly, for example:
opam install coq.8.14.1 coq-compcert.3.9 coq-vst.2.8
I'll try that.
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: *** [Makefile.coq:763: theories/utils/ByteCompare.vo] Error 1 # make: *** Waiting for unfinished jobs.... # make: *** [Makefile.coq:386: all] Error 2 # make: 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:6: coq] Error 2 # make: 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
The version number would suggest that metacoq package is for Coq 8.13... I guess this package was patched as well somewhere?
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
(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...)
Right, I've used the 8.15 branch too…
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
IIUC, this will just install the sources — the version number used by opam is somewhat arbitrary
IIRC you can pick another one when pinning
in this case, I think it takes after the latest released version
even though the
-k path forces local
separately, I wonder why
opam is giving uninformative error messages, maybe it depends on the solver that is enabled
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...
the official opam binaries produce much better messages
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.
that compilation problem [with Byte] will likely not happen when you use the MetaCoq from the CertiCoq repo submodule
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…
actually, let me check the pinned hash…
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.
@Anders Larsson and you followed the certicoq instructions using their
opam pin command, right?
are you using the
opam pin add coq-metacoq-* -k path . commands?
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…
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
@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).
the Certicoq README recommends
opam pin -n -y submodules/metacoq, but it’s reasonable it’d work as well
@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.
and regardless of what Coq does, should
From Coq Require Byte find
Big thanks for all the comments. I think I got through now . :-)
if all they need is MetaCoq-erasure, then it seems like a waste to pin+install all MetaCoq packages
ah, I guess the only redundant one is translations, in the end
are you using the opam pin add coq-metacoq-* -k path . commands?
$ opam pin -n -y submodules/metacoq
$ opam pin -n -y .
the whole thing with pinning a whole directory of
.opam files in one command seems shaky
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?
@Anders Larsson out of curiosity, which filesystem are you building on?
the only time I pin with
-n is in CI to install dependencies separately
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).
how often is Coq really IO bound? I think the consensus is that it's mostly memory bound
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).
I’ve confirmed that the MetaCoq issue reproduces on my end 😭 There’s definitely some work to be done here, sorry for the trouble.
Anything else so far?
building/installation of CertiCoq works fine once one does the pinning of the MetaCoq packages in the submodule
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:
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
OK, I can at least say that: "the error-free CI build of latest CertiCoq was replicated locally [by me]"
@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).
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.
the whole thing with
1.0~betaX+8.YZ for releases is difficult to reconcile with git branches - maybe
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.
You mean certicoq or metacoq? But :+1:
I meant CertiCoq, but since it depends on MetaCoq (afaik), this would include MetaCoq.
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
@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
I guess we should have tags in the git repo corresponding to each release, wouldn't that be enough?
Do you mean we can confuse the versioning logic of opam when we use
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
for example, many plugins have the following scheme:
8.15.0is the tag/release which compatible with Coq 8.15
8.15.devis the version of the opam package in the repo or in
this ensures that
8.15.dev is always greater than any
8.15.1 package version to opam
Right, I see that
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
Hopefully we can come to a point where CertiCoq and MetaCoq are decoupled enough so that submodules becomes unnecessary.
You mean this could be fixed by regularly updating the
version: in metacoq's .opam files?
in my view, you only need to update
version: when you branch. For example, here is what
version looks like in AAC Tactics branch
Ok, that sounds easy enough :)
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.
0.0.1 can't be used since it would be sorted before the last beta,
But were any non beta versions ever assigned? I didn't look like that in the repository.
Nope, there was no non-beta releases yet
Last updated: Feb 06 2023 at 07:03 UTC