Created
July 28, 2023 22:24
-
-
Save erikmd/c086e87301d337c70c68b5435e716e49 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [0KRunning with gitlab-runner 15.6.0~beta.186.ga889181a (a889181a)[0;m | |
| [0K on blue-3.shared.runners-manager.gitlab.com/default zxwgkjAP[0;m | |
| section_start:1668296743:prepare_executor | |
| [0K[0K[36;1mPreparing the "docker+machine" executor[0;m[0;m | |
| [0KUsing Docker executor with image docker:latest ...[0;m | |
| [0KStarting service docker:dind ...[0;m | |
| [0KPulling docker image docker:dind ...[0;m | |
| [0KUsing docker image sha256:5daac9489dc300a47bcb0ea96855ff17e5353aaab9065dbe19b890f480626683 for docker:dind with digest docker@sha256:659bd125658c3f2a28d1a51418853cf85c439df863e3eff0dcc3a0c30feadbb6 ...[0;m | |
| [0KWaiting for services to be up and running (timeout 30 seconds)...[0;m | |
| [0KPulling docker image docker:latest ...[0;m | |
| [0KUsing docker image sha256:adc767c402b48ba9eee78c8086eb1b66d77c2d903c43623638c2e6e7dfe22fb5 for docker:latest with digest docker@sha256:0b2c96ce1907a9df3505759cbc8a4af52bcb40e8a9dff18bb5809eb3a821414e ...[0;m | |
| section_end:1668296778:prepare_executor | |
| [0Ksection_start:1668296778:prepare_script | |
| [0K[0K[36;1mPreparing environment[0;m[0;m | |
| Running on runner-zxwgkjap-project-15404760-concurrent-0 via runner-zxwgkjap-shared-1668296705-7b710e92... | |
| section_end:1668296779:prepare_script | |
| [0Ksection_start:1668296779:get_sources | |
| [0K[0K[36;1mGetting source from Git repository[0;m[0;m | |
| [32;1m$ eval "$CI_PRE_CLONE_SCRIPT"[0;m | |
| [32;1mFetching changes with git depth set to 50...[0;m | |
| Initialized empty Git repository in /builds/erikmd/docker-coq-interval-primitive-floats/.git/ | |
| [32;1mCreated fresh repository.[0;m | |
| [32;1mChecking out cfff019d as master...[0;m | |
| [32;1mSkipping Git submodules setup[0;m | |
| section_end:1668296780:get_sources | |
| [0Ksection_start:1668296780:step_script | |
| [0K[0K[36;1mExecuting "step_script" stage of the job script[0;m[0;m | |
| [0KUsing docker image sha256:adc767c402b48ba9eee78c8086eb1b66d77c2d903c43623638c2e6e7dfe22fb5 for docker:latest with digest docker@sha256:0b2c96ce1907a9df3505759cbc8a4af52bcb40e8a9dff18bb5809eb3a821414e ...[0;m | |
| [32;1m$ docker pull "${IMAGE0}" || true[0;m | |
| Error response from daemon: manifest for registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-flambda-interval-4.5.2:latest not found: manifest unknown: manifest unknown | |
| [32;1m$ echo "${CI_JOB_TOKEN}" | docker login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}"[0;m | |
| WARNING! Your password will be stored unencrypted in /root/.docker/config.json. | |
| Configure a credential helper to remove this warning. See | |
| https://docs.docker.com/engine/reference/commandline/login/#credentials-store | |
| Login Succeeded | |
| [32;1m$ docker build "--cache-from=${IMAGE0}" "--build-arg=COQ_VERSION=${COQ_VERSION}" "--build-arg=MATHCOMP_VERSION=${MATHCOMP_VERSION}" "--build-arg=INTERVAL_VERSION=${INTERVAL_VERSION}" "--build-arg=INTERVAL_COMMIT=${INTERVAL_COMMIT}" "--build-arg=FLOCQ_VERSION=${FLOCQ_VERSION}" -t "${IMAGE}" .[0;m | |
| Sending build context to Docker daemon 3.584kB | |
| Step 1/9 : ARG COQ_VERSION="8.15" | |
| Step 2/9 : FROM coqorg/coq:${COQ_VERSION}-native-flambda | |
| 8.15-native-flambda: Pulling from coqorg/coq | |
| e9995326b091: Pulling fs layer | |
| 77f26ada63da: Pulling fs layer | |
| 3ac71a2c7352: Pulling fs layer | |
| 6da8a89e1f88: Pulling fs layer | |
| d1fdde637659: Pulling fs layer | |
| a9a294b71d9a: Pulling fs layer | |
| 6da8a89e1f88: Waiting | |
| d1fdde637659: Waiting | |
| a9a294b71d9a: Waiting | |
| 3ac71a2c7352: Verifying Checksum | |
| 3ac71a2c7352: Download complete | |
| 6da8a89e1f88: Verifying Checksum | |
| 6da8a89e1f88: Download complete | |
| e9995326b091: Verifying Checksum | |
| e9995326b091: Download complete | |
| 77f26ada63da: Verifying Checksum | |
| 77f26ada63da: Download complete | |
| d1fdde637659: Verifying Checksum | |
| d1fdde637659: Download complete | |
| a9a294b71d9a: Verifying Checksum | |
| a9a294b71d9a: Download complete | |
| e9995326b091: Pull complete | |
| 77f26ada63da: Pull complete | |
| 3ac71a2c7352: Pull complete | |
| 6da8a89e1f88: Pull complete | |
| d1fdde637659: Pull complete | |
| a9a294b71d9a: Pull complete | |
| Digest: sha256:672d70283e8a08f2c8f584ca5c4b0cc0572083c1db94783efcb79f7389785dd6 | |
| Status: Downloaded newer image for coqorg/coq:8.15-native-flambda | |
| ---> b5a23d41f591 | |
| Step 3/9 : ARG MATHCOMP_VERSION="dev" | |
| ---> Running in 94e597fe30d7 | |
| Removing intermediate container 94e597fe30d7 | |
| ---> db950709ef4a | |
| Step 4/9 : ARG INTERVAL_VERSION="dev" | |
| ---> Running in 95091a56d5a4 | |
| Removing intermediate container 95091a56d5a4 | |
| ---> dcacd080490c | |
| Step 5/9 : ARG INTERVAL_COMMIT="" | |
| ---> Running in 5a53065b7617 | |
| Removing intermediate container 5a53065b7617 | |
| ---> 633b66c03c42 | |
| Step 6/9 : ARG FLOCQ_VERSION="" | |
| ---> Running in 7b38c44d738e | |
| Removing intermediate container 7b38c44d738e | |
| ---> add149cb0a0e | |
| Step 7/9 : WORKDIR /home/coq | |
| ---> Running in a75f94e2ccda | |
| Removing intermediate container a75f94e2ccda | |
| ---> 5a023e36d289 | |
| Step 8/9 : RUN ["/bin/bash", "--login", "-c", "set -x && opam config list; opam repo list; opam list && if [ -n \"${FLOCQ_VERSION}\" ]; then opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev; fi && opam update -y && opam pin add -n -y -k version coq-mathcomp-ssreflect ${MATHCOMP_VERSION} && if [ -n \"${FLOCQ_VERSION}\" ]; then opam pin add -n -y -k version coq-flocq ${FLOCQ_VERSION}; fi && if [ -n \"${INTERVAL_COMMIT}\" ]; then opam pin add -n -y -k git coq-interval.${INTERVAL_VERSION} \"git+https://gitlab.inria.fr/coqinterval/interval.git#${INTERVAL_COMMIT}\"; else opam pin add -n -y -k version coq-interval ${INTERVAL_VERSION}; fi && ulimit -s && ulimit -s 32768 && ulimit -s && opam install -y -v -j ${NJOBS} coq-interval"] | |
| ---> Running in 85205362c905 | |
| [91m+ opam config list | |
| [0m | |
| <><> Global opam variables ><><><><><><><><><><><><><><><><><><><><><><><><><><> | |
| arch x86_64 # Inferred from system | |
| exe # Suffix needed for executable filenames (Windows) | |
| jobs 1 # The number of parallel jobs set up in opam configuration | |
| make make # The 'make' command to use | |
| opam-version 2.1.3 # The currently running opam version | |
| os linux # Inferred from system | |
| os-distribution debian # Inferred from system | |
| os-family debian # Inferred from system | |
| os-version 11 # Inferred from system | |
| root /home/coq/.opam # The current opam root directory | |
| switch 4.07.1+flambda # The identifier of the current switch | |
| sys-ocaml-arch # Target architecture of the OCaml compiler present on your system | |
| sys-ocaml-cc # Host C Compiler type of the OCaml compiler present on your system | |
| sys-ocaml-libc # Host C Runtime Library type of the OCaml compiler present on your system | |
| sys-ocaml-version # OCaml version present on your system independently of opam, if any | |
| <><> Configuration variables from the current switch ><><><><><><><><><><><><><> | |
| prefix /home/coq/.opam/4.07.1+flambda | |
| lib /home/coq/.opam/4.07.1+flambda/lib | |
| bin /home/coq/.opam/4.07.1+flambda/bin | |
| sbin /home/coq/.opam/4.07.1+flambda/sbin | |
| share /home/coq/.opam/4.07.1+flambda/share | |
| doc /home/coq/.opam/4.07.1+flambda/doc | |
| etc /home/coq/.opam/4.07.1+flambda/etc | |
| man /home/coq/.opam/4.07.1+flambda/man | |
| toplevel /home/coq/.opam/4.07.1+flambda/lib/toplevel | |
| stublibs /home/coq/.opam/4.07.1+flambda/lib/stublibs | |
| user coq | |
| group coq | |
| <><> Package variables ('opam var --package PKG' to show) <><><><><><><><><><><> | |
| PKG:name # Name of the package | |
| PKG:version # Version of the package | |
| PKG:depends # Resolved direct dependencies of the package | |
| PKG:installed # Whether the package is installed | |
| PKG:enable # Takes the value "enable" or "disable" depending on whether the package is installed | |
| PKG:pinned # Whether the package is pinned | |
| PKG:bin # Binary directory for this package | |
| PKG:sbin # System binary directory for this package | |
| PKG:lib # Library directory for this package | |
| PKG:man # Man directory for this package | |
| PKG:doc # Doc directory for this package | |
| PKG:share # Share directory for this package | |
| PKG:etc # Etc directory for this package | |
| PKG:build # Directory where the package was built | |
| PKG:hash # Hash of the package archive | |
| PKG:dev # True if this is a development package | |
| PKG:build-id # A hash identifying the precise package version with all its dependencies | |
| PKG:opamfile # Path of the curent opam file | |
| [91m+ opam repo list | |
| [0m[91m[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories. | |
| [0m | |
| <><> Repository configuration for switch 4.07.1+flambda <><><><><><><><><><><><> | |
| 1 coq-released https://coq.inria.fr/opam/released | |
| 2 default https://opam.ocaml.org | |
| [91m+ opam list | |
| [0m# Packages matching: installed | |
| # Name # Installed # Synopsis | |
| base v0.14.0 Full standard library replacement for OCaml | |
| base-bigarray base | |
| base-threads base | |
| base-unix base | |
| cmdliner 1.0.4 Declarative definition of command line interfaces for OCaml | |
| conf-findutils 1 Virtual package relying on findutils | |
| conf-gmp 4 Virtual package relying on a GMP lib system installation | |
| coq 8.15.2 pinned to version 8.15.2 | |
| coq-bignums 8.15.0 Bignums, the Coq library of arbitrary large numbers | |
| coq-native 1 Package flag enabling coq's native-compiler flag | |
| coq-serapi 8.15.0+0.15.1 Serialization library and protocol for machine interaction with the Coq proof assistant | |
| cppo 1.6.9 Code preprocessor like cpp for OCaml | |
| csexp 1.5.1 Parsing and printing of S-expressions in Canonical form | |
| dune 3.5.0 pinned to version 3.5.0 | |
| dune-configurator 3.5.0 Helper library for gathering system configuration | |
| num 1.4 pinned to version 1.4 | |
| ocaml 4.07.1 The OCaml compiler (virtual package) | |
| ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged | |
| ocaml-config 1 OCaml Switch Configuration | |
| ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler | |
| ocaml-variants 4.07.1+flambda Official release 4.07.1, with flambda activated | |
| ocamlfind 1.9.1 pinned to version 1.9.1 | |
| ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind | |
| opam-depext 1.2.1-1 Install OS distribution packages | |
| parsexp v0.14.2 S-expression parsing library | |
| ppx_derivers 1.2.1 Shared [@@deriving] plugin registry | |
| ppx_deriving 5.2.1 Type-driven code generation for OCaml | |
| ppx_deriving_yojson 3.6.1 JSON codec generator for OCaml | |
| ppx_import 1.9.1 A syntax extension for importing declarations from interface files | |
| ppx_sexp_conv v0.14.3 [@@deriving] plugin to generate S-expression conversion functions | |
| ppxlib 0.25.1 Standard library for ppx rewriters | |
| result 1.5 Compatibility Result module | |
| seq base Compatibility package for OCaml's standard iterator type starting from 4.07. | |
| sexplib v0.14.0 Library for serializing OCaml values to and from S-expressions | |
| sexplib0 v0.14.0 Library containing the definition of S-expressions and some base converters | |
| stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler | |
| yojson 2.0.2 Yojson is an optimized parsing and printing library for the JSON format | |
| zarith 1.12 pinned to version 1.12 | |
| [91m+ '[' -n '' ']' | |
| [0m[91m+ opam update -y | |
| [0m | |
| <><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><> | |
| [coq-released] synchronised from https://coq.inria.fr/opam/released | |
| [default] synchronised from https://opam.ocaml.org | |
| Now run 'opam upgrade' to apply any package updates. | |
| [91m+ opam pin add -n -y -k version coq-mathcomp-ssreflect 1.15.0 | |
| [0mcoq-mathcomp-ssreflect is now pinned to version 1.15.0 | |
| [91m+ '[' -n '' ']' | |
| [0m[91m+ '[' -n '' ']' | |
| [0m[91m+ opam pin add -n -y -k version coq-interval 4.5.2 | |
| [0mcoq-interval is now pinned to version 4.5.2 | |
| [91m+ ulimit -s | |
| [0m8192 | |
| [91m+ ulimit -s 32768 | |
| [0m[91m+ ulimit -s | |
| [0m32768 | |
| [91m+ opam install -y -v -j 2 coq-interval | |
| [0mThe following actions will be performed: | |
| - install conf-g++ 1.0 [required by coq-interval] | |
| - install coq-mathcomp-ssreflect 1.15.0* [required by coq-interval] | |
| - install coq-flocq 4.1.0 [required by coq-interval] | |
| - install coq-coquelicot 3.2.0 [required by coq-interval] | |
| - install coq-interval 4.5.2* | |
| ===== 5 to install ===== | |
| <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> | |
| Processing 2/15: [coq-coquelicot.3.2.0: http] | |
| Processing 3/15: [coq-coquelicot.3.2.0: http] [coq-flocq.4.1.0: http] | |
| Processing 4/15: [coq-coquelicot.3.2.0: http] [coq-flocq.4.1.0: http] [coq-interval.4.5.2: http] | |
| Processing 5/15: [coq-coquelicot.3.2.0: http] [coq-flocq.4.1.0: http] [coq-interval.4.5.2: http] [conf-g++: g++] | |
| Processing 5/15: [coq-flocq.4.1.0: http] [coq-interval.4.5.2: http] [conf-g++: g++] | |
| Processing 5/15: [coq-interval.4.5.2: http] [conf-g++: g++] | |
| Processing 5/15: [conf-g++: g++] | |
| - g++ (Debian 10.2.1-6) 10.2.1 20210110 | |
| - Copyright (C) 2020 Free Software Foundation, Inc. | |
| - This is free software; see the source for copying conditions. There is NO | |
| - warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. | |
| - | |
| -> compiled conf-g++.1.0 | |
| Processing 5/15: | |
| -> installed conf-g++.1.0 | |
| Processing 6/15: | |
| -> retrieved coq-coquelicot.3.2.0 (https://coquelicot.gitlabpages.inria.fr/releases/coquelicot-3.2.0.tar.gz) | |
| Processing 7/15: [coq-mathcomp-ssreflect.1.15.0: http] | |
| -> retrieved coq-flocq.4.1.0 (https://flocq.gitlabpages.inria.fr/releases/flocq-4.1.0.tar.gz) | |
| Processing 8/15: [coq-mathcomp-ssreflect.1.15.0: http] [coq-flocq: ./configure] | |
| -> retrieved coq-interval.4.5.2 (https://coqinterval.gitlabpages.inria.fr/releases/interval-4.5.2.tar.gz) | |
| Processing 8/15: [coq-flocq: ./configure] | |
| -> retrieved coq-mathcomp-ssreflect.1.15.0 (https://github.com/math-comp/math-comp/archive/mathcomp-1.15.0.tar.gz) | |
| Processing 9/15: [coq-flocq: ./configure] [coq-mathcomp-ssreflect: make 2] | |
| - checking for coqc... /home/coq/.opam/4.07.1+flambda/bin/coqc | |
| - checking Coq version... 8.15.2 | |
| - checking for coqdep... /home/coq/.opam/4.07.1+flambda/bin/coqdep | |
| - checking for coqdoc... /home/coq/.opam/4.07.1+flambda/bin/coqdoc | |
| - checking for g++... g++ | |
| - 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 we are using the GNU C++ compiler... yes | |
| - checking whether g++ accepts -g... yes | |
| - configure: building remake... | |
| - /usr/bin/ld: /tmp/ccgIQRZ2.o: in function `main': | |
| - remake.cpp:(.text.startup+0xb87): warning: the use of `tempnam' is dangerous, better use `mkstemp' | |
| - configure: creating ./config.status | |
| - config.status: creating Remakefile | |
| - config.status: creating src/Version.v | |
| - config.status: creating src/IEEE754/Int63Compat.v | |
| Processing 9/15: [coq-flocq: ./remake] [coq-mathcomp-ssreflect: make 2] | |
| - make: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-mathcomp-ssreflect.1.15.0/mathcomp/ssreflect' | |
| - /home/coq/.opam/4.07.1+flambda/bin/coq_makefile -f Make -o Makefile.coq | |
| - /usr/bin/make -f Makefile.coq --no-print-directory | |
| - COQDEP VFILES | |
| - COQC ssreflect.v | |
| - COQC ssrnotations.v | |
| - COQNATIVE ssrnotations.vo | |
| - File "./ssreflect.v", line 81, characters 0-93: | |
| - Warning: The default value for hint locality is currently "local" in a | |
| - section and "global" otherwise, but is scheduled to change in a future | |
| - release. For the time being, adding hints outside of sections without | |
| - specifying an explicit locality attribute is therefore deprecated. It is | |
| - recommended to use "export" whenever possible. Use the attributes #[local], | |
| - #[global] and #[export] depending on your choice. For example: "#[export] | |
| - Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated] | |
| - COQNATIVE ssreflect.vo | |
| - COQC ssrmatching.v | |
| - COQC ssrfun.v | |
| - COQNATIVE ssrmatching.vo | |
| - COQNATIVE ssrfun.vo | |
| - COQC ssrbool.v | |
| - COQNATIVE ssrbool.vo | |
| - COQC eqtype.v | |
| - COQNATIVE eqtype.vo | |
| - COQC ssrnat.v | |
| - COQNATIVE ssrnat.vo | |
| - COQC seq.v | |
| - COQNATIVE seq.vo | |
| - COQC choice.v | |
| - COQC path.v | |
| - COQNATIVE choice.vo | |
| - COQC div.v | |
| - COQNATIVE path.vo | |
| - COQNATIVE div.vo | |
| - COQC fintype.v | |
| - COQNATIVE fintype.vo | |
| - COQC fingraph.v | |
| - COQC tuple.v | |
| - COQNATIVE tuple.vo | |
| - COQC generic_quotient.v | |
| - COQNATIVE fingraph.vo | |
| - COQNATIVE generic_quotient.vo | |
| - COQC finfun.v | |
| - COQNATIVE finfun.vo | |
| - COQC bigop.v | |
| - COQNATIVE bigop.vo | |
| - COQC prime.v | |
| - COQC finset.v | |
| - COQNATIVE prime.vo | |
| - COQC ssrAC.v | |
| - COQNATIVE finset.vo | |
| - COQNATIVE ssrAC.vo | |
| - COQC order.v | |
| - COQC binomial.v | |
| - COQNATIVE binomial.vo | |
| - COQNATIVE order.vo | |
| - COQC all_ssreflect.v | |
| - COQNATIVE all_ssreflect.vo | |
| - make: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-mathcomp-ssreflect.1.15.0/mathcomp/ssreflect' | |
| -> compiled coq-mathcomp-ssreflect.1.15.0 | |
| Processing 9/15: [coq-flocq: ./remake] | |
| Processing 10/15: [coq-flocq: ./remake] [coq-mathcomp-ssreflect: make install] | |
| - make: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-mathcomp-ssreflect.1.15.0/mathcomp/ssreflect' | |
| - /home/coq/.opam/4.07.1+flambda/bin/coq_makefile -f Make -o Makefile.coq | |
| - /usr/bin/make -f Makefile.coq --no-print-directory install | |
| - INSTALL all_ssreflect.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL eqtype.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL seq.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrAC.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrbool.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssreflect.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrfun.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrnat.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL bigop.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL binomial.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL choice.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL div.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL finfun.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL fingraph.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL finset.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL fintype.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL generic_quotient.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL path.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL prime.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL tuple.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrnotations.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrmatching.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL order.vo /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL all_ssreflect.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL eqtype.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL seq.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrAC.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrbool.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssreflect.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrfun.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrnat.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL bigop.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL binomial.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL choice.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL div.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL finfun.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL fingraph.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL finset.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL fintype.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL generic_quotient.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL path.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL prime.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL tuple.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrnotations.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrmatching.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL order.v /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL all_ssreflect.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL eqtype.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL seq.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrAC.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrbool.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssreflect.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrfun.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrnat.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL bigop.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL binomial.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL choice.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL div.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL finfun.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL fingraph.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL finset.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL fintype.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL generic_quotient.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL path.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL prime.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL tuple.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrnotations.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ssrmatching.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL order.glob /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect/ | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_all_ssreflect.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_eqtype.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_seq.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrAC.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrbool.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssreflect.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrfun.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrnat.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_bigop.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_binomial.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_choice.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_div.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_finfun.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_fingraph.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_finset.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_fintype.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_generic_quotient.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_path.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_prime.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_tuple.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrnotations.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrmatching.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_order.cmi /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_all_ssreflect.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_eqtype.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_seq.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrAC.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrbool.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssreflect.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrfun.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrnat.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_bigop.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_binomial.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_choice.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_div.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_finfun.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_fingraph.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_finset.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_fintype.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_generic_quotient.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_path.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_prime.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_tuple.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrnotations.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrmatching.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_order.cmx /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_all_ssreflect.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_eqtype.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_seq.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrAC.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrbool.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssreflect.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrfun.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrnat.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_bigop.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_binomial.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_choice.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_div.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_finfun.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_fingraph.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_finset.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_fintype.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_generic_quotient.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_path.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_prime.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_tuple.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrnotations.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_ssrmatching.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - INSTALL ./.coq-native/Nmathcomp_ssreflect_order.cmxs /home/coq/.opam/4.07.1+flambda/lib/coq//user-contrib/mathcomp/ssreflect//.coq-native | |
| - make: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-mathcomp-ssreflect.1.15.0/mathcomp/ssreflect' | |
| -> installed coq-mathcomp-ssreflect.1.15.0 | |
| Processing 10/15: [coq-flocq: ./remake] | |
| Processing 11/15: [coq-coquelicot: ./configure] [coq-flocq: ./remake] | |
| - Building src/Version.vo | |
| - Building src/Core/Raux.vo | |
| - Building src/Core/Zaux.vo | |
| - Finished src/Version.vo | |
| - Building src/Core/Defs.vo | |
| - Building src/Core/Digits.vo | |
| - Building src/Core/Float_prop.vo | |
| - Building src/Core/FIX.vo | |
| - Building src/Core/Generic_fmt.vo | |
| - Building src/Core/Round_pred.vo | |
| - Building src/Core/Round_NE.vo | |
| - Building src/Core/Ulp.vo | |
| - Building src/Core/FLT.vo | |
| - Building src/Core/FLX.vo | |
| - Building src/Core/FTZ.vo | |
| - Finished src/Core/Zaux.vo | |
| - Finished src/Core/Raux.vo | |
| - Finished src/Core/Digits.vo | |
| - Building src/Core/Core.vo | |
| - Building src/Calc/Bracket.vo | |
| - Building src/Calc/Div.vo | |
| - Building src/Calc/Operations.vo | |
| - Building src/Calc/Plus.vo | |
| - Building src/Calc/Round.vo | |
| - Building src/Calc/Sqrt.vo | |
| - Building src/Prop/Div_sqrt_error.vo | |
| - Finished src/Core/Defs.vo | |
| - Building src/Prop/Mult_error.vo | |
| - Building src/Prop/Plus_error.vo | |
| - Building src/Prop/Relative.vo | |
| - Building src/Prop/Sterbenz.vo | |
| - Finished src/Core/Round_pred.vo | |
| - Building src/Prop/Round_odd.vo | |
| - Finished src/Core/Float_prop.vo | |
| - Finished src/Calc/Operations.vo | |
| - Finished src/Calc/Bracket.vo | |
| - Building src/Prop/Double_rounding.vo | |
| - Building src/IEEE754/BinarySingleNaN.vo | |
| - Building src/IEEE754/Binary.vo | |
| - Building src/IEEE754/Bits.vo | |
| - Building src/IEEE754/Int63Compat.vo | |
| - Building src/IEEE754/Int63Copy.vo | |
| - Finished src/IEEE754/Int63Copy.vo | |
| - Finished src/Core/Generic_fmt.vo | |
| - Finished src/IEEE754/Int63Compat.vo | |
| - Finished src/Prop/Sterbenz.vo | |
| - Finished src/Calc/Sqrt.vo | |
| - Finished src/Calc/Div.vo | |
| - Building src/IEEE754/PrimFloat.vo | |
| - Building src/Pff/Pff.vo | |
| - Finished src/Core/Ulp.vo | |
| - Finished src/Core/Round_NE.vo | |
| - Finished src/Core/FIX.vo | |
| - Finished src/Core/FLX.vo | |
| - Finished src/Core/FTZ.vo | |
| - Finished src/Core/FLT.vo | |
| - Finished src/Core/Core.vo | |
| - Finished src/Prop/Double_rounding.vo | |
| - Finished src/Prop/Round_odd.vo | |
| - Finished src/Prop/Relative.vo | |
| - Finished src/Prop/Plus_error.vo | |
| - Finished src/Prop/Mult_error.vo | |
| - Finished src/Prop/Div_sqrt_error.vo | |
| - Finished src/Calc/Round.vo | |
| - Finished src/IEEE754/BinarySingleNaN.vo | |
| - File "./src/IEEE754/PrimFloat.v", line 271, characters 10-15: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18: | |
| - Warning: Notation ldexp_spec is deprecated since 8.15.0. | |
| - Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18: | |
| - Warning: Notation ldexp_spec is deprecated since 8.15.0. | |
| - Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18: | |
| - Warning: Notation ldexp_spec is deprecated since 8.15.0. | |
| - Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 305, characters 16-21: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 309, characters 12-22: | |
| - Warning: Notation frexp_spec is deprecated since 8.15.0. | |
| - Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 309, characters 12-22: | |
| - Warning: Notation frexp_spec is deprecated since 8.15.0. | |
| - Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 310, characters 9-14: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 332, characters 0-13: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 332, characters 0-13: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 364, characters 5-10: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 364, characters 5-10: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 381, characters 14-24: | |
| - Warning: Notation frexp_spec is deprecated since 8.15.0. | |
| - Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 381, characters 14-24: | |
| - Warning: Notation frexp_spec is deprecated since 8.15.0. | |
| - Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 383, characters 7-12: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 383, characters 7-12: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57: | |
| - Warning: Notation ldexp_spec is deprecated since 8.15.0. | |
| - Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57: | |
| - Warning: Notation ldexp_spec is deprecated since 8.15.0. | |
| - Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57: | |
| - Warning: Notation ldexp_spec is deprecated since 8.15.0. | |
| - Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 513, characters 10-18: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 519, characters 8-21: | |
| - Warning: Notation of_int63_spec is deprecated since 8.14. | |
| - Use of_uint63_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 519, characters 8-21: | |
| - Warning: Notation of_int63_spec is deprecated since 8.14. | |
| - Use of_uint63_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./src/IEEE754/PrimFloat.v", line 519, characters 8-21: | |
| - Warning: Notation of_int63_spec is deprecated since 8.14. | |
| - Use of_uint63_spec instead. [deprecated-syntactic-definition,deprecated] | |
| - Finished src/IEEE754/PrimFloat.vo | |
| - Finished src/IEEE754/Binary.vo | |
| - Finished src/IEEE754/Bits.vo | |
| - Finished src/Calc/Plus.vo | |
| - Building src/Pff/Pff2FlocqAux.vo | |
| - Building src/Pff/Pff2Flocq.vo | |
| - Finished src/Pff/Pff.vo | |
| - Finished src/Pff/Pff2FlocqAux.vo | |
| - Finished src/Pff/Pff2Flocq.vo | |
| - Building all | |
| - Finished all | |
| -> compiled coq-flocq.4.1.0 | |
| Processing 11/15: [coq-coquelicot: ./configure] | |
| Processing 12/15: [coq-coquelicot: ./configure] [coq-flocq: ./remake install] | |
| - checking for coqc... /home/coq/.opam/4.07.1+flambda/bin/coqc | |
| - checking for coqdep... /home/coq/.opam/4.07.1+flambda/bin/coqdep | |
| - checking for coqdoc... /home/coq/.opam/4.07.1+flambda/bin/coqdoc | |
| - checking for SSReflect... yes | |
| - checking for g++... g++ | |
| - 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 we are using the GNU C++ compiler... yes | |
| - checking whether g++ accepts -g... yes | |
| - configure: building remake... | |
| - /usr/bin/ld: /tmp/ccnAlpsV.o: in function `main': | |
| - remake.cpp:(.text.startup+0xb87): warning: the use of `tempnam' is dangerous, better use `mkstemp' | |
| - configure: creating ./config.status | |
| - config.status: creating Remakefile | |
| Processing 12/15: [coq-coquelicot: ./remake] [coq-flocq: ./remake install] | |
| - Building install | |
| - Finished install | |
| -> installed coq-flocq.4.1.0 | |
| Processing 12/15: [coq-coquelicot: ./remake] | |
| + /home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-coquelicot.3.2.0/./remake "-j2" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-coquelicot.3.2.0) | |
| - Building theories/AutoDerive.vo | |
| - Building theories/Compactness.vo | |
| - Building theories/Rcomplements.vo | |
| - Building theories/Continuity.vo | |
| - Building theories/Hierarchy.vo | |
| - Building theories/Iter.vo | |
| - Building theories/Lub.vo | |
| - Building theories/Markov.vo | |
| - Building theories/Rbar.vo | |
| - Building theories/Lim_seq.vo | |
| - Building theories/Derive.vo | |
| - Building theories/Equiv.vo | |
| - Building theories/Derive_2d.vo | |
| - Building theories/ElemFct.vo | |
| - Building theories/PSeries.vo | |
| - Building theories/Seq_fct.vo | |
| - File "./theories/Rcomplements.v", line 660, characters 2-37: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Rcomplements.v", line 676, characters 2-20: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - Building theories/Series.vo | |
| - Building theories/RInt.vo | |
| - Building theories/SF_seq.vo | |
| - Building theories/RInt_analysis.vo | |
| - Building theories/Complex.vo | |
| - Building theories/Coquelicot.vo | |
| - File "./theories/Rcomplements.v", line 1383, characters 2-54: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - Building theories/RInt_gen.vo | |
| - File "./theories/Rcomplements.v", line 1413, characters 2-54: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - File "./theories/Rcomplements.v", line 1434, characters 2-49: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Rcomplements.v", line 1439, characters 2-26: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - Building theories/KHInt.vo | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1637, characters 19-28: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1638, characters 24-34: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1637, characters 19-28: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1638, characters 24-34: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1637, characters 19-28: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1630, characters 2-460: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1638, characters 24-34: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1656, characters 35-48: | |
| - Warning: Notation RList.Rlength is deprecated since 8.12. | |
| - use List.length instead [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1657, characters 19-29: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1657, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1658, characters 21-31: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1658, characters 36-46: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1666, characters 35-45: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Rcomplements.v", line 1666, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - Finished theories/Rcomplements.vo | |
| - File "./theories/Rbar.v", line 49, characters 0-27: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished theories/Markov.vo | |
| - File "./theories/Iter.v", line 187, characters 12-20: | |
| - Warning: Notation iota_add is deprecated since mathcomp 1.13.0. | |
| - Use iotaD instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Iter.v", line 187, characters 12-20: | |
| - Warning: Notation iota_add is deprecated since mathcomp 1.13.0. | |
| - Use iotaD instead. [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Iter.v", line 187, characters 12-20: | |
| - Warning: Notation iota_add is deprecated since mathcomp 1.13.0. | |
| - Use iotaD instead. [deprecated-syntactic-definition,deprecated] | |
| - Finished theories/Iter.vo | |
| - Finished theories/Rbar.vo | |
| - File "./theories/Lub.v", line 24, characters 0-40: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished theories/Compactness.vo | |
| - Finished theories/Lub.vo | |
| - File "./theories/Hierarchy.v", line 24, characters 0-49: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/Hierarchy.v", line 1917, characters 0-47: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 1940, characters 0-77: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2169, characters 0-20: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2183, characters 0-25: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2188, characters 0-25: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2397, characters 2-41: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2422, characters 2-37: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2554, characters 2-54: | |
| - Warning: Duplicate clear of HFc [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2559, characters 2-40: | |
| - Warning: Duplicate clear of H0 [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2560, characters 2-47: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2561, characters 2-61: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2615, characters 2-23: | |
| - Warning: Duplicate clear of Hfg [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2623, characters 2-23: | |
| - Warning: Duplicate clear of Hhl [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2662, characters 2-23: | |
| - Warning: Duplicate clear of Hfg [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2666, characters 2-115: | |
| - Warning: Duplicate clear of Hfh [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 2675, characters 2-64: | |
| - Warning: Duplicate clear of Hfh [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 4453, characters 2-36: | |
| - Warning: Duplicate clear of A [duplicate-clear,ssr] | |
| - File "./theories/Hierarchy.v", line 4488, characters 2-36: | |
| - Warning: Duplicate clear of A [duplicate-clear,ssr] | |
| - Finished theories/Hierarchy.vo | |
| - File "./theories/Equiv.v", line 24, characters 0-43: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/SF_seq.v", line 25, characters 0-47: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/SF_seq.v", line 38, characters 14-23: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 39, characters 14-24: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 41, characters 24-35: | |
| - Warning: Notation RList.Rlist is deprecated since 8.12. use (list R) instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 41, characters 0-134: | |
| - Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 41, characters 0-134: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 47, characters 25-36: | |
| - Warning: Notation RList.Rlist is deprecated since 8.12. use (list R) instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 59, characters 2-15: | |
| - Warning: Notation RList.Rlength is deprecated since 8.12. | |
| - use List.length instead [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/SF_seq.v", line 116, characters 2-78: | |
| - Warning: Duplicate clear of IHs [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 337, characters 2-18: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 403, characters 2-38: | |
| - Warning: Duplicate clear of IHst [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 845, characters 2-30: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - Finished theories/Equiv.vo | |
| - File "./theories/SF_seq.v", line 918, characters 2-31: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 1032, characters 2-74: | |
| - Warning: Duplicate clear of Hx' [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 1108, characters 2-30: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 24, characters 0-54: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/SF_seq.v", line 1302, characters 2-149: | |
| - Warning: Duplicate clear of Hdec [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 268, characters 2-211: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 268, characters 2-211: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 268, characters 2-211: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 268, characters 2-211: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 280, characters 2-121: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 284, characters 2-119: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 286, characters 2-88: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 290, characters 2-91: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 303, characters 2-211: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 303, characters 2-211: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 303, characters 2-211: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 303, characters 2-211: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 317, characters 2-121: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 321, characters 2-91: | |
| - Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 323, characters 2-119: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 325, characters 2-88: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 482, characters 2-235: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 508, characters 2-166: | |
| - Warning: Duplicate clear of Hiu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 508, characters 2-166: | |
| - Warning: Duplicate clear of Hsu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 517, characters 2-133: | |
| - Warning: Duplicate clear of Hiu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 520, characters 2-133: | |
| - Warning: Duplicate clear of Hsu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 536, characters 2-60: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 726, characters 2-38: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 744, characters 2-28: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 2104, characters 2-28: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 1512, characters 2-103: | |
| - Warning: Duplicate clear of Hcv [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 1517, characters 2-103: | |
| - Warning: Duplicate clear of Hcv [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2113, characters 2-31: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2130, characters 2-31: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2139, characters 2-31: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2178, characters 2-38: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2185, characters 2-38: | |
| - Warning: Duplicate clear of Hu [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2465, characters 4-58: | |
| - Warning: Duplicate clear of Hl [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 2659, characters 4-242: | |
| - Warning: Duplicate clear of Hw [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 2659, characters 4-242: | |
| - Warning: Duplicate clear of Hw [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 2774, characters 4-242: | |
| - Warning: Duplicate clear of Hw [duplicate-clear,ssr] | |
| - File "./theories/SF_seq.v", line 2774, characters 4-242: | |
| - Warning: Duplicate clear of Hw [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 2857, characters 2-43: | |
| - Warning: Duplicate clear of Ha [duplicate-clear,ssr] | |
| - File "./theories/Lim_seq.v", line 3155, characters 2-76: | |
| - Warning: Duplicate clear of H2 [duplicate-clear,ssr] | |
| - Finished theories/Lim_seq.vo | |
| - Finished theories/SF_seq.vo | |
| - File "./theories/Series.v", line 24, characters 0-51: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/Continuity.v", line 24, characters 0-63: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/Continuity.v", line 863, characters 4-75: | |
| - Warning: Duplicate clear of Cf [duplicate-clear,ssr] | |
| - File "./theories/Continuity.v", line 885, characters 2-68: | |
| - Warning: Duplicate clear of He [duplicate-clear,ssr] | |
| - File "./theories/Continuity.v", line 1000, characters 2-46: | |
| - Warning: Duplicate clear of Hab [duplicate-clear,ssr] | |
| - File "./theories/Series.v", line 967, characters 4-28: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Series.v", line 1026, characters 4-34: | |
| - Warning: Duplicate clear of Hda [duplicate-clear,ssr] | |
| - File "./theories/Series.v", line 1047, characters 2-16: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Continuity.v", line 1808, characters 2-66: | |
| - Warning: Duplicate clear of Cf [duplicate-clear,ssr] | |
| - File "./theories/Continuity.v", line 1820, characters 4-41: | |
| - Warning: Duplicate clear of eps [duplicate-clear,ssr] | |
| - Finished theories/Series.vo | |
| - Finished theories/Continuity.vo | |
| - File "./theories/Derive.v", line 26, characters 0-73: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/RInt.v", line 25, characters 0-80: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/RInt.v", line 177, characters 2-23: | |
| - Warning: Duplicate clear of Hex [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 191, characters 2-37: | |
| - Warning: Duplicate clear of Hex [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 352, characters 2-21: | |
| - Warning: Duplicate clear of Df [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 287, characters 2-23: | |
| - Warning: Duplicate clear of Hex [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 357, characters 4-35: | |
| - Warning: Duplicate clear of Hg [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 399, characters 2-22: | |
| - Warning: Duplicate clear of Hex [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 464, characters 2-74: | |
| - Warning: Duplicate clear of Hstep [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 552, characters 2-71: | |
| - Warning: Duplicate clear of Heq [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 557, characters 2-60: | |
| - Warning: Duplicate clear of Hstep [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 888, characters 2-22: | |
| - Warning: Duplicate clear of If [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 912, characters 2-212: | |
| - Warning: Duplicate clear of Hs [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 986, characters 2-97: | |
| - Warning: Duplicate clear of H1 [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 987, characters 2-97: | |
| - Warning: Duplicate clear of H2 [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2189, characters 2-63: | |
| - Warning: Duplicate clear of Cf [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2190, characters 2-63: | |
| - Warning: Duplicate clear of Cg [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2214, characters 2-33: | |
| - Warning: Duplicate clear of Cf [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2215, characters 2-33: | |
| - Warning: Duplicate clear of Cg [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2216, characters 2-62: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2306, characters 2-29: | |
| - Warning: Duplicate clear of Hbx [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2324, characters 2-29: | |
| - Warning: Duplicate clear of Hax [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2460, characters 2-29: | |
| - Warning: Duplicate clear of Hbx [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 2491, characters 2-29: | |
| - Warning: Duplicate clear of Hax [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 1805, characters 6-22: | |
| - Warning: Duplicate clear of H0 [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 3308, characters 6-22: | |
| - Warning: Duplicate clear of Hy [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 3387, characters 2-37: | |
| - Warning: Duplicate clear of f [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 3403, characters 2-38: | |
| - Warning: Duplicate clear of f [duplicate-clear,ssr] | |
| - File "./theories/Derive.v", line 3420, characters 2-38: | |
| - Warning: Duplicate clear of f [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 2928, characters 37-47: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2928, characters 53-63: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2928, characters 37-47: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2928, characters 53-63: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2929, characters 33-43: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2929, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2929, characters 33-43: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2929, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2977, characters 18-28: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2977, characters 18-28: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 2989, characters 2-27: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - Finished theories/Derive.vo | |
| - File "./theories/RInt.v", line 3029, characters 2-44: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - File "./theories/Complex.v", line 24, characters 0-61: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/Complex.v", line 71, characters 0-29: | |
| - Warning: Declaring a scope implicitly is deprecated; use in advance an | |
| - explicit "Declare Scope C_scope.". [undeclared-scope,deprecated] | |
| - File "./theories/Complex.v", line 507, characters 0-135: | |
| - Warning: Ignoring canonical projection to C by ModuleSpace.sort in | |
| - C_R_ModuleSpace: redundant with C_ModuleSpace | |
| - [redundant-canonical-projection,typechecker] | |
| - File "./theories/Complex.v", line 510, characters 0-167: | |
| - Warning: Ignoring canonical projection to C by NormedModuleAux.sort in | |
| - C_R_NormedModuleAux: redundant with C_NormedModuleAux | |
| - [redundant-canonical-projection,typechecker] | |
| - File "./theories/Complex.v", line 513, characters 0-113: | |
| - Warning: Ignoring canonical projection to C by NormedModule.sort in | |
| - C_R_NormedModule: redundant with C_NormedModule | |
| - [redundant-canonical-projection,typechecker] | |
| - File "./theories/Complex.v", line 590, characters 0-175: | |
| - Warning: Ignoring canonical projection to C by CompleteNormedModule.sort in | |
| - C_R_CompleteNormedModule: redundant with C_CompleteNormedModule | |
| - [redundant-canonical-projection,typechecker] | |
| - Finished theories/Complex.vo | |
| - File "./theories/RInt.v", line 3315, characters 2-30: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3317, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3317, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Seq_fct.v", line 23, characters 0-80: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/Seq_fct.v", line 159, characters 2-59: | |
| - Warning: Duplicate clear of H0 [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 180, characters 2-59: | |
| - Warning: Duplicate clear of H0 [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 243, characters 4-35: | |
| - Warning: Duplicate clear of Hy [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 279, characters 4-64: | |
| - Warning: Duplicate clear of Hfn [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 280, characters 4-41: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 281, characters 4-36: | |
| - Warning: Duplicate clear of Hex [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 316, characters 2-97: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 392, characters 4-36: | |
| - Warning: Duplicate clear of Edn [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3579, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3579, characters 50-60: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3579, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3579, characters 50-60: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3582, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3582, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3582, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3585, characters 33-43: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3585, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3585, characters 33-43: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3585, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3589, characters 33-43: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3589, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3589, characters 33-43: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3589, characters 49-59: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/Seq_fct.v", line 702, characters 4-82: | |
| - Warning: Duplicate clear of Hcvs [duplicate-clear,ssr] | |
| - File "./theories/Seq_fct.v", line 714, characters 4-82: | |
| - Warning: Duplicate clear of Hcvs [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3610, characters 2-51: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3610, characters 2-51: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3612, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3612, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3616, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3616, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3616, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3656, characters 2-55: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3656, characters 2-55: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3658, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3658, characters 34-44: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3662, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3662, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3662, characters 27-37: | |
| - Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./theories/RInt.v", line 3741, characters 2-107: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3797, characters 2-148: | |
| - Warning: Duplicate clear of Hptd [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3806, characters 2-159: | |
| - Warning: Duplicate clear of IH [duplicate-clear,ssr] | |
| - Finished theories/Seq_fct.vo | |
| - File "./theories/PSeries.v", line 24, characters 0-88: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/PSeries.v", line 537, characters 2-59: | |
| - Warning: Duplicate clear of Hnot_ex [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3896, characters 4-50: | |
| - Warning: Duplicate clear of Hab [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 3896, characters 4-50: | |
| - Warning: Duplicate clear of Hab [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4015, characters 4-79: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 660, characters 4-44: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4286, characters 2-23: | |
| - Warning: Duplicate clear of HIf [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4301, characters 2-23: | |
| - Warning: Duplicate clear of HIf [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4324, characters 2-22: | |
| - Warning: Duplicate clear of HIf [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 1268, characters 2-53: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 1306, characters 2-53: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4386, characters 2-23: | |
| - Warning: Duplicate clear of HIf [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 1474, characters 2-33: | |
| - Warning: Duplicate clear of H0 [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 1481, characters 2-26: | |
| - Warning: Duplicate clear of H0 [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4446, characters 6-34: | |
| - Warning: Duplicate clear of H1 [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4446, characters 6-34: | |
| - Warning: Duplicate clear of H1 [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4481, characters 6-34: | |
| - Warning: Duplicate clear of Ht [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4481, characters 6-34: | |
| - Warning: Duplicate clear of Ht [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4495, characters 6-34: | |
| - Warning: Duplicate clear of H1 [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4495, characters 6-34: | |
| - Warning: Duplicate clear of H1 [duplicate-clear,ssr] | |
| - File "./theories/RInt.v", line 4584, characters 2-23: | |
| - Warning: Duplicate clear of HIf [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 2045, characters 4-64: | |
| - Warning: Duplicate clear of Hn [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 2045, characters 4-64: | |
| - Warning: Duplicate clear of Hn [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 2441, characters 4-46: | |
| - Warning: Duplicate clear of r [duplicate-clear,ssr] | |
| - File "./theories/PSeries.v", line 2457, characters 3-82: | |
| - Warning: Duplicate clear of Hw [duplicate-clear,ssr] | |
| - Finished theories/PSeries.vo | |
| - Finished theories/RInt.vo | |
| - File "./theories/Derive_2d.v", line 1196, characters 2-43: | |
| - Warning: Duplicate clear of z [duplicate-clear,ssr] | |
| - Finished theories/Derive_2d.vo | |
| - Finished theories/KHInt.vo | |
| - File "./theories/RInt_analysis.v", line 27, characters 0-66: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/RInt_analysis.v", line 48, characters 4-104: | |
| - Warning: Duplicate clear of CIf [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 113, characters 2-114: | |
| - Warning: Duplicate clear of CIf [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 338, characters 2-59: | |
| - Warning: Duplicate clear of Hf [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 471, characters 2-95: | |
| - Warning: Duplicate clear of Ha [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 475, characters 2-95: | |
| - Warning: Duplicate clear of Hb [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 693, characters 2-60: | |
| - Warning: Duplicate clear of Hf [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 774, characters 0-57: | |
| - Warning: Duplicate clear of Ca [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 794, characters 0-57: | |
| - Warning: Duplicate clear of Ca [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 795, characters 0-57: | |
| - Warning: Duplicate clear of Cb [duplicate-clear,ssr] | |
| - File "./theories/RInt_analysis.v", line 1284, characters 0-58: | |
| - Warning: Duplicate clear of Hy [duplicate-clear,ssr] | |
| - Finished theories/RInt_analysis.vo | |
| - File "./theories/ElemFct.v", line 24, characters 0-96: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/RInt_gen.v", line 24, characters 0-88: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./theories/ElemFct.v", line 556, characters 2-30: | |
| - Warning: Duplicate clear of Hy [duplicate-clear,ssr] | |
| - File "./theories/ElemFct.v", line 570, characters 2-36: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - File "./theories/ElemFct.v", line 666, characters 2-56: | |
| - Warning: Duplicate clear of Hx [duplicate-clear,ssr] | |
| - File "./theories/ElemFct.v", line 674, characters 2-53: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - Finished theories/RInt_gen.vo | |
| - Finished theories/ElemFct.vo | |
| - File "./theories/AutoDerive.v", line 763, characters 0-65: | |
| - Warning: Duplicate clear of Dle [duplicate-clear,ssr] | |
| - File "./theories/AutoDerive.v", line 961, characters 0-45: | |
| - Warning: Duplicate clear of IHe1 [duplicate-clear,ssr] | |
| - Finished theories/AutoDerive.vo | |
| - File "./theories/Coquelicot.v", line 272, characters 0-52: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished theories/Coquelicot.vo | |
| - Building all | |
| - Finished all | |
| -> compiled coq-coquelicot.3.2.0 | |
| Processing 13/15: [coq-coquelicot: ./remake install] | |
| + /home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-coquelicot.3.2.0/./remake "install" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-coquelicot.3.2.0) | |
| - Building install | |
| - Finished install | |
| -> installed coq-coquelicot.3.2.0 | |
| Processing 14/15: [coq-interval: ./configure] | |
| + /home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-interval.4.5.2/./configure (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-interval.4.5.2) | |
| - 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 we are using the GNU C compiler... yes | |
| - checking whether gcc accepts -g... yes | |
| - checking for gcc option to accept ISO C89... none needed | |
| - checking how to run the C preprocessor... gcc -E | |
| - checking for coqc... /home/coq/.opam/4.07.1+flambda/bin/coqc | |
| - checking Coq version... 81502 | |
| - checking for coqdep... /home/coq/.opam/4.07.1+flambda/bin/coqdep | |
| - checking for coqdoc... /home/coq/.opam/4.07.1+flambda/bin/coqdoc | |
| - checking for ocamlfind... /home/coq/.opam/4.07.1+flambda/bin/ocamlfind | |
| - checking for Flocq... yes | |
| - checking for primitive floats... | |
| - yes | |
| - checking for Ssreflect... yes | |
| - 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 we are using the GNU C++ compiler... yes | |
| - checking whether g++ accepts -g... yes | |
| - configure: building remake... | |
| - /usr/bin/ld: /tmp/ccA5B6zV.o: in function `main': | |
| - remake.cpp:(.text.startup+0xb87): warning: the use of `tempnam' is dangerous, better use `mkstemp' | |
| - | |
| - === Summary === | |
| - Vernacular directory /home/coq/.opam/4.07.1+flambda/lib/coq/user-contrib/Interval | |
| - Plugin directory /home/coq/.opam/4.07.1+flambda/lib/coq/user-contrib/Interval | |
| - 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 | |
| Processing 14/15: [coq-interval: ./remake] | |
| + /home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-interval.4.5.2/./remake "-j2" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-interval.4.5.2) | |
| - Building src/Tactic_float.v | |
| - Building src/Plot/interval_plot.ml | |
| - Finished src/Tactic_float.v | |
| - Building src/Tactic.vo | |
| - Finished src/Plot/interval_plot.ml | |
| - Building src/Eval/Eval.vo | |
| - Building src/Eval/Prog.vo | |
| - 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/MathComp.vo | |
| - File "./src/Integral/Priority.v", line 527, characters 0-118: | |
| - Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - Finished src/Integral/Priority.vo | |
| - Building src/Missing/Stdlib.vo | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/MathComp.v", line 24, characters 0-88: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - Finished src/Missing/MathComp.vo | |
| - Building src/Poly/Basic_rec.vo | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Stdlib.v", line 1085, characters 0-37: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished src/Missing/Stdlib.vo | |
| - Finished src/Poly/Basic_rec.vo | |
| - Building src/Poly/Bound.vo | |
| - File "./src/Missing/Coquelicot.v", line 22, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Building src/Poly/Bound_quad.vo | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Missing/Coquelicot.v", line 23, characters 0-96: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - 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 | |
| - File "./src/Missing/Coquelicot.v", line 494, characters 0-17: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./src/Missing/Coquelicot.v", line 497, characters 0-17: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./src/Missing/Coquelicot.v", line 515, characters 0-17: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./src/Missing/Coquelicot.v", line 529, characters 0-17: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./src/Missing/Coquelicot.v", line 532, characters 0-17: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./src/Missing/Coquelicot.v", line 551, characters 0-17: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - Finished src/Missing/Coquelicot.vo | |
| - Building src/Real/Xreal.vo | |
| - File "./src/Real/Taylor.v", line 24, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./src/Real/Xreal.v", line 186, characters 0-31: | |
| - Warning: Declaring a scope implicitly is deprecated; use in advance an | |
| - explicit "Declare Scope XR_scope.". [undeclared-scope,deprecated] | |
| - Finished src/Real/Taylor.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 | |
| - Finished src/Real/Xreal.vo | |
| - Finished src/Float/Basic.vo | |
| - File "./src/Interval/Interval.v", line 21, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished src/Real/Xreal_derive.vo | |
| - Finished src/Interval/Interval.vo | |
| - File "./src/Poly/Datatypes.v", line 24, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Datatypes.v", line 25, characters 0-96: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - Finished src/Float/Sig.vo | |
| - File "./src/Poly/Datatypes.v", line 852, characters 0-70: | |
| - Warning: Declaring a scope implicitly is deprecated; use in advance an | |
| - explicit "Declare Scope ipoly_scope.". [undeclared-scope,deprecated] | |
| - File "./src/Poly/Datatypes.v", line 989, characters 0-34: | |
| - Warning: Declaring a scope implicitly is deprecated; use in advance an | |
| - explicit "Declare Scope ipoly_scope.". [undeclared-scope,deprecated] | |
| - Finished src/Interval/Univariate_sig.vo | |
| - Finished src/Poly/Datatypes.vo | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - Finished src/Poly/Taylor_poly.vo | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Bound.v", line 24, characters 0-96: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - Finished src/Poly/Bound.vo | |
| - 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] | |
| - 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] | |
| - 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] | |
| - 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] | |
| - 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] | |
| - 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/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 24, characters 0-84: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Interval/Interval_compl.v", line 25, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished src/Interval/Interval_compl.vo | |
| - File "./src/Poly/Taylor_model_sharp.v", line 25, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - 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] | |
| - 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 1853, characters 4-48: | |
| - Warning: Duplicate clear of X0 [duplicate-clear,ssr] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 1961, characters 4-48: | |
| - Warning: Duplicate clear of X0 [duplicate-clear,ssr] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 2053, characters 2-51: | |
| - Warning: Duplicate clear of x [duplicate-clear,ssr] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 2168, characters 4-45: | |
| - Warning: Duplicate clear of X0 [duplicate-clear,ssr] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 2310, characters 4-37: | |
| - Warning: Duplicate clear of n [duplicate-clear,ssr] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 2421, characters 2-189: | |
| - Warning: Duplicate clear of X [duplicate-clear,ssr] | |
| - File "./src/Poly/Taylor_model_sharp.v", line 2424, characters 4-45: | |
| - Warning: Duplicate clear of X0 [duplicate-clear,ssr] | |
| - Finished src/Poly/Taylor_model_sharp.vo | |
| - 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] | |
| - Finished src/Poly/Taylor_model.vo | |
| - File "./src/Integral/Refine.v", line 21, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished src/Integral/Refine.vo | |
| - File "./src/Integral/Integral.v", line 21, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - 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/Integral/Integral.vo | |
| - File "./src/Integral/Bertrand.v", line 3, characters 0-53: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ + _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ - _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ >= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ > _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ < _ < _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ * _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - File "./src/Integral/Bertrand.v", line 4, characters 0-77: | |
| - Warning: Notation "_ ^ _" was already used in scope nat_scope. | |
| - [notation-overridden,parsing] | |
| - Finished src/Integral/Bertrand.vo | |
| - Finished src/Float/Generic.vo | |
| - Finished src/Float/Generic_proof.vo | |
| - Finished src/Float/Specific_sig.vo | |
| - Finished src/Float/Specific_stdz.vo | |
| - Finished src/Float/Specific_ops.vo | |
| - Finished src/Float/Specific_bigint.vo | |
| - Finished src/Float/Generic_ops.vo | |
| - Finished src/Eval/Tree.vo | |
| - Finished src/Interval/Float.vo | |
| - File "./src/Interval/Transcend.v", line 52, characters 0-88: | |
| - Warning: Not a truly recursive cofixpoint. [non-recursive,fixpoints] | |
| - Finished src/Interval/Transcend.vo | |
| - Finished src/Interval/Float_full.vo | |
| - Building src/Tactics/Root_helper.vo | |
| - Building src/Tactic_float.vo | |
| - Finished src/Eval/Prog.vo | |
| - Building src/Float/Primitive_ops.vo | |
| - Building src/Missing/Int63Compat.vo | |
| - Building src/Missing/Int63Copy.vo | |
| - Finished src/Missing/Int63Copy.vo | |
| - Finished src/Eval/Reify.vo | |
| - Finished src/Missing/Int63Compat.vo | |
| - File "./src/Eval/Eval.v", line 23, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - File "./src/Float/Primitive_ops.v", line 41, characters 12-20: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 46, characters 15-23: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 56, characters 12-20: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 62, characters 6-11: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 62, characters 13-21: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 66, characters 15-23: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 72, characters 15-20: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 72, characters 24-32: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 81, characters 12-20: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 87, characters 17-22: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 87, characters 24-32: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 91, characters 15-23: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 97, characters 6-11: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 97, characters 15-23: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 108, characters 15-23: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 204, characters 66-74: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 204, characters 41-49: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 210, characters 10-18: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 207, characters 25-33: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 208, characters 42-50: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 215, characters 21-29: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 216, characters 38-46: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 213, characters 25-33: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 218, characters 18-26: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 222, characters 21-29: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 224, characters 56-64: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 224, characters 56-64: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 336, characters 7-15: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 361, characters 7-15: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Eval/Eval.v", line 522, characters 0-25: | |
| - Warning: Duplicate clear of H [duplicate-clear,ssr] | |
| - File "./src/Float/Primitive_ops.v", line 478, characters 34-42: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 478, characters 34-42: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 489, characters 28-33: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 489, characters 28-33: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 489, characters 28-33: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 540, characters 32-40: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 540, characters 32-40: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 559, characters 20-28: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 559, characters 20-28: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 627, characters 34-42: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 627, characters 34-42: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 642, characters 21-29: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 642, characters 21-29: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 700, characters 34-42: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 700, characters 34-42: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 712, characters 26-31: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 712, characters 26-31: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 712, characters 26-31: | |
| - Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - Finished src/Eval/Eval.vo | |
| - Finished src/Tactics/Interval_helper.vo | |
| - Finished src/Tactics/Root_helper.vo | |
| - Finished src/Tactics/Plot_helper.vo | |
| - File "./src/Tactics/Integral_helper.v", line 22, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished src/Tactics/Integral_helper.vo | |
| - Building src/Plot/interval_plot.cmxs | |
| - File "src/Plot/plot.c", line 22, characters 45-76: | |
| - Warning 3: deprecated: Coqlib.gen_reference_in_modules | |
| - Please use Coqlib.lib_ref | |
| - File "src/Plot/plot.c", line 147, characters 34-40: | |
| - Warning 20: this argument will not be used by the function. | |
| - File "src/Plot/plot.c", line 151, characters 28-34: | |
| - Warning 20: this argument will not be used by the function. | |
| - Finished src/Plot/interval_plot.cmxs | |
| - Building src/Plot/interval_plot.cmo | |
| - File "src/Plot/plot.c", line 22, characters 45-76: | |
| - Warning 3: deprecated: Coqlib.gen_reference_in_modules | |
| - Please use Coqlib.lib_ref | |
| - File "src/Plot/plot.c", line 147, characters 34-40: | |
| - Warning 20: this argument will not be used by the function. | |
| - File "src/Plot/plot.c", line 151, characters 28-34: | |
| - Warning 20: this argument will not be used by the function. | |
| - Finished src/Plot/interval_plot.cmo | |
| - Building src/Plot.vo | |
| - Finished src/Plot.vo | |
| - File "./src/Float/Primitive_ops.v", line 2550, characters 0-13: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2550, characters 0-13: | |
| - Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2591, characters 26-34: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2591, characters 26-34: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2591, characters 26-34: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2592, characters 26-34: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2592, characters 26-34: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - File "./src/Float/Primitive_ops.v", line 2592, characters 26-34: | |
| - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. | |
| - [deprecated-syntactic-definition,deprecated] | |
| - Finished src/Float/Primitive_ops.vo | |
| - Finished src/Tactic_float.vo | |
| - File "./src/Tactic.v", line 22, characters 0-42: | |
| - Warning: | |
| - New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. | |
| - [ambiguous-paths,typechecker] | |
| - Finished src/Tactic.vo | |
| - Building all | |
| - Finished all | |
| -> compiled coq-interval.4.5.2 | |
| Processing 15/15: [coq-interval: ./remake install] | |
| + /home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-interval.4.5.2/./remake "install" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-interval.4.5.2) | |
| - Building install | |
| - Finished install | |
| -> installed coq-interval.4.5.2 | |
| Done. | |
| Removing intermediate container 85205362c905 | |
| ---> 795d81ae51b1 | |
| Step 9/9 : CMD ["/bin/bash"] | |
| ---> Running in 0a1826faefa4 | |
| Removing intermediate container 0a1826faefa4 | |
| ---> 82bdf3ccd388 | |
| Successfully built 82bdf3ccd388 | |
| Successfully tagged registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-flambda-interval-4.5.2:20 | |
| [32;1m$ echo "${IMAGE}"[0;m | |
| registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-flambda-interval-4.5.2:20 | |
| [32;1m$ docker push "${IMAGE}"[0;m | |
| The push refers to repository [registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-flambda-interval-4.5.2] | |
| 711d250190b5: Preparing | |
| 564d8b0ff083: Preparing | |
| 82d93b3fc50f: Preparing | |
| 8481116e6731: Preparing | |
| b3c43a503570: Preparing | |
| 7c7f3bc82bd8: Preparing | |
| 7c7f3bc82bd8: Waiting | |
| a12586ed027f: Preparing | |
| a12586ed027f: Waiting | |
| 8481116e6731: Pushed | |
| b3c43a503570: Pushed | |
| 711d250190b5: Pushed | |
| a12586ed027f: Pushed | |
| 7c7f3bc82bd8: Pushed | |
| 82d93b3fc50f: Pushed | |
| 564d8b0ff083: Pushed | |
| 20: digest: sha256:bc2a24f836b8f520150145b2db14d5dde61f9eb4100a47de5776a1d8a71c214a size: 1796 | |
| [32;1m$ docker tag "${IMAGE}" "${IMAGE0}"[0;m | |
| [32;1m$ docker push "${IMAGE0}"[0;m | |
| The push refers to repository [registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-flambda-interval-4.5.2] | |
| 711d250190b5: Preparing | |
| 564d8b0ff083: Preparing | |
| 82d93b3fc50f: Preparing | |
| 8481116e6731: Preparing | |
| b3c43a503570: Preparing | |
| 7c7f3bc82bd8: Preparing | |
| a12586ed027f: Preparing | |
| 7c7f3bc82bd8: Waiting | |
| a12586ed027f: Waiting | |
| b3c43a503570: Layer already exists | |
| 564d8b0ff083: Layer already exists | |
| 82d93b3fc50f: Layer already exists | |
| 711d250190b5: Layer already exists | |
| 8481116e6731: Layer already exists | |
| 7c7f3bc82bd8: Layer already exists | |
| a12586ed027f: Layer already exists | |
| latest: digest: sha256:bc2a24f836b8f520150145b2db14d5dde61f9eb4100a47de5776a1d8a71c214a size: 1796 | |
| [32;1m$ docker logout "${CI_REGISTRY}"[0;m | |
| Removing login credentials for registry.gitlab.com | |
| section_end:1668297788:step_script | |
| [0Ksection_start:1668297788:cleanup_file_variables | |
| [0K[0K[36;1mCleaning up project directory and file based variables[0;m[0;m | |
| section_end:1668297789:cleanup_file_variables | |
| [0K[32;1mJob succeeded[0;m |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment