# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
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 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 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: "palmskog@gmail.com"
homepage: "https://github.com/coq-community/gaia"
dev-repo: "git+https://github.com/coq-community/gaia.git"
bug-reports: "https://github.com/coq-community/gaia/issues"
license: "MIT"
synopsis: "Implementation of the sets of numbers Z, Q, and R following Bourbaki's Elements of Mathematics in Coq"
description: """
Implementation of the sets of numbers Z, Q, and R following N. Bourbaki's book series
Elements of Mathematics in Coq using the Mathematical Components library."""
build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "2.8"}
"coq" {>= "8.16" & < "8.19"}
"coq-mathcomp-ssreflect" {>= "2.0"}
"coq-mathcomp-algebra"
"coq-gaia-theory-of-sets" {= version}
"coq-gaia-ordinals" {= version}
]
conflicts: [
"coq-gaia"
]
tags: [
"category:Mathematics/Arithmetic and Number Theory/Number theory"
"keyword:integers"
"keyword:rational numbers"
"keyword:real numbers"
"logpath:gaia.numbers"
"date:2023-08-05"
]
authors: [
"Joseฬ Grimm"
"Alban Quadrat"
]
url {
src: "https://github.com/coq-community/gaia/archive/v2.0.tar.gz"
checksum: "sha512=37551367ae132870235e2dfd433d420e814933c642068f4d1e0bc37ed3d001e1536ca24e176d490f4c3e05567bc99e426cd48e0a0b989bdff38a371a532f3328"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-gaia-numbers.2.0 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-gaia-numbers.2.0 coq.8.18.0# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
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 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 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
The following actions will be performed:
- install cppo 1.6.9
- install ppx_derivers 1.2.1
- install menhirCST 20231231
- install cmdliner 1.2.0
- install menhirSdk 20231231
- install easy-format 1.3.4
- install menhirLib 20231231
- install result 1.5
- install seq base
- install ocaml-compiler-libs v0.12.4
- install camlp-streams 5.0.1
- install sexplib0 v0.16.0
- install stdlib-shims 0.3.0
- install menhir 20231231
- install yojson 2.1.2
- install re 1.11.0
- install biniou 1.2.2
- install ppxlib 0.31.0
- install atd 2.15.0
- install atdgen-runtime 2.15.0
- install ppx_deriving 5.2.1
- install atdts 2.15.0
- install atdgen 2.15.0
- install elpi 1.18.1
- install coq-elpi 2.0.0
- install coq-hierarchy-builder 1.7.0
- install coq-mathcomp-ssreflect 2.2.0
- install coq-mathcomp-fingroup 2.2.0
- install coq-gaia-theory-of-sets 2.0
- install coq-gaia-schutte 2.0
- install coq-mathcomp-algebra 2.2.0
- install coq-gaia-ordinals 2.0
===== 32 to install =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[atd.2.15.0] downloaded from cache at https://opam.ocaml.org/cache
[atdts.2.15.0] found in cache
[atdgen.2.15.0] downloaded from cache at https://opam.ocaml.org/cache
[biniou.1.2.2] downloaded from cache at https://opam.ocaml.org/cache
[camlp-streams.5.0.1] downloaded from cache at https://opam.ocaml.org/cache
[cmdliner.1.2.0] downloaded from cache at https://opam.ocaml.org/cache
[atdgen-runtime.2.15.0] downloaded from cache at https://opam.ocaml.org/cache
[coq-elpi.2.0.0] downloaded from https://github.com/LPCIC/coq-elpi/releases/download/v2.0.0/coq-elpi-2.0.0.tar.gz
[coq-gaia-ordinals.2.0] downloaded from https://github.com/coq-community/gaia/archive/v2.0.tar.gz
[coq-gaia-schutte.2.0] found in cache
[coq-gaia-theory-of-sets.2.0] found in cache
[coq-hierarchy-builder.1.7.0] downloaded from https://github.com/math-comp/hierarchy-builder/releases/download/v1.7.0/hierarchy-builder-1.7.0.tar.gz
[coq-mathcomp-algebra.2.2.0] downloaded from https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz
[coq-mathcomp-fingroup.2.2.0] downloaded from https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz
[cppo.1.6.9] downloaded from cache at https://opam.ocaml.org/cache
[easy-format.1.3.4] downloaded from cache at https://opam.ocaml.org/cache
[coq-mathcomp-ssreflect.2.2.0] downloaded from https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz
[elpi.1.18.1] downloaded from cache at https://opam.ocaml.org/cache
[menhir.20231231] downloaded from cache at https://opam.ocaml.org/cache
[menhirCST.20231231] found in cache
[menhirLib.20231231] found in cache
[menhirSdk.20231231] found in cache
[ocaml-compiler-libs.v0.12.4] downloaded from cache at https://opam.ocaml.org/cache
[ppx_derivers.1.2.1] downloaded from cache at https://opam.ocaml.org/cache
[ppx_deriving.5.2.1] downloaded from cache at https://opam.ocaml.org/cache
[result.1.5] downloaded from cache at https://opam.ocaml.org/cache
[re.1.11.0] downloaded from cache at https://opam.ocaml.org/cache
[ppxlib.0.31.0] downloaded from cache at https://opam.ocaml.org/cache
[sexplib0.v0.16.0] downloaded from cache at https://opam.ocaml.org/cache
[stdlib-shims.0.3.0] downloaded from cache at https://opam.ocaml.org/cache
[yojson.2.1.2] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed camlp-streams.5.0.1
-> installed cppo.1.6.9
-> installed easy-format.1.3.4
-> installed cmdliner.1.2.0
-> installed menhirCST.20231231
-> installed menhirLib.20231231
-> installed menhirSdk.20231231
-> installed ocaml-compiler-libs.v0.12.4
-> installed ppx_derivers.1.2.1
-> installed result.1.5
-> installed seq.base
-> installed biniou.1.2.2
-> installed sexplib0.v0.16.0
-> installed stdlib-shims.0.3.0
-> installed re.1.11.0
-> installed yojson.2.1.2
-> installed atdgen-runtime.2.15.0
-> installed menhir.20231231
-> installed atd.2.15.0
-> installed ppxlib.0.31.0
-> installed atdgen.2.15.0
-> installed atdts.2.15.0
-> installed ppx_deriving.5.2.1
-> installed elpi.1.18.1
-> installed coq-elpi.2.0.0
-> installed coq-hierarchy-builder.1.7.0
-> installed coq-mathcomp-ssreflect.2.2.0
[ERROR] The compilation of coq-gaia-theory-of-sets failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-gaia-theory-of-sets -j 4".
-> installed coq-gaia-schutte.2.0
-> installed coq-mathcomp-fingroup.2.2.0
-> installed coq-mathcomp-algebra.2.2.0
#=== ERROR while compiling coq-gaia-theory-of-sets.2.0 ========================#
# context 2.0.10 | linux/x86_64 | ocaml-base-compiler.4.14.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/coq-gaia-theory-of-sets.2.0
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-gaia-theory-of-sets -j 4
# exit-code 1
# env-file ~/.opam/log/coq-gaia-theory-of-sets-23243-b39dcc.env
# output-file ~/.opam/log/coq-gaia-theory-of-sets-23243-b39dcc.out
### output ###
# Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
# 3.8 and will be removed in an upcoming Dune version.
# Hint: To disable this warning, add the following to your dune-project file:
# (warnings (deprecated_coq_lang_lt_08 disabled))
# (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.14.0/bin/coqc -q -w -notation-overridden -w -notation-incompatible-format -w -ambiguous-paths -w -deprecated-hint-without-locality -w -deprecated-ident-entry -w -deprecated-hint-rewrite-without-locality -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -I /home/bench/.opam/ocaml-base-compi[...]
# File "./theories/sets/sset1.v", line 2128, characters 19-26:
# Error: Unknown interpretation for notation "_ =1g _".
#
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-gaia-theory-of-sets 2.0
+-
+- The following changes have been performed (the rest was aborted)
| - install atd 2.15.0
| - install atdgen 2.15.0
| - install atdgen-runtime 2.15.0
| - install atdts 2.15.0
| - install biniou 1.2.2
| - install camlp-streams 5.0.1
| - install cmdliner 1.2.0
| - install coq-elpi 2.0.0
| - install coq-gaia-schutte 2.0
| - install coq-hierarchy-builder 1.7.0
| - install coq-mathcomp-algebra 2.2.0
| - install coq-mathcomp-fingroup 2.2.0
| - install coq-mathcomp-ssreflect 2.2.0
| - install cppo 1.6.9
| - install easy-format 1.3.4
| - install elpi 1.18.1
| - install menhir 20231231
| - install menhirCST 20231231
| - install menhirLib 20231231
| - install menhirSdk 20231231
| - install ocaml-compiler-libs v0.12.4
| - install ppx_derivers 1.2.1
| - install ppx_deriving 5.2.1
| - install ppxlib 0.31.0
| - install re 1.11.0
| - install result 1.5
| - install seq base
| - install sexplib0 v0.16.0
| - install stdlib-shims 0.3.0
| - install yojson 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.14.0/.opam-switch/backup/state-20240126095319.export"
trueNo files were installed.
true