ยซ Up

mathcomp-grobner dev Error with dependencies ๐Ÿš’

๐Ÿ“… (2022-05-14 08:21:45 UTC)

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                   dev         Formal proof management system
dune                  3.1.1       Fast, portable, and opinionated build system
ocaml                 4.12.1      The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.1      Official release 4.12.1
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
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: "Laurent.Thery@inria.fr"
homepage: "https://github.com/thery/grobner"
bug-reports: "https://github.com/thery/grobner/issues"
license: "MIT"
build: [
  ["./configure.sh"]
  [make "-j%{jobs}%"]
  [make "install"]
]
remove: [
  ["rm" "-R" "%{lib}%/coq/user-contrib/mathcomp/contrib/grobner"]
  ["sh" "-c" "rmdir %{lib}%/coq/user-contrib/mathcomp/contrib || true"]
]
depends: [
  "ocaml"
  "coq" {>= "8.5"}
  "coq-mathcomp-ssreflect" {>= "1.6"}
  "coq-mathcomp-algebra"
  "coq-mathcomp-multinomials" {= "1.6.dev"}
]
synopsis: "# grobner"
description: """
A fornalisation of Grobner basis in ssreflect.
It contains one file
grobner.v
It defines.
From mathcomp Require Import all_ssreflect all_algebra.
From SsrMultinomials Require Import ssrcomplements poset freeg mpoly.
From mathcomp.contrib.grobner Require Import grobner.
(* p belongs to the ideal generated by L *)
Check ideal.
ideal = 
fun (R : ringType) (n : nat) (L : seq {mpoly R[n]}) (p : {mpoly R[n]})
  =>
  exists t, p = \\sum_(i < size L) t`_i * L`_i
(* it is decidable *)
Check idealfP.
idealfP
     : forall (R : fieldType)  (n : nat) (p : {mpoly R[n]})
              (l : seq {mpoly R[n]}),
       reflect (ideal l p) (idealf l p)"""
url {
  src: "https://github.com/thery/grobner/archive/v1.0.1.zip"
  checksum: "md5=ee88f5010096f45a5be120de58910913"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-mathcomp-grobner.dev coq.dev
Return code
5120
Output
[NOTE] Package coq is already installed (current version is dev).
The following dependencies couldn't be met:
  - coq-mathcomp-grobner -> coq-mathcomp-multinomials = 1.6.dev
      no matching version
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-mathcomp-grobner.dev
Return code
5120
Output
The following actions will be performed:
  - remove coq dev
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.dev: not removing files that changed since:
            - share/texmf/tex/latex/misc/coqdoc.sty
            - man/man1/coqwc.1
            - man/man1/coqtop.opt.1
            - man/man1/coqtop.byte.1
            - man/man1/coqtop.1
            - man/man1/coqnative.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/stublibs/dllcoqrun_stubs.so
            - lib/coqide-server/protocol/xmlprotocol.mli
            - lib/coqide-server/protocol/xmlprotocol.ml
            - lib/coqide-server/protocol/xmlprotocol.cmx
            - lib/coqide-server/protocol/xmlprotocol.cmti
            - lib/coqide-server/protocol/xmlprotocol.cmt
            - lib/coqide-server/protocol/xmlprotocol.cmi
            - lib/coqide-server/protocol/xml_printer.mli
            - lib/coqide-server/protocol/xml_printer.ml
            - lib/coqide-server/protocol/xml_printer.cmx
            - lib/coqide-server/protocol/xml_printer.cmti
            - lib/coqide-server/protocol/xml_printer.cmt
            - lib/coqide-server/protocol/xml_printer.cmi
            - lib/coqide-server/protocol/xml_parser.mli
            - lib/coqide-server/protocol/xml_parser.ml
            - lib/coqide-server/protocol/xml_parser.cmx
            - lib/coqide-server/protocol/xml_parser.cmti
            - lib/coqide-server/protocol/xml_parser.cmt
            - lib/coqide-server/protocol/xml_parser.cmi
            - lib/coqide-server/protocol/xml_lexer.mli
            - lib/coqide-server/protocol/xml_lexer.ml
            - lib/coqide-server/protocol/xml_lexer.cmx
            - lib/coqide-server/protocol/xml_lexer.cmti
            - lib/coqide-server/protocol/xml_lexer.cmt
            - lib/coqide-server/protocol/xml_lexer.cmi
            - lib/coqide-server/protocol/serialize.mli
            - lib/coqide-server/protocol/serialize.ml
            - lib/coqide-server/protocol/serialize.cmx
            - lib/coqide-server/protocol/serialize.cmti
            - lib/coqide-server/protocol/serialize.cmt
            - lib/coqide-server/protocol/serialize.cmi
            - lib/coqide-server/protocol/richpp.mli
            - lib/coqide-server/protocol/richpp.ml
            - lib/coqide-server/protocol/richpp.cmx
            - lib/coqide-server/protocol/richpp.cmti
            - lib/coqide-server/protocol/richpp.cmt
            - lib/coqide-server/protocol/richpp.cmi
            - lib/coqide-server/protocol/protocol.cmxs
            - lib/coqide-server/protocol/protocol.cmxa
            - lib/coqide-server/protocol/protocol.cma
            - lib/coqide-server/protocol/protocol.a
            - lib/coqide-server/protocol/interface.ml
            - lib/coqide-server/protocol/interface.cmx
            - lib/coqide-server/protocol/interface.cmt
            - lib/coqide-server/protocol/interface.cmi
            - lib/coqide-server/opam
            - lib/coqide-server/dune-package
            - lib/coqide-server/core/document.mli
            - lib/coqide-server/core/document.ml
            - lib/coqide-server/core/document.cmx
            - lib/coqide-server/core/document.cmti
            - lib/coqide-server/core/document.cmt
            - lib/coqide-server/core/document.cmi
            - lib/coqide-server/core/core.cmxs
            - lib/coqide-server/core/core.cmxa
            - lib/coqide-server/core/core.cma
            - lib/coqide-server/core/core.a
            - lib/coqide-server/META
            - lib/coq/user-contrib/Ltac2/String.vos
            - lib/coq/user-contrib/Ltac2/String.vo
            - lib/coq/user-contrib/Ltac2/String.v
            - lib/coq/user-contrib/Ltac2/String.glob
            - lib/coq/user-contrib/Ltac2/Std.vos
            - lib/coq/user-contrib/Ltac2/Std.vo
            - lib/coq/user-contrib/Ltac2/Std.v
            - lib/coq/user-contrib/Ltac2/Std.glob
            - lib/coq/user-contrib/Ltac2/Printf.vos
            - lib/coq/user-contrib/Ltac2/Printf.vo
            - lib/coq/user-contrib/Ltac2/Printf.v
            - lib/coq/user-contrib/Ltac2/Printf.glob
            - lib/coq/user-contrib/Ltac2/Pattern.vos
            - lib/coq/user-contrib/Ltac2/Pattern.vo
            - lib/coq/user-contrib/Ltac2/Pattern.v
            - lib/coq/user-contrib/Ltac2/Pattern.glob
            - lib/coq/user-contrib/Ltac2/Option.vos
            - lib/coq/user-contrib/Ltac2/Option.vo
            - lib/coq/user-contrib/Ltac2/Option.v
            - lib/coq/user-contrib/Ltac2/Option.glob
            - lib/coq/user-contrib/Ltac2/Notations.vos
            - lib/coq/user-contrib/Ltac2/Notations.vo
            - lib/coq/user-contrib/Ltac2/Notations.v
            - lib/coq/user-contrib/Ltac2/Notations.glob
            - lib/coq/user-contrib/Ltac2/Message.vos
            - lib/coq/user-contrib/Ltac2/Message.vo
            - lib/coq/user-contrib/Ltac2/Message.v
            - lib/coq/user-contrib/Ltac2/Message.glob
            - lib/coq/user-contrib/Ltac2/Ltac2.vos
            - lib/coq/user-contrib/Ltac2/Ltac2.vo
            - lib/coq/user-contrib/Ltac2/Ltac2.v
            - lib/coq/user-contrib/Ltac2/Ltac2.glob
            - lib/coq/user-contrib/Ltac2/Ltac1.vos
            - lib/coq/user-contrib/Ltac2/Ltac1.vo
            - lib/coq/user-contrib/Ltac2/Ltac1.v
            - lib/coq/user-contrib/Ltac2/Ltac1.glob
            - lib/coq/user-contrib/Ltac2/List.vos
            - lib/coq/user-contrib/Ltac2/List.vo
            - lib/coq/user-contrib/Ltac2/List.v
            - lib/coq/user-contrib/Ltac2/List.glob
            - lib/coq/user-contrib/Ltac2/Int.vos
            - lib/coq/user-contrib/Ltac2/Int.vo
            - lib/coq/user-contrib/Ltac2/Int.v
            - lib/coq/user-contrib/Ltac2/Int.glob
            - lib/coq/user-contrib/Ltac2/Init.vos
            - lib/coq/user-contrib/Ltac2/Init.vo
            - lib/coq/user-contrib/Ltac2/Init.v
            - lib/coq/user-contrib/Ltac2/Init.glob
            - lib/coq/user-contrib/Ltac2/Ind.vos
            - lib/coq/user-contrib/Ltac2/Ind.vo
            - lib/coq/user-contrib/Ltac2/Ind.v
            - lib/coq/user-contrib/Ltac2/Ind.glob
            - lib/coq/user-contrib/Ltac2/Ident.vos
            - lib/coq/user-contrib/Ltac2/Ident.vo
            - lib/coq/user-contrib/Ltac2/Ident.v
            - lib/coq/user-contrib/Ltac2/Ident.glob
            - lib/coq/user-contrib/Ltac2/Fresh.vos
            - lib/coq/user-contrib/Ltac2/Fresh.vo
            - lib/coq/user-contrib/Ltac2/Fresh.v
            - lib/coq/user-contrib/Ltac2/Fresh.glob
            - lib/coq/user-contrib/Ltac2/Env.vos
            - lib/coq/user-contrib/Ltac2/Env.vo
            - lib/coq/user-contrib/Ltac2/Env.v
            - lib/coq/user-contrib/Ltac2/Env.glob
            - lib/coq/user-contrib/Ltac2/Control.vos
            - lib/coq/user-contrib/Ltac2/Control.vo
            - lib/coq/user-contrib/Ltac2/Control.v
            - lib/coq/user-contrib/Ltac2/Control.glob
            - lib/coq/user-contrib/Ltac2/Constr.vos
            - lib/coq/user-contrib/Ltac2/Constr.vo
            - lib/coq/user-contrib/Ltac2/Constr.v
            - lib/coq/user-contrib/Ltac2/Constr.glob
            - lib/coq/user-contrib/Ltac2/Char.vos
            - lib/coq/user-contrib/Ltac2/Char.vo
            - lib/coq/user-contrib/Ltac2/Char.v
            - lib/coq/user-contrib/Ltac2/Char.glob
            - lib/coq/user-contrib/Ltac2/Bool.vos
            - lib/coq/user-contrib/Ltac2/Bool.vo
            - lib/coq/user-contrib/Ltac2/Bool.v
            - lib/coq/user-contrib/Ltac2/Bool.glob
            - lib/coq/user-contrib/Ltac2/Array.vos
            - lib/coq/user-contrib/Ltac2/Array.vo
            - lib/coq/user-contrib/Ltac2/Array.v
            - lib/coq/user-contrib/Ltac2/Array.glob
            - lib/coq/theories/ssrmatching/ssrmatching.vos
            - lib/coq/theories/ssrmatching/ssrmatching.vo
            - lib/coq/theories/ssrmatching/ssrmatching.v
            - lib/coq/theories/ssrmatching/ssrmatching.glob
            - lib/coq/theories/ssr/ssrunder.vos
            - lib/coq/theories/ssr/ssrunder.vo
            - lib/coq/theories/ssr/ssrunder.v
            - lib/coq/theories/ssr/ssrunder.glob
            - lib/coq/theories/ssr/ssrsetoid.vos
            - lib/coq/theories/ssr/ssrsetoid.vo
            - lib/coq/theories/ssr/ssrsetoid.v
            - lib/coq/theories/ssr/ssrsetoid.glob
            - lib/coq/theories/ssr/ssrfun.vos
            - lib/coq/theories/ssr/ssrfun.vo
            - lib/coq/theories/ssr/ssrfun.v
            - lib/coq/theories/ssr/ssrfun.glob
            - lib/coq/theories/ssr/ssreflect.vos
            - lib/coq/theories/ssr/ssreflect.vo
            - lib/coq/theories/ssr/ssreflect.v
            - lib/coq/theories/ssr/ssreflect.glob
            - lib/coq/theories/ssr/ssrclasses.vos
            - lib/coq/theories/ssr/ssrclasses.vo
            - lib/coq/theories/ssr/ssrclasses.v
            - lib/coq/theories/ssr/ssrclasses.glob
            - lib/coq/theories/ssr/ssrbool.vos
            - lib/coq/theories/ssr/ssrbool.vo
            - lib/coq/theories/ssr/ssrbool.v
            - lib/coq/theories/ssr/ssrbool.glob
            - lib/coq/theories/setoid_ring/ZArithRing.vos
            - lib/coq/theories/setoid_ring/ZArithRing.vo
            - lib/coq/theories/setoid_ring/ZArithRing.v
            - lib/coq/theories/setoid_ring/ZArithRing.glob
            - lib/coq/theories/setoid_ring/Rings_Z.vos
            - lib/coq/theories/setoid_ring/Rings_Z.vo
            - lib/coq/theories/setoid_ring/Rings_Z.v
            - lib/coq/theories/setoid_ring/Rings_Z.glob
            - lib/coq/theories/setoid_ring/Rings_R.vos
            - lib/coq/theories/setoid_ring/Rings_R.vo
            - lib/coq/theories/setoid_ring/Rings_R.v
            - lib/coq/theories/setoid_ring/Rings_R.
[...] truncated
e/clib/hashset.ml
            - lib/coq-core/clib/hashset.cmx
            - lib/coq-core/clib/hashset.cmti
            - lib/coq-core/clib/hashset.cmt
            - lib/coq-core/clib/hashset.cmi
            - lib/coq-core/clib/hashcons.mli
            - lib/coq-core/clib/hashcons.ml
            - lib/coq-core/clib/hashcons.cmx
            - lib/coq-core/clib/hashcons.cmti
            - lib/coq-core/clib/hashcons.cmt
            - lib/coq-core/clib/hashcons.cmi
            - lib/coq-core/clib/hMap.mli
            - lib/coq-core/clib/hMap.ml
            - lib/coq-core/clib/hMap.cmx
            - lib/coq-core/clib/hMap.cmti
            - lib/coq-core/clib/hMap.cmt
            - lib/coq-core/clib/hMap.cmi
            - lib/coq-core/clib/exninfo.mli
            - lib/coq-core/clib/exninfo.ml
            - lib/coq-core/clib/exninfo.cmx
            - lib/coq-core/clib/exninfo.cmti
            - lib/coq-core/clib/exninfo.cmt
            - lib/coq-core/clib/exninfo.cmi
            - lib/coq-core/clib/dyn.mli
            - lib/coq-core/clib/dyn.ml
            - lib/coq-core/clib/dyn.cmx
            - lib/coq-core/clib/dyn.cmti
            - lib/coq-core/clib/dyn.cmt
            - lib/coq-core/clib/dyn.cmi
            - lib/coq-core/clib/diff2.mli
            - lib/coq-core/clib/diff2.ml
            - lib/coq-core/clib/diff2.cmx
            - lib/coq-core/clib/diff2.cmti
            - lib/coq-core/clib/diff2.cmt
            - lib/coq-core/clib/diff2.cmi
            - lib/coq-core/clib/clib.cmxs
            - lib/coq-core/clib/clib.cmxa
            - lib/coq-core/clib/clib.cma
            - lib/coq-core/clib/clib.a
            - lib/coq-core/clib/cUnix.mli
            - lib/coq-core/clib/cUnix.ml
            - lib/coq-core/clib/cUnix.cmx
            - lib/coq-core/clib/cUnix.cmti
            - lib/coq-core/clib/cUnix.cmt
            - lib/coq-core/clib/cUnix.cmi
            - lib/coq-core/clib/cThread.mli
            - lib/coq-core/clib/cThread.ml
            - lib/coq-core/clib/cThread.cmx
            - lib/coq-core/clib/cThread.cmti
            - lib/coq-core/clib/cThread.cmt
            - lib/coq-core/clib/cThread.cmi
            - lib/coq-core/clib/cString.mli
            - lib/coq-core/clib/cString.ml
            - lib/coq-core/clib/cString.cmx
            - lib/coq-core/clib/cString.cmti
            - lib/coq-core/clib/cString.cmt
            - lib/coq-core/clib/cString.cmi
            - lib/coq-core/clib/cSig.mli
            - lib/coq-core/clib/cSig.cmti
            - lib/coq-core/clib/cSig.cmi
            - lib/coq-core/clib/cSet.mli
            - lib/coq-core/clib/cSet.ml
            - lib/coq-core/clib/cSet.cmx
            - lib/coq-core/clib/cSet.cmti
            - lib/coq-core/clib/cSet.cmt
            - lib/coq-core/clib/cSet.cmi
            - lib/coq-core/clib/cObj.mli
            - lib/coq-core/clib/cObj.ml
            - lib/coq-core/clib/cObj.cmx
            - lib/coq-core/clib/cObj.cmti
            - lib/coq-core/clib/cObj.cmt
            - lib/coq-core/clib/cObj.cmi
            - lib/coq-core/clib/cMap.mli
            - lib/coq-core/clib/cMap.ml
            - lib/coq-core/clib/cMap.cmx
            - lib/coq-core/clib/cMap.cmti
            - lib/coq-core/clib/cMap.cmt
            - lib/coq-core/clib/cMap.cmi
            - lib/coq-core/clib/cList.mli
            - lib/coq-core/clib/cList.ml
            - lib/coq-core/clib/cList.cmx
            - lib/coq-core/clib/cList.cmti
            - lib/coq-core/clib/cList.cmt
            - lib/coq-core/clib/cList.cmi
            - lib/coq-core/clib/cEphemeron.mli
            - lib/coq-core/clib/cEphemeron.ml
            - lib/coq-core/clib/cEphemeron.cmx
            - lib/coq-core/clib/cEphemeron.cmti
            - lib/coq-core/clib/cEphemeron.cmt
            - lib/coq-core/clib/cEphemeron.cmi
            - lib/coq-core/clib/cArray.mli
            - lib/coq-core/clib/cArray.ml
            - lib/coq-core/clib/cArray.cmx
            - lib/coq-core/clib/cArray.cmti
            - lib/coq-core/clib/cArray.cmt
            - lib/coq-core/clib/cArray.cmi
            - lib/coq-core/boot/util.ml
            - lib/coq-core/boot/usage.mli
            - lib/coq-core/boot/usage.ml
            - lib/coq-core/boot/path.ml
            - lib/coq-core/boot/env.mli
            - lib/coq-core/boot/env.ml
            - lib/coq-core/boot/boot__Util.cmx
            - lib/coq-core/boot/boot__Util.cmt
            - lib/coq-core/boot/boot__Util.cmi
            - lib/coq-core/boot/boot__Usage.cmx
            - lib/coq-core/boot/boot__Usage.cmti
            - lib/coq-core/boot/boot__Usage.cmt
            - lib/coq-core/boot/boot__Usage.cmi
            - lib/coq-core/boot/boot__Path.cmx
            - lib/coq-core/boot/boot__Path.cmt
            - lib/coq-core/boot/boot__Path.cmi
            - lib/coq-core/boot/boot__Env.cmx
            - lib/coq-core/boot/boot__Env.cmti
            - lib/coq-core/boot/boot__Env.cmt
            - lib/coq-core/boot/boot__Env.cmi
            - lib/coq-core/boot/boot.ml
            - lib/coq-core/boot/boot.cmxs
            - lib/coq-core/boot/boot.cmxa
            - lib/coq-core/boot/boot.cmx
            - lib/coq-core/boot/boot.cmt
            - lib/coq-core/boot/boot.cmi
            - lib/coq-core/boot/boot.cma
            - lib/coq-core/boot/boot.a
            - lib/coq-core/META
            - doc/coq/coqide-server/README.md
            - doc/coq/coqide-server/LICENSE
            - doc/coq/coq-core/README.md
            - doc/coq/coq-core/LICENSE
            - bin/votour
            - bin/ocamllibdep
            - bin/csdpcert
            - bin/coqworkmgr
            - bin/coqwc
            - bin/coqtop.opt
            - bin/coqtop.byte
            - bin/coqtop
            - bin/coqtacticworker.opt
            - bin/coqqueryworker.opt
            - bin/coqproofworker.opt
            - bin/coqpp
            - bin/coqnative
            - bin/coqidetop.opt
            - bin/coqidetop.byte
            - bin/coqdoc
            - bin/coqdep
            - bin/coqchk
            - bin/coqc.byte
            - bin/coqc
            - bin/coq_makefile
            - bin/coq-tex
[NOTE] While removing coq.dev: not removing non-empty directories:
         - share/texmf/tex/latex/misc
         - lib/coqide-server/protocol
         - lib/coqide-server/core
         - lib/coq/user-contrib/Ltac2
         - lib/coq/theories/ssrmatching
         - lib/coq/theories/setoid_ring
         - lib/coq/theories/rtauto
         - lib/coq/theories/omega
         - lib/coq/theories/nsatz
         - lib/coq/theories/micromega
         - lib/coq/theories/funind
         - lib/coq/theories/extraction
         - lib/coq/theories/derive
         - lib/coq/theories/btauto
         - 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/Cauchy
         - lib/coq/theories/Reals/Abstract
         - lib/coq/theories/QArith
         - lib/coq/theories/Program
         - lib/coq/theories/PArith
         - lib/coq/theories/Numbers/Natural/Peano
         - lib/coq/theories/Numbers/Natural/Binary
         - lib/coq/theories/Numbers/Natural/Abstract
         - lib/coq/theories/Numbers/NatInt
         - lib/coq/theories/Numbers/Integer/NatPairs
         - lib/coq/theories/Numbers/Integer/Binary
         - lib/coq/theories/Numbers/Integer/Abstract
         - lib/coq/theories/Numbers/Cyclic/ZModulo
         - lib/coq/theories/Numbers/Cyclic/Int63
         - lib/coq/theories/Numbers/Cyclic/Int31
         - 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/Floats
         - lib/coq/theories/FSets
         - lib/coq/theories/Compat
         - lib/coq/theories/Classes
         - lib/coq/theories/Bool
         - lib/coq/theories/Array
         - lib/coq/theories/Arith
         - lib/coq-core/vm
         - lib/coq-core/vernac
         - lib/coq-core/toplevel
         - lib/coq-core/top_printers
         - lib/coq-core/tools/coqdoc
         - lib/coq-core/tactics
         - lib/coq-core/sysinit
         - lib/coq-core/stm
         - lib/coq-core/proofs
         - lib/coq-core/printing
         - lib/coq-core/pretyping
         - lib/coq-core/plugins/zify
         - lib/coq-core/plugins/tutorial/p3
         - lib/coq-core/plugins/tutorial/p2
         - lib/coq-core/plugins/tutorial/p1
         - lib/coq-core/plugins/tutorial/p0
         - lib/coq-core/plugins/tauto
         - lib/coq-core/plugins/ssrmatching
         - lib/coq-core/plugins/ssreflect
         - lib/coq-core/plugins/rtauto
         - lib/coq-core/plugins/ring
         - lib/coq-core/plugins/number_string_notation
         - lib/coq-core/plugins/nsatz
         - lib/coq-core/plugins/micromega
         - lib/coq-core/plugins/ltac2
         - lib/coq-core/plugins/funind
         - lib/coq-core/plugins/firstorder
         - lib/coq-core/plugins/extraction
         - lib/coq-core/plugins/derive
         - lib/coq-core/plugins/cc
         - lib/coq-core/plugins/btauto
         - lib/coq-core/parsing
         - lib/coq-core/library
         - lib/coq-core/kernel
         - lib/coq-core/interp
         - lib/coq-core/gramlib
         - lib/coq-core/engine
         - lib/coq-core/config
         - lib/coq-core/clib
         - lib/coq-core/boot
         - doc/coq/coqide-server
         - doc/coq/coq-core
-> removed   coq.dev
Done.
# Run eval $(opam env) to update the current shell environment
The following dependencies couldn't be met:
  - coq-mathcomp-grobner -> coq-mathcomp-multinomials = 1.6.dev
      no matching version
No solution found, exiting
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