« Up

mathcomp-odd-order 1.14.0 Error 🔥

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                 8.16.0      Formal proof management system
dune                3.7.0       Fast, portable, and opinionated build system
ocaml               4.11.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.2      Official release 4.11.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.5       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "git+https://github.com/math-comp/odd-order"
license: "CeCILL-B"
build: [
  [make "-j" "%{jobs}%"]
]
install: [ make "install" ]
depends: [
  "ocaml"
  "coq-mathcomp-character" { (>= "1.12.0") | (= "dev") }
]
tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
synopsis: "The formal proof of the Feit-Thompson theorem"
description: """
The formal proof of the Feit-Thompson theorem.
From mathcomp Require Import all_ssreflect all_fingroup all_solvable PFsection14.
Check Feit_Thompson.
   : forall (gT : finGroupType) (G : {group gT}), odd #|G| -> solvable G
From mathcomp Require Import all_ssreflect all_fingroup 
                             all_solvable stripped_odd_order_theorem.
Check stripped_Odd_Order.
   : forall (T : Type) (mul : T -> T -> T) (one : T) (inv : T -> T)
         (G : T -> Type) (n : natural),
       group_axioms T mul one inv ->
       group T mul one inv G ->
       finite_of_order T G n -> odd n -> solvable_group T mul one inv G"""
url {
  src: "https://github.com/math-comp/odd-order/archive/mathcomp-odd-order.1.14.0.tar.gz"
  checksum: "sha256=dd65bfae84f69f5ffd0784322b66c537d76d60da246b648b0c901b77b094c8d2"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-mathcomp-odd-order.1.14.0 coq.8.16.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-mathcomp-odd-order.1.14.0 coq.8.16.0
Return code
0
Duration
1 h 0 m

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-mathcomp-odd-order.1.14.0 coq.8.16.0
Return code
7936
Duration
8 m 0 s
Output
# 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.16.0      Formal proof management system
coq-mathcomp-algebra   1.16.0      Mathematical Components Library on Algebra
coq-mathcomp-character 1.16.0      Mathematical Components Library on character theory
coq-mathcomp-field     1.16.0      Mathematical Components Library on Fields
coq-mathcomp-fingroup  1.16.0      Mathematical Components Library on finite groups
coq-mathcomp-solvable  1.16.0      Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect 1.16.0      Small Scale Reflection
dune                   3.7.0       Fast, portable, and opinionated build system
ocaml                  4.11.2      The OCaml compiler (virtual package)
ocaml-base-compiler    4.11.2      Official release 4.11.2
ocaml-config           1           OCaml Switch Configuration
ocamlfind              1.9.5       A library manager for OCaml
zarith                 1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.16.0).
The following actions will be performed:
  - install coq-mathcomp-odd-order 1.14.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-mathcomp-odd-order.1.14.0: http]
[coq-mathcomp-odd-order.1.14.0] downloaded from https://github.com/math-comp/odd-order/archive/mathcomp-odd-order.1.14.0.tar.gz
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-mathcomp-odd-order: make 4]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j" "4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-mathcomp-odd-order.1.14.0)
- coq_makefile -f _CoqProject -o Makefile.coq
- make --no-print-directory -f Makefile.coq 
- COQDEP VFILES
- COQC theories/BGsection1.v
- COQC theories/PFsection1.v
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
- [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
- [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
- [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection1.v", line 6, characters 0-92:
- Warning:
- New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
- [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
- [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
- [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
- [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection1.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
- [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
- [ambiguous-paths,typechecker]
- COQC theories/BGsection2.v
- COQC theories/BGappendixC.v
- COQC theories/wielandt_fixpoint.v
- COQC theories/PFsection2.v
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
- [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
- [ambiguous-paths,typechecker]
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
- [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
- [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
- [ambiguous-paths,typechecker]
- File "./theories/wielandt_fixpoint.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is am
[...] truncated
osedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection2.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection2.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection2.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
- [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection2.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
- [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection2.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
- [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
- [ambiguous-paths,typechecker]
- File "./theories/BGsection2.v", line 10, characters 0-88:
- Warning:
- New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
- [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
- [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
- [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
- [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection2.v", line 6, characters 0-88:
- Warning:
- New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
- [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
- [ambiguous-paths,typechecker]
- COQC theories/PFsection3.v
- File "./theories/wielandt_fixpoint.v", line 347, characters 44-55:
- Error: The reference card_matrix was not found in the current environment.
- 
- make[2]: *** [Makefile.coq:793: theories/wielandt_fixpoint.vo] Error 1
- make[2]: *** Waiting for unfinished jobs....
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
- New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
- [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
- [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
- [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
- [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
- [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 6, characters 0-86:
- Warning:
- New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
- [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
- [ambiguous-paths,typechecker]
- File "./theories/PFsection3.v", line 1407, characters 33-43:
- Warning: Notation prod_curry is deprecated since 8.13. Use uncurry instead.
- [deprecated-syntactic-definition,deprecated]
- make[1]: *** [Makefile.coq:409: all] Error 2
- make: *** [Makefile:15: invoke-coqmakefile] Error 2
[ERROR] The compilation of coq-mathcomp-odd-order failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j 4".
#=== ERROR while compiling coq-mathcomp-odd-order.1.14.0 ======================#
# context              2.0.7 | linux/x86_64 | ocaml-base-compiler.4.11.2 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-mathcomp-odd-order.1.14.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j 4
# exit-code            2
# env-file             ~/.opam/log/coq-mathcomp-odd-order-31017-335865.env
# output-file          ~/.opam/log/coq-mathcomp-odd-order-31017-335865.out
### output ###
# [...]
# [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
# [ambiguous-paths,typechecker]
# File "./theories/PFsection3.v", line 6, characters 0-86:
# Warning:
# New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
# [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
# [ambiguous-paths,typechecker]
# File "./theories/PFsection3.v", line 1407, characters 33-43:
# Warning: Notation prod_curry is deprecated since 8.13. Use uncurry instead.
# [deprecated-syntactic-definition,deprecated]
# make[1]: *** [Makefile.coq:409: all] Error 2
# make: *** [Makefile:15: invoke-coqmakefile] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-mathcomp-odd-order 1.14.0
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-mathcomp-odd-order.1.14.0 coq.8.16.0' failed.
The middle of the output is truncated (maximum 20000 characters)

Installation size

No files were installed.

Uninstall 🧹

Command
true
Return code
0
Missing removes
none
Wrong removes
none