# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
coq 8.11.2 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.6 A library manager for OCaml
# 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 and Java.
"""
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.0" & < "8.13~"}
"coq-jsast" {>= "2.0.0"}
"menhir"
"base64"
"uri"
"calendar"
]
tags: [ "keyword:databases" "keyword:queries" "keyword:relational" "keyword:compiler" "date:2022-03-08" "logpath:Qcert" ]
url {
src: "https://github.com/querycert/qcert/archive/v2.1.1.tar.gz"
checksum: "351f5ae9b1380e6a0f673a21b483e6b2"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-qcert.2.1.1 coq.8.11.2Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-qcert.2.1.1 coq.8.11.2opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-qcert.2.1.1 coq.8.11.2# 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.1 Bigstring intrinsics and fast blits based on memcpy/memmove
calendar 3.0.0 Library for handling dates and times in your program
conf-findutils 1 Virtual package relying on findutils
coq 8.11.2 Formal proof management system
coq-jsast 3.0.0 A minimal JavaScript syntax tree carved out of the JsCert project
csexp 1.5.2 Parsing and printing of S-expressions in Canonical form
dune 3.12.1 Fast, portable, and opinionated build system
dune-configurator 3.12.1 Helper library for gathering system configuration
menhir 20230608 An LR(1) parser generator
menhirLib 20230608 Runtime support library for parsers generated by Menhir
menhirSdk 20230608 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.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocaml-syntax-shims 1.0.0 Backport new syntax to older OCaml versions
ocamlfind 1.9.6 A library manager for OCaml
re 1.11.0 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.
stringext 1.6.0 Extra string functions for OCaml
uri 4.4.0 An RFC3986 URI/URL parsing library
[NOTE] Package coq is already installed (current version is 8.11.2).
The following actions will be performed:
- install coq-qcert 2.1.1
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq-qcert.2.1.1: http]
[coq-qcert.2.1.1] downloaded from https://github.com/querycert/qcert/archive/v2.1.1.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.09.1/.opam-switch/build/coq-qcert.2.1.1)
- [Q*cert]
- [Q*cert] Configuring Build
- [Q*cert]
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
- make -C runtimes/javascript
- make[2]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1/runtimes/javascript'
- (for i in qcert-runtime-core.js qcert-runtime-tostring.js qcert-runtime-sql-date.js qcert-runtime-uri.js; do \
- cat $i; \
- done) > qcert-runtime.js
- (echo "let runtime = {runtime|"; \
- cat qcert-runtime.js; \
- echo '|runtime}' \
- ) > qcert_runtime.ml
- make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1/runtimes/javascript'
- cp runtimes/javascript/qcert_runtime.ml compiler/lib/js_runtime.ml
- echo "(* This file is generated *)" > compiler/lib/static_config.ml
- echo "let qcert_home = \"/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1\"" >> compiler/lib/static_config.ml
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
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.09.1/.opam-switch/build/coq-qcert.2.1.1)
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
- [Q*cert]
- [Q*cert] Building Compiler from Coq
- [Q*cert]
- make[2]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
- COQDEP VFILES
- COQC compiler/core/Version.v
- COQC compiler/core/Utils/CoqLibAdd.v
- COQC compiler/core/Utils/Lift.v
- COQC compiler/core/Utils/Float.v
- COQC compiler/core/Utils/Lattice.v
- COQC compiler/core/Utils/Monoid.v
- 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
- 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/SortingAdd.v
- COQC compiler/core/Utils/Assoc.v
- COQC compiler/core/Utils/OptimizerStep.v
- COQC compiler/core/Utils/OptimizerLogger.v
- COQC compiler/core/Utils/ToString.v
- COQC compiler/core/JSON/Model/JSON.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
- 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
- COQC compiler/core/JSON/JSONRuntime.v
- COQC compiler/core/JSON/JSONSystem.v
- COQC compiler/core/Utils/Utils.v
- COQC compiler/core/Brands/BrandRelation.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/Compiler/Component/LoggerComponent.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/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/Imp/Lang/ImpEq.v
- COQC compiler/core/JavaScriptAst/JavaScriptAstSystem.v
- COQC compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.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:678: compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.vo] Error 1
- make[3]: *** Waiting for unfinished jobs....
- make[2]: *** [Makefile.coq:327: all] Error 2
- make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
- make[1]: *** [Makefile:147: qcert-coq] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
- make: *** [Makefile:78: 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.1.1 ====================================#
# context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j 4 coq-qcert
# exit-code 2
# env-file ~/.opam/log/coq-qcert-6732-e4db2f.env
# output-file ~/.opam/log/coq-qcert-6732-e4db2f.out
### output ###
# [...]
# 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:678: compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.vo] Error 1
# make[3]: *** Waiting for unfinished jobs....
# make[2]: *** [Makefile.coq:327: all] Error 2
# make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
# make[1]: *** [Makefile:147: qcert-coq] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-qcert.2.1.1'
# make: *** [Makefile:78: coq-qcert] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-qcert 2.1.1
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-qcert.2.1.1 coq.8.11.2' failed.
No files were installed.
true