« Up

geometric-algebra 0.8.8 Error 🔥

📅 (2019-11-29 00:21:18 UTC)

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.11.dev    Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Laurent Théry"
homepage: "https://github.com/thery/GeometricAlgebra"
bug-reports: "https://github.com/thery/GeometricAlgebra"
dev-repo: "git+https://github.com/thery/GeometricAlgebra.git"
authors : "Laurent Théry"
license: "LGPL"
build: [
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/GeometricAlgebra"]
depends: [
  "ocaml"
  "coq" {>= "8.8~"}
]
synopsis: "Grassman Cayley and Clifford formalisations"
flags: light-uninstall
url {
  src: "https://github.com/thery/GeometricAlgebra/archive/v8.8.zip"
  checksum: "md5=12dfbc7869435e2777342fe0a0243283"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-geometric-algebra.0.8.8 coq.8.11.dev
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 2h opam install -y --deps-only coq-geometric-algebra.0.8.8 coq.8.11.dev
Return code
0
Duration
3 s

Install 🚀

Command
opam list; echo; ulimit -Sv 4000000; timeout 1h opam install -y -v coq-geometric-algebra.0.8.8 coq.8.11.dev
Return code
7936
Duration
44 s
Output
# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.11.dev    Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
[NOTE] Package coq is already installed (current version is 8.11.dev).
The following actions will be performed:
  - install coq-geometric-algebra 0.8.8
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-geometric-algebra.0.8.8: http]
[coq-geometric-algebra.0.8.8] downloaded from https://github.com/thery/GeometricAlgebra/archive/v8.8.zip
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-geometric-algebra: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-geometric-algebra.0.8.8)
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin//coq_makefile -f _CoqProject -o Makefile.coq
- COQDEP VFILES
- COQC Aux.v
- File "./Aux.v", line 357, characters 0-21:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- COQC Field.v
- File "./Field.v", line 18, characters 0-33:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope field_scope.". [undeclared-scope,deprecated]
- COQC VectorSpace.v
- File "./VectorSpace.v", line 3, characters 0-320:
- Warning:
- New coercion path [stype; K] : eparams >-> Sortclass is ambiguous with existing 
- [E] : eparams >-> Sortclass. [ambiguous-paths,typechecker]
- File "./VectorSpace.v", line 12, characters 0-34:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope vector_scope.". [undeclared-scope,deprecated]
- COQC Kn.v
- File "./Kn.v", line 1, characters 0-49:
- Warning:
- New coercion path [stype; K] : eparams >-> Sortclass is ambiguous with existing 
- [E] : eparams >-> Sortclass. [ambiguous-paths,typechecker]
- File "./Kn.v", line 13, characters 0-30:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope kn_scope.". [undeclared-scope,deprecated]
- File "./Kn.v", line 106, characters 0-16:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Kn.v", line 174, characters 0-25:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Kn.v", line 602, characters 0-57:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope Kn_scope.". [undeclared-scope,deprecated]
- File "./Kn.v", line 609, characters 0-25:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- COQC Grassmann.v
- File "./Grassmann.v", line 1, characters 0-81:
- Warning:
- New coercion path [stype; K] : eparams >-> Sortclass is ambiguous with existing 
- [E] : eparams >-> Sortclass. [ambiguous-paths,typechecker]
- File "./Grassmann.v", line 10, characters 0-29:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope g_scope.". [undeclared-scope,deprecated]
- File "./Grassmann.v", line 111, characters 0-16:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 323, characters 0-19:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 332, characters 0-19:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 412, characters 0-21:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 428, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 721, characters 0-21:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 1144, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 1525, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 1877, characters 0-24:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 2323, characters 0-24:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 2895, characters 0-23:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 3045, characters 0-28:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 3148, characters 0-25:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 3656, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 3919, characters 0-23:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 4289, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./Grassmann.v", line 5023, characters 0-31:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope Gn_scope.". [undeclared-scope,deprecated]
-      = [[ X: 1, Y: 0, X**Y: 0]]
-      : vect p p
-      = [[ X: 0, Y: 1, X**Y: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, X**Y: 1]]
-      : Vect p
-      = [[ X: -1, Y: 1, X**Y: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, X**Y: 2]]
-      : Vect p
-      = [[ X: 1, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : vect p p
-      = [[ X: 0, Y: 1, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 1, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 1]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 1, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 1]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 2]]
-      : Vect p
-      = Some
-          ([[ X: 0, Y: 1, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-           :: nil)
-      : option (list (Vect p))
-      = Some
-          ([[ X: 0, Y: -1, Z: 1, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-           :: [[ X: -1, Y: -1, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-              :: nil)
-      : option (list (Vect p))
-      = Some
-          ([[ X: 0, Y: 0, Z: 1, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-           :: [[ X: 0, Y: 1, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-              :: [[ X: -1, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0,
-                 X**Y**Z: 0]] :: nil)
-      : option (list (Vect p))
-      = Some
-          ([[ X: 0, Y: 1, Z: 1, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-           :: [[ X: -1, Y: -1, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-              :: nil)
-      : option (list (Vect p))
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: -1]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 1, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: -1, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 1]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: 1]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: 0, Y**Z: 0 , X**Z: 0, X**Y**Z: -1]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, X**Y: -1, Y**Z: 0 , X**Z: 0, X**Y**Z: 0]]
-      : Vect p
-      = [[ X: 1, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : vect p p
-      = [[ X: 0, Y: 1, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 1, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 0, T: 1, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 1,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 2, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 1, X**T: 0, Y**Z: 1,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: -1, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 1, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: -1, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 1, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 1, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: -1, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: -1, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 1, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: -1, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 1, K: 0 ]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, X**Y: 0, X**Z: 0, X**T: 0, Y**Z: 0,
-        Y**T: 0, Z**T: 0, X**Y**Z: 0, X**Y**T: 0, X**Z**T: 0, Y**Z**T: 0,
-        X**Y**Z**T: 0, K: 0 ]]
-      : Vect p
-      = [[ X: 1, Y: 0, Z: 0, T: 0, U: 0, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: 0, K: 0]]
-      : vect p p
-      = [[ X: 0, Y: 1, Z: 0, T: 0, U: 0, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: 0, K: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 1, T: 0, U: 0, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: 0, K: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 0, T: 1, U: 0, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: 0, K: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, U: 1, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: 0, K: 0]]
-      : vect p p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, U: 0, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: 1, K: 0]]
-      : Vect p
-      = [[ X: 0, Y: 0, Z: 0, T: 0, U: 0, X**Y: 0, X**Z: 0, X**T: 0, X**U: 0,
-        Y**Z: 0, Y**T: 0, Y**U: 0, Z**T: 0, Z**U: 0, T**U: 0, X**Y**Z: 0,
-        X**Y**T: 0, X**Y**U: 0, X**Z**T: 0, X**Z**U: 0, X**T**U: 0,
-        Y**Z**T: 0, Y**Z**U: 0, Y**T**U: 0, Z**T**U: 0, X**Y**Z**T: 0,
-        X**Y**Z**U: 0, X**Y**T**U: 0, X**Z**T**U: 0, Y**Z**T**U: 0,
-        X**Y**Z**T**U: -1, K: 0]]
-      : Vect p
-      = (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 1)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : vect p p
-      = (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 1))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : vect p p
-      = (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 1)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : vect p p
-      = (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 1), (0, 0, (0, 0))))))
-      : vect p p
-      = (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 1, (0, 0))))))
-      : vect p p
-      = (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (1, 0))))))
-      : vect p p
-      = (2, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : Vect p
-      = (0, 1, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : Vect p
-      = (0, -1, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : Vect p
-      = (0, 0, (0, 2), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0)))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))),
-        (0, 0, (0, 0), (0, 0, (0, 0)), (0, 0, (0, 0), (0, 0, (0, 0))))))
-      : Vect p
- COQC G3.v
- COQC Clifford.v
- File "./Clifford.v", line 2, characters 0-46:
- Warning:
- New coercion path [stype; K] : eparams >-> Sortclass is ambiguous with existing 
- [E] : eparams >-> Sortclass. [ambiguous-paths,typechecker]
- File "./Clifford.v", line 12, characters 0-29:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope g_scope.". [undeclared-scope,deprecated]
- File "./Clifford.v", line 47, characters 0-23:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./G3.v", line 1, characters 0-78:
- Warning:
- New coercion path [stype; K] : eparams >-> Sortclass is ambiguous with existing 
- [E] : eparams >-> Sortclass. [ambiguous-paths,typechecker]
- File "./G3.v", line 580, characters 53-57:
- Error: The reference ring was not found in the current environment.
- 
- Makefile.coq:672: recipe for target 'G3.vo' failed
- make[1]: *** [G3.vo] Error 1
- Makefile.coq:326: recipe for target 'all' failed
- make: *** [all] Error 2
[ERROR] The compilation of coq-geometric-algebra failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4".
#=== ERROR while compiling coq-geometric-algebra.0.8.8 ========================#
# context              2.0.5 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-geometric-algebra.0.8.8
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code            2
# env-file             ~/.opam/log/coq-geometric-algebra-16075-865888.env
# output-file          ~/.opam/log/coq-geometric-algebra-16075-865888.out
### output ###
# [...]
# [implicit-core-hint-db,deprecated]
# File "./G3.v", line 1, characters 0-78:
# Warning:
# New coercion path [stype; K] : eparams >-> Sortclass is ambiguous with existing 
# [E] : eparams >-> Sortclass. [ambiguous-paths,typechecker]
# File "./G3.v", line 580, characters 53-57:
# Error: The reference ring was not found in the current environment.
# 
# Makefile.coq:672: recipe for target 'G3.vo' failed
# make[1]: *** [G3.vo] Error 1
# Makefile.coq:326: recipe for target 'all' failed
# make: *** [all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-geometric-algebra 0.8.8
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-geometric-algebra.0.8.8 coq.8.11.dev' failed.

Installation size

No files were installed.

Uninstall 🧹

Command
true
Return code
0
Missing removes
none
Wrong removes
none