ยซ Up

gaia-ordinals 2.0 Error with dependencies ๐Ÿš’

Context

# 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.17.0      The Coq Proof Assistant
coq-core              8.17.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.17.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.17.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: "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 and properties of ordinals in Coq using Mathematical Components"
description: """
Implementation and properties of ordinals and cardinals 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-gaia-theory-of-sets" {= version}
  "coq-gaia-schutte" {= version}
]
conflicts: [
  "coq-gaia"
]
tags: [
  "category:Mathematics/Logic/Set theory"
  "category:Mathematics/Arithmetic and Number Theory/Number theory"
  "keyword:ordered sets"
  "keyword:ordinal arithmetic"
  "keyword:ordinal numbers"
  "keyword:cardinal numbers"
  "logpath:gaia.ordinals"
  "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"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-gaia-ordinals.2.0 coq.8.17.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; timeout 4h opam install -y --deps-only coq-gaia-ordinals.2.0 coq.8.17.0
Return code
7936
Duration
10 m 0 s
Output
# 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.17.0      The Coq Proof Assistant
coq-core              8.17.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.17.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.17.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
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.17.4
  - install coq-elpi                1.18.0
  - install coq-hierarchy-builder   1.6.0
  - install coq-mathcomp-ssreflect  2.2.0
  - install coq-gaia-theory-of-sets 2.0
  - install coq-gaia-schutte        2.0
===== 29 to install =====
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved atd.2.15.0  (https://opam.ocaml.org/cache)
-> retrieved atdts.2.15.0  (cached)
-> retrieved biniou.1.2.2  (https://opam.ocaml.org/cache)
-> retrieved atdgen.2.15.0  (https://opam.ocaml.org/cache)
-> retrieved camlp-streams.5.0.1  (https://opam.ocaml.org/cache)
-> retrieved atdgen-runtime.2.15.0  (https://opam.ocaml.org/cache)
-> retrieved cmdliner.1.2.0  (https://opam.ocaml.org/cache)
-> retrieved coq-elpi.1.18.0  (https://github.com/LPCIC/coq-elpi/releases/download/v1.18.0/coq-elpi-1.18.0.tar.gz)
-> retrieved coq-gaia-schutte.2.0  (https://github.com/coq-community/gaia/archive/v2.0.tar.gz)
-> installed camlp-streams.5.0.1
-> retrieved coq-hierarchy-builder.1.6.0  (https://github.com/math-comp/hierarchy-builder/releases/download/v1.6.0/hierarchy-builder-1.6.0.tar.gz)
-> retrieved coq-gaia-theory-of-sets.2.0  (https://github.com/coq-community/gaia/archive/v2.0.tar.gz)
-> retrieved cppo.1.6.9  (https://opam.ocaml.org/cache)
-> retrieved easy-format.1.3.4  (https://opam.ocaml.org/cache)
-> installed cppo.1.6.9
-> installed easy-format.1.3.4
-> retrieved coq-mathcomp-ssreflect.2.2.0  (https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz)
-> retrieved menhir.20231231  (https://opam.ocaml.org/cache)
-> retrieved menhirCST.20231231  (cached)
-> retrieved menhirLib.20231231  (cached)
-> retrieved menhirSdk.20231231  (cached)
-> retrieved ocaml-compiler-libs.v0.12.4  (https://opam.ocaml.org/cache)
-> retrieved ppx_derivers.1.2.1  (https://opam.ocaml.org/cache)
-> retrieved ppx_deriving.5.2.1  (https://opam.ocaml.org/cache)
-> installed menhirCST.20231231
-> retrieved elpi.1.17.4  (https://opam.ocaml.org/cache)
-> installed biniou.1.2.2
-> retrieved ppxlib.0.31.0  (https://opam.ocaml.org/cache)
-> retrieved re.1.11.0  (https://opam.ocaml.org/cache)
-> retrieved result.1.5  (https://opam.ocaml.org/cache)
-> retrieved stdlib-shims.0.3.0  (https://opam.ocaml.org/cache)
-> retrieved sexplib0.v0.16.0  (https://opam.ocaml.org/cache)
-> retrieved yojson.2.1.2  (https://opam.ocaml.org/cache)
-> installed cmdliner.1.2.0
-> installed menhirSdk.20231231
-> installed ppx_derivers.1.2.1
-> installed seq.base
-> installed menhirLib.20231231
-> installed result.1.5
-> installed ocaml-compiler-libs.v0.12.4
-> 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 ppxlib.0.31.0
-> installed menhir.20231231
-> installed ppx_deriving.5.2.1
-> installed atd.2.15.0
-> installed atdts.2.15.0
-> installed atdgen.2.15.0
-> installed elpi.1.17.4
-> installed coq-elpi.1.18.0
-> installed coq-hierarchy-builder.1.6.0
-> installed coq-mathcomp-ssreflect.2.2.0
[ERROR] The compilation of coq-gaia-theory-of-sets.2.0 failed at "dune build -p coq-gaia-theory-of-sets -j 4".
-> installed coq-gaia-schutte.2.0
#=== ERROR while compiling coq-gaia-theory-of-sets.2.0 ========================#
# 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-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-13119-14e4f6.env
# output-file          ~/.opam/log/coq-gaia-theory-of-sets-13119-14e4f6.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.5.0.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-compil[...]
# 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
| - 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               1.18.0
| - install coq-gaia-schutte       2.0
| - install coq-hierarchy-builder  1.6.0
| - install coq-mathcomp-ssreflect 2.2.0
| - install cppo                   1.6.9
| - install easy-format            1.3.4
| - install elpi                   1.17.4
| - 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:
    /usr/local/bin/opam switch import "/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/backup/state-20240129082653.export"

Install ๐Ÿš€

Command
true
Return code
0
Duration
0 s

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none