# 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 dev Formal proof management system
dune 3.1.1 Fast, portable, and opinionated build system
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-config 1 OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler
ocamlfind 1.9.1 A library manager for OCaml
ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "dev@clarus.me"
homepage: "https://github.com/clarus/coq-hello-world"
dev-repo: "git+https://github.com/clarus/coq-hello-world.git"
bug-reports: "https://github.com/clarus/coq-hello-world/issues"
authors: ["Guillaume Claret"]
license: "MIT"
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
[make "-C" "extraction"]
]
install: [
["install" "-T" "extraction/main.native" "%{bin}%/helloWorld"]
]
depends: [
"coq" {build}
"coq-io" {>= "4.0.0" & build}
"coq-io-system" {build}
"coq-io-system-ocaml" {>= "2.3.0"}
]
tags: [
"date:2019-07-30"
"keyword:effects"
"keyword:extraction"
]
synopsis: "A Hello World program in Coq"
url {
src: "https://github.com/coq-io/hello-world/archive/1.2.0.tar.gz"
checksum: "sha512=00f1beee8dbb62b6b619d9942f6701ef557ce3de3568f324103c1073968a3f07b7d5fa797e9ca955ec7d7ac36db5e039ef29c5666bfa4a5fe755b03615dface1"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-io-hello-world.1.2.0 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 4h opam install -y --deps-only coq-io-hello-world.1.2.0 coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-io-hello-world.1.2.0 coq.dev# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
bigarray-compat 1.1.0 Compatibility library to use Stdlib.Bigarray when possible
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev Formal proof management system
coq-io-system-ocaml 2.3.1 Extraction to OCaml of system effects
cppo 1.6.8 Code preprocessor like cpp for OCaml
dune 2.6.2 Fast, portable, and opinionated build system
lwt 4.2.1-1 Promises and event-driven I/O
mmap 1.2.0 File mapping functionality
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-config 1 OCaml Switch Configuration
ocamlbuild 0.14.1 OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind 1.9.1 A library manager for OCaml
result 1.5 Compatibility Result module
seq base Compatibility package for OCaml's standard iterator type starting from 4.07.
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is dev).
The following actions will be performed:
- install coq-list-plus 1.1.0 [required by coq-list-string]
- install coq-io 4.0.0 [required by coq-io-hello-world]
- install coq-cunit 1.0.0 [required by coq-list-string]
- install coq-error-handlers 1.2.0 [required by coq-list-string]
- install coq-function-ninjas 1.0.0 [required by coq-io-system]
- install coq-list-string 2.1.2 [required by coq-io-system]
- install coq-io-system 2.4.1 [required by coq-io-hello-world]
- install coq-io-hello-world 1.2.0
===== 8 to install =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/8: [coq-cunit.1.0.0: http]
Processing 2/8: [coq-cunit.1.0.0: http] [coq-error-handlers.1.2.0: http]
Processing 3/8: [coq-cunit.1.0.0: http] [coq-error-handlers.1.2.0: http] [coq-function-ninjas.1.0.0: http]
[coq-cunit.1.0.0] downloaded from https://github.com/clarus/coq-cunit/archive/1.0.0.tar.gz
Processing 3/8: [coq-error-handlers.1.2.0: http] [coq-function-ninjas.1.0.0: http]
[coq-error-handlers.1.2.0] downloaded from https://github.com/clarus/coq-error-handlers/archive/1.2.0.tar.gz
Processing 3/8: [coq-function-ninjas.1.0.0: http]
[coq-function-ninjas.1.0.0] downloaded from https://github.com/clarus/coq-function-ninjas/archive/1.0.0.tar.gz
Processing 3/8:
Processing 4/8: [coq-io.4.0.0: http]
Processing 5/8: [coq-io.4.0.0: http] [coq-io-hello-world.1.2.0: http]
Processing 6/8: [coq-io.4.0.0: http] [coq-io-hello-world.1.2.0: http] [coq-io-system.2.4.1: http]
[coq-io.4.0.0] downloaded from https://github.com/coq-io/io/archive/4.0.0.tar.gz
Processing 6/8: [coq-io-hello-world.1.2.0: http] [coq-io-system.2.4.1: http]
[coq-io-hello-world.1.2.0] downloaded from https://github.com/coq-io/hello-world/archive/1.2.0.tar.gz
Processing 6/8: [coq-io-system.2.4.1: http]
[coq-io-system.2.4.1] downloaded from https://github.com/coq-io/system/archive/2.4.1.tar.gz
Processing 6/8:
Processing 7/8: [coq-list-plus.1.1.0: http]
Processing 8/8: [coq-list-plus.1.1.0: http] [coq-list-string.2.1.2: http]
[coq-list-plus.1.1.0] downloaded from https://github.com/clarus/coq-list-plus/archive/1.1.0.tar.gz
Processing 8/8: [coq-list-string.2.1.2: http]
[coq-list-string.2.1.2] downloaded from https://github.com/clarus/coq-list-string/archive/2.1.2.tar.gz
Processing 8/8:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/16: [coq-cunit: ./configure.sh]
Processing 2/16: [coq-cunit: ./configure.sh] [coq-error-handlers: ./configure.sh]
Processing 3/16: [coq-cunit: ./configure.sh] [coq-error-handlers: ./configure.sh] [coq-function-ninjas: ./configure.sh]
Processing 4/16: [coq-cunit: ./configure.sh] [coq-error-handlers: ./configure.sh] [coq-function-ninjas: ./configure.sh] [coq-io: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-cunit.1.0.0)
Processing 4/16: [coq-cunit: make] [coq-error-handlers: ./configure.sh] [coq-function-ninjas: ./configure.sh] [coq-io: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0)
Processing 4/16: [coq-cunit: make] [coq-error-handlers: make] [coq-function-ninjas: ./configure.sh] [coq-io: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-function-ninjas.1.0.0)
Processing 4/16: [coq-cunit: make] [coq-error-handlers: make] [coq-function-ninjas: make] [coq-io: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-io.4.0.0)
Processing 4/16: [coq-cunit: make] [coq-error-handlers: make] [coq-function-ninjas: make] [coq-io: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0)
- COQDEP VFILES
- COQC src/All.v
- COQDEP VFILES
- COQC src/All.v
-> compiled coq-error-handlers.1.2.0
Processing 4/16: [coq-cunit: make] [coq-function-ninjas: make] [coq-io: make]
Processing 5/16: [coq-cunit: make] [coq-function-ninjas: make] [coq-io: make] [coq-list-plus: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-function-ninjas.1.0.0)
- COQDEP VFILES
- COQC All.v
- COQDEP VFILES
- COQC All.v
-> compiled coq-function-ninjas.1.0.0
Processing 5/16: [coq-cunit: make] [coq-io: make] [coq-list-plus: ./configure.sh]
Processing 6/16: [coq-cunit: make] [coq-io: make] [coq-list-plus: ./configure.sh] [coq-error-handlers: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-cunit.1.0.0)
- COQDEP VFILES
- COQC src/All.v
- COQDEP VFILES
- COQC src/All.v
-> compiled coq-cunit.1.0.0
Processing 6/16: [coq-io: make] [coq-list-plus: ./configure.sh] [coq-error-handlers: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-plus.1.1.0)
Processing 6/16: [coq-io: make] [coq-list-plus: make] [coq-error-handlers: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0)
- INSTALL src/All.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ErrorHandlers/
- INSTALL src/All.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ErrorHandlers/
- INSTALL src/All.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ErrorHandlers/
- # findlib needs the package to not be installed, so we remove it before
- # installing it
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0'
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0'
- INSTALL src/All.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ErrorHandlers/
- INSTALL src/All.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ErrorHandlers/
- INSTALL src/All.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ErrorHandlers/
- # findlib needs the package to not be installed, so we remove it before
- # installing it
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0'
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-error-handlers.1.2.0'
-> installed coq-error-handlers.1.2.0
Processing 6/16: [coq-io: make] [coq-list-plus: make]
Processing 7/16: [coq-io: make] [coq-list-plus: make] [coq-cunit: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-io.4.0.0)
- COQDEP VFILES
- COQC src/Effect.v
- COQC src/C.v
- COQC src/Run.v
- COQC src/Evaluate.v
- COQC src/List.v
- COQC src/Trace.v
- COQC src/UseCase.v
- File "./src/List.v", line 42, characters 9-10:
- Error: Syntax error: [identref] expected after 'let!' (in [binder_constr]).
-
- make[1]: *** [Makefile:790: src/List.vo] Error 1
- make[1]: *** Waiting for unfinished jobs....
- make: *** [Makefile:408: all] Error 2
- COQDEP VFILES
- COQC src/Effect.v
- COQC src/C.v
- COQC src/Run.v
- COQC src/Evaluate.v
- COQC src/List.v
- COQC src/Trace.v
- COQC src/UseCase.v
- File "./src/List.v", line 42, characters 9-10:
- Error: Syntax error: [identref] expected after 'let!' (in [binder_constr]).
-
- make[1]: *** [Makefile:790: src/List.vo] Error 1
- make[1]: *** Waiting for unfinished jobs....
- make: *** [Makefile:408: all] Error 2
[ERROR] The compilation of coq-io failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4".
Processing 7/16: [coq-list-plus: make] [coq-cunit: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-plus.1.1.0)
- COQDEP VFILES
- COQC src/List.v
- COQC src/Sort.v
- File "./src/Sort.v", line 46, characters 2-39:
- Warning: Use of “Require” inside a module is fragile. It is not recommended
- to use this functionality in finished proof scripts.
- [require-in-module,fragile]
- COQC src/All.v
- COQDEP VFILES
- COQC src/List.v
- COQC src/Sort.v
- File "./src/Sort.v", line 46, characters 2-39:
- Warning: Use of “Require” inside a module is fragile. It is not recommended
- to use this functionality in finished proof scripts.
- [require-in-module,fragile]
- COQC src/All.v
-> compiled coq-list-plus.1.1.0
Processing 7/16: [coq-cunit: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-cunit.1.0.0)
- INSTALL src/All.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/CUnit/
- INSTALL src/All.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/CUnit/
- INSTALL src/All.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/CUnit/
- # findlib needs the package to not be installed, so we remove it before
- # installing it
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-cunit.1.0.0'
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-cunit.1.0.0'
-> installed coq-cunit.1.0.0
Processing 8/16: [coq-function-ninjas: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-function-ninjas.1.0.0)
- INSTALL All.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/FunctionNinjas/
- INSTALL All.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/FunctionNinjas/
- INSTALL All.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/FunctionNinjas/
- # findlib needs the package to not be installed, so we remove it before
- # installing it
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-function-ninjas.1.0.0'
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-function-ninjas.1.0.0'
-> installed coq-function-ninjas.1.0.0
Processing 10/16: [coq-list-plus: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-plus.1.1.0)
- INSTALL src/All.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/List.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/Sort.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/All.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/List.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/Sort.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/All.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/List.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- INSTALL src/Sort.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListPlus/
- # findlib needs the package to not be installed, so we remove it before
- # installing it
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-plus.1.1.0'
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-plus.1.1.0'
-> installed coq-list-plus.1.1.0
Processing 11/16: [coq-list-string: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-string.2.1.2)
Processing 11/16: [coq-list-string: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-string.2.1.2)
- COQDEP VFILES
- COQC src/Bool.v
- COQC src/LString.v
- COQC src/Char.v
- COQC src/Case.v
- COQC src/Comparison.v
- COQC src/Conversion.v
- COQC src/Trim.v
- COQC src/Etc.v
- COQC src/All.v
- COQC src/UnitTests.v
-> compiled coq-list-string.2.1.2
Processing 12/16: [coq-list-string: make install]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-string.2.1.2)
- INSTALL src/All.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Bool.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Case.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Char.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Comparison.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Conversion.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Etc.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/LString.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Trim.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/UnitTests.vo /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/All.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Bool.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Case.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Char.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Comparison.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Conversion.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Etc.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/LString.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Trim.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/UnitTests.v /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/All.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Bool.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Case.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Char.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Comparison.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Conversion.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Etc.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/LString.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/Trim.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- INSTALL src/UnitTests.glob /home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq//user-contrib/ListString/
- # findlib needs the package to not be installed, so we remove it before
- # installing it
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-string.2.1.2'
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-list-string.2.1.2'
-> installed coq-list-string.2.1.2
#=== ERROR while compiling coq-io.4.0.0 =======================================#
# context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.07.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-io.4.0.0
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code 2
# env-file ~/.opam/log/coq-io-27788-835ba5.env
# output-file ~/.opam/log/coq-io-27788-835ba5.out
### output ###
# [...]
# COQC src/C.v
# COQC src/Run.v
# COQC src/Evaluate.v
# COQC src/List.v
# COQC src/Trace.v
# COQC src/UseCase.v
# File "./src/List.v", line 42, characters 9-10:
# Error: Syntax error: [identref] expected after 'let!' (in [binder_constr]).
#
# make[1]: *** [Makefile:790: src/List.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:408: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions were aborted
| - install coq-io-hello-world 1.2.0
| - install coq-io-system 2.4.1
+-
+- The following actions failed
| - build coq-io 4.0.0
+-
+- The following changes have been performed (the rest was aborted)
| - install coq-cunit 1.0.0
| - install coq-error-handlers 1.2.0
| - install coq-function-ninjas 1.0.0
| - install coq-list-plus 1.1.0
| - install coq-list-string 2.1.2
+-
# Run eval $(opam env) to update the current shell environment
The former state can be restored with:
opam switch import "/home/bench/.opam/ocaml-base-compiler.4.07.1/.opam-switch/backup/state-20220424135408.export"
'opam install -y -v coq-io-hello-world.1.2.0 coq.dev' failed.
No files were installed.
true