# 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 8.14.0 Formal proof management system
dune 3.7.0 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.8.14.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 4h opam install -y --deps-only coq-io-hello-world.1.2.0 coq.8.14.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-io-hello-world.1.2.0 coq.8.14.0Total: 5 M
../ocaml-base-compiler.4.07.1/bin/helloWorld../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/UnitTests.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Trace.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Evaluate.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Evaluate.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/Extraction.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/UnitTests.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Trace.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/System.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Run.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Etc.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/List.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Char.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Conversion.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Run.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Trim.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Comparison.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/UseCase.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/C.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/Extraction.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Exception.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Case.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/System.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/Sort.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/List.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Etc.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/C.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/List.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Trace.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/UnitTests.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/Sort.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/LString.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Evaluate.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/UseCase.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Char.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Conversion.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/Extraction.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Run.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Exception.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/System.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Comparison.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/C.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Bool.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Effect.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/List.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Char.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Trim.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/All.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Etc.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Conversion.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/List.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/UseCase.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Bool.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Comparison.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Exception.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/Sort.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Case.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Trim.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Effect.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/All.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/List.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/All.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Case.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Bool.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/All.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Effect.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/LString.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/All.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/All.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/LString.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/All.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/All.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/All.vopam remove -y coq-io-hello-world.1.2.0/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/FunctionNinjas/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/CUnit/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Run.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/UseCase.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Effect.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Exception.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/C.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Effect.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/List.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Evaluate.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Effect.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/UseCase.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/List.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/UseCase.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Evaluate.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/List.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Exception.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/C.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Trace.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Run.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Trace.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/C.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/System.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/System.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/System.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/Extraction.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/Extraction.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/System/Extraction.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Trace.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Evaluate.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Run.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Io/Exception.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ErrorHandlers/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/List.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/Sort.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/List.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/Sort.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/List.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/Sort.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListPlus/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/LString.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/UnitTests.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Trim.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Conversion.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Bool.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/All.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Char.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Case.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Case.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Comparison.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Etc.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Conversion.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/UnitTests.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Bool.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Etc.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Etc.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Char.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Char.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Trim.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Trim.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/UnitTests.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/All.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Comparison.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Bool.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Comparison.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Conversion.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/LString.vo/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/Case.v/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/All.glob/home/bench/.opam/ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ListString/LString.glob