# 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.13.0 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.6 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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-mathcomp-odd-order.1.14.0 coq.8.13.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-mathcomp-odd-order.1.14.0 coq.8.13.0opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-mathcomp-odd-order.1.14.0 coq.8.13.0# 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.13.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 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.6 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.13.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.07.1/.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/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. - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; - GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedB; GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_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. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_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] - File "./theories/BGsection1.v", line 10, characters 0-88: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - 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. - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; - GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedB; GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_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. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_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/PFsection1.v", line 6, characters 0-92: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - COQC theories/BGsection2.v - COQC theories/BGappendixC.v - COQC theories/wielandt_fixpoint.v - File "./theories/BGsection2.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/BGsection2.v", line 10, characters 0-88: - Warning: - New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRin [...] truncated .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/BGappendixC.v", line 6, characters 0-83: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> 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. - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; - GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedB; GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_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. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_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] - File "./theories/PFsection2.v", line 6, characters 0-88: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - COQC theories/PFsection3.v - File "./theories/wielandt_fixpoint.v", line 347, characters 13-73: - Error: The reference card_matrix was not found in the current environment. - - make[2]: *** [Makefile.coq:720: 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. - New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; - GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing - [GRing.divring_closedBM; GRing.subring_closedB; GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_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. - New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; - GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing - [GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_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 6, characters 0-86: - Warning: - New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; - GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing - [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. - [ambiguous-paths,typechecker] - make[1]: *** [Makefile.coq:343: 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.6 | linux/x86_64 | ocaml-base-compiler.4.07.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.07.1/.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-22868-335865.env # output-file ~/.opam/log/coq-mathcomp-odd-order-22868-335865.out ### output ### # [...] # 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 6, characters 0-86: # Warning: # New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; # GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing # [GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. # [ambiguous-paths,typechecker] # make[1]: *** [Makefile.coq:343: 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.13.0' failed. The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true