# 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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-geometric-algebra.0.8.8 coq.8.11.devDry 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 2h opam install -y --deps-only coq-geometric-algebra.0.8.8 coq.8.11.devopam list; echo; ulimit -Sv 4000000; timeout 1h opam install -y -v coq-geometric-algebra.0.8.8 coq.8.11.dev# 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.
No files were installed.
true