« Up

relation-algebra 1.4 Error

(2020-06-25 03:38:52 UTC)

Context

# 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"
}

Lint

Command
true
Return code
0

Dry install

Dry install with the current Coq version:

Command
opam install -y --show-action coq-relation-algebra.1.4 coq.8.5.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-relation-algebra.1.4 coq.8.5.0
Return code
0
Duration
4 s

Install

Command
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-relation-algebra.1.4 coq.8.5.0
Return code
7936
Duration
31 s
Output
# 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)

Installation size

No files were installed.

Uninstall

Command
true
Return code
0
Missing removes
none
Wrong removes
none