# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.7.1 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic 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 ocamlfind 1.9.5 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Hugo.Herbelin@inria.fr" homepage: "https://github.com/coq-contribs/quicksort-complexity" license: "BSD" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/QuicksortComplexity"] depends: [ "ocaml" "coq" {>= "8.7" & < "8.8~"} ] tags: [ "keyword: quicksort" "keyword: complexity" "keyword: average-case" "category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms" "date: 2010-06" ] authors: [ "Eelis" ] bug-reports: "https://github.com/coq-contribs/quicksort-complexity/issues" dev-repo: "git+https://github.com/coq-contribs/quicksort-complexity.git" synopsis: "Proofs of Quicksort's worst- and average-case complexity" description: """ The development contains: - a set of monads and monad transformers for measuring a (possibly nondeterministic) algorithm's use of designated operations; - monadically expressed deterministic and nondeterministic implementations of Quicksort; - proofs of these implementations' worst- and average case complexity. Most of the development is documented in the TYPES 2008 paper "A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq", available at the homepage.""" flags: light-uninstall url { src: "https://github.com/coq-contribs/quicksort-complexity/archive/v8.7.0.tar.gz" checksum: "md5=489ce4001974d6aae7171cbace5a4ba9" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-quicksort-complexity.8.7.0 coq.8.7.1
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-quicksort-complexity.8.7.0 coq.8.7.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-quicksort-complexity.8.7.0 coq.8.7.1
Total: 5 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/list_utils.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/list_utils.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/vec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_definitions.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/vec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/arith_lems.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/sums_and_averages.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_det_avg_complexity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_case_split.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_det_avg_complexity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_monad_trans.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_cmp_prob.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/sums_and_averages.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/indices.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_sound_cmps.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/expec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_worst.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_parts.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_tree_monad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/util.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_cases.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_tree.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_CM_U_expec_cost_eq.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/U.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/insertion_sort.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_nondet_avg_complexity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/nat_seqs.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_expec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monads.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_definitions.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_cases.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_det_parts.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_list.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/sort_order.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/indices.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/harmonic.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/arith_lems.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_tree_monad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/list_utils.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/list_length_expec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/fix_measure_utils.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_correct.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/nat_below.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_nondet_avg_complexity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/NDP.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/U.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_case_split.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/expec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/vec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/fix_measure_utils.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_expec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/insertion_sort.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_monad_trans.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/skip_list.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_tree_monad.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/sort_order.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/util.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_parts.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monads.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_tree.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_sound_cmps.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_CM_U_expec_cost_eq.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_worst.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_cmp_prob.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_det_parts.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/sums_and_averages.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/list_length_expec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/nat_seqs.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_det_avg_complexity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_list.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_definitions.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/indices.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/arith_lems.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/nat_below.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_correct.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_cases.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/harmonic.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/skip_list.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_nondet_avg_complexity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/U.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/expec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_sound_cmps.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_tree.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_case_split.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/insertion_sort.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_tree_monad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_expec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monads.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/sort_order.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/util.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_parts.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/fix_measure_utils.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_monad_trans.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_tree_monad.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_worst.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_CM_U_expec_cost_eq.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_cmp_prob.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/ne_list.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/NDP.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/nat_seqs.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_det_parts.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/list_length_expec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/nat_below.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/skip_list.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/qs_correct.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/harmonic.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/monoid_tree_monad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/QuicksortComplexity/NDP.v
opam remove -y coq-quicksort-complexity.8.7.0