(2020-06-25 03:38:52 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.12 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
coq 8.5.0 Formal proof management system.
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
# opam file:
opam-version: "2.0"
maintainer: "Damien Pous <Damien.Pous@ens-lyon.fr>"
homepage: "http://perso.ens-lyon.fr/damien.pous/ra/"
license: "LGPL"
build: [
["coq_makefile" "-f" "Make" "-o" "Makefile"]
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"ocaml"
"coq" {>= "8.5" & < "8.5.1" & != "8.5.0~camlp4"}
]
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>" ]
synopsis: "Relation Algebra and KAT"
description:
"A modular library about relation algebra, from idempotent semirings to residuated Kleene allegories, including a decision tactic for Kleene algebra with Tests (KAT)."
url {
src: "https://github.com/damien-pous/relation-algebra/archive/v1.4.tar.gz"
checksum: "md5=131ddcaf000cb5ebab381037651e17a5"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-relation-algebra.1.4 coq.8.5.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 2h opam install -y --deps-only coq-relation-algebra.1.4 coq.8.5.0opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-relation-algebra.1.4 coq.8.5.0# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.12 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
coq 8.5.0 Formal proof management system.
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
[NOTE] Package coq is already installed (current version is 8.5.0).
The following actions will be performed:
- install coq-relation-algebra 1.4
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq-relation-algebra.1.4: http]
[coq-relation-algebra.1.4] downloaded from https://github.com/damien-pous/relation-algebra/archive/v1.4.tar.gz
Processing 1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/2: [coq-relation-algebra: coq_makefile Make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "coq_makefile" "-f" "Make" "-o" "Makefile" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-relation-algebra.1.4)
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.05.0/.opam-switch/build/coq-relation-algebra.1.4)
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamldep.opt -slash -I "." "kat_dec.mli" > "kat_dec.mli.d" || ( RV=$?; rm -f "kat_dec.mli.d"; exit ${RV} )
- "coqdep" -c -I "." -c "kat_reification.mllib" > "kat_reification.mllib.d" || ( RV=$?; rm -f "kat_reification.mllib.d"; exit ${RV} )
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamldep.opt -slash -I "." "kat_dec.ml" > "kat_dec.ml.d" || ( RV=$?; rm -f "kat_dec.ml.d"; exit ${RV} )
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamldep.opt -slash -I "." "ra_common.ml" > "ra_common.ml.d" || ( RV=$?; rm -f "ra_common.ml.d"; exit ${RV} )
- *** Warning: kat_reification.mllib already found in . (discarding ./kat_reification.mllib)
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/ocaml-base-compiler.4.05.0/bin/camlp5o -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/ -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/threads/ -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/pretyping" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/interp" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/printing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/intf" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/proofs" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tactics" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tools" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/toplevel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/stm" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/grammar" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/config" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/btauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/cc" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/derive" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/extraction" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/firstorder" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/fourier" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/funind" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/micromega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/nsatz" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/omega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/quote" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/romega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/rtauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/syntax" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "kat_reification.ml4" > "kat_reification.ml4.d" || ( RV=$?; rm -f "kat_reification.ml4.d"; exit ${RV} )
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/ocaml-base-compiler.4.05.0/bin/camlp5o -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/ -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/threads/ -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/pretyping" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/interp" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/printing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/intf" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/proofs" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tactics" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tools" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/toplevel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/stm" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/grammar" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/config" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/btauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/cc" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/derive" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/extraction" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/firstorder" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/fourier" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/funind" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/micromega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/nsatz" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/omega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/quote" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/romega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/rtauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/syntax" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_reification.ml4" > "ra_reification.ml4.d" || ( RV=$?; rm -f "ra_reification.ml4.d"; exit ${RV} )
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/ocaml-base-compiler.4.05.0/bin/camlp5o -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/ -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/threads/ -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/pretyping" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/interp" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/printing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/intf" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/proofs" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tactics" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tools" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/toplevel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/stm" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/grammar" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/config" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/btauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/cc" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/derive" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/extraction" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/firstorder" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/fourier" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/funind" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/micromega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/nsatz" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/omega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/quote" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib
[...] truncated
/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/pretyping" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/interp" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/printing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/intf" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/proofs" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tactics" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tools" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/toplevel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/stm" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/grammar" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/config" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/btauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/cc" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/derive" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/extraction" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/firstorder" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/fourier" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/funind" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/micromega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/nsatz" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/omega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/quote" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/romega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/rtauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/syntax" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/xml" -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/camlp5 -shared -o ra_reification.cmxs ra_reification.cmx
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamlopt.opt -rectypes -thread -I "." -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/pretyping" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/interp" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/printing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/intf" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/proofs" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tactics" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tools" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/toplevel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/stm" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/grammar" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/config" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/btauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/cc" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/derive" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/extraction" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/firstorder" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/fourier" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/funind" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/micromega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/nsatz" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/omega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/quote" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/romega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/rtauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/syntax" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/xml" -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/camlp5 -a -o kat_reification.cmxa kat_dec.cmx kat_reification.cmx
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamlopt.opt -rectypes -thread -I "." -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/pretyping" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/interp" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/printing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/intf" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/proofs" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tactics" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/tools" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/toplevel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/stm" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/grammar" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/config" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/btauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/cc" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/derive" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/extraction" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/firstorder" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/fourier" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/funind" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/micromega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/nsatz" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/omega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/quote" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/romega" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/rtauto" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/syntax" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq//plugins/xml" -I /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/camlp5 -linkall -shared -o kat_reification.cmxs kat_reification.cmxa
- "coqc" -q -R "." RelationAlgebra -I "." denum
- "coqc" -q -R "." RelationAlgebra -I "." pair
- "coqc" -q -R "." RelationAlgebra -I "." monoid
- "coqc" -q -R "." RelationAlgebra -I "." prop
- "coqc" -q -R "." RelationAlgebra -I "." lset
- "coqc" -q -R "." RelationAlgebra -I "." sups
- "coqc" -q -R "." RelationAlgebra -I "." lsyntax
- File "./monoid.v", line 515, characters 0-28:
- Error: while loading ./ra_fold.cmxs: interface mismatch on Ra_common
- make: *** [Makefile:456: monoid.vo] Error 1
[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.4 ===========================#
# context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-relation-algebra.1.4
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code 2
# env-file ~/.opam/log/coq-relation-algebra-15566-e4db2f.env
# output-file ~/.opam/log/coq-relation-algebra-15566-e4db2f.out
### output ###
# [...]
# /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamlopt.opt -rectypes -thread -I "." -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0[...]
# /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamlopt.opt -rectypes -thread -I "." -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/kernel" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/lib" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/library" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/parsing" -I "/home/bench/.opam/ocaml-base-compiler.4.05.0[...]
# "coqc" -q -R "." RelationAlgebra -I "." denum
# "coqc" -q -R "." RelationAlgebra -I "." pair
# "coqc" -q -R "." RelationAlgebra -I "." monoid
# "coqc" -q -R "." RelationAlgebra -I "." prop
# "coqc" -q -R "." RelationAlgebra -I "." lset
# "coqc" -q -R "." RelationAlgebra -I "." sups
# "coqc" -q -R "." RelationAlgebra -I "." lsyntax
# File "./monoid.v", line 515, characters 0-28:
# Error: while loading ./ra_fold.cmxs: interface mismatch on Ra_common
# make: *** [Makefile:456: monoid.vo] Error 1
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-relation-algebra 1.4
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-relation-algebra.1.4 coq.8.5.0' failed.
The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true