# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.18.0 The Coq Proof Assistant
coq-core 8.18.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.18.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.18.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 5.0.0 The OCaml compiler (virtual package)
ocaml-base-compiler 5.0.0 Official release 5.0.0
ocaml-config 3 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "thery@sophia.inria.fr"
homepage: "https://github.com/thery/coqprime"
bug-reports: "https://github.com/thery/coqprime/issues"
dev-repo: "git+https://github.com/thery/coqprime.git"
license: "LGPL-2.1-only"
authors: ["Laurent Théry"]
build: [
# cd to a subfolder in opam is tricky, so just move gencertif to the root folder
[ "find" "gencertif" "-type" "f" "-exec" "mv" "{}" "." ";" ]
[ "autoreconf" "-i" "-s" ]
[ "./configure" "--prefix" prefix
# Optiosn for finding opam local gmp-ecm
"CPPFLAGS=-I%{prefix}%/include"
"LDFLAGS=-L%{lib}%"
# Options for homebrew on Intel silicon (overwriting the above)
"CPPFLAGS=-I%{prefix}%/include -I/opt/local/include" { os-distribution = "macports" & os = "macos" }
"LDFLAGS=-L%{lib}% -L/opt/local/lib" { os-distribution = "macports" & os = "macos" }
# Options for homebrew on Apple silicon (overwriting the above)
"CPPFLAGS=-I%{prefix}%/include -I/opt/homebrew/include" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
"LDFLAGS=-L%{lib}% -L/opt/homebrew/lib" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
# Options for Windows cygwin
"--build=%{arch}%-pc-cygwin" { os = "win32" & os-distribution = "cygwinports" }
"--host=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
"--target=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
]
[ make "-j" "%{jobs}%" ]
]
install: [
[make "install"]
]
depends: [
"ocaml"
"num"
"conf-gmp"
"gmp-ecm"
]
synopsis: "Certificate generator for prime numbers in Coq"
url {
src: "https://github.com/thery/coqprime/archive/v8.14.1.tar.gz"
checksum: "sha512=cd5d4ff31a2ac3039e5c49e9da627a0f4722ff7d9269bbe521531a162c0f0dfc190779eeafa8749d563c65dc787d17e9193fdd0664b273d01220272f3abb17ca"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-coqprime-generator.1.1.1 coq.8.18.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-coqprime-generator.1.1.1 coq.8.18.0opam list; echo; timeout 4h opam install -y -v coq-coqprime-generator.1.1.1 coq.8.18.0# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
base-threads base
base-unix base
conf-autoconf 0.1 Virtual package relying on autoconf installation
conf-automake 1 Virtual package relying on GNU automake
conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++)
conf-gmp 4 Virtual package relying on a GMP lib system installation
conf-libtool 1 Virtual package relying on libtool installation
conf-which 1 Virtual package relying on which
coq 8.18.0 The Coq Proof Assistant
coq-core 8.18.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.18.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.18.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
gmp-ecm 7.0.3 GMP-ECM library for the Elliptic Curve Method (ECM) for integer factorization
num 1.5 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 5.0.0 The OCaml compiler (virtual package)
ocaml-base-compiler 5.0.0 Official release 5.0.0
ocaml-config 3 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.18.0).
The following actions will be performed:
- install coq-coqprime-generator 1.1.1
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/3: [coq-coqprime-generator.1.1.1: http]
Processing 1/3:
-> retrieved coq-coqprime-generator.1.1.1 (https://github.com/thery/coqprime/archive/v8.14.1.tar.gz)
Processing 2/3: [coq-coqprime-generator: find gencertif]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "find" "gencertif" "-type" "f" "-exec" "mv" "{}" "." ";" (CWD=/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-coqprime-generator.1.1.1)
Processing 2/3: [coq-coqprime-generator: autoreconf]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "autoreconf" "-i" "-s" (CWD=/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-coqprime-generator.1.1.1)
Processing 2/3: [coq-coqprime-generator: ./configure]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "--prefix" "/home/bench/.opam/ocaml-base-compiler.5.0.0" "CPPFLAGS=-I/home/bench/.opam/ocaml-base-compiler.5.0.0/include" "LDFLAGS=-L/home/bench/.opam/ocaml-base-compiler.5.0.0/lib" (CWD=/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-coqprime-generator.1.1.1)
- checking for gcc... gcc
- checking whether the C compiler works... yes
- checking for C compiler default output file name... a.out
- checking for suffix of executables...
- checking whether we are cross compiling... no
- checking for suffix of object files... o
- checking whether the compiler supports GNU C... yes
- checking whether gcc accepts -g... yes
- checking for gcc option to enable C11 features... none needed
- checking for log in -lm... yes
- checking for __gmpz_init in -lgmp... yes
- checking for ecm_init in -lecm...
- yes
- configure: creating ./config.status
- config.status: creating Makefile
Processing 2/3: [coq-coqprime-generator: make 4]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j" "4" (CWD=/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-coqprime-generator.1.1.1)
- gcc -I/home/bench/.opam/ocaml-base-compiler.5.0.0/include -g -O2 -I -I -Wall -pedantic -c certif.c
- gcc -I/home/bench/.opam/ocaml-base-compiler.5.0.0/include -g -O2 -I -I -Wall -pedantic -c factorize.c
- gcc -I/home/bench/.opam/ocaml-base-compiler.5.0.0/include -g -O2 -I -I -Wall -pedantic -c pocklington.c
- gcc -I/home/bench/.opam/ocaml-base-compiler.5.0.0/include -g -O2 -I -I -Wall -pedantic -c firstprimes.c
- pocklington.c: In function 'main':
- pocklington.c:255:3: warning: 'p' may be used uninitialized in this function [-Wmaybe-uninitialized]
- 255 | print_file(filename, lemmaname, p, lc);
- | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- pocklington.c:255:3: warning: 'filename' may be used uninitialized in this function [-Wmaybe-uninitialized]
- ocamlc -o o2v nums.cma str.cma parser.ml
- File "_none_", line 1:
- Alert ocaml_deprecated_auto_include:
- OCaml's lib directory layout changed in 5.0. The str subdirectory has been
- automatically added to the search path, but you should add -I +str to the
- command-line to silence this alert (e.g. by adding str to the list of
- libraries in your dune file, or adding use_str to your _tags file for
- ocamlbuild, or using -package str for ocamlfind).
- File "parser.ml", line 3, characters 5-12:
- 3 | open Big_int
- ^^^^^^^
- Error: Unbound module Big_int
- make: *** [Makefile:27: o2v] Error 2
- make: *** Waiting for unfinished jobs....
[ERROR] The compilation of coq-coqprime-generator.1.1.1 failed at "make -j 4".
#=== ERROR while compiling coq-coqprime-generator.1.1.1 =======================#
# context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.0.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-coqprime-generator.1.1.1
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j 4
# exit-code 2
# env-file ~/.opam/log/coq-coqprime-generator-2028-196226.env
# output-file ~/.opam/log/coq-coqprime-generator-2028-196226.out
### output ###
# [...]
# Alert ocaml_deprecated_auto_include:
# OCaml's lib directory layout changed in 5.0. The str subdirectory has been
# automatically added to the search path, but you should add -I +str to the
# command-line to silence this alert (e.g. by adding str to the list of
# libraries in your dune file, or adding use_str to your _tags file for
# ocamlbuild, or using -package str for ocamlfind).
# File "parser.ml", line 3, characters 5-12:
# 3 | open Big_int
# ^^^^^^^
# Error: Unbound module Big_int
# make: *** [Makefile:27: o2v] Error 2
# make: *** Waiting for unfinished jobs....
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-coqprime-generator 1.1.1
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-coqprime-generator.1.1.1 coq.8.18.0' failed.
No files were installed.
true