(2020-04-14 10:21:03 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq dev Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.10.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.0 Official release 4.10.0
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
# opam file:
opam-version: "2.0"
name: "coq-relation-algebra"
synopsis: "Relation Algebra and KAT in Coq"
maintainer: "Damien Pous <Damien.Pous@ens-lyon.fr>"
version: "1.7.3"
homepage: "http://perso.ens-lyon.fr/damien.pous/ra/"
license: "LGPL"
depends: [
"ocaml"
"coq" {>= "8.11"}
]
depopts: [ "coq-mathcomp-ssreflect" ]
build: [
["sh" "-exc" "./configure --%{coq-mathcomp-ssreflect:enable}%-ssr"]
[make "-j%{jobs}%"]
]
install: [make "install"]
tags: [
"keyword:relation algebra"
"keyword:kleene algebra with tests"
"keyword:kat"
"keyword:allegories"
"keyword:residuated structures"
"keyword:automata"
"keyword:regular expressions"
"keyword:matrices"
"category:Mathematics/Algebra"
"logpath:RelationAlgebra" ]
authors: [
"Damien Pous <Damien.Pous@ens-lyon.fr>"
"Christian Doczkal <christian.doczkal@ens-lyon.fr>"
]
url {
src:
"https://github.com/damien-pous/relation-algebra/archive/v1.7.3.tar.gz"
checksum: "md5=69c916214840e742d3a78d6d3cb55a1c"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-relation-algebra.1.7.3 coq.devDry 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 2h opam install -y --deps-only coq-relation-algebra.1.7.3 coq.devopam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-relation-algebra.1.7.3 coq.dev# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq dev Formal proof management system num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.0 Official release 4.10.0 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.8.1 A library manager for OCaml [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-relation-algebra 1.7.3 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-relation-algebra.1.7.3: http] [coq-relation-algebra.1.7.3] downloaded from https://github.com/damien-pous/relation-algebra/archive/v1.7.3.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-relation-algebra: sh] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "sh" "-exc" "./configure --disable-ssr" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3) - + ./configure --disable-ssr Processing 1/2: [coq-relation-algebra: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3) - coq_makefile -f _CoqProject -o Makefile.coq - make -f Makefile.coq Makefile - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3' - COQDEP VFILES - COQPP ra_fold.mlg - COQPP mrewrite.mlg - COQPP ra_reification.mlg - COQPP kat_reification.mlg - CAMLDEP kat_dec.mli - OCAMLLIBDEP kat_reification.mllib - OCAMLLIBDEP ra_reification.mllib - OCAMLLIBDEP ra_common.mllib - OCAMLLIBDEP mrewrite.mllib - OCAMLLIBDEP ra_fold.mllib - CAMLDEP kat_dec.ml - CAMLDEP ra_common.ml - CAMLDEP kat_reification.ml - CAMLDEP ra_reification.ml - CAMLDEP mrewrite.ml - CAMLDEP ra_fold.ml - make[1]: Nothing to be done for 'Makefile'. - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3' - make -f Makefile.coq all - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3' - COQC common.v - COQC comparisons.v - CAMLOPT -c ra_common.ml - CAMLC -c kat_dec.mli - File "ra_common.ml", line 52, characters 18-35: - 52 | let convertible = Tacmach.pf_conv_x - ^^^^^^^^^^^^^^^^^ - Alert deprecated: Tacmach.pf_conv_x - Use the version in Tacmach.New - File "ra_common.ml", line 61, characters 65-86: - 61 | lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.find_reference "RelationAlgebra.reification" dir s))) - ^^^^^^^^^^^^^^^^^^^^^ - Alert deprecated: Coqlib.find_reference - Please use Coqlib.lib_ref - CAMLOPT -c kat_dec.ml - CAMLOPT -a -o ra_common.cmxa - CAMLOPT -c ra_fold.ml - CAMLOPT -c mrewrite.ml - File "ra_fold.mlg", line 28, characters 13-38: - Alert deprecated: Tacmach.pf_unsafe_type_of - Use [type_of] or retyping according to your needs. - File "mrewrite.mlg", line 109, characters 10-39: - Alert deprecated: Tacmach.New.pf_unsafe_type_of - Use [type_of] or retyping according to your needs. - File "ra_fold.mlg", line 93, characters 12-33: - Alert deprecated: Typing.unsafe_type_of - Use [type_of] or retyping according to your needs. - CAMLOPT -c ra_reification.ml - CAMLOPT -c kat_reification.ml - COQC powerfix.v - COQC level.v - CAMLOPT -shared -o ra_common.cmxs - CAMLOPT -a -o ra_fold.cmxa - CAMLOPT -a -o mrewrite.cmxa - CAMLOPT -a -o ra_reification.cmxa - CAMLOPT -a -o kat_reification.cmxa - COQC positives.v - COQC ordinal.v - CAMLOPT -shared -o ra_fold.cmxs - CAMLOPT -shared -o mrewrite.cmxs - CAMLOPT -shared -o ra_reification.cmxs - CAMLOPT -shared -o kat_reification.cmxs - COQC lattice.v - COQC denum.v - COQC pair.v - COQC monoid.v - COQC prop.v - COQC lset.v - COQC sups.v - COQC lsyntax.v - COQC rewriting.v - COQC kleene.v - COQC syntax.v - COQC boolean.v - File "./boolean.v", line 35, characters 2-8: - Error: Tactic failure: tauto failed. - - make[2]: *** [Makefile.coq:699: boolean.vo] Error 1 - make[2]: *** Waiting for unfinished jobs.... - make[1]: *** [Makefile.coq:335: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3' - make: *** [Makefile:2: all] Error 2 [ERROR] The compilation of coq-relation-algebra failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-relation-algebra.1.7.3 =========================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-relation-algebra-31083-e4db2f.env # output-file ~/.opam/log/coq-relation-algebra-31083-e4db2f.out ### output ### # [...] # COQC rewriting.v # COQC kleene.v # COQC syntax.v # COQC boolean.v # File "./boolean.v", line 35, characters 2-8: # Error: Tactic failure: tauto failed. # # make[2]: *** [Makefile.coq:699: boolean.vo] Error 1 # make[2]: *** Waiting for unfinished jobs.... # make[1]: *** [Makefile.coq:335: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-relation-algebra.1.7.3' # make: *** [Makefile:2: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-relation-algebra 1.7.3 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-relation-algebra.1.7.3 coq.dev' failed.
No files were installed.
true