# 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.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.8.2 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
ocamlfind 1.9.6 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "dev@clarus.me"
homepage: "https://github.com/clarus/coq-of-ocaml"
dev-repo: "git+https://github.com/clarus/coq-of-ocaml.git"
bug-reports: "https://github.com/clarus/coq-of-ocaml/issues"
authors: ["Guillaume Claret"]
license: "MIT"
build: [
["sh" "-c" "cd OCaml && ./configure.sh"]
[make "-C" "OCaml" "-j%{jobs}%"]
[make "-j%{jobs}%"]
]
install: [make "-C" "OCaml" "install"]
depends: [
"conf-ruby" {build}
"coq" {>= "8.5" & < "8.14~"}
"ocaml" {>= "4.05.0" & < "4.06.0"}
"ocamlbuild" {build}
"smart-print"
"yojson"
]
tags: [
"date:2015-08-31"
"keyword:compilation"
"keyword:OCaml"
]
synopsis: "Compile OCaml to Coq"
extra-files: ["coq-of-ocaml.install" "md5=aaa1f52ec40bedefd2674f46a44cd578"]
url {
src: "https://github.com/clarus/coq-of-ocaml/archive/1.2.1.tar.gz"
checksum: "md5=e8cb5565b8ce622d2afa5bcc59873ad2"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-of-ocaml.1.2.1 coq.8.8.2Dry 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-of-ocaml.1.2.1 coq.8.8.2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-of-ocaml.1.2.1 coq.8.8.2# 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.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl conf-ruby 1.0.0 Virtual package relying on Ruby coq 8.8.2 Formal proof management system cppo 1.6.9 Code preprocessor like cpp for OCaml dune 3.7.1 Fast, portable, and opinionated build 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 ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlbuild 0.14.2 OCamlbuild is a build system with builtin rules to easily build most OCaml projects ocamlfind 1.9.1 A library manager for OCaml ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind seq 0.3.1 Compatibility package for OCaml's standard iterator type starting from 4.07 smart-print 0.3.0 A pretty-printing library in OCaml yojson 2.0.2 Yojson is an optimized parsing and printing library for the JSON format [NOTE] Package coq is already installed (current version is 8.8.2). The following actions will be performed: - install coq-of-ocaml 1.2.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-of-ocaml.1.2.1: http] [coq-of-ocaml.1.2.1] downloaded from https://github.com/clarus/coq-of-ocaml/archive/1.2.1.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-of-ocaml: sh] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "sh" "-c" "cd OCaml && ./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-of-ocaml.1.2.1) Processing 1/2: [coq-of-ocaml: make OCaml] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-C" "OCaml" "-j7" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-of-ocaml.1.2.1) - make: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-of-ocaml.1.2.1/OCaml' - COQDEP VFILES - COQC Libraries.v - COQC Effect.v - COQC Basics.v - COQC List.v - COQC OCaml.v - make: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-of-ocaml.1.2.1/OCaml' Processing 1/2: [coq-of-ocaml: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j7" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-of-ocaml.1.2.1) - ocamlbuild src/coqOfOCaml.native -lflags -I,+compiler-libs,ocamlcommon.cmxa -use-ocamlfind -package smart_print,compiler-libs,yojson,str - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/coqOfOCaml.ml > src/coqOfOCaml.ml.depends - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/effect.ml > src/effect.ml.depends - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/boundName.ml > src/boundName.ml.depends - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/name.ml > src/name.ml.depends - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/error.ml > src/error.ml.depends - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/loc.ml > src/loc.ml.depends - ocamlfind ocamlc -c -package smart_print,compiler-libs,yojson,str -I src -o src/loc.cmo src/loc.ml - + ocamlfind ocamlc -c -package smart_print,compiler-libs,yojson,str -I src -o src/loc.cmo src/loc.ml - findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml, /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/compiler-libs - ocamlfind ocamlc -c -package smart_print,compiler-libs,yojson,str -I src -o src/error.cmo src/error.ml - + ocamlfind ocamlc -c -package smart_print,compiler-libs,yojson,str -I src -o src/error.cmo src/error.ml - findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml, /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/compiler-libs - ocamlfind ocamldep -package smart_print,compiler-libs,yojson,str -modules src/pathName.ml > src/pathName.ml.depends - ocamlfind ocamlc -c -package smart_print,compiler-libs,yojson,str -I src -o src/name.cmo src/name.ml - + ocamlfind ocamlc -c -package smart_print,compiler-libs,yojson,str -I src -o src/name.cmo src/name.ml - findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml, /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/compiler-libs - File "src/name.ml", line 83, characters 22-26: - Error: Unbound type constructor json - Command exited with code 2. - Hint: Recursive traversal of subdirectories was not enabled for this build, - as the working directory does not look like an ocamlbuild project (no - '_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories, - you should add the option "-r" or create an empty '_tags' file. - - To enable recursive traversal for some subdirectories only, you can use the - following '_tags' file: - - true: -traverse - <dir1> or <dir2>: traverse - - make: *** [Makefile:6: default] Error 10 [ERROR] The compilation of coq-of-ocaml failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j7". #=== ERROR while compiling coq-of-ocaml.1.2.1 =================================# # context 2.0.1 | 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-of-ocaml.1.2.1 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j7 # exit-code 2 # env-file ~/.opam/log/coq-of-ocaml-20580-335865.env # output-file ~/.opam/log/coq-of-ocaml-20580-335865.out ### output ### # [...] # Hint: Recursive traversal of subdirectories was not enabled for this build, # as the working directory does not look like an ocamlbuild project (no # '_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories, # you should add the option "-r" or create an empty '_tags' file. # # To enable recursive traversal for some subdirectories only, you can use the # following '_tags' file: # # true: -traverse # <dir1> or <dir2>: traverse # # make: *** [Makefile:6: default] Error 10 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-of-ocaml 1.2.1 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-of-ocaml.1.2.1 coq.8.8.2' failed.
No files were installed.
true