ยซ Up

qcert 2.2.0 Error ๐Ÿ”ฅ

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-gmp            4           Virtual package relying on a GMP lib system installation
coq                 8.16.0      Formal proof management system
dune                3.6.2       Fast, portable, and opinionated build system
ocaml               4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2      Official release 4.10.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.5       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
synopsis: "Verified compiler for data-centric languages"
description: """
This is the Coq library for Q*cert, a platform for implementing and verifying data languages and compilers. It includes abstract syntax and semantics for several source query languages (OQL, SQL), for intermediate database representations (nested relational algebra and calculus), and correctness proofs for part of the compilation to JavaScript, Java and WASM.
"""
maintainer: "Jerome Simeon <jeromesimeon@me.com>"
authors: [ "Josh Auerbach <>" "Martin Hirzel <>" "Louis Mandel <>" "Avi Shinnar <>" "Jerome Simeon <>" ]
license: "Apache-2.0"
homepage: "https://querycert.github.io"
bug-reports: "https://github.com/querycert/qcert/issues"
dev-repo: "git+https://github.com/querycert/qcert"
build: [
  [make "configure"]
  [make "-j" jobs name]
  ["dune" "build" "-j" jobs "-p" name]
]
install: [
  [make "install-coqdev"]
]
depends: [
  "ocaml" {>= "4.09.1"}
  "ocamlfind"
  "dune"
  "coq" {>= "8.11.2"}
  "coq-jsast" {= "2.0.0"}
  "menhir"
  "base64"
  "js_of_ocaml"
  "js_of_ocaml-ppx"
  "uri"
  "wasm" {= "1.0.1"}
  "calendar"
]
tags: [ "keyword:databases" "keyword:queries" "keyword:relational" "keyword:compiler" "date:2020-08-22" "logpath:Qcert" ]
url {
  src: "https://github.com/querycert/qcert/archive/refs/tags/v2.2.0.tar.gz"
  checksum: "1dd98e96ba80da9a0e45a295354b1acb"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-qcert.2.2.0 coq.8.16.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-qcert.2.2.0 coq.8.16.0
Return code
0
Duration
10 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-qcert.2.2.0 coq.8.16.0
Return code
7936
Duration
1 m 0 s
Output
# Packages matching: installed
# Name               # Installed # Synopsis
angstrom             0.15.0      Parser combinators built for speed and memory-efficiency
base-bigarray        base
base-threads         base
base-unix            base
base64               3.5.1       Base64 encoding for OCaml
bigstringaf          0.9.0       Bigstring intrinsics and fast blits based on memcpy/memmove
calendar             3.0.0       Library for handling dates and times in your program
cmdliner             1.1.1       Declarative definition of command line interfaces for OCaml
conf-findutils       1           Virtual package relying on findutils
conf-gmp             4           Virtual package relying on a GMP lib system installation
conf-pkg-config      2           Check if pkg-config is installed and create an opam switch local pkgconfig folder
coq                  8.16.0      Formal proof management system
coq-jsast            2.0.0       A minimal JavaScript syntax tree carved out of the JsCert project
cppo                 1.6.9       Code preprocessor like cpp for OCaml
dune                 3.6.2       Fast, portable, and opinionated build system
js_of_ocaml          5.0.1       Compiler from OCaml bytecode to JavaScript
js_of_ocaml-compiler 5.0.1       Compiler from OCaml bytecode to JavaScript
js_of_ocaml-ppx      5.0.1       Compiler from OCaml bytecode to JavaScript
menhir               20220210    An LR(1) parser generator
menhirLib            20220210    Runtime support library for parsers generated by Menhir
menhirSdk            20220210    Compile-time library for auxiliary tools related to Menhir
ocaml                4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler  4.10.2      Official release 4.10.2
ocaml-compiler-libs  v0.12.4     OCaml compiler libraries repackaged
ocaml-config         1           OCaml Switch Configuration
ocaml-syntax-shims   1.0.0       Backport new syntax to older OCaml versions
ocamlbuild           0.14.2      OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind            1.9.5       A library manager for OCaml
ppx_derivers         1.2.1       Shared [@@deriving] plugin registry
ppxlib               0.29.1      Standard library for ppx rewriters
re                   1.10.4      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.15.1     Library containing the definition of S-expressions and some base converters
stdlib-shims         0.3.0       Backport some of the new stdlib features to older compiler
stringext            1.6.0       Extra string functions for OCaml
uri                  4.2.0       An RFC3986 URI/URL parsing library
wasm                 1.0.1       Library to read and write WebAssembly (Wasm) files and manipulate their AST
yojson               2.0.2       Yojson is an optimized parsing and printing library for the JSON format
zarith               1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.16.0).
The following actions will be performed:
  - install coq-qcert 2.2.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-qcert.2.2.0: http]
[coq-qcert.2.2.0] downloaded from https://github.com/querycert/qcert/archive/refs/tags/v2.2.0.tar.gz
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-qcert: make configure]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0)
- [Q*cert] 
- [Q*cert] Configuring Build
- [Q*cert] 
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
- echo "(* This file is generated *)" > compiler/lib/static_config.ml
- echo "let qcert_home = \"/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0\"" >> compiler/lib/static_config.ml
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
Processing  1/2: [coq-qcert: make 4]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j" "4" "coq-qcert" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0)
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
- [Q*cert] 
- [Q*cert] Building Compiler from Coq
- [Q*cert] 
- make[2]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
- COQDEP VFILES
- COQC compiler/core/Version.v
- COQC compiler/core/Utils/CoqLibAdd.v
- COQC compiler/core/Utils/Lift.v
- COQC compiler/core/Utils/FloatAdd.v
- COQC compiler/core/Utils/Lattice.v
- File "./compiler/core/Utils/Lift.v", line 340, characters 0-31:
- Warning: The default value for rewriting hint locality is currently "local"
- in a section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding rewriting hints outside of sections
- without specifying an explicit locality attribute is therefore deprecated. It
- is recommended to use "export" whenever possible. Use the attributes
- #[local], #[global] and #[export] depending on your choice. For example:
- "#[export] Hint Rewrite foo : bar." This is supported since Coq 8.14.
- [deprecated-hint-rewrite-without-locality,deprecated]
- File "./compiler/core/Utils/Lift.v", line 341, characters 0-34:
- Warning: The default value for rewriting hint locality is currently "local"
- in a section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding rewriting hints outside of sections
- without specifying an explicit locality attribute is therefore deprecated. It
- is recommended to use "export" whenever possible. Use the attributes
- #[local], #[global] and #[export] depending on your choice. For example:
- "#[export] Hint Rewrite foo : bar." This is supported since Coq 8.14.
- [deprecated-hint-rewrite-without-locality,deprecated]
- File "./compiler/core/Utils/Lift.v", line 342, characters 0-33:
- Warning: The default value for rewriting hint locality is currently "local"
- in a section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding rewriting hints outside of sections
- without specifying an explicit locality attribute is therefore deprecated. It
- is recommended to use "export" whenever possible. Use the attributes
- #[local], #[global] and #[export] depending on your choice. For example:
- "#[export] Hint Rewrite foo : bar." This is supported since Coq 8.14.
- [deprecated-hint-rewrite-without-locality,deprecated]
- COQC compiler/core/Utils/Monoid.v
- COQC compiler/core/Utils/Digits.v
- COQC compiler/core/Utils/Var.v
- COQC compiler/core/Utils/Closure.v
- File "./compiler/core/Utils/Digits.v", line 62, characters 19-26:
- Warning: Notation le_Sn_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.nle_succ_diag_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/Digits.v", line 62, characters 19-26:
- Warning: Notation le_Sn_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.nle_succ_diag_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/Digits.v", line 68, characters 19-26:
- Warning: Notation le_Sn_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.nle_succ_diag_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/Digits.v", line 68, characters 19-26:
- Warning: Notation le_Sn_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.nle_succ_diag_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/Digits.v", line 152, characters 80-81:
- Error: The reference H was not found in the current environment.
- 
- make[3]: *** [Makefile.coq:792: compiler/core/Utils/Digits.vo] Error 1
- make[3]: *** Waiting for unfinished jobs....
- File "./compiler/core/Utils/CoqLibAdd.v", line 576, characters 14-32:
- Warning: Notation Min.succ_min_distr is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.succ_min_distr instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 576, characters 14-32:
- Warning: Notation Min.succ_min_distr is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.succ_min_distr instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 576, characters 14-32:
- Warning: Notation Min.succ_min_distr is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.succ_min_distr instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 623, characters 14-31:
- Warning: Notation mult_plus_distr_l is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_add_distr_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 623, characters 14-31:
- Warning: Notation mult_plus_distr_l is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_add_distr_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 623, characters 14-31:
- Warning: Notation mult_plus_distr_l is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_add_distr_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 624, characters 14-31:
- Warning: Notation mult_plus_distr_l is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_add_distr_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 624, characters 14-31:
- Warning: Notation mult_plus_distr_l is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_add_distr_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 624, characters 14-31:
- Warning: Notation mult_plus_distr_l is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_add_distr_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 634, characters 42-51:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./compiler/core/Utils/CoqLibAdd.v", line 634, characters 42-51:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- make[2]: *** [Makefile.coq:409: all] Error 2
- make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
- make[1]: *** [Makefile:140: qcert-coq] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
- make: *** [Makefile:79: coq-qcert] Error 2
[ERROR] The compilation of coq-qcert failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j 4 coq-qcert".
#=== ERROR while compiling coq-qcert.2.2.0 ====================================#
# context              2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.2 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j 4 coq-qcert
# exit-code            2
# env-file             ~/.opam/log/coq-qcert-20754-e4db2f.env
# output-file          ~/.opam/log/coq-qcert-20754-e4db2f.out
### output ###
# [...]
# Warning: Notation plus_comm is deprecated since 8.16.
# The Arith.Plus file is obsolete. Use Nat.add_comm instead.
# [deprecated-syntactic-definition,deprecated]
# File "./compiler/core/Utils/CoqLibAdd.v", line 634, characters 42-51:
# Warning: Notation plus_comm is deprecated since 8.16.
# The Arith.Plus file is obsolete. Use Nat.add_comm instead.
# [deprecated-syntactic-definition,deprecated]
# make[2]: *** [Makefile.coq:409: all] Error 2
# make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
# make[1]: *** [Makefile:140: qcert-coq] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-qcert.2.2.0'
# make: *** [Makefile:79: coq-qcert] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-qcert 2.2.0
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-qcert.2.2.0 coq.8.16.0' failed.

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none