ยซ Up

stdpp 1.5.0 Black list ๐Ÿดโ€โ˜ ๏ธ

Context

# 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.13.2      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2      Official release 4.10.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.3       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The std++ team"
license: "BSD-3-Clause"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
synopsis: "std++ is an extended \"Standard Library\" for Coq"
description: """
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
  structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `โˆ…`, `โˆช`, and Haskell-style
  monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
  having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
  equality can be used as much as possible (for example, for maps we have
  `m1 = m2` iff `โˆ€ i, m1 !! i = m2 !! i`). On top of that, the library provides
  setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
  `done` tactic for finishing trivial goals, a simple breadth-first solver
  `naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
  for proving compatibility of functions with respect to relations, and a solver
  `set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
"""
tags: [
  "date:2021-02-16"
  "logpath:stdpp"
]
depends: [
  "coq" { (>= "8.10.2" & < "8.14~") | (= "dev") }
]
patches: [ "0001-Windows-CI-strip-CR-in-result-comparison.patch" ]
build: [make "-j%{jobs}%"]
install: [make "install"]
url {
  src:
    "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/coq-stdpp-1.5.0.tar.gz"
  checksum:
    "sha512=393ae68782370e4206e452d46c44300d5e6e27be15d9aa1dfd33ef0ccef1640f83e741f0a799c106453f305c59c5af1698ef276b47522daaefc86ece0b40f530"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-stdpp.1.5.0 coq.8.13.2
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; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-stdpp.1.5.0 coq.8.13.2
Return code
0
Duration
1 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-stdpp.1.5.0 coq.8.13.2
Return code
10240
Duration
1 m 0 s
Output
# 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.13.2      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2      Official release 4.10.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.3       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.13.2).
The following actions will be performed:
  - install coq-stdpp 1.5.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-stdpp.1.5.0: http]
[ERROR] The sources of the following couldn't be obtained, aborting:
          - coq-stdpp.1.5.0:
            https://gitlab.mpi-sws.org/iris/stdpp/-/archive/coq-stdpp-1.5.0.tar.gz (Curl failed: "/usr/bin/curl --write-out %{http_code}\\n --retry 3 --retry-delay 2 --user-agent opam/2.0.6 -L -o /home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/sources/coq-stdpp.1.5.0/coq-stdpp-1.5.0.tar.gz.part https://gitlab.mpi-sws.org/iris/stdpp/-/archive/coq-stdpp-1.5.0.tar.gz" exited with code 7)
'opam install -y -v coq-stdpp.1.5.0 coq.8.13.2' failed.

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none