# 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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-qcert.2.2.0 coq.8.14.0Dry 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.2.0 coq.8.14.0opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-qcert.2.2.0 coq.8.14.0# 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.
No files were installed.
true