ยซ 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.14.0      Formal proof management system
dune                3.2.0       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.3       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.14.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.14.0
Return code
0
Duration
11 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-qcert.2.2.0 coq.8.14.0
Return code
7936
Duration
5 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-bytes           base        Bytes library distributed with the OCaml compiler
base-threads         base
base-unix            base
base64               3.5.0       Base64 encoding for OCaml
bigstringaf          0.9.0       Bigstring intrinsics and fast blits based on memcpy/memmove
biniou               1.2.1       Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
calendar             2.04        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.14.0      Formal proof management system
coq-jsast            3.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.2.0       Fast, portable, and opinionated build system
easy-format          1.3.3       High-level and functional interface to the Format module of the OCaml standard library
js_of_ocaml          4.0.0       Compiler from OCaml bytecode to JavaScript
js_of_ocaml-compiler 4.0.0       Compiler from OCaml bytecode to JavaScript
js_of_ocaml-ppx      4.0.0       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.1      OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind            1.9.3       A library manager for OCaml
ppx_derivers         1.2.1       Shared [@@deriving] plugin registry
ppxlib               0.26.0      Standard library for ppx rewriters
result               1.5         Compatibility Result module
sexplib0             v0.15.0     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
uchar                0.0.2       Compatibility library for OCaml's Uchar module
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               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
[NOTE] Package coq is already installed (current version is 8.14.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
- COQC compiler/core/Utils/Monoid.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."
- [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."
- [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."
- [deprecated-hint-rewrite-without-locality,deprecated]
- COQC compiler/core/Utils/Digits.v
- COQC compiler/core/Utils/Var.v
- COQC compiler/core/Utils/Closure.v
- COQC compiler/core/Utils/Result.v
- COQC compiler/core/Utils/Apply.v
- COQC compiler/core/TypeSystem/ForeignType.v
- COQC compiler/core/JavaScriptAst/Lang/JavaScriptAst.v
- COQC compiler/core/Extraction/ExtrOcamlFloatNatIntZInt.v
- COQC compiler/core/Utils/ListAdd.v
- COQC compiler/core/Utils/StringAdd.v
- COQC compiler/core/Data/Model/ForeignData.v
- File "./compiler/core/Utils/StringAdd.v", line 191, characters 2-6:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- COQC compiler/core/Utils/NativeString.v
- COQC compiler/core/Utils/EmitUtil.v
- COQC compiler/core/JavaScript/Lang/JavaScript.v
- COQC compiler/core/SparkDF/Lang/SparkDF.v
- COQC compiler/core/JavaScript/JavaScriptRuntime.v
- COQC compiler/core/SparkDF/SparkDFRuntime.v
- COQC compiler/core/JavaScript/JavaScriptSystem.v
- COQC compiler/core/SparkDF/SparkDFSystem.v
- COQC compiler/core/Utils/ToString.v
- COQC compiler/core/Utils/SortingAdd.v
- COQC compiler/core/Utils/Assoc.v
- COQC compiler/core/Utils/OptimizerStep.v
- COQC compiler/core/JSON/Model/JSON.v
- COQC compiler/core/Utils/OptimizerLogger.v
- COQC compiler/core/EJson/Model/ForeignEJson.v
- COQC compiler/core/Translation/Operators/ForeignToJavaScriptAst.v
- COQC compiler/core/Utils/Sublist.v
- COQC compiler/core/Utils/Compat.v
- COQC compiler/core/Utils/LiftIterators.v
- COQC compiler/core/Utils/Bag.v
- COQC compiler/core/Utils/Bindings.v
- COQC compiler/core/Utils/Fresh.v
- File "./compiler/core/Utils/Bag.v", line 1567, characters 0-179:
- 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."
- [deprecated-hint-rewrite-without-locality,deprecated]
- COQC compiler/core/Utils/GroupByDomain.v
- COQC compiler/core/Utils/Interleaved.v
- COQC compiler/core/Utils/BindingsNat.v
- COQC compiler/core/Utils/SortingDesc.v
- COQC compiler/core/Utils/Encode.v
- COQC compiler/core/JSON/Model/JSONNorm.v
- File "./compiler/core/Utils/SortingDesc.v", line 143, characters 2-6:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- COQC compiler/core/JSON/JSONRuntime.v
- COQC compiler/core/JSON/JSONSystem.v
- File "./compiler/core/Utils/SortingDesc.v", line 309, characters 2-6:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- COQC compiler/core/Utils/Utils.v
- COQC compiler/core/Brands/BrandRelation.v
- COQC compiler/core/WSON/Model/ForeignWSON.v
- COQC compiler/core/WSON/Operators/ForeignWSONRuntime.v
- COQC compiler/core/EJson/Model/EJson.v
- COQC compiler/core/Translation/Model/ForeignEJsonToJSON.v
- COQC compiler/core/Translation/Model/ForeignTypeToJSON.v
- COQC compiler/core/Imp/Lang/Imp.v
- COQC compiler/core/JavaScriptAst/Lang/JavaScriptAstUtil.v
- COQC compiler/core/Java/Lang/Java.v
- COQC compiler/core/Translation/Operators/ForeignToWasmAst.v
- COQC compiler/core/Compiler/Component/LoggerComponent.v
- COQC compiler/core/WSON/WSONRuntime.v
- COQC compiler/core/EJson/Model/EJsonNorm.v
- COQC compiler/core/EJson/Operators/ForeignEJsonRuntime.v
- COQC compiler/core/EJson/Operators/EJsonOperators.v
- COQC compiler/core/EJson/Operators/EJsonGroupBy.v
- COQC compiler/core/EJson/Operators/EJsonSortBy.v
- COQC compiler/core/Translation/Model/ForeignEJsonToWSON.v
- COQC compiler/core/Imp/Lang/ImpSize.v
- COQC compiler/core/Imp/Lang/ImpEval.v
- COQC compiler/core/JavaScriptAst/JavaScriptAstRuntime.v
- COQC compiler/core/Java/JavaRuntime.v
- COQC compiler/core/WSON/WSONSystem.v
- COQC compiler/core/JavaScriptAst/JavaScriptAstSystem.v
- COQC compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.v
- COQC compiler/core/Imp/Lang/ImpEq.v
- COQC compiler/core/Java/JavaSystem.v
- File "./compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.v", line 64, characters 2-295:
- Error: Non exhaustive pattern-matching: no clause found for pattern
- literal_bigint _
- 
- make[3]: *** [Makefile.coq:763: compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.vo] Error 1
- make[3]: *** Waiting for unfinished jobs....
- File "./compiler/core/Brands/BrandRelation.v", line 1423, characters 0-96:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- make[2]: *** [Makefile.coq:386: 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-25979-e4db2f.env
# output-file          ~/.opam/log/coq-qcert-25979-e4db2f.out
### output ###
# [...]
# Warning: The default value for instance locality is currently "local" in a
# section and "global" otherwise, but is scheduled to change in a future
# release. For the time being, adding instances 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]
# Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
# make[2]: *** [Makefile.coq:386: 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.14.0' failed.

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none