ยซ Up

mathcomp-finmap 2.1.0 Error with dependencies ๐Ÿš’

Context

# opam file:
opam-version: "2.0"
maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
homepage: "https://github.com/math-comp/finmap"
dev-repo: "git+https://github.com/math-comp/finmap.git"
bug-reports: "https://github.com/math-comp/finmap/issues"
license: "CECILL-B"
synopsis: "Finite sets, finite maps, finitely supported functions"
description: """
This library is an extension of mathematical component in order to
support finite sets and finite maps on choicetypes (rather that finite
types). This includes support for functions with finite support and
multisets. The library also contains a generic order and set libary,
which will be used to subsume notations for finite sets, eventually."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" { (>= "8.16" & < "8.20~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.3~") | (= "dev") }
]
tags: [
  "keyword:finmap"
  "keyword:finset"
  "keyword:multiset"
  "date:2024-01-17"
  "logpath:mathcomp.finmap"
]
authors: [
  "Cyril Cohen"
  "Kazuhiko Sakaguchi"
]
url {
  src: "https://github.com/math-comp/finmap/archive/2.1.0.tar.gz"
  checksum: "sha512=8909143c454c90f8669dcf9232581fee7cbb18bceb5082e1448481fb544709ad9077d29c44931d26a39e1ee78560f28429758c3c24cbaa6dea3942d256f2c008"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-mathcomp-finmap.2.1.0 coq.
Return code
512
Output
opam: PACKAGES... arguments: Invalid character in package name "coq."
Usage: opam install [OPTION]... [PACKAGES]...
Try `opam install --help' or `opam --help' for more information.

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

Command
opam remove -y coq; opam install -y --show-action --unlock-base coq-mathcomp-finmap.2.1.0
Return code
25344
Output
Fatal error:
Out of memory
Fatal error:
Out of memory

Install dependencies

Command
true
Return code
0
Duration
0 s

Install ๐Ÿš€

Command
true
Return code
0
Duration
1 m 0 s

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none