# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils coq 8.12.0 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.5 A library manager for OCaml # 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: "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:2022-08-17" "logpath:stdpp" ] depends: [ "coq" { (>= "8.12" & < "8.17~") | (= "dev") } ] build: ["./make-package" "stdpp" "-j%{jobs}%"] install: ["./make-package" "stdpp" "install"] url { src: "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/coq-stdpp-1.8.0.tar.gz" checksum: "sha512=c894cc0574ab00efa41c807628f97abdeff917bee71b40e2f98251bcdc91ebfb7a2964683e61e7cefbe6e578b2e123098ddd7694252406f8c4835176c1d0df37" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-stdpp.1.8.0 coq.8.12.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-stdpp.1.8.0 coq.8.12.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-stdpp.1.8.0 coq.8.12.0
Total: 15 M
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/list.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_maps.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_maps.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/list.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/sets.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/base.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/numbers.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/gmultiset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/sets.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/numbers.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_sets.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_map_dom.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/base.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/list.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/finite.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/gmap.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/coPset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/option.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/natmap.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/list_numbers.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/pmap.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_maps.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/strings.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/pretty.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/countable.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/relations.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/coPset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_sets.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/gmultiset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/tactics.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_map_dom.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/vector.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/hashset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/relations.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/coGset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/sorting.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/infinite.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/mapset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/zmap.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/option.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/lexico.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/list_numbers.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/finite.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/binders.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/nmap.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/decidable.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/natmap.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/namespaces.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/base.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/gmap.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/countable.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/stringmap.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/listset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/telescopes.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/pmap.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/nat_cancel.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/vector.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/propset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/sets.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/boolset.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/numbers.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/listset_nodup.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/orders.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/hlist.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/hashset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/streams.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/sorting.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/prelude.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/functions.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/decidable.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/lexico.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/tactics.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/telescopes.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/gmultiset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/coGset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/proof_irrel.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/tactics.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/mapset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_sets.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/well_founded.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/pretty.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/infinite.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/option.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/relations.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/binders.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/coPset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/finite.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/zmap.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/list_numbers.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/gmap.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/natmap.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin_map_dom.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/pmap.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/orders.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/namespaces.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/countable.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/vector.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/propset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/well_founded.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/nat_cancel.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/strings.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/nmap.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/decidable.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/listset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/hlist.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/sorting.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/stringmap.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/telescopes.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/functions.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/proof_irrel.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/streams.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/boolset.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/coGset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/hashset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/infinite.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/lexico.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/mapset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/namespaces.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/listset_nodup.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/pretty.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/binders.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/nat_cancel.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/fin.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/zmap.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/strings.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/orders.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/nmap.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/listset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/well_founded.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/stringmap.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/propset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/hlist.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/streams.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/proof_irrel.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/listset_nodup.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/options.vo
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/boolset.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/functions.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/options.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/prelude.glob
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/prelude.v
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/stdpp/options.glob
opam remove -y coq-stdpp.1.8.0