# 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.7.0 Fast, portable, and opinionated build system
ocaml 4.11.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.2 Official release 4.11.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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-qcert.2.2.0 coq.8.16.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.16.0opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-qcert.2.2.0 coq.8.16.0# 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.7.0 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.11.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.2 Official release 4.11.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.11.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.11.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.11.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.11.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.11.2/.opam-switch/build/coq-qcert.2.2.0) - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.11.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.11.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.11.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.11.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.7 | linux/x86_64 | ocaml-base-compiler.4.11.2 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.11.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-17499-e4db2f.env # output-file ~/.opam/log/coq-qcert-17499-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.11.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.11.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.
No files were installed.
true