« Up

interval 4.8.0 Error 🔥

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
coq                 8.11.2      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.09.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1      Official release 4.09.1
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.6       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "guillaume.melquiond@inria.fr"
homepage: "https://coqinterval.gitlabpages.inria.fr/"
dev-repo: "git+https://gitlab.inria.fr/coqinterval/interval.git"
bug-reports: "https://gitlab.inria.fr/coqinterval/interval/issues"
license: "CeCILL-C"
build: [
  ["autoconf"] {dev}
  ["./configure"]
  ["./remake" "-j%{jobs}%"]
]
install: ["./remake" "install"]
depends: [
  "coq" {>= "8.11" & < "8.18~"}
  "coq-bignums"
  "coq-flocq" {>= "3.1"}
  "coq-mathcomp-ssreflect" {>= "1.6"}
  "coq-coquelicot" {>= "3.0"}
  "conf-autoconf" {build & dev}
  ("conf-g++" {build} | "conf-clang" {build})
]
tags: [
  "keyword:interval arithmetic"
  "keyword:decision procedure"
  "keyword:floating-point arithmetic"
  "keyword:reflexive tactic"
  "keyword:Taylor models"
  "category:Mathematics/Real Calculus and Topology"
  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
  "logpath:Interval"
  "date:2023-07-20"
]
authors: [
  "Guillaume Melquiond <guillaume.melquiond@inria.fr>"
  "Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
  "Pierre Roux <pierre.roux@onera.fr>"
  "Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>"
]
synopsis: "A Coq tactic for proving bounds on real-valued expressions automatically"
url {
  src: "https://coqinterval.gitlabpages.inria.fr/releases/interval-4.8.0.tar.gz"
  checksum: "sha512=7dc5015226b2d91b00167df1ccdc8a01b40959eef03772bf0eaeddf1c717fefbb96c63a52259cd01d77135647f2187f2a99aedab2442c199ba5c13f109c8b274"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-interval.4.8.0 coq.8.11.2
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-interval.4.8.0 coq.8.11.2
Return code
0
Duration
16 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-interval.4.8.0 coq.8.11.2
Return code
7936
Duration
8 m 0 s
Output
# Packages matching: installed
# Name                 # Installed # Synopsis
base-bigarray          base
base-threads           base
base-unix              base
conf-findutils         1           Virtual package relying on findutils
conf-g++               1.0         Virtual package relying on the g++ compiler (for C++)
coq                    8.11.2      Formal proof management system
coq-bignums            8.11.0      Bignums, the Coq library of arbitrary large numbers
coq-coquelicot         3.2.0       A Coq formalization of real analysis compatible with the standard library
coq-flocq              3.4.3       A formalization of floating-point arithmetic for the Coq system
coq-mathcomp-ssreflect 1.14.0      Small Scale Reflection
num                    1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                  4.09.1      The OCaml compiler (virtual package)
ocaml-base-compiler    4.09.1      Official release 4.09.1
ocaml-config           1           OCaml Switch Configuration
ocamlfind              1.9.6       A library manager for OCaml
[NOTE] Package coq is already installed (current version is 8.11.2).
The following actions will be performed:
  - install coq-interval 4.8.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-interval.4.8.0: http]
[coq-interval.4.8.0] downloaded from https://coqinterval.gitlabpages.inria.fr/releases/interval-4.8.0.tar.gz
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-interval: ./configure]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-interval.4.8.0)
- checking for gcc... gcc
- checking whether the C compiler works... yes
- checking for C compiler default output file name... a.out
- checking for suffix of executables... 
- checking whether we are cross compiling... no
- checking for suffix of object files... o
- checking whether the compiler supports GNU C... 
- yes
- checking whether gcc accepts -g... yes
- checking for gcc option to enable C11 features... none needed
- checking how to run the C preprocessor... 
- gcc -E
- checking for coqc... /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc
- checking Coq version... 81102
- checking for coqdep... /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqdep
- checking for coqdoc... /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqdoc
- checking for ocamlfind... /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/ocamlfind
- checking for Flocq... 
- yes
- checking for Flocq >= 4.1... 
- no
- checking for primitive floats... 
- yes
- checking for Ssreflect... yes
- checking for MathComp version... 
- 1
- checking for Coquelicot... 
- yes
- checking for Bignums... 
- yes
- checking for native development files... yes
- checking for bytecode development files... yes
- checking for g++... g++
- checking whether the compiler supports GNU C++... yes
- checking whether g++ accepts -g... 
- yes
- checking for g++ option to enable C++11 features... none needed
- configure: building remake...
- /usr/bin/ld: /tmp/cczI28JT.o: in function `main':
- remake.cpp:(.text.startup+0xae0): warning: the use of `tempnam' is dangerous, better use `mkstemp'
- 
- === Summary ===
- Vernacular directory    /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Interval
- Plugin directory        /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Interval
- Primitive floats        yes
- Language tactics        no
- Plot tactic             native bytecode
- 
- configure: creating ./config.status
- config.status: creating Remakefile
- config.status: creating src/Plot.v
- config.status: creating src/Missing/Int63Compat.v
- config.status: creating src/Missing/MathComp1or2.v
Processing  1/2: [coq-interval: ./remake]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./remake" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-interval.4.8.0)
- Building src/Tactic_float.v
- Building src/Plot/interval_plot.ml
- Finished src/Tactic_float.v
- Building src/Tactic.vo
- Building src/Eval/Eval.vo
- Building src/Eval/Prog.vo
- Finished src/Plot/interval_plot.ml
- Building src/Eval/Reify.vo
- Building src/Eval/Tree.vo
- Building src/Float/Basic.vo
- Building src/Float/Generic.vo
- Building src/Float/Generic_ops.vo
- Building src/Float/Generic_proof.vo
- Building src/Float/Specific_bigint.vo
- Building src/Float/Specific_ops.vo
- Building src/Float/Specific_sig.vo
- Building src/Float/Specific_stdz.vo
- Building src/Float/Sig.vo
- Building src/Integral/Bertrand.vo
- Building src/Integral/Integral.vo
- Building src/Integral/Priority.vo
- Building src/Integral/Refine.vo
- Building src/Interval/Interval.vo
- Building src/Interval/Interval_compl.vo
- Building src/Interval/Float.vo
- Building src/Interval/Float_full.vo
- Building src/Interval/Transcend.vo
- Building src/Interval/Univariate_sig.vo
- Building src/Missing/Coquelicot.vo
- Building src/Missing/MathComp1.vo
- Building src/Missing/MathComp1or2.vo
- Building src/Missing/MathComp.vo
- Building src/Missing/Stdlib.vo
- Building src/Poly/Basic_rec.vo
- Building src/Poly/Bound.vo
- Building src/Poly/Bound_quad.vo
- Building src/Poly/Datatypes.vo
- Building src/Poly/Taylor_model.vo
- Building src/Poly/Taylor_model_sharp.vo
- Building src/Poly/Taylor_poly.vo
- Building src/Real/Taylor.vo
- Building src/Real/Xreal.vo
- Building src/Real/Xreal_derive.vo
- Building src/Tactics/Integral_helper.vo
- Building src/Tactics/Interval_helper.vo
- Building src/Tactics/Plot_helper.vo
- Building src/Tactics/Root_helper.vo
- Building src/Tactic_float.vo
- Building src/Plot/interval_plot.cmxs
- File "src/Plot/plot.c", line 22, characters 45-76:
- Alert deprecated: Coqlib.gen_reference_in_modules
- Please use Coqlib.lib_ref
- File "./src/Integral/Priority.v", line 21, characters 0-62:
- Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Priority.v", line 21, characters 0-62:
- Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Priority.v", line 21, characters 0-62:
- Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope
- fun_scope. [notation-overridden,parsing]
- File "./src/Integral/Priority.v", line 21, characters 0-62:
- Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Priority.v", line 21, characters 0-62:
- Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Priority.v", line 21, characters 0-62:
- Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope
- fun_scope. [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ + _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ - _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ <= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ >= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ > _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ < _ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ * _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Missing/MathComp1.v", line 24, characters 0-88:
- Warning: Notation "_ ^ _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- Finished src/Plot/interval_plot.cmxs
- Building src/Pl
[...] truncated
 _ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Bound_quad.v", line 25, characters 0-96:
- Warning: Notation "_ * _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Bound_quad.v", line 25, characters 0-96:
- Warning: Notation "_ ^ _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- Finished src/Poly/Bound_quad.vo
- File "./src/Poly/Taylor_model_sharp.v", line 1348, characters 4-45:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1357, characters 2-76:
- Warning: Duplicate clear of n [duplicate-clear,ssr]
- Finished src/Float/Specific_sig.vo
- File "./src/Poly/Taylor_model_sharp.v", line 1580, characters 4-45:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1682, characters 6-32:
- Warning: Duplicate clear of x [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1720, characters 4-48:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1742, characters 4-53:
- Warning: Duplicate clear of X [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1751, characters 2-28:
- Warning: Duplicate clear of E0 [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1854, characters 4-48:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 1963, characters 4-48:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 2055, characters 2-51:
- Warning: Duplicate clear of x [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 2170, characters 4-45:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- Finished src/Float/Specific_stdz.vo
- File "./src/Poly/Taylor_model_sharp.v", line 2312, characters 4-37:
- Warning: Duplicate clear of n [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 2423, characters 2-189:
- Warning: Duplicate clear of X [duplicate-clear,ssr]
- File "./src/Poly/Taylor_model_sharp.v", line 2426, characters 4-45:
- Warning: Duplicate clear of X0 [duplicate-clear,ssr]
- Finished src/Poly/Taylor_model_sharp.vo
- Finished src/Float/Specific_bigint.vo
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope
- fun_scope. [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ + _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ - _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ <= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ >= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ > _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ < _ < _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ * _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Poly/Taylor_model.v", line 21, characters 0-88:
- Warning: Notation "_ ^ _" was already used in scope nat_scope.
- [notation-overridden,parsing]
- File "./src/Float/Specific_ops.v", line 22, characters 0-47:
- Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Float/Specific_ops.v", line 22, characters 0-47:
- Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Float/Specific_ops.v", line 22, characters 0-47:
- Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope
- fun_scope. [notation-overridden,parsing]
- File "./src/Float/Specific_ops.v", line 22, characters 0-47:
- Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Float/Specific_ops.v", line 22, characters 0-47:
- Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Float/Specific_ops.v", line 22, characters 0-47:
- Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- Finished src/Float/Specific_ops.vo
- Finished src/Float/Generic_ops.vo
- Finished src/Eval/Tree.vo
- Finished src/Poly/Taylor_model.vo
- File "./src/Integral/Integral.v", line 22, characters 0-64:
- Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Integral.v", line 22, characters 0-64:
- Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Integral.v", line 22, characters 0-64:
- Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope
- fun_scope. [notation-overridden,parsing]
- File "./src/Integral/Integral.v", line 22, characters 0-64:
- Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Integral.v", line 22, characters 0-64:
- Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- File "./src/Integral/Integral.v", line 22, characters 0-64:
- Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope.
- [notation-overridden,parsing]
- Finished src/Eval/Prog.vo
- File "./src/Integral/Integral.v", line 583, characters 2-57:
- Warning: Duplicate clear of HPint [duplicate-clear,ssr]
- File "./src/Integral/Integral.v", line 742, characters 2-57:
- Warning: Duplicate clear of HPint [duplicate-clear,ssr]
- Finished src/Eval/Reify.vo
- Finished src/Integral/Integral.vo
- File "./src/Eval/Eval.v", line 523, characters 0-25:
- Warning: Duplicate clear of H [duplicate-clear,ssr]
- Finished src/Eval/Eval.vo
- Finished src/Tactics/Interval_helper.vo
- Finished src/Tactics/Root_helper.vo
- Finished src/Tactics/Plot_helper.vo
- Finished src/Tactics/Integral_helper.vo
- Finished src/Interval/Float.vo
- Finished src/Interval/Transcend.vo
- Finished src/Interval/Float_full.vo
- Finished src/Float/Primitive_ops.vo
- File "./src/Interval/Float_full_primfloat.v", line 42, characters 11-13:
- Error: Syntax Error: Lexer: Undefined token
- 
- Failed to build src/Interval/Float_full_primfloat.vo
- Failed to build all
- Failed to build src/Tactic_float.vo
- Failed to build src/Tactic.vo
[ERROR] The compilation of coq-interval failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build ./remake -j4".
#=== ERROR while compiling coq-interval.4.8.0 =================================#
# context              2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-interval.4.8.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j4
# exit-code            1
# env-file             ~/.opam/log/coq-interval-18456-2dea01.env
# output-file          ~/.opam/log/coq-interval-18456-2dea01.out
### output ###
# [...]
# Finished src/Tactics/Integral_helper.vo
# Finished src/Interval/Float.vo
# Finished src/Interval/Transcend.vo
# Finished src/Interval/Float_full.vo
# Finished src/Float/Primitive_ops.vo
# File "./src/Interval/Float_full_primfloat.v", line 42, characters 11-13:
# Error: Syntax Error: Lexer: Undefined token
# 
# Failed to build src/Interval/Float_full_primfloat.vo
# Failed to build all
# Failed to build src/Tactic_float.vo
# Failed to build src/Tactic.vo
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-interval 4.8.0
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-interval.4.8.0 coq.8.11.2' 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