# 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.15.2 Formal proof management system dune 3.4.1 Fast, portable, and opinionated build system ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlfind 1.9.1 A library manager for OCaml ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "johnw@newartisans.com" homepage: "https://github.com/jwiegley/coq-haskell" dev-repo: "git+https://github.com/jwiegley/coq-haskell.git" bug-reports: "https://github.com/jwiegley/coq-haskell/issues" license: "BSD-3-Clause" synopsis: "A library to provide Haskell-familiar constructions in Coq" description: """ This library is designed for Haskell users who are either using Coq to build code intended for extraction to Haskell, or who wish to prototype/prove their algorithms in Coq. It provides a collection of definitions and notations to make Gallina more familiar to Haskellers. """ build: [make] install: [make "install"] depends: [ "coq" {(>= "8.10" & < "8.16~") | (= "dev")} ] url { src: "https://github.com/jwiegley/coq-haskell/archive/refs/tags/1.0.tar.gz" checksum: "sha256=64b6958f4eca641b933977a047272dea00ef5ceff33206da66f10fe792dbf3f2" } authors: [ "John Wiegley" ] tags: [ "keyword:haskell" "category:Computer Science/Data Types and Data Structures" "date:2022-03-29" "logpath:Hask" ]
true
Dry install with the current Coq version:
opam install -y --show-action coq-haskell.1.0.0 coq.8.15.2
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-haskell.1.0.0 coq.8.15.2
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-haskell.1.0.0 coq.8.15.2
Total: 3 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Indexed.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/List.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Yoneda.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/State.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/State.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Category.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Freer.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Compose.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Free.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Container.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Class.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Morph.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Indexed.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Control.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Impl.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Category.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Lens.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Applicative.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Maybe.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Free.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Fix.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Reader.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Comonad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Contravariant.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Crush.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/List.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Either.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/List.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Semigroup.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/FiatState.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Ltac.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Prelude.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Tuple.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Base.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/LogicT.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Identity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Haskell.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Either.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Monoid.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Cont.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Extract.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/IntMap.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/IntSet.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/NonEmpty.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Kan.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Yoneda.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Applicative.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Vector.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Const.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Eq.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Control.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/List/Church.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Category.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Lens.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Maybe.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Tuple.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Freer.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Indexed.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Compose.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Free.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Free.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/State.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Vector.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Container.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Crush.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/FiatState.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Contravariant.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Either.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Reader.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/State.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/NonEmpty.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Crush.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Haskell.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/FiatState.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Ltac.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Impl.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Prelude.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Either.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Free.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/IntMap.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Freer.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/State.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Either.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Yoneda.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Class.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Cont.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Control.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Morph.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/LogicT.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Kan.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Ssr.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Container.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Ssr.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Applicative.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Maybe.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Ltac.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Semigroup.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Free.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Compose.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Prelude.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Base.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Lens.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Tuple.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Either.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Identity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/State.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/LogicT.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Cont.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Contravariant.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Extract.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/IntSet.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Morph.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Impl.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Comonad.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/List/Church.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Reader.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Comonad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Fix.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Monoid.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Semigroup.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Trans/Class.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Vector.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Fix.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Identity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Kan.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Control/Monad/Base.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/NonEmpty.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Extract.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Haskell.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Const.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Eq.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Ssr.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/List/Church.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Monoid.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Functor/Const.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/Eq.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/IntMap.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Hask/Data/IntSet.glob
opam remove -y coq-haskell.1.0.0