« Up

corn 8.12.0 Error 🔥

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
camlp5              7.14        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-perl           2           Virtual package relying on perl
coq                 8.8.1       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.5       A library manager for OCaml
# 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-only"
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.7" & < "8.13~"}
  "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:2020-09-03"
]
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.12.0.tar.gz"
  checksum: "sha512=759ab0e0fc4b4ee8b6029d0090cf8b7ee731def85aacc9d240dfb29d4692e4f41821463f8d8180202587ee9b7c9239be8512c24b0594537e56aa235f31923ec3"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-corn.8.12.0 coq.8.8.1
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-corn.8.12.0 coq.8.8.1
Return code
0
Duration
10 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.8.12.0 coq.8.8.1
Return code
7936
Duration
26 m 0 s
Output
# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
camlp5              7.14        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-perl           2           Virtual package relying on perl
coq                 8.8.1       Formal proof management system
coq-bignums         8.8.0       Bignums, the Coq library of arbitrary large numbers
coq-math-classes    8.12.0      A library of abstract interfaces for mathematical structures in Coq
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.5       A library manager for OCaml
[NOTE] Package coq is already installed (current version is 8.8.1).
The following actions will be performed:
  - install coq-corn 8.12.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-corn.8.12.0: http]
[coq-corn.8.12.0] downloaded from https://github.com/coq-community/corn/archive/8.12.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.07.1/.opam-switch/build/coq-corn.8.12.0)
- ./configure.sh: 12: [: Illegal number: 8.1
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.07.1/.opam-switch/build/coq-corn.8.12.0)
- COQDEP VFILES
- 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 "./stdlib_omissions/P.v", line 4, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- File "./algebra/RSetoid.v", line 25, characters 0-55:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./algebra/RSetoid.v", line 25, characters 0-55:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC algebra/OperationClasses.v
- File "./util/Container.v", line 1, characters 0-54:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./util/Container.v", line 1, characters 0-54:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC tactics/DiffTactics1.v
- COQC logic/PropDecid.v
- COQC reals/fast/LazyNat.v
- COQC order/PartialOrder.v
- COQC metric2/Metric.v
- COQC stdlib_omissions/Z.v
- COQC util/PointFree.v
- COQC liouville/RingClass.v
- COQC stdlib_omissions/List.v
- COQC logic/CornBasics.v
- COQC util/SetoidPermutation.v
- COQC stdlib_omissions/Q.v
- File "./logic/CornBasics.v", line 73, characters 0-38:
- Warning: Option Automatic Coercions Import is deprecated
- [deprecated-option,deprecated]
- File "./logic/CornBasics.v", line 75, characters 0-34:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC logic/Classic.v
- File "./stdlib_omissions/Q.v", line 8, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC metric2/list_separates.v
- COQC raster/Raster.v
- COQC stdlib_omissions/N.v
- COQC logic/CLogic.v
- COQC util/Qdlog.v
- File "./logic/CLogic.v", line 54, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- File "./logic/CLogic.v", line 233, characters 0-103:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./util/Qdlog.v", line 2, characters 0-371:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./util/Qdlog.v", line 2, characters 0-371:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/Zmod/ZBasics.v
- COQC algebra/CSetoids.v
- File "./model/Zmod/ZBasics.v", line 39, characters 0-33:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./algebra/CSetoids.v", line 54, characters 0-33:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/structures/Nsec.v
- COQC tactics/AlgReflection.v
- File "./model/structures/Nsec.v", line 41, characters 0-33:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./tactics/AlgReflection.v", line 38, characters 0-33:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/structures/Zsec.v
- COQC model/setoids/Nfinsetoid.v
- File "./model/structures/Zsec.v", line 40, characters 0-33:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/structures/Npossec.v
- File "./model/setoids/Nfinsetoid.v", line 37, characters 0-37:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/Nfinsetoid.v", line 38, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC model/setoids/decsetoid.v
- COQC model/setoids/Zfinsetoid.v
- File "./model/setoids/decsetoid.v", line 7, characters 0-109:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/decsetoid.v", line 13, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- File "./model/setoids/Zfinsetoid.v", line 37, characters 0-37:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/Zfinsetoid.v", line 38, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC model/Zmod/ZDivides.v
- COQC algebra/CSetoidFun.v
- File "./model/Zmod/ZDivides.v", line 38, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/structures/Qsec.v
- File "./algebra/CSetoidFun.v", line 37, characters 0-37:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/structures/Qsec.v", line 43, characters 0-33:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/structures/Qsec.v", line 326, characters 0-6:
- Warning: Deprecated syntax; use "," as separator
- [firstorder-deprecated-syntax,deprecated]
- COQC algebra/CSetoidInc.v
- COQC tactics/csetoid_rewrite.v
- COQC model/setoids/Qsetoid.v
- File "./algebra/CSetoidInc.v", line 39, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/setoids/Zsetoid.v
- File "./tactics/csetoid_rewrite.v", line 48, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/Qsetoid.v", line 38, characters 0-42:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/setoids/Nsetoid.v
- COQC model/Zmod/ZGcd.v
- File "./model/setoids/Zsetoid.v", line 39, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC algebra/CSemiGroups.v
- File "./model/Zmod/ZGcd.v", line 38, characters 0-40:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/Nsetoid.v", line 38, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/Nsetoid.v", line 40, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC model/setoids/Npossetoid.v
- File "./algebra/CSemiGroups.v", line 40, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/setoids/Npossetoid.v", line 39, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/semigroups/Qsemigroup.v
- COQC model/semigroups/Zsemigroup.v
- File "./model/semigroups/Zsemigroup.v", line 37, characters 0-42:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/semigroups/Nsemigroup.v
- File "./model/semigroups/Qsemigroup.v", line 37, characters 0-42:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/semigroups/Nsemigroup.v", line 38, characters 0-40:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/semigroups/Npossemigroup.v
- COQC order/SemiLattice.v
- File "./model/semigroups/Npossemigroup.v", line 37, characters 0-40:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./order/SemiLattice.v", line 96, characters 2-9:
- Warning: Deprecated syntax; use "," as separator
- [firstorder-deprecated-syntax,deprecated]
- File "./order/SemiLattice.v", line 111, characters 1-8:
- Warning: Deprecated syntax; use "," as separator
- [firstorder-deprecated-syntax,deprec
[...] truncated
scope.
- [notation-overridden,parsing]
- File "./ode/metric.v", line 4, characters 0-322:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ode/metric.v", line 10, characters 0-58:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/monoids/CRmonoid.v
- COQC reals/RealFuncts.v
- File "./model/monoids/CRmonoid.v", line 26, characters 0-49:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/CSumsReals.v
- File "./reals/RealFuncts.v", line 37, characters 0-34:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/RealLists.v
- File "./reals/CSumsReals.v", line 37, characters 0-34:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/RealLists.v", line 37, characters 0-34:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/metric2/LinfMetric.v
- COQC reals/CMetricFields.v
- File "./model/metric2/LinfMetric.v", line 33, characters 0-46:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/CMetricFields.v", line 37, characters 0-34:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/CMetricFields.v", line 39, characters 0-26:
- Warning: There is no option Nested Proofs Allowed. [unknown-option,option]
- File "./reals/CMetricFields.v", line 146, characters 1-16:
- Warning: Nested proofs are deprecated and will stop working in a future Coq
- version [deprecated-nested-proofs,deprecated]
- COQC reals/Bridges_iso.v
- File "./reals/Bridges_iso.v", line 46, characters 0-38:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/fast/RasterQ.v
- COQC model/groups/CRgroup.v
- File "./model/groups/CRgroup.v", line 26, characters 0-43:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/CPoly_Contin.v
- File "./reals/CPoly_Contin.v", line 40, characters 0-37:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/Intervals.v
- File "./reals/Intervals.v", line 37, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/metric2/BoundedFunction.v
- File "./reals/Intervals.v", line 39, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC reals/fast/RasterizeQ.v
- COQC model/abgroups/CRabgroup.v
- File "./model/abgroups/CRabgroup.v", line 25, characters 0-41:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/IVT.v
- COQC model/metric2/IntegrableFunction.v
- File "./reals/IVT.v", line 37, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/fast/Plot.v
- COQC model/rings/CRring.v
- COQC ftc/PartFunEquality.v
- COQC metrics/CPseudoMSpaces.v
- File "./model/rings/CRring.v", line 26, characters 0-45:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ftc/PartFunEquality.v", line 39, characters 0-36:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC ode/FromMetric2.v
- File "./metrics/CPseudoMSpaces.v", line 37, characters 0-36:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC ode/BanachFixpoint.v
- File "./ode/FromMetric2.v", line 6, characters 0-244:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ode/FromMetric2.v", line 6, characters 0-244:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/fields/CRfield.v
- File "./ode/BanachFixpoint.v", line 4, characters 0-328:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ode/BanachFixpoint.v", line 4, characters 0-328:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ode/BanachFixpoint.v", line 7, characters 0-58:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ode/FromMetric2.v", line 101, characters 0-43:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- File "./ode/FromMetric2.v", line 138, characters 0-187:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- File "./ode/FromMetric2.v", line 138, characters 0-187:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/fields/CRfield.v", line 26, characters 0-39:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/OddPolyRootIR.v
- COQC metrics/ContFunctions.v
- File "./reals/OddPolyRootIR.v", line 37, characters 0-30:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./metrics/ContFunctions.v", line 37, characters 0-43:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/faster/ARQ.v
- File "./ode/FromMetric2.v", line 289, characters 0-11:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/faster/ARabs.v
- File "./reals/faster/ARQ.v", line 4, characters 0-352:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/faster/ARQ.v", line 4, characters 0-352:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/faster/ARsign.v
- COQC reals/faster/ARbigD.v
- File "./reals/faster/ARabs.v", line 4, characters 0-183:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/faster/ARabs.v", line 4, characters 0-183:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/faster/ARsign.v", line 4, characters 0-59:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/faster/ARsign.v", line 4, characters 0-59:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC model/ordfields/CRordfield.v
- File "./reals/faster/ARbigD.v", line 4, characters 0-460:
- Warning: Notation _ = _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./reals/faster/ARbigD.v", line 4, characters 0-460:
- Warning: Notation _ ≠ _ was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./model/ordfields/CRordfield.v", line 26, characters 0-41:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC reals/NRootIR.v
- File "./reals/NRootIR.v", line 40, characters 0-40:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- COQC ftc/FunctSums.v
- File "./ftc/FunctSums.v", line 41, characters 0-37:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./ftc/FunctSums.v", line 43, characters 0-27:
- Warning: Option Automatic Introduction is deprecated
- [deprecated-option,deprecated]
- COQC ftc/IntervalFunct.v
- File "./ftc/IntervalFunct.v", line 37, characters 0-40:
- Warning: Notation { _ : _ | _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- 
- Error: System error: "No space left on device"
- 
- make[1]: *** [Makefile:656: ftc/IntervalFunct.vo] Error 1
- make[1]: *** Waiting for unfinished jobs....
- 
- Error: System error: "No space left on device"
- 
- 
- Error: System error: "No space left on device"
- 
- make[1]: *** [Makefile:656: reals/NRootIR.vo] Error 1
- make[1]: *** [Makefile:656: ode/BanachFixpoint.vo] Error 1
- 
- Error: System error: "No space left on device"
- 
- make[1]: *** [Makefile:656: ftc/FunctSums.vo] Error 1
- make: *** [Makefile:318: 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.12.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-corn.8.12.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code            2
# env-file             ~/.opam/log/coq-corn-13969-2dea01.env
# output-file          ~/.opam/log/coq-corn-13969-2dea01.out
### output ###
# [...]
# Error: System error: "No space left on device"
# 
# 
# Error: System error: "No space left on device"
# 
# make[1]: *** [Makefile:656: reals/NRootIR.vo] Error 1
# make[1]: *** [Makefile:656: ode/BanachFixpoint.vo] Error 1
# 
# Error: System error: "No space left on device"
# 
# make[1]: *** [Makefile:656: ftc/FunctSums.vo] Error 1
# make: *** [Makefile:318: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-corn 8.12.0
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-corn.8.12.0 coq.8.8.1' 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