Anders Larsson (Apr 02 2022 at 07:20): 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
Can you show the output of opam repo list and opam list?
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.
Paolo Giarrusso (Apr 02 2022 at 07:27):Or rather, try simulating their installation with --dry-run.
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)
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
$ 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.
Paolo Giarrusso (Apr 02 2022 at 07:46):You have a different coq version there
Paolo Giarrusso (Apr 02 2022 at 07:49):you could upgrade coq, but creating a new opam switch is likely safer
Paolo Giarrusso (Apr 02 2022 at 07:51):sorry, nevermind, there might be something wrong with coq-certicoq…
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.
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?
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.
Paolo Giarrusso (Apr 02 2022 at 08:01):IIUC @Tim Carstens set up that Docker image?
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)
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
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"
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
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).
Notification Bot (Apr 02 2022 at 11:35):Anders Larsson has marked this topic as resolved.
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)
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" .
Karl Palmskog (Apr 02 2022 at 18:39):dev-repo is not used during opam package installation in any way
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
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
$
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)
Notification Bot (Apr 02 2022 at 19:48):Karl Palmskog has marked this topic as unresolved.
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
I'll try that.
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
The version number would suggest that metacoq package is for Coq 8.13... I guess this package was patched as well somewhere?
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
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...)
Paolo Giarrusso (Apr 02 2022 at 22:03):Right, I've used the 8.15 branch too…
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
Paolo Giarrusso (Apr 02 2022 at 22:04):IIUC, this will just install the sources — the version number used by opam is somewhat arbitrary
Paolo Giarrusso (Apr 02 2022 at 22:05):IIRC you can pick another one when pinning
Karl Palmskog (Apr 02 2022 at 22:05):in this case, I think it takes after the latest released version
Karl Palmskog (Apr 02 2022 at 22:06):even though the -k path forces local
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
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...
Paolo Giarrusso (Apr 02 2022 at 22:07):the official opam binaries produce much better messages
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.
that compilation problem [with Byte] will likely not happen when you use the MetaCoq from the CertiCoq repo submodule
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…
Paolo Giarrusso (Apr 02 2022 at 22:10):actually, let me check the pinned hash…
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.
Paolo Giarrusso (Apr 02 2022 at 22:12):@Anders Larsson and you followed the certicoq instructions using their opam pin command, right?
Karl Palmskog (Apr 02 2022 at 22:12):are you using the opam pin add coq-metacoq-* -k path . commands?
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…
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
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).
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
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.
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?
Anders Larsson (Apr 02 2022 at 22:15):Big thanks for all the comments. I think I got through now . :-)
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
Karl Palmskog (Apr 02 2022 at 22:18):ah, I guess the only redundant one is translations, in the end
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 .
the whole thing with pinning a whole directory of .opam files in one command seems shaky
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?
Paolo Giarrusso (Apr 02 2022 at 22:24):@Anders Larsson out of curiosity, which filesystem are you building on?
Karl Palmskog (Apr 02 2022 at 22:25):the only time I pin with -n is in CI to install dependencies separately
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).
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
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).
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:
Anything else so far?
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
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"
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
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]"
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).
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.
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?
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.
Paolo Giarrusso (Apr 04 2022 at 06:16):You mean certicoq or metacoq? But :+1:
Michael Soegtrop (Apr 04 2022 at 07:11):I meant CertiCoq, but since it depends on MetaCoq (afaik), this would include MetaCoq.
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
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
Karl Palmskog (Apr 04 2022 at 08:23):for example, 1.0+8.XY vs. 1.0+8.XY.dev
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?
Matthieu Sozeau (Apr 04 2022 at 08:24):Do you mean we can confuse the versioning logic of opam when we use +?
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
Karl Palmskog (Apr 04 2022 at 08:25):for example, many plugins have the following scheme:
8.15.0 is the tag/release which compatible with Coq 8.158.15.dev is the version of the opam package in the repo or in extra-dev 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
Matthieu Sozeau (Apr 04 2022 at 08:27):Right, I see that
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
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.
Matthieu Sozeau (Apr 04 2022 at 08:29):You mean this could be fixed by regularly updating the version: in metacoq's .opam files?
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"
Ok, that sounds easy enough :)
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.
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
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.
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