coq-community / bignums Goto Github PK

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

License: GNU Lesser General Public License v2.1

Coq 92.15% OCaml 7.73% Makefile 0.12%

coq-plugin large-numbers coq docker-coq-action coq-platform coq-ci

bignums's Introduction

Bignums

This Coq library provides BigN, BigZ, and BigQ that used to be part of the standard library.

Building and installation instructions

The easiest way to install the latest released version of Bignums is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-bignums

To instead build and install manually, do:

git clone https://github.com/coq-community/bignums.git
cd bignums
make   # or make -j <number-of-cores-on-your-machine> 
make install

bignums's People

Stargazers

Watchers

bignums's Issues

`Make` should be `_CoqProject`

...so that we can edit files from Bignums under CoqIDE without having to manually set options.

Clarify exact license in repo and packages

We are trying to use SPDX identifiers everywhere for licenses, which does not include "LGPL-2.1" - the possibilities are either LGPL-2.1-only or LGPL-2.1-or-later. This project should clarify in its README.md (and meta.yml) which one it is.

From 02fd659 it seems the intent was to follow Coq's license, which is LGPL-2.1-only.

Branches for 8.14 and 8.15

Would be nice to have the usual branches v8.14 and v8.15 if we need some bugfixes for the platform.

[external issue] compilation error using `coqorg/coq:dev` with `opam unpin coq; opam upgrade`

https://circleci.com/gh/liyishuai/QuickChick/116

### output ###
# File "dune", line 5, characters 14-25:
# 5 |  (public_name coq-bignums)
#                   ^^^^^^^^^^^
# Warning: (public_name ...) is deprecated and will be removed in the Coq
# language version 1.0, please use (package ...) instead
#         coqc BigNumPrelude.vo (exit 1)
# (cd _build/default && /home/coq/.opam/4.05.0/bin/coqc -I /home/coq/.opam/4.05.0/lib/coq/clib -I /home/coq/.opam/4.05.0/lib/coq/config -I /home/coq/.opam/4.05.0/lib/coq/engine -I /home/coq/.opam/4.05.0/lib/coq/gramlib/.pack -I /home/coq/.opam/4.05.0/lib/coq/interp -I /home/coq/.opam/4.05.0/lib/coq/kernel -I /home/coq/.opam/4.05.0/lib/coq/kernel/byterun -I /home/coq/.opam/4.05.0/lib/coq/lib -I [...]
# File "./BigNumPrelude.v", line 28, characters 0-42:
# Error: Dynlink error: interface mismatch on Vernacexpr

Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.19.0.

Coq Platform CI is currently testing opam package coq-bignums.9.0.0+coq8.19
from official repository https://coq.inria.fr/opam/released/packages/coq-bignums/coq-bignums.9.0.0+coq8.19/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2024.01, please inform us as soon as possible and before March 31st, 2024!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

coq-bignums.8.11.dev fails with coq.8.11+alpha since 2019-11-22

Cc @palmskog @ejgallego @vbgl FYI

Since last night, the build of coqorg/coq:8.11-alpha with coq-bignums.8.11.dev (based on coq_makefile) fails:

Executing build hook...
### Building with custom build arguments
BUILD_DATE: 2019-11-22T00:47:16Z
VCS_REF: 57d03d5
COQ_COMMIT: 57d03d5a7a00022717c3644f911efa3afd52d510
COQ_VERSION: 8.11+alpha
Sending build context to Docker daemon 4.608kB
Step 1/11 : FROM coqorg/base:latest
latest: Pulling from coqorg/base
4a56a430b2ba: Pulling fs layer
d5e23f758864: Pulling fs layer
a8470d88261e: Pulling fs layer
aff0e72e7fcf: Pulling fs layer
0d6a3dadaa28: Pulling fs layer
6ee64e4a8ab0: Pulling fs layer
aff0e72e7fcf: Waiting
0d6a3dadaa28: Waiting
6ee64e4a8ab0: Waiting
a8470d88261e: Verifying Checksum
a8470d88261e: Download complete
aff0e72e7fcf: Verifying Checksum
aff0e72e7fcf: Download complete
4a56a430b2ba: Verifying Checksum
4a56a430b2ba: Download complete
d5e23f758864: Verifying Checksum
d5e23f758864: Download complete
0d6a3dadaa28: Verifying Checksum
0d6a3dadaa28: Download complete
6ee64e4a8ab0: Verifying Checksum
6ee64e4a8ab0: Download complete
4a56a430b2ba: Pull complete
d5e23f758864: Pull complete
a8470d88261e: Pull complete
aff0e72e7fcf: Pull complete
0d6a3dadaa28: Pull complete
6ee64e4a8ab0: Pull complete
Digest: sha256:38e84146eaf9b219fe8079cea9b54050db52ce2ba3711518926fe083458fdfcd
Status: Downloaded newer image for coqorg/base:latest
---> 20143da9ed22
Step 2/11 : ARG BUILD_DATE
---> Running in bac333811814
Removing intermediate container bac333811814
---> f7d64e0cb360
Step 3/11 : ARG VCS_REF
---> Running in d48bf50c458c
Removing intermediate container d48bf50c458c
---> a6a7fc584945
Step 4/11 : ARG COQ_COMMIT
---> Running in a8b12f8a5cb6
Removing intermediate container a8b12f8a5cb6
---> 2214f1d41239
Step 5/11 : ARG COQ_VERSION
---> Running in 707c7316236d
Removing intermediate container 707c7316236d
---> b62494eb6c17
Step 6/11 : LABEL maintainer="[email protected]"
---> Running in 8ab465ccfd37
Removing intermediate container 8ab465ccfd37
---> 5719f2016d3a
Step 7/11 : LABEL org.label-schema.build-date=${BUILD_DATE} org.label-schema.name="The Coq Proof Assistant" org.label-schema.description="Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs." org.label-schema.url="https://coq.inria.fr/" org.label-schema.vcs-ref=${VCS_REF} org.label-schema.vcs-url="https://github.com/coq/coq" org.label-schema.vendor="The Coq Development Team" org.label-schema.version=${COQ_VERSION} org.label-schema.schema-version="1.0"
---> Running in f57575d8f720
Removing intermediate container f57575d8f720
---> 5d1fbc8512ab
Step 8/11 : ENV COQ_VERSION="${COQ_VERSION}"
---> Running in 75533654343a
Removing intermediate container 75533654343a
---> 21243b400243
Step 9/11 : ENV COQ_EXTRA_OPAM="coq-bignums"
---> Running in f51950bb19c6
Removing intermediate container f51950bb19c6
---> a99a0a0541d9
Step 10/11 : RUN ["/bin/bash", "--login", "-c", "set -x && eval $(opam env --switch=${COMPILER_EDGE} --set-switch) && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev && opam update -y -u && opam pin add -n -y -k git coq.${COQ_VERSION} \"git+https://github.com/coq/coq#${COQ_COMMIT}\" && opam install -y -v -j ${NJOBS} coq ${COQ_EXTRA_OPAM} && opam clean -a -s --logs && opam config list && opam list"]
---> Running in 9c57c8388e88
++ opam env --switch=4.07.1+flambda --set-switch
+ eval 'OPAMSWITCH='\''4.07.1+flambda'\'';' export 'OPAMSWITCH;' 'OPAM_SWITCH_PREFIX='\''/home/coq/.opam/4.07.1+flambda'\'';' export 'OPAM_SWITCH_PREFIX;' 'CAML_LD_LIBRARY_PATH='\''/home/coq/.opam/4.07.1+flambda/lib/stublibs:/home/coq/.opam/4.07.1+flambda/lib/ocaml/stublibs:/home/coq/.opam/4.07.1+flambda/lib/ocaml'\'';' export 'CAML_LD_LIBRARY_PATH;' 'OCAML_TOPLEVEL_PATH='\''/home/coq/.opam/4.07.1+flambda/lib/toplevel'\'';' export 'OCAML_TOPLEVEL_PATH;' 'MANPATH='\'':/home/coq/.opam/4.07.1+flambda/man'\'';' export 'MANPATH;' 'PATH='\''/home/coq/.opam/4.07.1+flambda/bin:/home/coq/.local/bin:/home/coq/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games'\'';' export 'PATH;'
++ OPAMSWITCH=4.07.1+flambda
++ export OPAMSWITCH
++ OPAM_SWITCH_PREFIX=/home/coq/.opam/4.07.1+flambda
++ export OPAM_SWITCH_PREFIX
++ CAML_LD_LIBRARY_PATH=/home/coq/.opam/4.07.1+flambda/lib/stublibs:/home/coq/.opam/4.07.1+flambda/lib/ocaml/stublibs:/home/coq/.opam/4.07.1+flambda/lib/ocaml
++ export CAML_LD_LIBRARY_PATH
++ OCAML_TOPLEVEL_PATH=/home/coq/.opam/4.07.1+flambda/lib/toplevel
++ export OCAML_TOPLEVEL_PATH
++ MANPATH=:/home/coq/.opam/4.07.1+flambda/man
++ export MANPATH
++ PATH=/home/coq/.opam/4.07.1+flambda/bin:/home/coq/.local/bin:/home/coq/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games
++ export PATH
+ opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev
[coq-extra-dev] Initialised
+ opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev
[coq-core-dev] Initialised
+ opam update -y -u
<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
[coq-core-dev] no changes from https://coq.inria.fr/opam/core-dev
[coq-extra-dev] no changes from https://coq.inria.fr/opam/extra-dev
[coq-released] synchronised from https://coq.inria.fr/opam/released
[default] synchronised from https://opam.ocaml.org
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
+ opam pin add -n -y -k git coq.8.11+alpha git+https://github.com/coq/coq#57d03d5a7a00022717c3644f911efa3afd52d510
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha: git]
[coq.8.11+alpha] synchronised from git+https://github.com/coq/coq#57d03d5a7a00022717c3644f911efa3afd52d510
coq is now pinned to git+https://github.com/coq/coq#57d03d5a7a00022717c3644f911efa3afd52d510 (version 8.11+alpha)
+ opam install -y -v -j 2 coq coq-bignums
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq.8.11+alpha: git]
[coq.8.11+alpha] no changes from git+https://github.com/coq/coq#57d03d5a7a00022717c3644f911efa3afd52d510
The following actions will be performed:
- install dune 1.11.4 [required by coq]
- install conf-m4 1 [required by ocamlfind]
- install ocamlfind 1.8.1 [required by coq]
- install num 1.3 [required by coq]
- install coq 8.11+alpha*
- install coq-bignums 8.11.dev
===== 6 to install =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 2/6: [coq.8.11+alpha: git]
Processing 3/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git]
Processing 4/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git] [dune.1.11.4: dl]
[dune.1.11.4] downloaded from cache at https://opam.ocaml.org/cache
Processing 4/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git]
Processing 5/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git] [num.1.3: dl]
[num.1.3] downloaded from cache at https://opam.ocaml.org/cache
Processing 5/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git]
Processing 6/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git] [ocamlfind.1.8.1: dl]
[ocamlfind.1.8.1] downloaded from cache at https://opam.ocaml.org/cache
Processing 6/6: [coq.8.11+alpha: git] [coq-bignums.8.11.dev: git]
[coq-bignums.8.11.dev] synchronised from git+https://github.com/coq/bignums.git#v8.11
Processing 6/6: [coq.8.11+alpha: git]
[coq.8.11+alpha] synchronised from git+https://github.com/coq/coq#57d03d5a7a00022717c3644f911efa3afd52d510
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/12: [conf-m4: sh echo | m4]
Processing 2/12: [conf-m4: sh echo | m4] [dune: ocaml bootstrap.ml]
+ /bin/sh "-exc" "echo | m4" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/conf-m4.1)
- + m4
- + echo
-
- + m4
- + echo
-
-> compiled conf-m4.1
Processing 2/12: [dune: ocaml bootstrap.ml]
-> installed conf-m4.1
Processing 3/12: [dune: ocaml bootstrap.ml]
Processing 4/12: [dune: ocaml bootstrap.ml] [ocamlfind: ./configure]
+ /home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/./configure "-bindir" "/home/coq/.opam/4.07.1+flambda/bin" "-sitelib" "/home/coq/.opam/4.07.1+flambda/lib" "-mandir" "/home/coq/.opam/4.07.1+flambda/man" "-config" "/home/coq/.opam/4.07.1+flambda/lib/findlib.conf" "-no-custom" "-no-camlp4" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1)
- Welcome to findlib version 1.8.1
- Configuring core...
- Checking for #remove_directory...
- Testing threading model...
- systhread_supported: true
- Testing DLLs...
- Testing whether ppxopt can be supported...
- Checking for ocamlc -opaque...
- Configuring libraries...
- native dynlink: found
- labltk: not present
- ocamlbuild: not present
- camlp4: disabled
- compiler-libs: found
- dbm: not present (normal since OCaml-4.00)
- num: not present (normal since OCaml-4.06)
- bytes: found, installing fake library
- spacetime: found
- graphics: not found
- Configuration for dynlink written to site-lib-src/dynlink/META
- Configuration for str written to site-lib-src/str/META
- Configuration for threads written to site-lib-src/threads/META
- Configuration for unix written to site-lib-src/unix/META
- Configuration for stdlib written to site-lib-src/stdlib/META
- Configuration for bigarray written to site-lib-src/bigarray/META
- Configuration for ocamldoc written to site-lib-src/ocamldoc/META
- Configuration for compiler-libs written to site-lib-src/compiler-libs/META
- Configuration for bytes written to site-lib-src/bytes/META
- Configuration for raw_spacetime written to site-lib-src/raw_spacetime/META
- Detecting compiler arguments: (extractor built) ok
-
- About the OCAML core installation:
- Standard library: /home/coq/.opam/4.07.1+flambda/lib/ocaml
- Binaries: /home/coq/.opam/4.07.1+flambda/bin
- Manual pages: /home/coq/.opam/4.07.1+flambda/man
- Multi-threading type: posix
- The directory of site-specific packages will be
- site-lib: /home/coq/.opam/4.07.1+flambda/lib
- The configuration file is written to:
- findlib config file: /home/coq/.opam/4.07.1+flambda/lib/findlib.conf
- Software will be installed:
- Libraries: in <site-lib>/findlib
- Binaries: /home/coq/.opam/4.07.1+flambda/bin
- Manual pages: /home/coq/.opam/4.07.1+flambda/man
- topfind script: /home/coq/.opam/4.07.1+flambda/lib/ocaml
- Topfind ppxopt support: yes
- Toolbox: no
- Link custom runtime: no
- Need bytes compatibility: no
-
- Configuration has been written to Makefile.config
-
- You can now do 'make all', and optionally 'make opt', to build ocamlfind.
- Welcome to findlib version 1.8.1
- Configuring core...
- Checking for #remove_directory...
- Testing threading model...
- systhread_supported: true
- Testing DLLs...
- Testing whether ppxopt can be supported...
- Checking for ocamlc -opaque...
- Configuring libraries...
- native dynlink: found
- labltk: not present
- ocamlbuild: not present
- camlp4: disabled
- compiler-libs: found
- dbm: not present (normal since OCaml-4.00)
- num: not present (normal since OCaml-4.06)
- bytes: found, installing fake library
- spacetime: found
- graphics: not found
- Configuration for dynlink written to site-lib-src/dynlink/META
- Configuration for str written to site-lib-src/str/META
- Configuration for threads written to site-lib-src/threads/META
- Configuration for unix written to site-lib-src/unix/META
- Configuration for stdlib written to site-lib-src/stdlib/META
- Configuration for bigarray written to site-lib-src/bigarray/META
- Configuration for ocamldoc written to site-lib-src/ocamldoc/META
- Configuration for compiler-libs written to site-lib-src/compiler-libs/META
- Configuration for bytes written to site-lib-src/bytes/META
- Configuration for raw_spacetime written to site-lib-src/raw_spacetime/META
- Detecting compiler arguments: (extractor built) ok
-
- About the OCAML core installation:
- Standard library: /home/coq/.opam/4.07.1+flambda/lib/ocaml
- Binaries: /home/coq/.opam/4.07.1+flambda/bin
- Manual pages: /home/coq/.opam/4.07.1+flambda/man
- Multi-threading type: posix
- The directory of site-specific packages will be
- site-lib: /home/coq/.opam/4.07.1+flambda/lib
- The configuration file is written to:
- findlib config file: /home/coq/.opam/4.07.1+flambda/lib/findlib.conf
- Software will be installed:
- Libraries: in <site-lib>/findlib
- Binaries: /home/coq/.opam/4.07.1+flambda/bin
- Manual pages: /home/coq/.opam/4.07.1+flambda/man
- topfind script: /home/coq/.opam/4.07.1+flambda/lib/ocaml
- Topfind ppxopt support: yes
- Toolbox: no
- Link custom runtime: no
- Need bytes compatibility: no
-
- Configuration has been written to Makefile.config
-
- You can now do 'make all', and optionally 'make opt', to build ocamlfind.
Processing 4/12: [dune: ocaml bootstrap.ml] [ocamlfind: make all]
+ /usr/bin/make "all" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1)
- for p in findlib; do ( cd src/$p; /usr/bin/make all ) || exit; done
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- ocamllex fl_meta.mll
- 22 states, 392 transitions, table size 1700 bytes
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat findlib_config.mlp | \
- ../../tools/patch '@CONFIGFILE@' '/home/coq/.opam/4.07.1+flambda/lib/findlib.conf' | \
- ../../tools/patch '@STDLIB@' '/home/coq/.opam/4.07.1+flambda/lib/ocaml' | \
- sed -e 's;@AUTOLINK@;true;g' \
- -e 's;@SYSTEM@;linux;g' \
- >findlib_config.ml
- if [ "true" = "true" ]; then \
- cp topfind.ml.in topfind.ml; \
- else \
- sed -e '/PPXOPT_BEGIN/,/PPXOPT_END/ d' topfind.ml.in \
- > topfind.ml ; \
- fi
- ocamldep *.ml *.mli >depend
- ocamlc -I +compiler-libs -opaque -g -c findlib_config.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_split.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_metatoken.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_meta.ml
- ocamlc -I +compiler-libs -opaque -c fl_metascanner.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_metascanner.ml
- ocamlc -I +compiler-libs -opaque -c fl_topo.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_topo.ml
- ocamlc -I +compiler-libs -opaque -c fl_package_base.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_package_base.ml
- ocamlc -I +compiler-libs -opaque -c findlib.mli
- ocamlc -I +compiler-libs -opaque -g -c findlib.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_args.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_lint.ml
- ocamlc -I +compiler-libs -a -o findlib.cma findlib_config.cmo fl_split.cmo fl_metatoken.cmo fl_meta.cmo fl_metascanner.cmo fl_topo.cmo fl_package_base.cmo findlib.cmo fl_args.cmo fl_lint.cmo
- ocamlc -I +compiler-libs -opaque -g -c ocaml_args.ml
- ocamlc -I +compiler-libs -opaque -g -c frontend.ml
- File "frontend.ml", line 1826, characters 16-29:
- Warning 3: deprecated: Stdlib.String.create
- Use Bytes.create instead.
- ocamlc -I +compiler-libs -o ocamlfind -g findlib.cma unix.cma \
- ocaml_args.cmo frontend.cmo
- ocamlc -I +compiler-libs -opaque -c topfind.mli
- ocamlc -I +compiler-libs -opaque -g -c topfind.ml
- ocamlc -I +compiler-libs -a -o findlib_top.cma topfind.cmo
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat topfind_rd1.p | \
- ../../tools/patch '@SITELIB@' '/home/coq/.opam/4.07.1+flambda/lib' \
- >topfind
- ocamlc -I +compiler-libs -opaque -c fl_dynload.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_dynload.ml
- ocamlc -I +compiler-libs -a -o findlib_dynload.cma fl_dynload.cmo
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- /usr/bin/make all-config
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat findlib.conf.in | \
- tools/patch '@SITELIB@' '/home/coq/.opam/4.07.1+flambda/lib' >findlib.conf
- if ./tools/cmd_from_same_dir ocamlc; then \
- echo 'ocamlc="ocamlc.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamlopt; then \
- echo 'ocamlopt="ocamlopt.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamldep; then \
- echo 'ocamldep="ocamldep.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamldoc; then \
- echo 'ocamldoc="ocamldoc.opt"' >>findlib.conf; \
- fi
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- for p in findlib; do ( cd src/$p; /usr/bin/make all ) || exit; done
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- ocamllex fl_meta.mll
- 22 states, 392 transitions, table size 1700 bytes
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat findlib_config.mlp | \
- ../../tools/patch '@CONFIGFILE@' '/home/coq/.opam/4.07.1+flambda/lib/findlib.conf' | \
- ../../tools/patch '@STDLIB@' '/home/coq/.opam/4.07.1+flambda/lib/ocaml' | \
- sed -e 's;@AUTOLINK@;true;g' \
- -e 's;@SYSTEM@;linux;g' \
- >findlib_config.ml
- if [ "true" = "true" ]; then \
- cp topfind.ml.in topfind.ml; \
- else \
- sed -e '/PPXOPT_BEGIN/,/PPXOPT_END/ d' topfind.ml.in \
- > topfind.ml ; \
- fi
- ocamldep *.ml *.mli >depend
- ocamlc -I +compiler-libs -opaque -g -c findlib_config.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_split.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_metatoken.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_meta.ml
- ocamlc -I +compiler-libs -opaque -c fl_metascanner.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_metascanner.ml
- ocamlc -I +compiler-libs -opaque -c fl_topo.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_topo.ml
- ocamlc -I +compiler-libs -opaque -c fl_package_base.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_package_base.ml
- ocamlc -I +compiler-libs -opaque -c findlib.mli
- ocamlc -I +compiler-libs -opaque -g -c findlib.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_args.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_lint.ml
- ocamlc -I +compiler-libs -a -o findlib.cma findlib_config.cmo fl_split.cmo fl_metatoken.cmo fl_meta.cmo fl_metascanner.cmo fl_topo.cmo fl_package_base.cmo findlib.cmo fl_args.cmo fl_lint.cmo
- ocamlc -I +compiler-libs -opaque -g -c ocaml_args.ml
- ocamlc -I +compiler-libs -opaque -g -c frontend.ml
- File "frontend.ml", line 1826, characters 16-29:
- Warning 3: deprecated: Stdlib.String.create
- Use Bytes.create instead.
- ocamlc -I +compiler-libs -o ocamlfind -g findlib.cma unix.cma \
- ocaml_args.cmo frontend.cmo
- ocamlc -I +compiler-libs -opaque -c topfind.mli
- ocamlc -I +compiler-libs -opaque -g -c topfind.ml
- ocamlc -I +compiler-libs -a -o findlib_top.cma topfind.cmo
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat topfind_rd1.p | \
- ../../tools/patch '@SITELIB@' '/home/coq/.opam/4.07.1+flambda/lib' \
- >topfind
- ocamlc -I +compiler-libs -opaque -c fl_dynload.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_dynload.ml
- ocamlc -I +compiler-libs -a -o findlib_dynload.cma fl_dynload.cmo
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- /usr/bin/make all-config
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat findlib.conf.in | \
- tools/patch '@SITELIB@' '/home/coq/.opam/4.07.1+flambda/lib' >findlib.conf
- if ./tools/cmd_from_same_dir ocamlc; then \
- echo 'ocamlc="ocamlc.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamlopt; then \
- echo 'ocamlopt="ocamlopt.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamldep; then \
- echo 'ocamldep="ocamldep.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamldoc; then \
- echo 'ocamldoc="ocamldoc.opt"' >>findlib.conf; \
- fi
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
Processing 4/12: [dune: ocaml bootstrap.ml] [ocamlfind: make opt]
+ /usr/bin/make "opt" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1)
- for p in findlib; do ( cd src/$p; /usr/bin/make opt ) || exit; done
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- ocamlopt -I +compiler-libs -g -opaque -c findlib_config.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_split.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_metatoken.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_meta.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_metascanner.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_topo.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_package_base.ml
- ocamlopt -I +compiler-libs -g -opaque -c findlib.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_args.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_lint.ml
- ocamlopt -I +compiler-libs -g -a -o findlib.cmxa findlib_config.cmx fl_split.cmx fl_metatoken.cmx fl_meta.cmx fl_metascanner.cmx fl_topo.cmx fl_package_base.cmx findlib.cmx fl_args.cmx fl_lint.cmx
- if [ 1 -gt 0 ]; then \
- ocamlopt -I +compiler-libs -g -shared -o findlib.cmxs findlib_config.cmx fl_split.cmx fl_metatoken.cmx fl_meta.cmx fl_metascanner.cmx fl_topo.cmx fl_package_base.cmx findlib.cmx fl_args.cmx fl_lint.cmx; \
- fi
- ocamlopt -I +compiler-libs -g -opaque -c ocaml_args.ml
- ocamlopt -I +compiler-libs -g -opaque -c frontend.ml
- File "frontend.ml", line 1826, characters 16-29:
- Warning 3: deprecated: Stdlib.String.create
- Use Bytes.create instead.
- ocamlopt -I +compiler-libs -g -o ocamlfind_opt findlib.cmxa unix.cmxa \
- ocaml_args.cmx frontend.cmx
- ocamlopt -I +compiler-libs -g -opaque -c topfind.ml
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Topdirs, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Toploop, and its interface was not compiled with -opaque
- ocamlopt -I +compiler-libs -g -a -o findlib_top.cmxa topfind.cmx
- if [ 1 -gt 0 ]; then \
- ocamlopt -I +compiler-libs -g -shared -o findlib_top.cmxs topfind.cmx; \
- fi
- ocamlopt -I +compiler-libs -g -opaque -c fl_dynload.ml
- ocamlopt -I +compiler-libs -g -a -o findlib_dynload.cmxa fl_dynload.cmx
- if [ 1 -gt 0 ]; then \
- ocamlopt -I +compiler-libs -g -shared -o findlib_dynload.cmxs fl_dynload.cmx; \
- fi
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- for p in findlib; do ( cd src/$p; /usr/bin/make opt ) || exit; done
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- ocamlopt -I +compiler-libs -g -opaque -c findlib_config.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_split.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_metatoken.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_meta.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_metascanner.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_topo.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_package_base.ml
- ocamlopt -I +compiler-libs -g -opaque -c findlib.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_args.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_lint.ml
- ocamlopt -I +compiler-libs -g -a -o findlib.cmxa findlib_config.cmx fl_split.cmx fl_metatoken.cmx fl_meta.cmx fl_metascanner.cmx fl_topo.cmx fl_package_base.cmx findlib.cmx fl_args.cmx fl_lint.cmx
- if [ 1 -gt 0 ]; then \
- ocamlopt -I +compiler-libs -g -shared -o findlib.cmxs findlib_config.cmx fl_split.cmx fl_metatoken.cmx fl_meta.cmx fl_metascanner.cmx fl_topo.cmx fl_package_base.cmx findlib.cmx fl_args.cmx fl_lint.cmx; \
- fi
- ocamlopt -I +compiler-libs -g -opaque -c ocaml_args.ml
- ocamlopt -I +compiler-libs -g -opaque -c frontend.ml
- File "frontend.ml", line 1826, characters 16-29:
- Warning 3: deprecated: Stdlib.String.create
- Use Bytes.create instead.
- ocamlopt -I +compiler-libs -g -o ocamlfind_opt findlib.cmxa unix.cmxa \
- ocaml_args.cmx frontend.cmx
- ocamlopt -I +compiler-libs -g -opaque -c topfind.ml
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Topdirs, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Toploop, and its interface was not compiled with -opaque
- ocamlopt -I +compiler-libs -g -a -o findlib_top.cmxa topfind.cmx
- if [ 1 -gt 0 ]; then \
- ocamlopt -I +compiler-libs -g -shared -o findlib_top.cmxs topfind.cmx; \
- fi
- ocamlopt -I +compiler-libs -g -opaque -c fl_dynload.ml
- ocamlopt -I +compiler-libs -g -a -o findlib_dynload.cmxa fl_dynload.cmx
- if [ 1 -gt 0 ]; then \
- ocamlopt -I +compiler-libs -g -shared -o findlib_dynload.cmxs fl_dynload.cmx; \
- fi
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
-> compiled ocamlfind.1.8.1
Processing 4/12: [dune: ocaml bootstrap.ml]
Processing 5/12: [dune: ocaml bootstrap.ml] [ocamlfind: make install]
+ /usr/bin/make "install" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1)
- mkdir -p "/home/coq/.opam/4.07.1+flambda/bin"
- mkdir -p "/home/coq/.opam/4.07.1+flambda/man"
- /usr/bin/make install-config
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- mkdir -p "`dirname \"/home/coq/.opam/4.07.1+flambda/lib/findlib.conf\"`"
- test -f "/home/coq/.opam/4.07.1+flambda/lib/findlib.conf" || cp findlib.conf "/home/coq/.opam/4.07.1+flambda/lib/findlib.conf"
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- for p in findlib; do ( cd src/$p; /usr/bin/make install ); done
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- mkdir -p "/home/coq/.opam/4.07.1+flambda/lib/findlib"
- mkdir -p "/home/coq/.opam/4.07.1+flambda/bin"
- test 1 -eq 0 || cp topfind "/home/coq/.opam/4.07.1+flambda/lib/ocaml"
- files=` ../../tools/collect_files ../../Makefile.config findlib.cmi findlib.mli findlib.cma findlib.cmxa findlib.a findlib.cmxs topfind.cmi topfind.mli fl_package_base.mli fl_package_base.cmi fl_metascanner.mli fl_metascanner.cmi fl_metatoken.cmi findlib_top.cma findlib_top.cmxa findlib_top.a findlib_top.cmxs findlib_dynload.cma findlib_dynload.cmxa findlib_dynload.a findlib_dynload.cmxs fl_dynload.mli fl_dynload.cmi META` && \
- cp $files "/home/coq/.opam/4.07.1+flambda/lib/findlib"
- f="ocamlfind"; { test -f ocamlfind_opt && f="ocamlfind_opt"; }; \
- cp $f "/home/coq/.opam/4.07.1+flambda/bin/ocamlfind"
- # the following "if" block is only needed for 4.00beta2
- if [ 1 -eq 0 -a -f "/home/coq/.opam/4.07.1+flambda/lib/ocaml/compiler-libs/topdirs.cmi" ]; then \
- cd "/home/coq/.opam/4.07.1+flambda/lib/ocaml/compiler-libs/"; \
- cp topdirs.cmi toploop.cmi "/home/coq/.opam/4.07.1+flambda/lib/findlib/"; \
- fi
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- /usr/bin/make install-meta
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- for x in `ls site-lib-src`; do if [ -f "site-lib-src/$x/META" ]; then mkdir -p "/home/coq/.opam/4.07.1+flambda/lib/$x"; cp site-lib-src/$x/META "/home/coq/.opam/4.07.1+flambda/lib/$x"; fi; done
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- test -z "" || { cd src/findlib; /usr/bin/make install-num-top; }
- if [ 0 -eq 1 ]; then \
- cp tools/safe_camlp4 "/home/coq/.opam/4.07.1+flambda/bin"; \
- fi
- /usr/bin/make install-doc
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- mkdir -p "/home/coq/.opam/4.07.1+flambda/man/man1" "/home/coq/.opam/4.07.1+flambda/man/man3" "/home/coq/.opam/4.07.1+flambda/man/man5"
- cp doc/ref-man/ocamlfind.1 "/home/coq/.opam/4.07.1+flambda/man/man1"
- cp doc/ref-man/META.5 doc/ref-man/site-lib.5 doc/ref-man/findlib.conf.5 "/home/coq/.opam/4.07.1+flambda/man/man5"
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- mkdir -p "/home/coq/.opam/4.07.1+flambda/bin"
- mkdir -p "/home/coq/.opam/4.07.1+flambda/man"
- /usr/bin/make install-config
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- mkdir -p "`dirname \"/home/coq/.opam/4.07.1+flambda/lib/findlib.conf\"`"
- test -f "/home/coq/.opam/4.07.1+flambda/lib/findlib.conf" || cp findlib.conf "/home/coq/.opam/4.07.1+flambda/lib/findlib.conf"
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- for p in findlib; do ( cd src/$p; /usr/bin/make install ); done
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- mkdir -p "/home/coq/.opam/4.07.1+flambda/lib/findlib"
- mkdir -p "/home/coq/.opam/4.07.1+flambda/bin"
- test 1 -eq 0 || cp topfind "/home/coq/.opam/4.07.1+flambda/lib/ocaml"
- files=` ../../tools/collect_files ../../Makefile.config findlib.cmi findlib.mli findlib.cma findlib.cmxa findlib.a findlib.cmxs topfind.cmi topfind.mli fl_package_base.mli fl_package_base.cmi fl_metascanner.mli fl_metascanner.cmi fl_metatoken.cmi findlib_top.cma findlib_top.cmxa findlib_top.a findlib_top.cmxs findlib_dynload.cma findlib_dynload.cmxa findlib_dynload.a findlib_dynload.cmxs fl_dynload.mli fl_dynload.cmi META` && \
- cp $files "/home/coq/.opam/4.07.1+flambda/lib/findlib"
- f="ocamlfind"; { test -f ocamlfind_opt && f="ocamlfind_opt"; }; \
- cp $f "/home/coq/.opam/4.07.1+flambda/bin/ocamlfind"
- # the following "if" block is only needed for 4.00beta2
- if [ 1 -eq 0 -a -f "/home/coq/.opam/4.07.1+flambda/lib/ocaml/compiler-libs/topdirs.cmi" ]; then \
- cd "/home/coq/.opam/4.07.1+flambda/lib/ocaml/compiler-libs/"; \
- cp topdirs.cmi toploop.cmi "/home/coq/.opam/4.07.1+flambda/lib/findlib/"; \
- fi
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1/src/findlib'
- /usr/bin/make install-meta
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- for x in `ls site-lib-src`; do if [ -f "site-lib-src/$x/META" ]; then mkdir -p "/home/coq/.opam/4.07.1+flambda/lib/$x"; cp site-lib-src/$x/META "/home/coq/.opam/4.07.1+flambda/lib/$x"; fi; done
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- test -z "" || { cd src/findlib; /usr/bin/make install-num-top; }
- if [ 0 -eq 1 ]; then \
- cp tools/safe_camlp4 "/home/coq/.opam/4.07.1+flambda/bin"; \
- fi
- /usr/bin/make install-doc
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
- mkdir -p "/home/coq/.opam/4.07.1+flambda/man/man1" "/home/coq/.opam/4.07.1+flambda/man/man3" "/home/coq/.opam/4.07.1+flambda/man/man5"
- cp doc/ref-man/ocamlfind.1 "/home/coq/.opam/4.07.1+flambda/man/man1"
- cp doc/ref-man/META.5 doc/ref-man/site-lib.5 doc/ref-man/findlib.conf.5 "/home/coq/.opam/4.07.1+flambda/man/man5"
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/ocamlfind.1.8.1'
-> installed ocamlfind.1.8.1
Processing 5/12: [dune: ocaml bootstrap.ml]
Processing 6/12: [dune: ocaml bootstrap.ml] [num: patch]
Processing 6/12: [dune: ocaml bootstrap.ml] [num: make]
+ /usr/bin/make (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3)
- /usr/bin/make -C src all
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- ocamlc -ccopt -DBNG_ARCH_amd64 -c bng.c
- ocamlc -ccopt -DBNG_ARCH_amd64 -c nat_stubs.c
- ocamlmklib -oc nums bng.o nat_stubs.o
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c int_misc.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c int_misc.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c nat.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c nat.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c big_int.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c big_int.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_flags.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_flags.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c ratio.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c ratio.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c num.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c num.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_status.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_status.ml
- ocamlmklib -o nums -oc nums -linkall int_misc.cmo nat.cmo big_int.cmo arith_flags.cmo ratio.cmo num.cmo arith_status.cmo
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c int_misc.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c nat.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c big_int.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c arith_flags.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c ratio.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c num.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c arith_status.ml
- ocamlmklib -o nums -oc nums -linkall int_misc.cmx nat.cmx big_int.cmx arith_flags.cmx ratio.cmx num.cmx arith_status.cmx
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -I . -shared -o nums.cmxs nums.cmxa
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- /usr/bin/make -C toplevel all
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top_printers.mli
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top_printers.ml
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top.mli
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top.ml
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -a -o num_top.cma num_top_printers.cmo num_top.cmo
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
- /usr/bin/make -C src all
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- ocamlc -ccopt -DBNG_ARCH_amd64 -c bng.c
- ocamlc -ccopt -DBNG_ARCH_amd64 -c nat_stubs.c
- ocamlmklib -oc nums bng.o nat_stubs.o
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c int_misc.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c int_misc.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c nat.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c nat.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c big_int.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c big_int.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_flags.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_flags.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c ratio.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c ratio.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c num.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c num.ml
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_status.mli
- ocamlc -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -c arith_status.ml
- ocamlmklib -o nums -oc nums -linkall int_misc.cmo nat.cmo big_int.cmo arith_flags.cmo ratio.cmo num.cmo arith_status.cmo
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c int_misc.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c nat.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c big_int.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c arith_flags.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c ratio.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c num.ml
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -c arith_status.ml
- ocamlmklib -o nums -oc nums -linkall int_misc.cmx nat.cmx big_int.cmx arith_flags.cmx ratio.cmx num.cmx arith_status.cmx
- ocamlopt -w +a-4-9-41-42-44-45-48 -warn-error A -bin-annot -g -safe-string -strict-sequence -strict-formats -O3 -I . -shared -o nums.cmxs nums.cmxa
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- /usr/bin/make -C toplevel all
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top_printers.mli
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top_printers.ml
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top.mli
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -c num_top.ml
- ocamlc -I ../src -I +compiler-libs -w +a-4-9-41-42-44-45-48 -warn-error A -safe-string -strict-sequence -strict-formats -a -o num_top.cma num_top_printers.cmo num_top.cmo
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
-> compiled num.1.3
Processing 6/12: [dune: ocaml bootstrap.ml]
Processing 7/12: [dune: ocaml bootstrap.ml] [num: make install]
+ /usr/bin/make "install" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3)
- /usr/bin/make -C src install
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- install -d /home/coq/.opam/4.07.1+flambda/lib/ocaml
- sed -e 's/%%VERSION%%/1.3/g' META.in > META
- ocamlfind install num META
- Installed /home/coq/.opam/4.07.1+flambda/lib/num/META
- rm -f META
- install -m 644 nums.cma libnums.a big_int.cmi nat.cmi num.cmi ratio.cmi arith_status.cmi big_int.mli nat.mli num.mli ratio.mli arith_status.mli big_int.cmti nat.cmti num.cmti ratio.cmti arith_status.cmti nums.cmxa nums.a int_misc.cmx nat.cmx big_int.cmx arith_flags.cmx ratio.cmx num.cmx arith_status.cmx nums.cmxs /home/coq/.opam/4.07.1+flambda/lib/ocaml
- install -d /home/coq/.opam/4.07.1+flambda/lib/ocaml/stublibs
- install dllnums.so /home/coq/.opam/4.07.1+flambda/lib/ocaml/stublibs
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- /usr/bin/make -C toplevel install
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
- sed -e 's/%%VERSION%%/1.3/g' META.in > META
- ocamlfind install num-top META num_top.cma num_top.cmi num_top_printers.cmi
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/num_top_printers.cmi
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/num_top.cmi
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/num_top.cma
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/META
- rm -f META
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
- /usr/bin/make -C src install
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- install -d /home/coq/.opam/4.07.1+flambda/lib/ocaml
- sed -e 's/%%VERSION%%/1.3/g' META.in > META
- ocamlfind install num META
- Installed /home/coq/.opam/4.07.1+flambda/lib/num/META
- rm -f META
- install -m 644 nums.cma libnums.a big_int.cmi nat.cmi num.cmi ratio.cmi arith_status.cmi big_int.mli nat.mli num.mli ratio.mli arith_status.mli big_int.cmti nat.cmti num.cmti ratio.cmti arith_status.cmti nums.cmxa nums.a int_misc.cmx nat.cmx big_int.cmx arith_flags.cmx ratio.cmx num.cmx arith_status.cmx nums.cmxs /home/coq/.opam/4.07.1+flambda/lib/ocaml
- install -d /home/coq/.opam/4.07.1+flambda/lib/ocaml/stublibs
- install dllnums.so /home/coq/.opam/4.07.1+flambda/lib/ocaml/stublibs
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/src'
- /usr/bin/make -C toplevel install
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
- sed -e 's/%%VERSION%%/1.3/g' META.in > META
- ocamlfind install num-top META num_top.cma num_top.cmi num_top_printers.cmi
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/num_top_printers.cmi
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/num_top.cmi
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/num_top.cma
- Installed /home/coq/.opam/4.07.1+flambda/lib/num-top/META
- rm -f META
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/num.1.3/toplevel'
-> installed num.1.3
Processing 7/12: [dune: ocaml bootstrap.ml]
+ /home/coq/.opam/4.07.1+flambda/bin/ocaml "bootstrap.ml" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/dune.1.11.4)
- cp src/ocaml-syntax-shims/pp.real.ml src/ocaml-syntax-shims/pp.ml
- cp src/ocaml-syntax-shims/shims.406.ml src/ocaml-syntax-shims/shims.ml
- /home/coq/.opam/4.07.1+flambda/bin/ocamllex.opt -q src/ocaml-syntax-shims/let_trail.mll
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules src/ocaml-syntax-shims/let_trail.mli src/ocaml-syntax-shims/let_trail.ml src/ocaml-syntax-shims/pp.ml src/ocaml-syntax-shims/shims.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamlopt.opt -g -w -40 -o boot-pp.exe -I +compiler-libs ocamlcommon.cmxa boot_pp.ml
- /home/coq/.opam/4.07.1+flambda/bin/ocamllex.opt -q src/ocamlobjinfo.mll
- /home/coq/.opam/4.07.1+flambda/bin/ocamllex.opt -q src/meta_lexer.mll
- /home/coq/.opam/4.07.1+flambda/bin/ocamllex.opt -q src/dune_lexer.mll
- /home/coq/.opam/4.07.1+flambda/bin/ocamllex.opt -q src/dune_lang/dune_lexer.mll
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/action.mli src/action.ml src/action_ast.ml src/action_dune_lang.mli src/action_dune_lang.ml src/action_exec.mli src/action_exec.ml src/action_intf.ml src/action_mapper.mli src/action_mapper.ml src/action_to_sh.mli src/action_to_sh.boot.ml src/action_unexpanded.mli src/action_unexpanded.ml src/alias.mli src/alias.ml src/artifact_substitution.mli src/artifact_substitution.ml src/artifacts.mli src/artifacts.ml src/binary_kind.mli src/binary_kind.ml src/bindings.mli src/bindings.ml src/blang.mli src/blang.ml src/bootstrap.mli src/bootstrap.boot.ml src/build.mli src/build.ml otherlibs/build-info/src/build_info.mli otherlibs/build-info/src/build_info.ml otherlibs/build-info/src/build_info_data.mli otherlibs/build-info/src/build_info_data.boot.ml src/build_system.mli src/build_system.ml src/c.mli src/c.ml src/c_sources.mli src/c_sources.ml src/cached_digest.mli src/cached_digest.ml src/check_rules.mli src/check_rules.ml src/cinaps.mli src/cinaps.boot.ml src/clflags.mli src/clflags.ml src/cm_files.mli src/cm_files.ml src/cm_kind.mli src/cm_kind.ml src/colors.mli src/colors.ml src/command.mli src/command.ml src/compilation_context.mli src/compilation_context.ml src/config.mli src/config.ml src/context.mli src/context.ml src/coq_module.mli src/coq_module.ml src/coq_rules.mli src/coq_rules.boot.ml src/dep.mli src/dep.ml src/dep_graph.mli src/dep_graph.ml src/dep_path.mli src/dep_path.ml src/dep_rules.mli src/dep_rules.ml src/dialect.mli src/dialect.ml src/diff.mli src/diff.ml src/dir_contents.mli src/dir_contents.ml src/dir_set.mli src/dir_set.ml src/dir_status.mli src/dir_status.ml src/dir_with_dune.mli src/dir_with_dune.ml src/dpath.mli src/dpath.ml src/dune_env.mli src/dune_env.ml src/dune_file.mli src/dune_file.ml src/dune_init.mli src/dune_init.ml src/dune_lexer.mli src/dune_lexer.ml src/dune_load.mli src/dune_load.ml src/dune_package.mli src/dune_package.ml src/dune_project.mli src/dune_project.ml vendor/boot/dune_re.ml src/dynlink_supported.mli src/dynlink_supported.ml src/env_node.mli src/env_node.ml src/exe.mli src/exe.ml src/exe_rules.mli src/exe_rules.ml src/expander.mli src/expander.ml src/file_binding.mli src/file_binding.ml src/file_selector.mli src/file_selector.ml src/file_tree.mli src/file_tree.ml src/findlib.mli src/findlib.ml src/format_dune_lang.mli src/format_dune_lang.ml src/format_rules.mli src/format_rules.ml src/gen_meta.mli src/gen_meta.ml src/gen_rules.mli src/gen_rules.ml src/glob.mli src/glob.ml src/glob_lexer.mli src/glob_lexer.boot.ml src/hooks.mli src/hooks.ml src/import.ml src/inline_tests.mli src/inline_tests.boot.ml src/install.mli src/install.ml src/install_rules.mli src/install_rules.ml src/installed_dune_file.mli src/installed_dune_file.ml src/js_of_ocaml_rules.mli src/js_of_ocaml_rules.boot.ml src/lib.mli src/lib.ml src/lib_archives.mli src/lib_archives.ml src/lib_config.mli src/lib_config.ml src/lib_deps_info.mli src/lib_deps_info.ml src/lib_file_deps.mli src/lib_file_deps.ml src/lib_info.mli src/lib_info.ml src/lib_kind.mli src/lib_kind.ml src/lib_name.mli src/lib_name.ml src/lib_rules.mli src/lib_rules.ml src/link_time_code_gen.mli src/link_time_code_gen.ml src/local_package.mli src/local_package.ml src/main.mli src/main.ml src/menhir.mli src/menhir.boot.ml src/merlin.mli src/merlin.ml src/meta.mli src/meta.ml src/meta_lexer.mli src/meta_lexer.ml src/ml_kind.mli src/ml_kind.ml src/mode.mli src/mode.ml src/module.mli src/module.ml src/module_compilation.mli src/module_compilation.ml src/modules.mli src/modules.ml src/modules_field_evaluator.mli src/modules_field_evaluator.ml src/obj_dir.mli src/obj_dir.ml src/ocaml_flags.mli src/ocaml_flags.ml src/ocaml_version.mli src/ocaml_version.ml src/ocamldep.mli src/ocamldep.ml src/ocamlobjinfo.mli src/ocamlobjinfo.ml src/odoc.mli src/odoc.boot.ml vendor/boot/opamBaseParser.ml vendor/boot/opamLexer.ml vendor/boot/opamParserTypes.ml vendor/boot/opamPrinter.ml src/opam_create.mli src/opam_create.boot.ml src/opam_file.mli src/opam_file.ml src/ordered_set_lang.mli src/ordered_set_lang.ml src/package.mli src/package.ml src/packages.mli src/packages.ml src/per_item.mli src/per_item.ml src/persistent.mli src/persistent.ml src/pform.mli src/pform.ml src/predicate.mli src/predicate.ml src/predicate_lang.mli src/predicate_lang.ml src/preprocessing.mli src/preprocessing.ml src/print_diff.mli src/print_diff.ml src/process.mli src/process.ml src/promotion.mli src/promotion.ml src/report_error.mli src/report_error.ml src/response_file.mli src/response_file.ml src/rule.mli src/rule.ml src/rules.mli src/rules.ml src/scheduler.mli src/scheduler.ml src/scheme.mli src/scheme.ml src/scope.mli src/scope.ml src/setup.mli src/setup.boot.ml src/simple_rules.mli src/simple_rules.ml src/spawn.mli src/spawn.ml src/stanza.mli src/stanza.ml src/static_deps.mli src/static_deps.ml src/stats.mli src/stats.boot.ml src/string_with_vars.mli src/string_with_vars.ml src/sub_dirs.mli src/sub_dirs.ml src/sub_system.mli src/sub_system.ml src/sub_system_info.mli src/sub_system_info.ml src/sub_system_intf.ml src/sub_system_name.mli src/sub_system_name.ml src/super_context.mli src/super_context.ml src/syntax.mli src/syntax.ml src/test_rules.mli src/test_rules.boot.ml src/top_closure.mli src/top_closure.ml src/toplevel.mli src/toplevel.ml src/upgrader.mli src/upgrader.boot.ml src/utils.mli src/utils.ml src/utop.mli src/utop.boot.ml src/value.mli src/value.ml src/variant.mli src/variant.ml src/vcs.mli src/vcs.ml src/versioned_file.mli src/versioned_file.ml src/vimpl.mli src/vimpl.ml src/virtual_rules.mli src/virtual_rules.ml src/visibility.mli src/visibility.ml src/watermarks.mli src/watermarks.ml src/workspace.mli src/workspace.ml src/wrapped.mli src/wrapped.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/dag/dag.mli src/dag/dag.ml src/dag/dag_intf.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/stdune/caml/dune_caml.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/dune_lang/dune_lang.mli src/dune_lang/dune_lang.ml src/dune_lang/atom.mli src/dune_lang/atom.ml src/dune_lang/combinators.ml src/dune_lang/dune_lexer.mli src/dune_lang/dune_lexer.ml src/dune_lang/escape.mli src/dune_lang/escape.ml src/dune_lang/file_syntax.mli src/dune_lang/file_syntax.ml src/dune_lang/jbuild_lexer.mli src/dune_lang/jbuild_lexer.boot.ml src/dune_lang/lexer.mli src/dune_lang/lexer.ml src/dune_lang/lexer_shared.mli src/dune_lang/lexer_shared.ml src/dune_lang/template.mli src/dune_lang/template.ml src/dune_lang/types.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/stdune/result/dune_result.ml src/stdune/result/result.mli src/stdune/result/result.ml src/stdune/result/result_compat.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/fiber/fiber.mli src/fiber/fiber.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' vendor/incremental-cycles/src/incremental_cycles.mli vendor/incremental-cycles/src/incremental_cycles.ml vendor/incremental-cycles/src/incremental_cycles_intf.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/memo/memo.mli src/memo/memo.ml src/memo/implicit_output.mli src/memo/implicit_output.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/ocaml-config/ocaml_config.mli src/ocaml-config/ocaml_config.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/stdune/stdune.ml src/stdune/ansi_color.mli src/stdune/ansi_color.ml src/stdune/appendable_list.mli src/stdune/appendable_list.ml src/stdune/array.ml src/stdune/bin.mli src/stdune/bin.ml src/stdune/bool.mli src/stdune/bool.ml src/stdune/bytes.mli src/stdune/bytes.ml src/stdune/char.ml src/stdune/code_error.mli src/stdune/code_error.ml src/stdune/common.ml src/stdune/comparable.mli src/stdune/comparable.ml src/stdune/comparable_intf.ml src/stdune/comparator.mli src/stdune/comparator.ml src/stdune/console.mli src/stdune/console.ml src/stdune/csexp.mli src/stdune/csexp.ml src/stdune/digest.mli src/stdune/digest.ml src/stdune/dyn.mli src/stdune/dyn.ml src/stdune/either.mli src/stdune/either.ml src/stdune/env.mli src/stdune/env.ml src/stdune/escape.mli src/stdune/escape.ml src/stdune/exn.mli src/stdune/exn.ml src/stdune/exn_with_backtrace.mli src/stdune/exn_with_backtrace.ml src/stdune/fdecl.mli src/stdune/fdecl.ml src/stdune/filename.mli src/stdune/filename.ml src/stdune/float.mli src/stdune/float.ml src/stdune/fmt.mli src/stdune/fmt.ml src/stdune/fn.mli src/stdune/fn.ml src/stdune/hashable.ml src/stdune/hashtbl.mli src/stdune/hashtbl.ml src/stdune/hashtbl_intf.ml src/stdune/id.mli src/stdune/id.ml src/stdune/int.mli src/stdune/int.ml src/stdune/interned.mli src/stdune/interned.ml src/stdune/io.mli src/stdune/io.ml src/stdune/lexbuf.mli src/stdune/lexbuf.ml src/stdune/list.mli src/stdune/list.ml src/stdune/loc.mli src/stdune/loc.ml src/stdune/loc0.ml src/stdune/log.mli src/stdune/log.ml src/stdune/map.mli src/stdune/map.ml src/stdune/map_intf.ml src/stdune/monad.mli src/stdune/monad.ml src/stdune/nothing.mli src/stdune/nothing.ml src/stdune/option.mli src/stdune/option.ml src/stdune/or_exn.mli src/stdune/or_exn.ml src/stdune/ordered.mli src/stdune/ordered.ml src/stdune/ordering.mli src/stdune/ordering.ml src/stdune/path.mli src/stdune/path.ml src/stdune/path_intf.ml src/stdune/poly.mli src/stdune/poly.ml src/stdune/pp.mli src/stdune/pp.ml src/stdune/proc.mli src/stdune/proc.ml src/stdune/result.mli src/stdune/result.ml src/stdune/set.mli src/stdune/set.ml src/stdune/set_intf.ml src/stdune/sexp.mli src/stdune/sexp.ml src/stdune/signal.mli src/stdune/signal.ml src/stdune/staged.mli src/stdune/staged.ml src/stdune/string.mli src/stdune/string.ml src/stdune/string_split.mli src/stdune/string_split.ml src/stdune/table.mli src/stdune/table.ml src/stdune/tuple.mli src/stdune/tuple.ml src/stdune/type_eq.mli src/stdune/type_eq.ml src/stdune/unit.mli src/stdune/unit.ml src/stdune/univ_map.mli src/stdune/univ_map.ml src/stdune/user_error.mli src/stdune/user_error.ml src/stdune/user_message.mli src/stdune/user_message.ml src/stdune/user_warning.mli src/stdune/user_warning.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/wp/wp.mli src/wp/wp.boot.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamldep.opt -modules -pp './boot-pp.exe -dump-ast' src/xdg/xdg.mli src/xdg/xdg.ml > boot-depends.txt
- /home/coq/.opam/4.07.1+flambda/bin/ocamlc.opt -g -w -40 -o boot.exe -pp './boot-pp.exe -dump-ast' -I +threads unix.cma threads.cma boot.ml
Processing 7/12: [dune: ./boot.exe 2]
+ /home/coq/.opam/4.07.1+flambda/.opam-switch/build/dune.1.11.4/./boot.exe "--release" "-j" "2" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/dune.1.11.4)
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Incremental_cycles, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Build_info__Build_info_data, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Build_info__Build_info_data, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Dune__Colors, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Cmdliner, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Fiber, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Stdune__Exn_with_backtrace, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Dune__Report_error, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Dune__Colors, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Cmdliner, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Fiber, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Stdune__Exn_with_backtrace, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Dune__Report_error, and its interface was not compiled with -opaque
-> compiled dune.1.11.4
-> installed dune.1.11.4
Processing 9/12: [coq: ./configure no]
+ /home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq.8.11+alpha/./configure "-prefix" "/home/coq/.opam/4.07.1+flambda" "-native-compiler" "no" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq.8.11+alpha)
- Creating pre-commit hook in .git/hooks/pre-commit
- You have OCaml 4.07.1. Good!
- You have OCamlfind 1.8.1. Good!
- You have native-code compilation. Good!
- You have the Num library installed. Good!
- LablGtk3 not found:
- => no CoqIde will be built.
-
- Architecture : Linux
- Sys.os_type : Unix
- Coq VM bytecode link flags : -dllib -lcoqrun -dllpath /home/coq/.opam/4.07.1+flambda/lib/coq/kernel/byterun
- Other bytecode link flags :
- OCaml version : 4.07.1
- OCaml binaries in : /home/coq/.opam/4.07.1+flambda/bin/
- OCaml library in : /home/coq/.opam/4.07.1+flambda/lib/ocaml
- OCaml flambda flags :
- Native dynamic link support : true
- CoqIde : no
- Documentation : None
- Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
- Coq web site : http://coq.inria.fr/
- Bytecode VM enabled : true
- Native Compiler enabled : false
-
- Paths for true installation:
- - the Coq binaries will be copied in /home/coq/.opam/4.07.1+flambda/bin
- - the Coq library will be copied in /home/coq/.opam/4.07.1+flambda/lib/coq
- - the Coqide configuration files will be copied in /home/coq/.opam/4.07.1+flambda/etc/xdg/coq
- - the Coqide data files will be copied in /home/coq/.opam/4.07.1+flambda/share/coq
- - the Coq man pages will be copied in /home/coq/.opam/4.07.1+flambda/share/man
- - the Coq documentation will be copied in /home/coq/.opam/4.07.1+flambda/share/doc/coq
- - the Coqdoc LaTeX files will be copied in /home/coq/.opam/4.07.1+flambda/share/texmf/tex/latex/misc
-
- If anything is wrong above, please restart './configure'.
-
- *Warning* To compile the system for a new architecture
- don't forget to do a 'make clean' before './configure'.
Processing 9/12: [coq: dune build]
+ /home/coq/.opam/4.07.1+flambda/bin/dune "build" "@vodeps" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq.8.11+alpha)
Processing 9/12: [coq: dune exec]
+ /home/coq/.opam/4.07.1+flambda/bin/dune "exec" "coq_dune" "_build/default/.vfiles.d" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq.8.11+alpha)
Processing 9/12: [coq: dune build]
+ /home/coq/.opam/4.07.1+flambda/bin/dune "build" "-p" "coq" "-j" "2" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq.8.11+alpha)
-> compiled coq.8.11+alpha
-> installed coq.8.11+alpha
Processing 11/12: [coq-bignums: make]
+ /usr/bin/make "-j2" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev)
- coq_makefile -f _CoqProject -o Makefile.coq
- Warning: -extra and -extra-phony are deprecated.
- Warning: Write the extra targets in Makefile.coq.local.
-
- make -f Makefile.coq Makefile
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev'
- ocaml BigN/gen/NMake_gen.ml > BigN/NMake_gen.v || (RV=$?; rm -f BigN/NMake_gen.v; exit ${RV})
- COQDEP plugin/bignums_syntax_plugin.mlpack
- CAMLDEP plugin/bignums_syntax.ml
- COQDEP VFILES
- make[1]: Nothing to be done for 'Makefile'.
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev'
- make -f Makefile.coq all
- make[1]: Entering directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev'
- CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
- COQC SpecViaZ/NSig.v
- File "plugin/bignums_syntax.ml", line 47, characters 2-47:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 55, characters 15-42:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 56, characters 15-42:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 65, characters 14-41:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- COQC SpecViaZ/ZSig.v
- COQC SpecViaQ/QSig.v
- CAMLOPT -pack -o plugin/bignums_syntax_plugin.cmx
- COQC SpecViaZ/NSigNAxioms.v
- COQC SpecViaZ/ZSigZAxioms.v
- CAMLOPT -a -o plugin/bignums_syntax_plugin.cmxa
- CAMLOPT -shared -o plugin/bignums_syntax_plugin.cmxs
- COQC BigNumPrelude.v
- File "./BigNumPrelude.v", line 51, characters 0-242:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./BigNumPrelude.v", line 58, characters 0-227:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- COQC CyclicDouble/DoubleBase.v
- COQC BigQ/QMake.v
- COQC BigZ/ZMake.v
- COQC CyclicDouble/DoubleAdd.v
- COQC CyclicDouble/DoubleSub.v
- COQC CyclicDouble/DoubleMul.v
- COQC CyclicDouble/DoubleSqrt.v
- File "./CyclicDouble/DoubleSqrt.v", line 685, characters 1-23:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "./BigQ/QMake.v", line 613, characters 1-5:
- Error: Anomaly "the kernel does not support existential variables."
- Please report at http://coq.inria.fr/bugs/.
-
- make[2]: *** [Makefile.coq:670: BigQ/QMake.vo] Error 129
- make[2]: *** Waiting for unfinished jobs....
- make[1]: *** [Makefile.coq:324: all] Error 2
- make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev'
- make: *** [Makefile:2: all] Error 2
[ERROR] The compilation of coq-bignums failed at "/usr/bin/make -j2".
#=== ERROR while compiling coq-bignums.8.11.dev ===============================#
# context 2.0.5 | linux/x86_64 | ocaml-variants.4.07.1+flambda | https://coq.inria.fr/opam/extra-dev#2019-11-19 15:40
# path ~/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev
# command /usr/bin/make -j2
# exit-code 2
# env-file ~/.opam/log/coq-bignums-158-afaca3.env
# output-file ~/.opam/log/coq-bignums-158-afaca3.out
### output ###
# [...]
# Warning: Adding and removing hints in the core database implicitly is
# deprecated. Please specify a hint database.
# [implicit-core-hint-db,deprecated]
# File "./BigQ/QMake.v", line 613, characters 1-5:
# Error: Anomaly "the kernel does not support existential variables."
# Please report at http://coq.inria.fr/bugs/.
#
# make[2]: *** [Makefile.coq:670: BigQ/QMake.vo] Error 129
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [Makefile.coq:324: all] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.8.11.dev'
# make: *** [Makefile:2: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-bignums 8.11.dev
+-
+- The following changes have been performed
| - install conf-m4 1
| - install coq 8.11+alpha
| - install dune 1.11.4
| - install num 1.3
| - install ocamlfind 1.8.1
+-
The former state can be restored with:
opam switch import "/home/coq/.opam/4.07.1+flambda/.opam-switch/backup/state-20191122005421.export"
'opam install -y -v -j 2 coq coq-bignums' failed.
Removing intermediate container 9c57c8388e88
The command '/bin/bash --login -c set -x && eval $(opam env --switch=${COMPILER_EDGE} --set-switch) && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev && opam update -y -u && opam pin add -n -y -k git coq.${COQ_VERSION} "git+https://github.com/coq/coq#${COQ_COMMIT}" && opam install -y -v -j ${NJOBS} coq ${COQ_EXTRA_OPAM} && opam clean -a -s --logs && opam config list && opam list' returned a non-zero code: 31

Do you think this error is expected?

Anyway as suggested in #26 (comment), we could now replace coq_makefile with dune for the coq-bignums.dev extra-dev opam file…

New branch for coq-bignums.8.11.dev

Hi, to implement coq-community/docker-coq#3 I'll prepare a PR to to add coq-bignums.8.11.dev in
https://github.com/coq/opam-coq-archive/tree/master/extra-dev/packages/coq-bignums

However there is currently no v8.11 branch in https://github.com/coq/bignums/branches

@vbgl @maximedenes @Zimmi48 I can create that branch if you want, but before that could one of you confirm you're OK with selecting the last commit of master (a5dfe68) as the tip of this branch?

Compilation fails on OCaml >= 4.13

As first reported by @mukeshtiwari on Zulip, Bignums 8.14.0 cannot be built using OCaml 4.13, due to a compilation warning being turned into an error:

CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
File "plugin/bignums_syntax.ml", line 1:
Error (warning 70 [missing-mli]): Cannot find interface file.

Parallel build errors

Hi,

This library has some errors when installing with opam and parallel build. For example:

opam list:

# Packages matching: installed
# Name              # Installed       # Synopsis
base-bigarray       base
base-num            base              Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
camlp5              7.06.10-g84ce6cc4 Preprocessor-pretty-printer of OCaml
conf-m4             1                 Virtual package relying on m4
coq                 8.6               Formal proof management system.
num                 0                 The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0            The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0            Official 4.05.0 release
ocaml-config        1                 OCaml Switch Configuration
ocamlfind           1.8.1             A library manager for OCaml

opam install -y -v coq-bignums.8.6.0:

The following actions will be performed:
  - install coq-bignums 8.6.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-bignums.8.6.0: http]
[coq-bignums.8.6.0] downloaded from https://github.com/coq/bignums/archive/v8.6.0.tar.gz
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-bignums: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j7" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-bignums.8.6.0)
- CAMLDEP bignums_syntax.ml
- COQDEP bignums_syntax_plugin.mlpack
- COQDEP BigZ/BigZ.v
- COQDEP BigZ/ZMake.v
- COQDEP BigNumPrelude.v
- COQDEP CyclicDouble/DoubleCyclic.v
- COQDEP CyclicDouble/DoubleLift.v
- COQDEP CyclicDouble/DoubleSqrt.v
- COQDEP CyclicDouble/DoubleDivn1.v
- COQDEP CyclicDouble/DoubleSub.v
- COQDEP CyclicDouble/DoubleMul.v
- COQDEP CyclicDouble/DoubleDiv.v
- COQDEP CyclicDouble/DoubleBase.v
- COQDEP CyclicDouble/DoubleAdd.v
- COQDEP BigQ/QMake.v
- COQDEP BigQ/BigQ.v
- COQDEP SpecViaZ/ZSigZAxioms.v
- COQDEP SpecViaZ/NSigNAxioms.v
- COQDEP SpecViaZ/ZSig.v
- COQDEP SpecViaQ/QSig.v
- COQDEP SpecViaZ/NSig.v
- ocaml BigN/NMake_gen.ml > BigN/NMake_gen.v || (RV=$?; rm -f BigN/NMake_gen.v; exit ${RV})
- COQDEP BigN/BigN.v
- COQDEP BigN/Nbasic.v
- COQDEP BigN/NMake.v
- COQDEP BigN/NMake_gen.v
- CAMLC -c bignums_syntax.ml
- CAMLOPT -c -for-pack Bignums_syntax_plugin bignums_syntax.ml
- COQC SpecViaZ/NSig.v
- COQC SpecViaZ/ZSig.v
- COQC SpecViaQ/QSig.v
- CAMLC -pack -o bignums_syntax_plugin.cmo
- File "_none_", line 1:
- Error: Corrupted compiled interface
- bignums_syntax.cmi
- Makefile:435: recipe for target 'bignums_syntax_plugin.cmo' failed
- make: *** [bignums_syntax_plugin.cmo] Error 2
- make: *** Waiting for unfinished jobs....
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Bigint, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module CErrors, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Coqlib, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Globnames, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Libnames, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Loc, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Mltop, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Names, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Nametab, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Notation, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Pp, and its interface was not compiled with -opaque
[ERROR] The compilation of coq-bignums failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j7".
#=== ERROR while compiling coq-bignums.8.6.0 ==================================#
# context              2.0.1 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-bignums.8.6.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code            2
# env-file             ~/.opam/log/coq-bignums-372-d0f245.env
# output-file          ~/.opam/log/coq-bignums-372-d0f245.out
### output ###
# [...]
# File "_none_", line 1:
# Warning 58: no cmx file was found in path for module Loc, and its interface was not compiled with -opaque
# File "_none_", line 1:
# Warning 58: no cmx file was found in path for module Mltop, and its interface was not compiled with -opaque
# File "_none_", line 1:
# Warning 58: no cmx file was found in path for module Names, and its interface was not compiled with -opaque
# File "_none_", line 1:
# Warning 58: no cmx file was found in path for module Nametab, and its interface was not compiled with -opaque
# File "_none_", line 1:
# Warning 58: no cmx file was found in path for module Notation, and its interface was not compiled with -opaque
# File "_none_", line 1:
# Warning 58: no cmx file was found in path for module Pp, and its interface was not compiled with -opaque
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-bignums 8.6.0
+- 
- No changes have been performed

This seems to affect all package versions. I am opening some pull-requests to remove the parallel -j build option from the package.

Need for a new release (coq-bignums.8.10.0)

Dear coq-bignums maintainers,

coq.8.10.0 is now available in https://github.com/ocaml/opam-repository
but coq-bignums.8.10.0 is not yet part of https://github.com/coq/opam-coq-archive

Please could you make a new release of bignums ?

(if it helps, I'll be able to open a PR in https://github.com/coq/opam-coq-archive then)

Related: coq-community/docker-coq#2

Need for an opam release (coq-bignums.8.9.0)

Dear coq-bignums maintainers,

As coq.8.9.0 is now available in opam's default repository, could you prepare a compatible package for coq-bignums in released?

Indeed this is blocking for preparing a corresponding Docker image, and replace coqorg/coq:8.9-beta1 with coqorg/coq:8.9.0 on Docker Hub (cf. the related docker-coq wiki).

The bignums repo does not contain a v8.9 branch but I've checked the v8.8 branch (as well as the V8.8.0 tag) still compile with coq.8.9.0:

opam install coq.8.9.0
opam repository add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-bignums.8.8.dev  # ok
opam install --ignore-constraints-on=coq coq-bignums.8.8.0  # ok

Still, although it could suffice to relax the constraint of coq-bignums.8.8.0 in released to also accept coq.8.9.0, given the naming convention chosen up to now in released:

opam show coq-bignums | grep all-versions
all-versions           8.6.0  8.7.0  8.8.0

I suspect it'd be preferable to:

create a v8.9 branch from 649dad4,
a tag V8.9.0,
and a separated opam package coq-bignums.8.9.0 in released (?)

Thanks!

There should be an 8.7.0 compatible release of bignums.

Please create a tag for upcoming release of Coq 8.13

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit aafdd43
on branch https://github.com/coq/bignums/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!
CC: coq/coq#12334

Compilation broken if Coq compiled without native compiler

Apparently coqc is broken if Coq does not support native compilation but you pass the flag as per #38 . On windows we disable the native compiler (it is the default).

Relevant logs:
https://coq.gitlab.io/-/coq/-/jobs/501853273/artifacts/artifacts/buildlogs/bignums-a33927c06eb0701025f873f7e5951f7b07a89e6e-make_log.txt
https://coq.gitlab.io/-/coq/-/jobs/501853273/artifacts/artifacts/buildlogs/bignums-a33927c06eb0701025f873f7e5951f7b07a89e6e-make_err.txt

I report the bug here, but it is unclear to me, since clients have (AFAICT) no way to ask Coq if native compilation is supported.

CC @maximedenes

Should the opam package install the bytecode plugin?

I came into a situation where I want to run coqtop.byte in ocamldebug to analyze some runtime behavior. From those plugins which I use from the Coq Platform, the Bignums syntax plugin is the only one which does not install the bytecode plugin (.cmo) file. When I do a make byte; make install-byte for Bignums, I can run my code in coqtop.byte.

Since this the only missing basic plugin, I would suggest that the opam package also installs the bytecode plugin.

coq-bignums.dev fails with coq.dev since 2019-11-02

Kind: bug

Last known successful build:

BUILD_DATE=2019-11-01T03:56:55Z COQ_COMMIT=6694a1811dc4e961a81fb4464cf5aaf05f1b5752

Currently failing build:

coq-bignums.dev with https://github.com/coq/coq/tree/b0fe318ea3b54f6f5f4c911bfb0e8523405e8c5c

Docker Hub build log

[…]
-> compiled coq.dev
-> installed coq.dev
Processing 11/12: [coq-bignums: dune build]
+ /home/coq/.opam/4.07.1+flambda/bin/dune "build" "-p" "coq-bignums" "-j" "2" (CWD=/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-bignums.dev)
- ocamlc plugin/.bignums_syntax_plugin.objs/byte/bignums_syntax_plugin__Bignums_syntax.{cmi,cmo,cmt}
- File "plugin/bignums_syntax.ml", line 47, characters 2-47:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 55, characters 15-42:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 56, characters 15-42:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 65, characters 14-41:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- ocamlopt plugin/.bignums_syntax_plugin.objs/native/bignums_syntax_plugin__Bignums_syntax.{cmx,o}
- File "plugin/bignums_syntax.ml", line 47, characters 2-47:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 55, characters 15-42:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 56, characters 15-42:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- File "plugin/bignums_syntax.ml", line 65, characters 14-41:
- Warning 3: deprecated: ConstructRef
- Use Names.GlobRef.ConstructRef
- Error: coqdep returned invalid output for default/BigN/NMake.v / [phase:
- line]
- Error: coqdep returned invalid output for default/BigN/NMake_gen.v / [phase:
- line]
- Error: coqdep returned invalid output for default/BigN/Nbasic.v / [phase:
- line]
- Error: coqdep returned invalid output for default/BigNumPrelude.v / [phase:
- line]
- Error: coqdep returned invalid output for default/BigQ/BigQ.v / [phase: line]
- Error: coqdep returned invalid output for default/BigZ/BigZ.v / [phase: line]
- Error: coqdep returned invalid output for default/BigQ/QMake.v / [phase:
- line]
- Error: coqdep returned invalid output for default/BigZ/ZMake.v / [phase:
- line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleAdd.v /
- [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleBase.v /
- [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleCyclic.v
- / [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleDivn1.v
- / [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleDiv.v /
- [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleLift.v /
- [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleMul.v /
- [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleSub.v /
- [phase: line]
- Error: coqdep returned invalid output for default/CyclicDouble/DoubleSqrt.v /
- [phase: line]
- Error: coqdep returned invalid output for default/SpecViaQ/QSig.v / [phase:
- line]
- Error: coqdep returned invalid output for default/SpecViaZ/NSig.v / [phase:
- line]
- Error: coqdep returned invalid output for default/SpecViaZ/NSigNAxioms.v /
- [phase: line]
- Error: coqdep returned invalid output for default/SpecViaZ/ZSig.v / [phase:
- line]
- Error: coqdep returned invalid output for default/BigN/BigN.v / [phase: line]
- Error: coqdep returned invalid output for default/SpecViaZ/ZSigZAxioms.v /
- [phase: line]
[ERROR] The compilation of coq-bignums failed at "/home/coq/.opam/4.07.1+flambda/bin/dune build -p coq-bignums -j 2".

Maybe this comes from a breaking change from these commits, but I didn't figure out yet which one…

Ideas on how to fix this? Cc @ppedrot @maximedenes

[Note that this issue is currently blocking for the coqorg/coq:dev Docker Hub nightly build]

coq-bignums.dev does not compile with coq.dev

Hi
With opam, when compiling coq-bignums.dev with the last version of coq.dev, I get the following error:

CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
File "plugin/bignums_syntax.ml", line 101, characters 57-112:
# 101 |       DAst.make ?loc @@ GApp (ref_W0, [DAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous)])
#                                                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: The constructor GHole expects 3 argument(s),
#        but is applied here to 2 argument(s)

Thanks!

Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0.

Coq Platform CI is currently testing opam package coq-bignums.9.0.0+coq8.18
from official repository https://coq.inria.fr/opam/released/packages/coq-bignums/coq-bignums.9.0.0+coq8.18/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10, please inform us as soon as possible and before October 31st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372

Circular dependency between `Make` and `Makefile.coq`

There is some obvious circularity in the Makefile of Bignums.

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.

coq-community / bignums Goto Github PK

bignums's Introduction

Bignums

Meta

Building and installation instructions

bignums's People

Stargazers

Watchers

Forkers

bignums's Issues

Recommend Projects

Recommend Topics

Recommend Org