ยซ Up

chick-blog 1.0.0 Black list ๐Ÿดโ€โ˜ ๏ธ

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-ocamlbuild     base        OCamlbuild binary and libraries distributed with the OCaml compiler
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.4.5       Formal proof management system.
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.02.3      The OCaml compiler (virtual package)
ocaml-base-compiler 4.02.3      Official 4.02.3 release
ocaml-config        1           OCaml Switch Configuration
ocamlbuild          0           Build system distributed with the OCaml compiler since OCaml 3.10.0
# opam file:
opam-version: "2.0"
maintainer: "dev@clarus.me"
homepage: "https://github.com/clarus/coq-chick-blog"
dev-repo: "git+https://github.com/clarus/coq-chick-blog.git"
bug-reports: "https://github.com/clarus/coq-chick-blog/issues"
authors: ["Guillaume Claret"]
license: "MIT"
build: [
  ["./configure.sh"]
  [make "-j%{jobs}%"]
  [make "-C" "extraction" "-j%{jobs}%"]
]
depends: [
  "cohttp-lwt-unix"
  "coq-error-handlers"
  "coq-function-ninjas"
  "coq-list-string"
  "coq-moment"
  "coq" {< "8.9~"}
  "lwt"
  "ocaml" {>= "4.03"}
  "ocamlfind" {build}
]
tags: [
  "date:2019-11-26"
  "keyword:blog"
  "keyword:effects"
  "keyword:extraction"
]
synopsis: "A blog engine written and proven in Coq"
url {
  src: "https://github.com/clarus/coq-chick-blog/archive/1.0.0.tar.gz"
  checksum: "sha512=f54224caafc490f01896ff1fa1e6e9c71ff91ca5bf04fe00f4761dbd9e32758628f6be045b56f4a466574c05ae98edaf41931a1851ae59b8ab0686d83bb28036"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-chick-blog.1.0.0 coq.8.4.5
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.4.5).
The following dependencies couldn't be met:
  - coq-chick-blog -> ocaml >= 4.03
      base of this switch (use `--unlock-base' to force)
No solution found, exiting

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-chick-blog.1.0.0
Return code
15360
Output
The following actions will be performed:
  - remove coq 8.4.5
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.4.5: not removing files that changed since:
            - share/emacs/site-lisp/coqdoc.sty
            - share/emacs/site-lisp/coq.el
            - share/emacs/site-lisp/coq-syntax.el
            - share/emacs/site-lisp/coq-inferior.el
            - share/emacs/site-lisp/coq-font-lock.el
            - share/emacs/site-lisp/coq-db.el
            - share/coq/coq.png
            - man/man1/gallina.1
            - man/man1/coqwc.1
            - man/man1/coqtop.opt.1
            - man/man1/coqtop.byte.1
            - man/man1/coqtop.1
            - man/man1/coqmktop.1
            - man/man1/coqide.1
            - man/man1/coqdoc.1
            - man/man1/coqdep.1
            - man/man1/coqchk.1
            - man/man1/coqc.1
            - man/man1/coq_makefile.1
            - man/man1/coq-tex.1
            - lib/coq/toplevel/whelp.cmi
            - lib/coq/toplevel/vernacinterp.cmi
            - lib/coq/toplevel/vernacexpr.cmi
            - lib/coq/toplevel/vernacentries.cmi
            - lib/coq/toplevel/vernac.cmi
            - lib/coq/toplevel/usage.cmi
            - lib/coq/toplevel/toplevel.cmxa
            - lib/coq/toplevel/toplevel.cmi
            - lib/coq/toplevel/toplevel.cma
            - lib/coq/toplevel/toplevel.a
            - lib/coq/toplevel/search.cmi
            - lib/coq/toplevel/record.cmi
            - lib/coq/toplevel/mltop.cmi
            - lib/coq/toplevel/metasyntax.cmi
            - lib/coq/toplevel/libtypes.cmi
            - lib/coq/toplevel/lemmas.cmi
            - lib/coq/toplevel/interface.cmi
            - lib/coq/toplevel/indschemes.cmi
            - lib/coq/toplevel/ind_tables.cmi
            - lib/coq/toplevel/ide_slave.cmi
            - lib/coq/toplevel/ide_intf.cmi
            - lib/coq/toplevel/himsg.cmi
            - lib/coq/toplevel/discharge.cmi
            - lib/coq/toplevel/coqtop.cmi
            - lib/coq/toplevel/coqinit.cmi
            - lib/coq/toplevel/command.cmi
            - lib/coq/toplevel/classes.cmi
            - lib/coq/toplevel/class.cmi
            - lib/coq/toplevel/cerrors.cmi
            - lib/coq/toplevel/backtrack.cmi
            - lib/coq/toplevel/autoinstance.cmi
            - lib/coq/toplevel/auto_ind_decl.cmi
            - lib/coq/tools/coqdoc/coqdoc.sty
            - lib/coq/tools/coqdoc/coqdoc.css
            - lib/coq/theories/ZArith/auxiliary.vo
            - lib/coq/theories/ZArith/Zwf.vo
            - lib/coq/theories/ZArith/Zsqrt_compat.vo
            - lib/coq/theories/ZArith/Zquot.vo
            - lib/coq/theories/ZArith/Zpower.vo
            - lib/coq/theories/ZArith/Zpow_facts.vo
            - lib/coq/theories/ZArith/Zpow_def.vo
            - lib/coq/theories/ZArith/Zpow_alt.vo
            - lib/coq/theories/ZArith/Zorder.vo
            - lib/coq/theories/ZArith/Znumtheory.vo
            - lib/coq/theories/ZArith/Znat.vo
            - lib/coq/theories/ZArith/Zmisc.vo
            - lib/coq/theories/ZArith/Zminmax.vo
            - lib/coq/theories/ZArith/Zmin.vo
            - lib/coq/theories/ZArith/Zmax.vo
            - lib/coq/theories/ZArith/Zlogarithm.vo
            - lib/coq/theories/ZArith/Zhints.vo
            - lib/coq/theories/ZArith/Zgcd_alt.vo
            - lib/coq/theories/ZArith/Zeven.vo
            - lib/coq/theories/ZArith/Zeuclid.vo
            - lib/coq/theories/ZArith/Zdiv.vo
            - lib/coq/theories/ZArith/Zdigits.vo
            - lib/coq/theories/ZArith/Zcomplements.vo
            - lib/coq/theories/ZArith/Zcompare.vo
            - lib/coq/theories/ZArith/Zbool.vo
            - lib/coq/theories/ZArith/Zabs.vo
            - lib/coq/theories/ZArith/ZOdiv_def.vo
            - lib/coq/theories/ZArith/ZOdiv.vo
            - lib/coq/theories/ZArith/ZArith_dec.vo
            - lib/coq/theories/ZArith/ZArith_base.vo
            - lib/coq/theories/ZArith/ZArith.vo
            - lib/coq/theories/ZArith/Wf_Z.vo
            - lib/coq/theories/ZArith/Int.vo
            - lib/coq/theories/ZArith/BinIntDef.vo
            - lib/coq/theories/ZArith/BinInt.vo
            - lib/coq/theories/Wellfounded/Wellfounded.vo
            - lib/coq/theories/Wellfounded/Well_Ordering.vo
            - lib/coq/theories/Wellfounded/Union.vo
            - lib/coq/theories/Wellfounded/Transitive_Closure.vo
            - lib/coq/theories/Wellfounded/Lexicographic_Product.vo
            - lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
            - lib/coq/theories/Wellfounded/Inverse_Image.vo
            - lib/coq/theories/Wellfounded/Inclusion.vo
            - lib/coq/theories/Wellfounded/Disjoint_Union.vo
            - lib/coq/theories/Vectors/VectorSpec.vo
            - lib/coq/theories/Vectors/VectorDef.vo
            - lib/coq/theories/Vectors/Vector.vo
            - lib/coq/theories/Vectors/Fin.vo
            - lib/coq/theories/Unicode/Utf8_core.vo
            - lib/coq/theories/Unicode/Utf8.vo
            - lib/coq/theories/Structures/OrdersTac.vo
            - lib/coq/theories/Structures/OrdersLists.vo
            - lib/coq/theories/Structures/OrdersFacts.vo
            - lib/coq/theories/Structures/OrdersEx.vo
            - lib/coq/theories/Structures/OrdersAlt.vo
            - lib/coq/theories/Structures/Orders.vo
            - lib/coq/theories/Structures/OrderedTypeEx.vo
            - lib/coq/theories/Structures/OrderedTypeAlt.vo
            - lib/coq/theories/Structures/OrderedType.vo
            - lib/coq/theories/Structures/GenericMinMax.vo
            - lib/coq/theories/Structures/EqualitiesFacts.vo
            - lib/coq/theories/Structures/Equalities.vo
            - lib/coq/theories/Structures/DecidableTypeEx.vo
            - lib/coq/theories/Structures/DecidableType.vo
            - lib/coq/theories/Strings/String.vo
            - lib/coq/theories/Strings/Ascii.vo
            - lib/coq/theories/Sorting/Sorting.vo
            - lib/coq/theories/Sorting/Sorted.vo
            - lib/coq/theories/Sorting/Permutation.vo
            - lib/coq/theories/Sorting/PermutSetoid.vo
            - lib/coq/theories/Sorting/PermutEq.vo
            - lib/coq/theories/Sorting/Mergesort.vo
            - lib/coq/theories/Sorting/Heap.vo
            - lib/coq/theories/Sets/Uniset.vo
            - lib/coq/theories/Sets/Relations_3_facts.vo
            - lib/coq/theories/Sets/Relations_3.vo
            - lib/coq/theories/Sets/Relations_2_facts.vo
            - lib/coq/theories/Sets/Relations_2.vo
            - lib/coq/theories/Sets/Relations_1_facts.vo
            - lib/coq/theories/Sets/Relations_1.vo
            - lib/coq/theories/Sets/Powerset_facts.vo
            - lib/coq/theories/Sets/Powerset_Classical_facts.vo
            - lib/coq/theories/Sets/Powerset.vo
            - lib/coq/theories/Sets/Permut.vo
            - lib/coq/theories/Sets/Partial_Order.vo
            - lib/coq/theories/Sets/Multiset.vo
            - lib/coq/theories/Sets/Integers.vo
            - lib/coq/theories/Sets/Infinite_sets.vo
            - lib/coq/theories/Sets/Image.vo
            - lib/coq/theories/Sets/Finite_sets_facts.vo
            - lib/coq/theories/Sets/Finite_sets.vo
            - lib/coq/theories/Sets/Ensembles.vo
            - lib/coq/theories/Sets/Cpo.vo
            - lib/coq/theories/Sets/Constructive_sets.vo
            - lib/coq/theories/Sets/Classical_sets.vo
            - lib/coq/theories/Setoids/Setoid.vo
            - lib/coq/theories/Relations/Relations.vo
            - lib/coq/theories/Relations/Relation_Operators.vo
            - lib/coq/theories/Relations/Relation_Definitions.vo
            - lib/coq/theories/Relations/Operators_Properties.vo
            - lib/coq/theories/Reals/Sqrt_reg.vo
            - lib/coq/theories/Reals/SplitRmult.vo
            - lib/coq/theories/Reals/SplitAbsolu.vo
            - lib/coq/theories/Reals/SeqSeries.vo
            - lib/coq/theories/Reals/SeqProp.vo
            - lib/coq/theories/Reals/Rtrigo_reg.vo
            - lib/coq/theories/Reals/Rtrigo_fun.vo
            - lib/coq/theories/Reals/Rtrigo_def.vo
            - lib/coq/theories/Reals/Rtrigo_calc.vo
            - lib/coq/theories/Reals/Rtrigo_alt.vo
            - lib/coq/theories/Reals/Rtrigo1.vo
            - lib/coq/theories/Reals/Rtrigo.vo
            - lib/coq/theories/Reals/Rtopology.vo
            - lib/coq/theories/Reals/Rsqrt_def.vo
            - lib/coq/theories/Reals/Rsigma.vo
            - lib/coq/theories/Reals/Rseries.vo
            - lib/coq/theories/Reals/Rprod.vo
            - lib/coq/theories/Reals/Rpower.vo
            - lib/coq/theories/Reals/Rpow_def.vo
            - lib/coq/theories/Reals/Rminmax.vo
            - lib/coq/theories/Reals/Rlogic.vo
            - lib/coq/theories/Reals/Rlimit.vo
            - lib/coq/theories/Reals/RiemannInt_SF.vo
            - lib/coq/theories/Reals/RiemannInt.vo
            - lib/coq/theories/Reals/Rgeom.vo
            - lib/coq/theories/Reals/Rfunctions.vo
            - lib/coq/theories/Reals/Reals.vo
            - lib/coq/theories/Reals/Rderiv.vo
            - lib/coq/theories/Reals/Rdefinitions.vo
            - lib/coq/theories/Reals/Rcomplete.vo
            - lib/coq/theories/Reals/Rbasic_fun.vo
            - lib/coq/theories/Reals/Rbase.vo
            - lib/coq/theories/Reals/Raxioms.vo
            - lib/coq/theories/Reals/Ratan.vo
            - lib/coq/theories/Reals/Ranalysis_reg.vo
            - lib/coq/theories/Reals/Ranalysis5.vo
            - lib/coq/theories/Reals/Ranalysis4.vo
            - lib/coq/theories/Reals/Ranalysis3.vo
            - lib/coq/theories/Reals/Ranalysis2.vo
            - lib/coq/theories/Reals/Ranalysis1.vo
            - lib/coq/theories/Reals/Ranalysis.vo
            - lib/coq/theories/Reals/R_sqrt.vo
            - lib/coq/theories/Reals/R_sqr.vo
            - lib/coq/theories/Reals/R_Ifp.vo
            - lib/coq/theories/Reals/ROrderedType.vo
            - lib/coq/theories/Reals/RList.vo
[...] truncated
t.vo
            - lib/coq/plugins/extraction/ExtrOcamlIntConv.vo
            - lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
            - lib/coq/plugins/extraction/ExtrOcamlBasic.vo
            - lib/coq/plugins/decl_mode/ppdecl_proof.cmi
            - lib/coq/plugins/decl_mode/g_decl_mode.cmi
            - lib/coq/plugins/decl_mode/decl_proof_instr.cmi
            - lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
            - lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
            - lib/coq/plugins/decl_mode/decl_mode_plugin.cma
            - lib/coq/plugins/decl_mode/decl_mode.cmi
            - lib/coq/plugins/decl_mode/decl_interp.cmi
            - lib/coq/plugins/decl_mode/decl_expr.cmi
            - lib/coq/plugins/cc/g_congruence.cmi
            - lib/coq/plugins/cc/cctac.cmi
            - lib/coq/plugins/cc/ccproof.cmi
            - lib/coq/plugins/cc/ccalgo.cmi
            - lib/coq/plugins/cc/cc_plugin_mod.cmi
            - lib/coq/plugins/cc/cc_plugin.cmxs
            - lib/coq/plugins/cc/cc_plugin.cma
            - lib/coq/parsing/tok.cmi
            - lib/coq/parsing/tactic_printer.cmi
            - lib/coq/parsing/q_util.cmi
            - lib/coq/parsing/printmod.cmi
            - lib/coq/parsing/printer.cmi
            - lib/coq/parsing/prettyp.cmi
            - lib/coq/parsing/ppvernac.cmi
            - lib/coq/parsing/pptactic.cmi
            - lib/coq/parsing/ppconstr.cmi
            - lib/coq/parsing/pcoq.cmi
            - lib/coq/parsing/parsing.cmxa
            - lib/coq/parsing/parsing.cma
            - lib/coq/parsing/parsing.a
            - lib/coq/parsing/lexer.cmi
            - lib/coq/parsing/highparsing.cmxa
            - lib/coq/parsing/highparsing.cma
            - lib/coq/parsing/highparsing.a
            - lib/coq/parsing/grammar.cma
            - lib/coq/parsing/g_xml.cmi
            - lib/coq/parsing/g_vernac.cmi
            - lib/coq/parsing/g_tactic.cmi
            - lib/coq/parsing/g_proofs.cmi
            - lib/coq/parsing/g_prim.cmi
            - lib/coq/parsing/g_ltac.cmi
            - lib/coq/parsing/g_constr.cmi
            - lib/coq/parsing/extrawit.cmi
            - lib/coq/parsing/extend.cmi
            - lib/coq/parsing/egrammar.cmi
            - lib/coq/library/summary.cmi
            - lib/coq/library/states.cmi
            - lib/coq/library/nametab.cmi
            - lib/coq/library/nameops.cmi
            - lib/coq/library/library.cmxa
            - lib/coq/library/library.cmi
            - lib/coq/library/library.cma
            - lib/coq/library/library.a
            - lib/coq/library/libobject.cmi
            - lib/coq/library/libnames.cmi
            - lib/coq/library/lib.cmi
            - lib/coq/library/impargs.cmi
            - lib/coq/library/heads.cmi
            - lib/coq/library/goptionstyp.cmi
            - lib/coq/library/goptions.cmi
            - lib/coq/library/global.cmi
            - lib/coq/library/dischargedhypsmap.cmi
            - lib/coq/library/decls.cmi
            - lib/coq/library/declaremods.cmi
            - lib/coq/library/declare.cmi
            - lib/coq/library/decl_kinds.cmi
            - lib/coq/library/assumptions.cmi
            - lib/coq/libcoqrun.a
            - lib/coq/lib/xml_utils.cmi
            - lib/coq/lib/xml_parser.cmi
            - lib/coq/lib/xml_lexer.cmi
            - lib/coq/lib/util.cmi
            - lib/coq/lib/unionfind.cmi
            - lib/coq/lib/unicodetable.cmi
            - lib/coq/lib/tries.cmi
            - lib/coq/lib/system.cmi
            - lib/coq/lib/store.cmi
            - lib/coq/lib/segmenttree.cmi
            - lib/coq/lib/rtree.cmi
            - lib/coq/lib/profile.cmi
            - lib/coq/lib/predicate.cmi
            - lib/coq/lib/pp_control.cmi
            - lib/coq/lib/pp.cmi
            - lib/coq/lib/option.cmi
            - lib/coq/lib/lib.cmxa
            - lib/coq/lib/lib.cma
            - lib/coq/lib/lib.a
            - lib/coq/lib/heap.cmi
            - lib/coq/lib/hashtbl_alt.cmi
            - lib/coq/lib/hashcons.cmi
            - lib/coq/lib/gmapl.cmi
            - lib/coq/lib/gmap.cmi
            - lib/coq/lib/fset.cmi
            - lib/coq/lib/fmap.cmi
            - lib/coq/lib/flags.cmi
            - lib/coq/lib/explore.cmi
            - lib/coq/lib/errors.cmi
            - lib/coq/lib/envars.cmi
            - lib/coq/lib/dyn.cmi
            - lib/coq/lib/dnet.cmi
            - lib/coq/lib/compat.cmi
            - lib/coq/lib/bigint.cmi
            - lib/coq/kernel/vm.cmi
            - lib/coq/kernel/vconv.cmi
            - lib/coq/kernel/univ.cmi
            - lib/coq/kernel/typeops.cmi
            - lib/coq/kernel/type_errors.cmi
            - lib/coq/kernel/term_typing.cmi
            - lib/coq/kernel/term.cmi
            - lib/coq/kernel/subtyping.cmi
            - lib/coq/kernel/sign.cmi
            - lib/coq/kernel/safe_typing.cmi
            - lib/coq/kernel/retroknowledge.cmi
            - lib/coq/kernel/reduction.cmi
            - lib/coq/kernel/pre_env.cmi
            - lib/coq/kernel/names.cmi
            - lib/coq/kernel/modops.cmi
            - lib/coq/kernel/mod_typing.cmi
            - lib/coq/kernel/mod_subst.cmi
            - lib/coq/kernel/kernel.cmxa
            - lib/coq/kernel/kernel.cma
            - lib/coq/kernel/kernel.a
            - lib/coq/kernel/inductive.cmi
            - lib/coq/kernel/indtypes.cmi
            - lib/coq/kernel/esubst.cmi
            - lib/coq/kernel/environ.cmi
            - lib/coq/kernel/entries.cmi
            - lib/coq/kernel/declarations.cmi
            - lib/coq/kernel/csymtable.cmi
            - lib/coq/kernel/copcodes.cmi
            - lib/coq/kernel/cooking.cmi
            - lib/coq/kernel/conv_oracle.cmi
            - lib/coq/kernel/closure.cmi
            - lib/coq/kernel/cemitcodes.cmi
            - lib/coq/kernel/cbytegen.cmi
            - lib/coq/kernel/cbytecodes.cmi
            - lib/coq/interp/topconstr.cmi
            - lib/coq/interp/syntax_def.cmi
            - lib/coq/interp/smartlocate.cmi
            - lib/coq/interp/reserve.cmi
            - lib/coq/interp/ppextend.cmi
            - lib/coq/interp/notation.cmi
            - lib/coq/interp/modintern.cmi
            - lib/coq/interp/interp.cmxa
            - lib/coq/interp/interp.cma
            - lib/coq/interp/interp.a
            - lib/coq/interp/implicit_quantifiers.cmi
            - lib/coq/interp/genarg.cmi
            - lib/coq/interp/dumpglob.cmi
            - lib/coq/interp/coqlib.cmi
            - lib/coq/interp/constrintern.cmi
            - lib/coq/interp/constrextern.cmi
            - lib/coq/dllcoqrun.so
            - lib/coq/config/coqide-gtk2rc
            - lib/coq/config/coq_config.o
            - lib/coq/config/coq_config.cmx
            - lib/coq/config/coq_config.cmo
            - lib/coq/config/coq_config.cmi
            - doc/FAQ-CoqIde
            - bin/coqtop.opt
            - bin/coqtop.byte
            - bin/coqchk.opt
[NOTE] While removing coq.8.4.5: not removing non-empty directories:
         - share/emacs/site-lisp
         - share/coq
         - lib/coq/toplevel
         - lib/coq/tools/coqdoc
         - lib/coq/theories/ZArith
         - lib/coq/theories/Wellfounded
         - lib/coq/theories/Vectors
         - lib/coq/theories/Unicode
         - lib/coq/theories/Structures
         - lib/coq/theories/Strings
         - lib/coq/theories/Sorting
         - lib/coq/theories/Sets
         - lib/coq/theories/Setoids
         - lib/coq/theories/Relations
         - lib/coq/theories/Reals
         - lib/coq/theories/QArith
         - lib/coq/theories/Program
         - lib/coq/theories/PArith
         - lib/coq/theories/Numbers/Rational/SpecViaQ
         - lib/coq/theories/Numbers/Rational/BigQ
         - lib/coq/theories/Numbers/Natural/SpecViaZ
         - lib/coq/theories/Numbers/Natural/Peano
         - lib/coq/theories/Numbers/Natural/Binary
         - lib/coq/theories/Numbers/Natural/BigN
         - lib/coq/theories/Numbers/Natural/Abstract
         - lib/coq/theories/Numbers/NatInt
         - lib/coq/theories/Numbers/Integer/SpecViaZ
         - lib/coq/theories/Numbers/Integer/NatPairs
         - lib/coq/theories/Numbers/Integer/Binary
         - lib/coq/theories/Numbers/Integer/BigZ
         - lib/coq/theories/Numbers/Integer/Abstract
         - lib/coq/theories/Numbers/Cyclic/ZModulo
         - lib/coq/theories/Numbers/Cyclic/Int31
         - lib/coq/theories/Numbers/Cyclic/DoubleCyclic
         - lib/coq/theories/Numbers/Cyclic/Abstract
         - lib/coq/theories/NArith
         - lib/coq/theories/MSets
         - lib/coq/theories/Logic
         - lib/coq/theories/Lists
         - lib/coq/theories/Init
         - lib/coq/theories/FSets
         - lib/coq/theories/Classes
         - lib/coq/theories/Bool
         - lib/coq/theories/Arith
         - lib/coq/tactics
         - lib/coq/states
         - lib/coq/proofs
         - lib/coq/pretyping
         - lib/coq/plugins/xml
         - lib/coq/plugins/syntax
         - lib/coq/plugins/subtac
         - lib/coq/plugins/setoid_ring
         - lib/coq/plugins/rtauto
         - lib/coq/plugins/romega
         - lib/coq/plugins/ring
         - lib/coq/plugins/quote
         - lib/coq/plugins/omega
         - lib/coq/plugins/nsatz
         - lib/coq/plugins/micromega
         - lib/coq/plugins/funind
         - lib/coq/plugins/fourier
         - lib/coq/plugins/firstorder
         - lib/coq/plugins/field
         - lib/coq/plugins/extraction
         - lib/coq/plugins/decl_mode
         - lib/coq/plugins/cc
         - lib/coq/parsing
         - lib/coq/library
         - lib/coq/kernel
         - lib/coq/interp
         - lib/coq/config
-> removed   coq.8.4.5
Done.
# Run eval $(opam env) to update the current shell environment
[ERROR] Sorry, resolution of the request timed out.
        Try to specify a simpler request, use a different solver, or increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger value (currently, it is set to 600.0 seconds).
The middle of the output is truncated (maximum 20000 characters)

Install dependencies

Command
true
Return code
0
Duration
0 s

Install ๐Ÿš€

Command
true
Return code
0
Duration
0 s

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none