# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev The Coq Proof Assistant
coq-core dev The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib dev The Coq Proof Assistant -- Standard Library
coqide-server dev The Coq Proof Assistant, XML protocol server
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "b.a.w.spitters@gmail.com"
homepage: "https://github.com/coq-community/corn"
dev-repo: "git+https://github.com/coq-community/corn.git"
bug-reports: "https://github.com/coq-community/corn/issues"
license: "GPL-2.0"
synopsis: "The Coq Constructive Repository at Nijmegen."
description: """
CoRN includes the following parts:
- Algebraic Hierarchy
An axiomatic formalization of the most common algebraic
structures, including setoids, monoids, groups, rings,
fields, ordered fields, rings of polynomials, real and
complex numbers
- Model of the Real Numbers
Construction of a concrete real number structure
satisfying the previously defined axioms
- Fundamental Theorem of Algebra
A proof that every non-constant polynomial on the complex
plane has at least one root
- Real Calculus
A collection of elementary results on real analysis,
including continuity, differentiability, integration,
Taylor's theorem and the Fundamental Theorem of Calculus
- Exact Real Computation
Fast verified computation inside Coq. This includes: real numbers, functions,
integrals, graphs of functions, differential equations.
"""
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"coq" {(>= "8.14" & < "8.19~") | (= "dev")}
"coq-math-classes" {>= "8.8.1"}
"coq-bignums"
]
tags: [
"category:Mathematics/Algebra"
"category:Mathematics/Real Calculus and Topology"
"category:Mathematics/Exact Real computation"
"keyword:constructive mathematics"
"keyword:algebra"
"keyword:real calculus"
"keyword:real numbers"
"keyword:Fundamental Theorem of Algebra"
"logpath:CoRN"
"date:2023-10-16"
]
authors: [
"Evgeny Makarov"
"Robbert Krebbers"
"Eelis van der Weegen"
"Bas Spitters"
"Jelle Herold"
"Russell O'Connor"
"Cezary Kaliszyk"
"Dan Synek"
"Luís Cruz-Filipe"
"Milad Niqui"
"Iris Loeb"
"Herman Geuvers"
"Randy Pollack"
"Freek Wiedijk"
"Jan Zwanenburg"
"Dimitri Hendriks"
"Henk Barendregt"
"Mariusz Giero"
"Rik van Ginneken"
"Dimitri Hendriks"
"Sébastien Hinderer"
"Bart Kirkels"
"Pierre Letouzey"
"Lionel Mamane"
"Nickolay Shmyrev"
"Vincent Semeria"
]
url {
src: "https://github.com/coq-community/corn/archive/8.18.0.tar.gz"
checksum: "sha512=cd61c8314fcbec3b38429e94c77ff76caccfb38cbfbc95faf9bbe127f86756299d9744a288a36c4cf9c02e0a8701e57491eab0eab44747458bcbc021e8f3b408"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-corn.8.18.0 coq.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 4h opam install -y --deps-only coq-corn.8.18.0 coq.devopam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.8.18.0 coq.dev# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq dev The Coq Proof Assistant coq-bignums dev Bignums, the Coq library of arbitrary large numbers coq-core dev The Coq Proof Assistant -- Core Binaries and Tools coq-math-classes dev A library of abstract interfaces for mathematical structures in Coq. coq-stdlib dev The Coq Proof Assistant -- Standard Library coqide-server dev The Coq Proof Assistant, XML protocol server dune 3.12.1 Fast, portable, and opinionated build system ocaml 4.14.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.14.0 Official release 4.14.0 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.6 A library manager for OCaml zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-corn 8.18.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-corn.8.18.0: http] [coq-corn.8.18.0] downloaded from https://github.com/coq-community/corn/archive/8.18.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-corn: ./configure.sh] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/coq-corn.8.18.0) Processing 1/2: [coq-corn: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/coq-corn.8.18.0) - COQDEP VFILES - Warning: in file logic/CLogic.v, library - Coq.Arith.Div2 is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file logic/CornBasics.v, library - Coq.Arith.Even is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file logic/CornBasics.v, library - Coq.Arith.Max is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file logic/CornBasics.v, library - Coq.Arith.Min is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file metric2/Compact.v, library - Coq.Arith.Div2 is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file stdlib_omissions/Z.v, library - Coq.Numbers.Natural.Peano.NPeano is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file util/Qsums.v, library - Coq.Numbers.Natural.Peano.NPeano is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - Warning: in file ode/SimpleIntegration.v, library - Coq.Numbers.Natural.Peano.NPeano is required and has not been found in the loadpath! - [module-not-found,filesystem,default] - COQC tactics/CornTac.v - COQC stdlib_omissions/Pair.v - COQC tactics/Step.v - COQC algebra/RSetoid.v - COQC stdlib_omissions/P.v - COQC util/Container.v - File "./algebra/RSetoid.v", line 28, characters 0-55: - Warning: Notation "_ = _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./algebra/RSetoid.v", line 28, characters 0-55: - Warning: Notation "_ ≠ _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./algebra/RSetoid.v", line 83, characters 0-88: - Warning: Declaring a scope implicitly is deprecated; use in advance an - explicit "Declare Scope setoid_scope.". - [undeclared-scope,deprecated-since-8.10,deprecated,default] - File "./util/Container.v", line 1, characters 0-54: - Warning: Notation "_ = _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./util/Container.v", line 1, characters 0-54: - Warning: Notation "_ ≠ _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./util/Container.v", line 4, 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-since-8.10,deprecated,default] - COQC algebra/OperationClasses.v - COQC tactics/DiffTactics1.v - COQC logic/PropDecid.v - File "./stdlib_omissions/P.v", line 37, characters 0-42: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated-since-8.10,deprecated,default] - COQC reals/fast/LazyNat.v - COQC reals/stdlib/ConstructiveDiagonal.v - COQC reals/stdlib/Markov.v - COQC stdlib_omissions/List.v - COQC order/PartialOrder.v - File "./order/PartialOrder.v", line 55, characters 0-76: - Warning: Declaring a scope implicitly is deprecated; use in advance an - explicit "Declare Scope po_scope.". - [undeclared-scope,deprecated-since-8.10,deprecated,default] - File "./stdlib_omissions/List.v", line 30, characters 0-30: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated-since-8.10,deprecated,default] - File "./stdlib_omissions/List.v", line 73, characters 2-12: - Warning: - "auto with *" was used through the default "intuition_solver" tactic. - This will be replaced by just "auto" in the future. - [intuition-auto-with-star,deprecated-since-8.17,deprecated,default] - File "./stdlib_omissions/List.v", line 75, characters 1-11: - Warning: - "auto with *" was used through the default "intuition_solver" tactic. - This will be replaced by just "auto" in the future. - [intuition-auto-with-star,deprecated-since-8.17,deprecated,default] - File "./stdlib_omissions/List.v", line 152, characters 0-31: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated-since-8.10,deprecated,default] - File "./stdlib_omissions/List.v", line 154, characters 0-31: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated-since-8.10,deprecated,default] - COQC metric2/Metric.v - File "./reals/stdlib/ConstructiveDiagonal.v", line 288, characters 12-27: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - File "./reals/stdlib/ConstructiveDiagonal.v", line 288, characters 12-27: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - File "./reals/stdlib/ConstructiveDiagonal.v", line 301, characters 12-27: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - File "./reals/stdlib/ConstructiveDiagonal.v", line 301, characters 12-27: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - COQC stdlib_omissions/Z.v - File "./reals/stdlib/ConstructiveDiagonal.v", line 436, characters 8-23: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - File "./reals/stdlib/ConstructiveDiagonal.v", line 436, characters 8-23: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - File "./stdlib_omissions/Z.v", line 2, characters 0-90: - Error: Cannot find a physical path bound to logical path - Coq.Numbers.Natural.Peano.NPeano. - - make[1]: *** [Makefile:847: stdlib_omissions/Z.vo] Error 1 - make[1]: *** [stdlib_omissions/Z.vo] Deleting file 'stdlib_omissions/Z.glob' - make[1]: *** Waiting for unfinished jobs.... - File "./metric2/Metric.v", line 25, characters 0-54: - Warning: Notation "_ = _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./metric2/Metric.v", line 25, characters 0-54: - Warning: Notation "_ ≠ _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./metric2/Metric.v", line 26, characters 0-55: - Warning: Notation "_ ≠ _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./metric2/Metric.v", line 26, characters 0-55: - Warning: Notation "_ ≠ _" was already used in scope type_scope. - [notation-overridden,parsing,default] - File "./reals/stdlib/ConstructiveDiagonal.v", line 561, characters 43-58: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - File "./reals/stdlib/ConstructiveDiagonal.v", line 561, characters 43-58: - Warning: Notation Nat.div_le_mono is deprecated since 8.17. - Use Div0.div_le_mono instead. - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] - make: *** [Makefile:417: all] Error 2 [ERROR] The compilation of coq-corn failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-corn.8.18.0 ====================================# # context 2.0.10 | linux/x86_64 | ocaml-base-compiler.4.14.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/coq-corn.8.18.0 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-corn-28074-2dea01.env # output-file ~/.opam/log/coq-corn-28074-2dea01.out ### output ### # [...] # File "./metric2/Metric.v", line 26, characters 0-55: # Warning: Notation "_ ≠ _" was already used in scope type_scope. # [notation-overridden,parsing,default] # File "./reals/stdlib/ConstructiveDiagonal.v", line 561, characters 43-58: # Warning: Notation Nat.div_le_mono is deprecated since 8.17. # Use Div0.div_le_mono instead. # [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] # File "./reals/stdlib/ConstructiveDiagonal.v", line 561, characters 43-58: # Warning: Notation Nat.div_le_mono is deprecated since 8.17. # Use Div0.div_le_mono instead. # [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] # make: *** [Makefile:417: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-corn 8.18.0 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-corn.8.18.0 coq.dev' failed.
No files were installed.
true