Build:
- 0
2024-01-29 15:19.02: New job: Voodoo prep coq-lsp.0.1.3+v8.16; 8d2b270a4ae7c5bd7b16c79259f1b7a9 2024-01-29 15:19.02: Waiting for resource in pool OCluster 2024-01-29 18:42.38: Waiting for worker… 2024-01-29 18:44.53: Got resource from pool OCluster 2024-01-29 18:44.53: Using cache hint "docs-universe-prep-4.14.1" To reproduce locally: cat > prep.spec <<'END-OF-SPEC' ((build tools ((from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) (user (uid 1000) (gid 1000)) (workdir /home/opam) (run (shell "sudo chown opam:opam /home/opam")) (run (network host) (shell "sudo apt-get update && sudo apt-get install -yy m4 pkg-config")) (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam pin -ny https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 && opam depext -iy voodoo-prep")) (run (shell "cp $(opam config var bin)/voodoo-prep /home/opam")))) (from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) (user (uid 1000) (gid 1000)) (workdir /home/opam) (run (shell "sudo chown opam:opam /home/opam")) (run (shell "sudo mkdir /src")) (copy (src packages) (dst /src/packages)) (copy (src repo) (dst /src/repo)) (run (network host) (shell "sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam && opam init --reinit -ni")) (run (shell "opam repo remove default && opam repo add opam /src")) (copy (from (build tools)) (src /home/opam/voodoo-prep) (dst /home/opam/)) (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam install dune.3.13.0 ocamlfind.1.9.6")) (env DUNE_CACHE enabled) (env DUNE_CACHE_TRANSPORT direct) (env DUNE_CACHE_DUPLICATION copy) (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "(sudo apt update) && ((opam depext -viy coq-lsp.0.1.3+v8.16 zarith.1.13 yojson.2.1.2 stdlib-shims.0.3.0 sexplib0.v0.15.1 sexplib.v0.15.1 seq.base result.1.5 ppxlib.0.31.0 ppx_sexp_conv.v0.15.1 ppx_import.1.10.0 ppx_hash.v0.15.0 ppx_deriving_yojson.3.7.0 ppx_deriving.5.2.1 ppx_derivers.1.2.1 ppx_compare.v0.15.0 parsexp.v0.15.0 ocamlfind.1.9.6 ocaml-compiler-libs.v0.12.4 num.1.5 dune-configurator.3.13.0 dune.3.13.0 csexp.1.5.2 cppo.1.6.9 coq-serapi.8.16.0+0.16.3 coq.8.16.1 conf-gmp.4 conf-findutils.1 cmdliner.1.2.0 camlp-streams.5.0.1 base.v0.15.1 2>&1 | tee ~/opam.err.log) || echo 'Failed to install all packages')")) (run (shell "opam exec -- ~/voodoo-prep -u coq-lsp:8d2b270a4ae7c5bd7b16c79259f1b7a9")) (run (network host) (secrets (ssh_privkey (target /home/opam/.ssh/id_rsa)) (ssh_pubkey (target /home/opam/.ssh/id_rsa.pub)) (ssh_config (target /home/opam/.ssh/config))) (shell "(echo '0.242925') && (for DATA in prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16,coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9,coq-lsp.0.1.3+v8.16; do IFS=\",\"; set -- $DATA; ([ -d $1 ] || (echo \"FAILED:$2\" && mkdir -p $1 && cp ~/opam.err.log $1 && opam show $3 --raw > $1/opam)) && (shopt -s nullglob && ((tar -cvf $1.tar $1/* && rm -R $1/* && mv $1.tar $1/content.tar) || (echo 'Empty directory'))) done) && (for DATA in prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16,coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9,coq-lsp.0.1.3+v8.16; do IFS=\",\"; set -- $DATA; rsync -aR --no-p ./$1 docs.ci.ocaml.org:/data/.; done) && (for DATA in prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16,coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9,coq-lsp.0.1.3+v8.16; do IFS=\",\"; set -- $DATA; HASH=$((sha256sum $1/content.tar | cut -d \" \" -f 1) || echo -n 'empty'); printf \"HASHES:$2:$HASH\\n\"; done)")) ) END-OF-SPEC ocluster-client submit-obuilder https://github.com/ocaml/opam-repository.git 9fc3fa05d7b0bd182f65b5988f8caf2647c8f3fe --local-file prep.spec \ --pool linux-x86_64 --connect ocluster-submission.cap --cache-hint docs-universe-prep-4.14.1 \ --secret ssh_privkey:id_rsa --secret ssh_pubkey:id_rsa.pub--secret ssh_config:ssh_config 2024-01-29 18:44.53: RETRYING: 2024-01-29/151902-voodoo-prep-0411b9 Number of retries: 0 (retriable error condition) Building on toxis.caelum.ci.dev All commits already cached Updating files: 69% (22681/32633) Updating files: 70% (22844/32633) Updating files: 71% (23170/32633) Updating files: 72% (23496/32633) Updating files: 73% (23823/32633) Updating files: 74% (24149/32633) Updating files: 75% (24475/32633) Updating files: 76% (24802/32633) Updating files: 77% (25128/32633) Updating files: 78% (25454/32633) Updating files: 79% (25781/32633) Updating files: 80% (26107/32633) Updating files: 81% (26433/32633) Updating files: 82% (26760/32633) Updating files: 83% (27086/32633) Updating files: 84% (27412/32633) Updating files: 85% (27739/32633) Updating files: 86% (28065/32633) Updating files: 87% (28391/32633) Updating files: 88% (28718/32633) Updating files: 89% (29044/32633) Updating files: 90% (29370/32633) Updating files: 91% (29697/32633) Updating files: 92% (30023/32633) Updating files: 93% (30349/32633) Updating files: 94% (30676/32633) Updating files: 95% (31002/32633) Updating files: 96% (31328/32633) Updating files: 97% (31655/32633) Updating files: 98% (31981/32633) Updating files: 99% (32307/32633) Updating files: 100% (32633/32633) Updating files: 100% (32633/32633), done. HEAD is now at 9fc3fa05d7 [new release] dune (15 packages) (3.13.0) (build "tools" …) (from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) Unable to find image 'ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef' locally docker.io/ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef: Pulling from ocaml/opam 82e8c0c7d92b: Pulling fs layer 82e8c0c7d92b: Verifying Checksum 82e8c0c7d92b: Download complete 82e8c0c7d92b: Pull complete Digest: sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef Status: Downloaded newer image for ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef 2024-01-29 18:39.55 ---> using "1f16aa8fbc1a229ca02cdf7d8b4234eb4608a9074cec5292a9e72517b48fb577" from cache /: (user (uid 1000) (gid 1000)) /: (workdir /home/opam) /home/opam: (run (shell "sudo chown opam:opam /home/opam")) 2024-01-29 18:39.55 ---> using "258ae3900365106d3b475f7327e1977f1a9ae54d4b6cd6e024f1ed5ef4f3381c" from cache /home/opam: (run (network host) (shell "sudo apt-get update && sudo apt-get install -yy m4 pkg-config")) Hit:1 http://deb.debian.org/debian bookworm InRelease Get:2 http://deb.debian.org/debian bookworm-updates InRelease [52.1 kB] Get:3 http://deb.debian.org/debian-security bookworm-security InRelease [48.0 kB] Get:4 http://deb.debian.org/debian-security bookworm-security/main amd64 Packages [134 kB] Fetched 234 kB in 1s (337 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... The following additional packages will be installed: libpkgconf3 pkgconf pkgconf-bin Suggested packages: m4-doc The following NEW packages will be installed: libpkgconf3 m4 pkg-config pkgconf pkgconf-bin 0 upgraded, 5 newly installed, 0 to remove and 0 not upgraded. Need to get 392 kB of archives. After this operation, 969 kB of additional disk space will be used. Get:1 http://deb.debian.org/debian bookworm/main amd64 libpkgconf3 amd64 1.8.1-1 [36.1 kB] Get:2 http://deb.debian.org/debian bookworm/main amd64 m4 amd64 1.4.19-3 [287 kB] Get:3 http://deb.debian.org/debian bookworm/main amd64 pkgconf-bin amd64 1.8.1-1 [29.5 kB] Get:4 http://deb.debian.org/debian bookworm/main amd64 pkgconf amd64 1.8.1-1 [25.9 kB] Get:5 http://deb.debian.org/debian bookworm/main amd64 pkg-config amd64 1.8.1-1 [13.7 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 392 kB in 2s (243 kB/s) Selecting previously unselected package libpkgconf3:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 18743 files and directories currently installed.) Preparing to unpack .../libpkgconf3_1.8.1-1_amd64.deb ... Unpacking libpkgconf3:amd64 (1.8.1-1) ... Selecting previously unselected package m4. Preparing to unpack .../archives/m4_1.4.19-3_amd64.deb ... Unpacking m4 (1.4.19-3) ... Selecting previously unselected package pkgconf-bin. Preparing to unpack .../pkgconf-bin_1.8.1-1_amd64.deb ... Unpacking pkgconf-bin (1.8.1-1) ... Selecting previously unselected package pkgconf:amd64. Preparing to unpack .../pkgconf_1.8.1-1_amd64.deb ... Unpacking pkgconf:amd64 (1.8.1-1) ... Selecting previously unselected package pkg-config:amd64. Preparing to unpack .../pkg-config_1.8.1-1_amd64.deb ... Unpacking pkg-config:amd64 (1.8.1-1) ... Setting up m4 (1.4.19-3) ... Setting up libpkgconf3:amd64 (1.8.1-1) ... Setting up pkgconf-bin (1.8.1-1) ... Setting up pkgconf:amd64 (1.8.1-1) ... Setting up pkg-config:amd64 (1.8.1-1) ... Processing triggers for libc-bin (2.36-9+deb12u3) ... 2024-01-29 18:39.55 ---> using "d64ddc7053307a6e5bac376e2af0af138c2728532db1941a0e2c7ed3dcb6923f" from cache /home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam pin -ny https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 && opam depext -iy voodoo-prep")) [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 This will pin the following packages: voodoo-prep, voodoo-lib, voodoo-gen, voodoo-do. Continue? [Y/n] y Package voodoo-prep does not exist, create as a NEW package? [Y/n] y [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-prep is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) Package voodoo-lib does not exist, create as a NEW package? [Y/n] y [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-lib is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) Package voodoo-gen does not exist, create as a NEW package? [Y/n] y [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-gen is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) Package voodoo-do does not exist, create as a NEW package? [Y/n] y [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-do is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) # Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian # No extra OS packages requirements found. # All required OS packages found. # Now letting opam install the packages <><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><> [voodoo-prep.~dev] no changes from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 The following actions will be performed: - install ocamlbuild 0.14.3 [required by bos] - install cmdliner 1.2.0 [required by voodoo-prep] - install dune 3.13.0 [required by voodoo-prep] - install ocamlfind 1.9.6 [required by bos] - install seq base [required by re] - install stdlib-shims 0.3.0 [required by ocamlgraph] - install opam-file-format 2.1.6 [required by opam-format] - install cppo 1.6.9 [required by opam-core] - install topkg 1.0.7 [required by bos] - install re 1.11.0 [required by opam-format] - install ocamlgraph 2.1.0 [required by opam-core] - install rresult 0.7.0 [required by bos] - install fmt 0.9.0 [required by bos] - install astring 0.8.5 [required by bos] - install opam-core 2.1.5 [required by opam-format] - install logs 0.7.0 [required by bos] - install fpath 0.7.3 [required by voodoo-prep] - install opam-format 2.1.5 [required by voodoo-prep] - install bos 0.2.1 [required by voodoo-prep] - install voodoo-prep ~dev* ===== 20 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [astring.0.8.5] found in cache [bos.0.2.1] found in cache [cmdliner.1.2.0] found in cache [cppo.1.6.9] found in cache [dune.3.13.0] found in cache [fmt.0.9.0] found in cache [fpath.0.7.3] found in cache [logs.0.7.0] found in cache [ocamlbuild.0.14.3] found in cache [ocamlfind.1.9.6] found in cache [ocamlgraph.2.1.0] found in cache [opam-core.2.1.5] found in cache [opam-file-format.2.1.6] found in cache [opam-format.2.1.5] found in cache [re.1.11.0] found in cache [rresult.0.7.0] found in cache [stdlib-shims.0.3.0] found in cache [topkg.1.0.7] found in cache [voodoo-prep.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed seq.base -> installed cmdliner.1.2.0 -> installed ocamlfind.1.9.6 -> installed ocamlbuild.0.14.3 -> installed topkg.1.0.7 -> installed rresult.0.7.0 -> installed fmt.0.9.0 -> installed astring.0.8.5 -> installed fpath.0.7.3 -> installed logs.0.7.0 -> installed bos.0.2.1 -> installed dune.3.13.0 -> installed stdlib-shims.0.3.0 -> installed opam-file-format.2.1.6 -> installed re.1.11.0 -> installed cppo.1.6.9 -> installed ocamlgraph.2.1.0 -> installed opam-core.2.1.5 -> installed opam-format.2.1.5 -> installed voodoo-prep.~dev Done. # Run eval $(opam env) to update the current shell environment 2024-01-29 18:39.55 ---> using "d95d2426ec6638d4946232810cc7377b78e0b12578cf93755f6aecdc254fcd78" from cache /home/opam: (run (shell "cp $(opam config var bin)/voodoo-prep /home/opam")) 2024-01-29 18:39.55 ---> using "200b9dc9bbc6b05727626f4e73227cdcfa87e5df3b69dfe480b404d6323d60f8" from cache 2024-01-29 18:39.55 --> finished "tools" (from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) Unable to find image 'ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef' locally docker.io/ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef: Pulling from ocaml/opam 82e8c0c7d92b: Pulling fs layer 82e8c0c7d92b: Verifying Checksum 82e8c0c7d92b: Download complete 82e8c0c7d92b: Pull complete Digest: sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef Status: Downloaded newer image for ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef 2024-01-29 18:39.55 ---> using "1f16aa8fbc1a229ca02cdf7d8b4234eb4608a9074cec5292a9e72517b48fb577" from cache /: (user (uid 1000) (gid 1000)) /: (workdir /home/opam) /home/opam: (run (shell "sudo chown opam:opam /home/opam")) 2024-01-29 18:39.55 ---> using "258ae3900365106d3b475f7327e1977f1a9ae54d4b6cd6e024f1ed5ef4f3381c" from cache /home/opam: (run (shell "sudo mkdir /src")) 2024-01-29 18:39.55 ---> using "50a061015e57b489daec5893a083c81b93ec0b29b89dbcf9b55da6d4003431c6" from cache /home/opam: (copy (src packages) (dst /src/packages)) 2024-01-29 18:39.57 ---> using "01aa3de5fbb7da6355a5a3f9fa1564dc626ae86abf688775884c1ab94bb65d0b" from cache /home/opam: (copy (src repo) (dst /src/repo)) 2024-01-29 18:39.57 ---> using "2f80ca12a98e6c8d13b2d4313d2e1042fd6f790370cc08f16159385ad3fc5996" from cache /home/opam: (run (network host) (shell "sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam && opam init --reinit -ni")) Configuring from /home/opam/.opamrc and then from built-in defaults. Checking for available remotes: rsync and local, git. - you won't be able to use mercurial repositories unless you install the hg command on your system. - you won't be able to use darcs repositories unless you install the darcs command on your system. This version of opam requires an update to the layout of /home/opam/.opam from version 2.0 to version 2.1, which can't be reverted. You may want to back it up before going further. Continue? [Y/n] y Format upgrade done. <><> Updating repositories ><><><><><><><><><><><><><><><><><><><><><><><><><><> [default] synchronised from file:///home/opam/opam-repository 2024-01-29 18:39.57 ---> using "5080f4d462ceb6f0e8f61edcf012437834ade0821fc592cdddca031349d9cf72" from cache /home/opam: (run (shell "opam repo remove default && opam repo add opam /src")) Repositories removed from the selections of switch 4.14. Use '--all' to forget about them altogether. [opam] Initialised [NOTE] Repository opam has been added to the selections of switch 4.14 only. Run `opam repository add opam --all-switches|--set-default' to use it in all existing switches, or in newly created switches, respectively. 2024-01-29 18:39.57 ---> using "52bf3f5f6e7a46ac8833cf5cd91e39754db742f33dddb3831406ffa0cde994a1" from cache /home/opam: (copy (from (build tools)) (src /home/opam/voodoo-prep) (dst /home/opam/)) 2024-01-29 18:39.57 ---> using "e11031127d8519055a60a4dd91b72f34724cc3bc999b18218ffd0ca30feb91a0" from cache /home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam install dune.3.13.0 ocamlfind.1.9.6")) The following actions will be performed: - install dune 3.13.0 - install ocamlfind 1.9.6 ===== 2 to install ===== <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved ocamlfind.1.9.6 (cached) -> retrieved dune.3.13.0 (cached) -> installed ocamlfind.1.9.6 -> installed dune.3.13.0 Done. # Run eval $(opam env) to update the current shell environment 2024-01-29 18:39.57 ---> using "462495e74868d8de1c53b9bcbfb005507d496482410bb54355644040bbde4ddb" from cache /home/opam: (env DUNE_CACHE enabled) /home/opam: (env DUNE_CACHE_TRANSPORT direct) /home/opam: (env DUNE_CACHE_DUPLICATION copy) /home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "(sudo apt update) && ((opam depext -viy coq-lsp.0.1.3+v8.16 zarith.1.13 yojson.2.1.2 stdlib-shims.0.3.0 sexplib0.v0.15.1 sexplib.v0.15.1 seq.base result.1.5 ppxlib.0.31.0 ppx_sexp_conv.v0.15.1 ppx_import.1.10.0 ppx_hash.v0.15.0 ppx_deriving_yojson.3.7.0 ppx_deriving.5.2.1 ppx_derivers.1.2.1 ppx_compare.v0.15.0 parsexp.v0.15.0 ocamlfind.1.9.6 ocaml-compiler-libs.v0.12.4 num.1.5 dune-configurator.3.13.0 dune.3.13.0 csexp.1.5.2 cppo.1.6.9 coq-serapi.8.16.0+0.16.3 coq.8.16.1 conf-gmp.4 conf-findutils.1 cmdliner.1.2.0 camlp-streams.5.0.1 base.v0.15.1 2>&1 | tee ~/opam.err.log) || echo 'Failed to install all packages')")) WARNING: apt does not have a stable CLI interface. Use with caution in scripts. Hit:1 http://deb.debian.org/debian bookworm InRelease Get:2 http://deb.debian.org/debian bookworm-updates InRelease [52.1 kB] Get:3 http://deb.debian.org/debian-security bookworm-security InRelease [48.0 kB] Get:4 http://deb.debian.org/debian-security bookworm-security/main amd64 Packages [134 kB] Fetched 234 kB in 0s (764 kB/s) Reading package lists... Building dependency tree... Reading state information... All packages are up to date. Opam plugin "depext" may require upgrading/reinstalling. Reinstall the plugin on the current switch? [Y/n] y The following actions will be performed: - recompile opam-depext 1.2.1-1 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved opam-depext.1.2.1-1 (cached) -> removed opam-depext.1.2.1-1 -> installed opam-depext.1.2.1-1 Done. <><> opam-depext.1.2.1-1 installed successfully <><><><><><><><><><><><><><><><> => opam-depext is unnecessary when used with opam >= 2.1. Please use opam install directly instead # Run eval $(opam env) to update the current shell environment <><> Carrying on to "opam depext -viy coq-lsp.0.1.3+v8.16 zarith.1.13 yojson.2.1.2 stdlib-shims.0.3.0 sexplib0.v0.15.1 sexplib.v0.15.1 seq.base result.1.5 ppxlib.0.31.0 ppx_sexp_conv.v0.15.1 ppx_import.1.10.0 ppx_hash.v0.15.0 ppx_deriving_yojson.3.7.0 ppx_deriving.5.2.1 ppx_derivers.1.2.1 ppx_compare.v0.15.0 parsexp.v0.15.0 ocamlfind.1.9.6 ocaml-compiler-libs.v0.12.4 num.1.5 dune-configurator.3.13.0 dune.3.13.0 csexp.1.5.2 cppo.1.6.9 coq-serapi.8.16.0+0.16.3 coq.8.16.1 conf-gmp.4 conf-findutils.1 cmdliner.1.2.0 camlp-streams.5.0.1 base.v0.15.1" You are using opam 2.1+, where external dependency handling has been integrated: consider calling opam directly, the 'depext' plugin interface is provided for backwards compatibility only # Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian # The following system packages are needed: findutils libgmp-dev [NOTE] Package dune is already installed (current version is 3.13.0). [NOTE] Package ocamlfind is already installed (current version is 1.9.6). The following actions will be performed: - install cppo 1.6.9 - install ppx_derivers 1.2.1 - install conf-gmp 4 - install num 1.5 - install cmdliner 1.2.0 - install conf-findutils 1 - install result 1.5 - install seq base - install csexp 1.5.2 - install ocaml-compiler-libs v0.12.4 - install sexplib0 v0.15.1 - install camlp-streams 5.0.1 - install stdlib-shims 0.3.0 - install zarith 1.13 - install yojson 2.1.2 - install dune-configurator 3.13.0 - install ppxlib 0.31.0 - install coq 8.16.1 - install base v0.15.1 - install ppx_import 1.10.0 - install ppx_deriving 5.2.1 - install ppx_sexp_conv v0.15.1 - install ppx_compare v0.15.0 - install parsexp v0.15.0 - install ppx_deriving_yojson 3.7.0 - install ppx_hash v0.15.0 - install sexplib v0.15.1 - install coq-serapi 8.16.0+0.16.3 - install coq-lsp 0.1.3+v8.16 ===== 29 to install ===== The following system packages will first need to be installed: libgmp-dev <><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><> Let opam run your package manager to install the required system packages? (answer 'n' for other options) [Y/n] y + /usr/bin/sudo "apt-get" "install" "-qq" "-yy" "libgmp-dev" - debconf: delaying package configuration, since apt-utils is not installed - Selecting previously unselected package libgmpxx4ldbl:amd64. - (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 18743 files and directories currently installed.) - Preparing to unpack .../libgmpxx4ldbl_2%3a6.2.1+dfsg1-1.1_amd64.deb ... - Unpacking libgmpxx4ldbl:amd64 (2:6.2.1+dfsg1-1.1) ... - Selecting previously unselected package libgmp-dev:amd64. - Preparing to unpack .../libgmp-dev_2%3a6.2.1+dfsg1-1.1_amd64.deb ... - Unpacking libgmp-dev:amd64 (2:6.2.1+dfsg1-1.1) ... - Setting up libgmpxx4ldbl:amd64 (2:6.2.1+dfsg1-1.1) ... - Setting up libgmp-dev:amd64 (2:6.2.1+dfsg1-1.1) ... - Processing triggers for libc-bin (2.36-9+deb12u3) ... <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/87: Processing 2/87: Processing 3/87: -> retrieved camlp-streams.5.0.1 (cached) Processing 4/87: Processing 5/87: Processing 6/87: Processing 7/87: [camlp-streams: dune build] Processing 8/87: [camlp-streams: dune build] [conf-findutils: sh find . -name .] Processing 9/87: [camlp-streams: dune build] [conf-findutils: sh find . -name .] [conf-gmp: sh] -> retrieved base.v0.15.1 (cached) Processing 10/87: [coq-lsp.0.1.3+v8.16: http] [camlp-streams: dune build] [conf-findutils: sh find . -name .] [conf-gmp: sh] -> retrieved cmdliner.1.2.0 (cached) Processing 11/87: [coq-lsp.0.1.3+v8.16: http] [camlp-streams: dune build] [conf-findutils: sh find . -name .] [conf-gmp: sh] Processing 12/87: [coq-lsp.0.1.3+v8.16: http] [camlp-streams: dune build] [cmdliner: make all] [conf-findutils: sh find . -name .] [conf-gmp: sh] -> retrieved coq.8.16.1 (cached) Processing 13/87: [coq-lsp.0.1.3+v8.16: http] [camlp-streams: dune build] [cmdliner: make all] [conf-findutils: sh find . -name .] [conf-gmp: sh] -> compiled camlp-streams.5.0.1 Processing 13/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [conf-findutils: sh find . -name .] [conf-gmp: sh] -> installed camlp-streams.5.0.1 Processing 14/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [conf-findutils: sh find . -name .] [conf-gmp: sh] - + find . -name . - . -> compiled conf-findutils.1 Processing 14/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [conf-gmp: sh] -> installed conf-findutils.1 Processing 15/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [conf-gmp: sh] - + cc -c -I/usr/local/include test.c -> compiled conf-gmp.4 Processing 15/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] -> installed conf-gmp.4 Processing 16/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] -> retrieved coq-serapi.8.16.0+0.16.3 (cached) Processing 17/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] -> retrieved cppo.1.6.9 (cached) Processing 18/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] Processing 19/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] -> retrieved csexp.1.5.2 (cached) Processing 20/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] Processing 21/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] -> retrieved num.1.5 (cached) Processing 22/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] Processing 23/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] -> retrieved ocaml-compiler-libs.v0.12.4 (cached) Processing 24/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] Processing 25/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] -> retrieved parsexp.v0.15.0 (cached) Processing 26/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] -> retrieved ppx_compare.v0.15.0 (cached) Processing 27/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] -> retrieved ppx_derivers.1.2.1 (cached) Processing 28/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] Processing 29/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> retrieved ppx_deriving.5.2.1 (cached) Processing 30/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> retrieved ppx_deriving_yojson.3.7.0 (cached) Processing 31/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> retrieved ppx_hash.v0.15.0 (cached) Processing 32/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> retrieved ppx_import.1.10.0 (cached) Processing 33/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> retrieved ppx_sexp_conv.v0.15.1 (cached) Processing 34/87: [coq-lsp.0.1.3+v8.16: http] [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] Processing 34/87: [cmdliner: make all] [cppo: dune build] [csexp: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> compiled csexp.1.5.2 Processing 34/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> installed csexp.1.5.2 Processing 35/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [ppx_derivers: dune build] -> compiled ppx_derivers.1.2.1 Processing 35/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] -> installed ppx_derivers.1.2.1 Processing 36/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] -> retrieved ppxlib.0.31.0 (cached) Processing 37/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] -> retrieved result.1.5 (cached) Processing 38/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] Processing 39/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] Processing 40/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] Processing 41/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] -> installed seq.base Processing 42/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] -> retrieved sexplib.v0.15.1 (cached) Processing 43/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] -> retrieved sexplib0.v0.15.1 (cached) Processing 44/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] Processing 45/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] -> retrieved stdlib-shims.0.3.0 (cached) Processing 46/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] Processing 47/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] -> retrieved yojson.2.1.2 (cached) Processing 48/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] -> retrieved zarith.1.13 (cached) Processing 49/87: [cmdliner: make all] [cppo: dune build] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [zarith: ./configure] -> retrieved dune-configurator.3.13.0 (cached) Processing 50/87: [cmdliner: make all] [cppo: dune build] [dune-configurator: rm] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [zarith: ./configure] -> compiled cppo.1.6.9 Processing 50/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [zarith: ./configure] -> installed cppo.1.6.9 Processing 51/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [zarith: ./configure] Processing 52/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [ocaml-compiler-libs: dune build] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> compiled ocaml-compiler-libs.v0.12.4 Processing 52/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> installed ocaml-compiler-libs.v0.12.4 Processing 53/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [result: dune build] [sexplib0: dune build] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> compiled result.1.5 Processing 53/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [sexplib0: dune build] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> installed result.1.5 Processing 54/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [sexplib0: dune build] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> compiled sexplib0.v0.15.1 Processing 54/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> installed sexplib0.v0.15.1 Processing 55/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [stdlib-shims: dune build] [yojson: dune build] [zarith: ./configure] -> compiled stdlib-shims.0.3.0 Processing 55/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [yojson: dune build] [zarith: ./configure] -> installed stdlib-shims.0.3.0 Processing 56/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [yojson: dune build] [zarith: ./configure] Processing 57/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [ppxlib: dune build] [yojson: dune build] [zarith: ./configure] - binary ocaml: found in /home/opam/.opam/4.14/bin - binary ocamlc: found in /home/opam/.opam/4.14/bin - binary ocamldep: found in /home/opam/.opam/4.14/bin - binary ocamlmklib: found in /home/opam/.opam/4.14/bin - binary ocamldoc: found in /home/opam/.opam/4.14/bin - binary ocamlopt: found in /home/opam/.opam/4.14/bin - checking compilation with ocamlc -O3 -Wall -Wextra : working - include caml/mlvalues.h: found - library dynlink.cmxa: found - binary ocamlfind: found in /home/opam/.opam/4.14/bin - OCaml's word size is 64 - include gmp.h: found - library gmp: found - OCaml supports -bin-annot to produce documentation - - detected configuration: - - native-code: yes - dynamic linking: yes - defines: -DHAS_GMP - includes: -I/home/opam/.opam/4.14/lib/ocaml - libraries: -lgmp - linker options: - C options: -O3 -Wall -Wextra - installation path: /home/opam/.opam/4.14/lib - installation method findlib - - configuration successful! - now type "make" to build - then type "make install" or "sudo make install" to install Processing 57/87: [cmdliner: make all] [dune-configurator: rm] [num: make opam-legacy] [ppxlib: dune build] [yojson: dune build] [zarith: make] Processing 57/87: [cmdliner: make all] [dune-configurator: dune build] [num: make opam-legacy] [ppxlib: dune build] [yojson: dune build] [zarith: make] - /usr/bin/make -C src all - make[1]: Entering directory '/home/opam/.opam/4.14/.opam-switch/build/num.1.5/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 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c int_misc.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c int_misc.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c nat.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c nat.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c big_int.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c big_int.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c arith_flags.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c arith_flags.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c ratio.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c ratio.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c arith_status.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -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 - cp ../toplevel/num_top_printers.mli ../toplevel/num_top.mli ../toplevel/num_top_printers.ml ../toplevel/num_top.ml . - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num_top_printers.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num_top_printers.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num_top.mli - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num_top.ml - ocamlc -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -a -o num_top.cma num_top_printers.cmo num_top.cmo - echo 'version = "1.6~dev"' > META.top - cat META.num-top.in >> META.top - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c int_misc.ml - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c nat.ml - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c big_int.ml - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c arith_flags.ml - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c ratio.ml - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -c num.ml - ocamlopt -w +a-4-9-41-42-44-45-48 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -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 -bin-annot -g -safe-string -strict-sequence -strict-formats -I +compiler-libs -I . -shared -o nums.cmxs nums.cmxa - make[1]: Leaving directory '/home/opam/.opam/4.14/.opam-switch/build/num.1.5/src' - cp src/num-legacy.install num.install -> compiled num.1.5 Processing 57/87: [cmdliner: make all] [dune-configurator: dune build] [ppxlib: dune build] [yojson: dune build] [zarith: make] -> installed num.1.5 Processing 58/87: [cmdliner: make all] [dune-configurator: dune build] [ppxlib: dune build] [yojson: dune build] [zarith: make] -> retrieved coq-lsp.0.1.3+v8.16 (https://github.com/ejgallego/coq-lsp/releases/download/0.1.3%2Bv8.16/coq-lsp-0.1.3.v8.16.tbz) - ocaml build.ml cma - ocaml build.ml cmxa - ocaml build.ml cmxs -> compiled cmdliner.1.2.0 Processing 58/87: [dune-configurator: dune build] [ppxlib: dune build] [yojson: dune build] [zarith: make] Processing 59/87: [dune-configurator: dune build] [ppxlib: dune build] [yojson: dune build] [zarith: make] [cmdliner: make install] -> compiled yojson.2.1.2 Processing 59/87: [dune-configurator: dune build] [ppxlib: dune build] [zarith: make] [cmdliner: make install] -> compiled dune-configurator.3.13.0 Processing 59/87: [ppxlib: dune build] [zarith: make] [cmdliner: make install] - install -d "/home/opam/.opam/4.14/lib/cmdliner" - install pkg/META _build/cmdliner.mli _build/cmdliner.cmi _build/cmdliner.cmti "/home/opam/.opam/4.14/lib/cmdliner" - install cmdliner.opam "/home/opam/.opam/4.14/lib/cmdliner/opam" - install _build/cmdliner.cma "/home/opam/.opam/4.14/lib/cmdliner" - install _build/cmdliner.cmxa _build/cmdliner.a _build/cmdliner.cmx _build/cmdliner_arg.cmx _build/cmdliner_base.cmx _build/cmdliner_cline.cmx _build/cmdliner_cmd.cmx _build/cmdliner_docgen.cmx _build/cmdliner_eval.cmx _build/cmdliner_exit.cmx _build/cmdliner_info.cmx _build/cmdliner_manpage.cmx _build/cmdliner_msg.cmx _build/cmdliner_term.cmx _build/cmdliner_term_deprecated.cmx _build/cmdliner_trie.cmx \ - "/home/opam/.opam/4.14/lib/cmdliner" - install _build/cmdliner.cmxs "/home/opam/.opam/4.14/lib/cmdliner" Processing 59/87: [ppxlib: dune build] [zarith: make] [cmdliner: make install-doc] - install -d "/home/opam/.opam/4.14/doc/cmdliner/odoc-pages" - install CHANGES.md LICENSE.md README.md "/home/opam/.opam/4.14/doc/cmdliner" - install doc/index.mld doc/cli.mld doc/examples.mld doc/tutorial.mld \ - doc/tool_man.mld "/home/opam/.opam/4.14/doc/cmdliner/odoc-pages" -> installed cmdliner.1.2.0 Processing 59/87: [ppxlib: dune build] [zarith: make] -> installed dune-configurator.3.13.0 Processing 60/87: [ppxlib: dune build] [zarith: make] Processing 61/87: [base: dune build] [ppxlib: dune build] [zarith: make] -> installed yojson.2.1.2 Processing 62/87: [base: dune build] [ppxlib: dune build] [zarith: make] - (echo "let"; grep "version" META | head -1) > zarith_version.ml - ocamldep zarith_version.ml z.ml q.ml big_int_Z.ml z.mli q.mli big_int_Z.mli > depend - ocamlc -g -I +compiler-libs -bin-annot -c zarith_version.ml - ocamlc -g -I +compiler-libs -bin-annot -c z.mli - ocamlc -g -I +compiler-libs -bin-annot -c z.ml - ocamlc -g -I +compiler-libs -bin-annot -c q.mli - ocamlc -g -I +compiler-libs -bin-annot -c q.ml - ocamlc -g -I +compiler-libs -bin-annot -c big_int_Z.mli - ocamlc -g -I +compiler-libs -bin-annot -c big_int_Z.ml - ocamlmklib -g -failsafe -o zarith zarith_version.cmo z.cmo q.cmo big_int_Z.cmo -lgmp - ocamlc -ccopt "-I/home/opam/.opam/4.14/lib/ocaml -DHAS_GMP -O3 -Wall -Wextra " -c caml_z.c - ocamlmklib -g -failsafe -o zarith caml_z.o -lgmp - ocamlc -g -I +compiler-libs -bin-annot -c zarith_top.ml - ocamlc -g -o zarith_top.cma -a zarith_top.cmo - ocamlopt -g -I +compiler-libs -c zarith_version.ml - ocamlopt -g -I +compiler-libs -c z.ml - ocamlopt -g -I +compiler-libs -c q.ml - ocamlopt -g -I +compiler-libs -c big_int_Z.ml - ocamlmklib -g -failsafe -o zarith zarith_version.cmx z.cmx q.cmx big_int_Z.cmx -lgmp - ocamlopt -shared -o zarith.cmxs -I . zarith.cmxa -linkall -> compiled zarith.1.13 Processing 62/87: [base: dune build] [ppxlib: dune build] Processing 63/87: [base: dune build] [ppxlib: dune build] [zarith: make install] - ocamlfind install -destdir "/home/opam/.opam/4.14/lib" zarith META zarith.cma libzarith.a z.cmi q.cmi big_int_Z.cmi zarith_top.cma z.mli zarith.cmxa zarith_version.cmx z.cmx q.cmx big_int_Z.cmx zarith.cmxs zarith.h q.mli big_int_Z.mli zarith.a z.cmti q.cmti big_int_Z.cmti -optional dllzarith.so - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.cmti - Installed /home/opam/.opam/4.14/lib/zarith/q.cmti - Installed /home/opam/.opam/4.14/lib/zarith/z.cmti - Installed /home/opam/.opam/4.14/lib/zarith/zarith.a - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.mli - Installed /home/opam/.opam/4.14/lib/zarith/q.mli - Installed /home/opam/.opam/4.14/lib/zarith/zarith.h - Installed /home/opam/.opam/4.14/lib/zarith/zarith.cmxs - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.cmx - Installed /home/opam/.opam/4.14/lib/zarith/q.cmx - Installed /home/opam/.opam/4.14/lib/zarith/z.cmx - Installed /home/opam/.opam/4.14/lib/zarith/zarith_version.cmx - Installed /home/opam/.opam/4.14/lib/zarith/zarith.cmxa - Installed /home/opam/.opam/4.14/lib/zarith/z.mli - Installed /home/opam/.opam/4.14/lib/zarith/zarith_top.cma - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.cmi - Installed /home/opam/.opam/4.14/lib/zarith/q.cmi - Installed /home/opam/.opam/4.14/lib/zarith/z.cmi - Installed /home/opam/.opam/4.14/lib/zarith/libzarith.a - Installed /home/opam/.opam/4.14/lib/zarith/zarith.cma - Installed /home/opam/.opam/4.14/lib/stublibs/dllzarith.so - Installed /home/opam/.opam/4.14/lib/stublibs/dllzarith.so.owner - ocamlfind: [WARNING] You have installed DLLs but the directory /home/opam/.opam/4.14/lib/stublibs is not mentioned in ld.conf - Installed /home/opam/.opam/4.14/lib/zarith/META -> installed zarith.1.13 Processing 63/87: [base: dune build] [ppxlib: dune build] Processing 64/87: [base: dune build] [coq: ./configure no] [ppxlib: dune build] - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - You have OCaml 4.14.1. Good! - You have OCamlfind 1.9.6. Good! - You have native-code compilation. Good! - You have the Zarith library 1.13 installed. Good! - CoqIde manually disabled: - => no CoqIDE will be built. - - Architecture : Linux - Sys.os_type : Unix - OCaml version : 4.14.1 - OCaml binaries in : /home/opam/.opam/4.14/bin/ - OCaml library in : /home/opam/.opam/4.14/lib/ocaml - 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 : no - - Paths for true installation: - - Coq will be copied in /home/opam/.opam/4.14 - - the Coq library will be copied in /home/opam/.opam/4.14/lib/coq - - the Coqide configuration files will be copied in /home/opam/.opam/4.14/lib/coq/config - - the Coqide data files will be copied in /home/opam/.opam/4.14/share/coq - - the Coq man pages will be copied in /home/opam/.opam/4.14/man - - documentation prefix path for all Coq packages will be copied in /home/opam/.opam/4.14/doc/coq - - 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 64/87: [base: dune build] [coq: make] [ppxlib: dune build] -> compiled base.v0.15.1 Processing 64/87: [coq: make] [ppxlib: dune build] -> installed base.v0.15.1 Processing 65/87: [coq: make] [ppxlib: dune build] Processing 66/87: [coq: make] [parsexp: dune build] [ppxlib: dune build] -> compiled parsexp.v0.15.0 Processing 66/87: [coq: make] [ppxlib: dune build] -> installed parsexp.v0.15.0 Processing 67/87: [coq: make] [ppxlib: dune build] Processing 68/87: [coq: make] [ppxlib: dune build] [sexplib: dune build] -> compiled sexplib.v0.15.1 Processing 68/87: [coq: make] [ppxlib: dune build] -> installed sexplib.v0.15.1 Processing 69/87: [coq: make] [ppxlib: dune build] -> compiled ppxlib.0.31.0 Processing 69/87: [coq: make] -> installed ppxlib.0.31.0 Processing 70/87: [coq: make] Processing 71/87: [coq: make] [ppx_compare: dune build] Processing 72/87: [coq: make] [ppx_compare: dune build] [ppx_deriving: dune build] Processing 73/87: [coq: make] [ppx_compare: dune build] [ppx_deriving: dune build] [ppx_import: dune build] Processing 74/87: [coq: make] [ppx_compare: dune build] [ppx_deriving: dune build] [ppx_import: dune build] [ppx_sexp_conv: dune build] -> compiled ppx_compare.v0.15.0 Processing 74/87: [coq: make] [ppx_deriving: dune build] [ppx_import: dune build] [ppx_sexp_conv: dune build] -> installed ppx_compare.v0.15.0 Processing 75/87: [coq: make] [ppx_deriving: dune build] [ppx_import: dune build] [ppx_sexp_conv: dune build] -> compiled ppx_import.1.10.0 Processing 75/87: [coq: make] [ppx_deriving: dune build] [ppx_sexp_conv: dune build] -> installed ppx_import.1.10.0 Processing 76/87: [coq: make] [ppx_deriving: dune build] [ppx_sexp_conv: dune build] -> compiled ppx_sexp_conv.v0.15.1 Processing 76/87: [coq: make] [ppx_deriving: dune build] -> installed ppx_sexp_conv.v0.15.1 Processing 77/87: [coq: make] [ppx_deriving: dune build] Processing 78/87: [coq: make] [ppx_deriving: dune build] [ppx_hash: dune build] -> compiled ppx_deriving.5.2.1 Processing 78/87: [coq: make] [ppx_hash: dune build] -> installed ppx_deriving.5.2.1 Processing 79/87: [coq: make] [ppx_hash: dune build] Processing 80/87: [coq: make] [ppx_deriving_yojson: dune build] [ppx_hash: dune build] -> compiled ppx_hash.v0.15.0 Processing 80/87: [coq: make] [ppx_deriving_yojson: dune build] -> installed ppx_hash.v0.15.0 Processing 81/87: [coq: make] [ppx_deriving_yojson: dune build] -> compiled ppx_deriving_yojson.3.7.0 Processing 81/87: [coq: make] -> installed ppx_deriving_yojson.3.7.0 Processing 82/87: [coq: make] + /usr/bin/make "COQ_USE_DUNE=" "-j255" (CWD=/home/opam/.opam/4.14/.opam-switch/build/coq.8.16.1) - /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build - make[1]: Entering directory '/home/opam/.opam/4.14/.opam-switch/build/coq.8.16.1' - MKDIR BUILD_OUT - DUNE _build/install/default/bin/coqdep - DUNE sources - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -no-alias-deps -o lib/.lib.objs/byte/util.cmi -c -intf lib/util.mli) - File "lib/util.mli", line 81, characters 27-35: - 81 | val stream_nth : int -> 'a Stream.t -> 'a - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/util.mli", line 82, characters 29-37: - 82 | val stream_njunk : int -> 'a Stream.t -> unit - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/native/util.cmx -c -impl lib/util.ml) - File "lib/util.ml", line 126, characters 16-28: - 126 | try List.nth (Stream.npeek (n+1) st) n - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/util.ml", line 127, characters 26-40: - 127 | with Failure _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/util.ml", line 130, characters 11-22: - 130 | repeat n Stream.junk st - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/native/coqProject_file.cmx -c -impl lib/coqProject_file.ml) - File "lib/coqProject_file.ml", line 86, characters 35-46: - 86 | let rec parse_string buf s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 94, characters 12-26: - 94 | | exception Stream.Failure -> buffer buf - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 96, characters 32-43: - 96 | and parse_string2 buf s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 101, characters 12-26: - 101 | | exception Stream.Failure -> raise (Parsing_error "unterminated string") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 103, characters 33-44: - 103 | and parse_skip_comment s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 106, characters 12-26: - 106 | | exception Stream.Failure -> () - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 108, characters 34-45: - 108 | and parse_args buf accu s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 120, characters 12-26: - 120 | | exception Stream.Failure -> accu - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 127, characters 31-48: - 127 | let res = parse_args buf [] (Stream.of_channel c) in - ^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/native/lStream.cmx -c -impl lib/lStream.ml) - File "lib/lStream.ml", line 14, characters 12-20: - 14 | strm : 'a Stream.t; - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 26, characters 4-15: - 26 | Stream.from - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 35, characters 17-29: - 35 | let count strm = Stream.count strm.strm - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 38, characters 16-28: - 38 | strm.fun_loc (Stream.count strm.strm) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 57, characters 10-21: - 57 | let a = Stream.peek strm.strm in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 58, characters 22-33: - 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 58, characters 72-84: - 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek; - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 62, characters 10-22: - 62 | let l = Stream.npeek n strm.strm in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 63, characters 24-36: - 63 | strm.max_peek <- max (Stream.count strm.strm + List.length l) strm.max_peek; - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 67, characters 13-25: - 67 | let list = Stream.npeek (n + 1) strm.strm in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 70, characters 36-48: - 70 | x :: _, 0 -> strm.max_peek <- Stream.count strm.strm + n + 1; x - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 72, characters 32-44: - 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 72, characters 72-86: - 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 76, characters 16-27: - 76 | let junk strm = Stream.junk strm.strm - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 78, characters 16-27: - 78 | let next strm = Stream.next strm.strm - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I tools/coqdep/.coqdeplib.objs/byte -I tools/coqdep/.coqdeplib.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Coqdeplib -o tools/coqdep/.coqdeplib.objs/native/coqdeplib__Common.cmx -c -impl tools/coqdep/common.ml) - File "tools/coqdep/common.ml", line 254, characters 4-16: - 254 | | Stream.Error msg -> Error.cannot_parse_meta_file package msg - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQDEP VFILES - DUNE sources - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - DUNE _build/install/default/bin/coqc - DUNE _build/default/plugins/ltac/ltac_plugin.cmxs - DUNE _build/default/plugins/syntax/number_string_notation_plugin.cmxs - DUNE _build/default/plugins/ltac/tauto_plugin.cmxs - DUNE _build/default/plugins/cc/cc_plugin.cmxs - DUNE _build/default/plugins/firstorder/firstorder_plugin.cmxs - DUNE _build/default/plugins/ssrmatching/ssrmatching_plugin.cmxs - DUNE _build/default/plugins/ssr/ssreflect_plugin.cmxs - DUNE _build/default/plugins/ring/ring_plugin.cmxs - DUNE _build/default/plugins/micromega/zify_plugin.cmxs - DUNE _build/default/plugins/micromega/micromega_plugin.cmxs - DUNE _build/default/plugins/rtauto/rtauto_plugin.cmxs - DUNE _build/default/plugins/nsatz/nsatz_plugin.cmxs - DUNE _build/default/plugins/extraction/extraction_plugin.cmxs - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - DUNE _build/default/plugins/funind/funind_plugin.cmxs - DUNE _build/default/plugins/derive/derive_plugin.cmxs - DUNE _build/default/plugins/btauto/btauto_plugin.cmxs - DUNE _build/default/plugins/ltac2/ltac2_plugin.cmxs - DUNE _build/install/default/bin/coqproofworker.opt - DUNE _build/install/default/bin/coqtacticworker.opt - DUNE _build/install/default/bin/coqqueryworker.opt - DUNE _build/install/default/bin/coqtop - DUNE _build/install/default/bin/coqchk - DUNE _build/install/default/bin/csdpcert - DUNE _build/install/default/bin/coqnative - DUNE _build/install/default/bin/votour - DUNE _build/install/default/bin/coqdoc - DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty - DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css - DUNE _build/install/default/bin/coqwc - DUNE _build/install/default/bin/coq_makefile - DUNE _build/default/tools/CoqMakefile.in - DUNE _build/install/default/bin/ocamllibdep - DUNE _build/default/doc/tools/docgram/doc_grammar.exe - DUNE _build/default/coq-core.install - DUNE _build/default/coqide-server.install - DUNE revision - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Plexing.cmi -c -intf gramlib/plexing.mli) - File "gramlib/plexing.mli", line 14, characters 41-49: - 14 | type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/native/gramlib__Plexing.cmx -c -impl gramlib/plexing.ml) - File "gramlib/plexing.ml", line 5, characters 41-49: - 5 | type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Grammar.cmi -c -intf gramlib/grammar.mli) - File "gramlib/grammar.mli", line 31, characters 34-42: - 31 | val make : ?loc:Loc.t -> char Stream.t -> t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/native/gramlib__Grammar.cmx -c -impl gramlib/grammar.ml) - File "gramlib/grammar.ml", line 21, characters 34-42: - 21 | val make : ?loc:Loc.t -> char Stream.t -> t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1093, characters 15-29: - 1093 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1102, characters 15-29: - 1102 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1111, characters 27-41: - 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1111, characters 61-75: - 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1115, characters 13-27: - 1115 | else raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1121, characters 6-20: - 1121 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son)) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1121, characters 31-43: - 1121 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1140, characters 4-18: - 1140 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1147, characters 62-76: - 1147 | skip_if_empty bp (fun (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1149, characters 11-25: - 1149 | with Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1182, characters 52-66: - 1182 | DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1193, characters 53-67: - 1193 | try Some (entry.estart alevn strm__) with Stream.Failure -> None - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1203, characters 31-45: - 1203 | try p1 strm__ with Stream.Failure -> p2 strm__) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1213, characters 17-31: - 1213 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1214, characters 26-38: - 1214 | raise (Stream.Error (tree_failed entry a s son)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1224, characters 43-57: - 1224 | match try Some (ps strm) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1227, characters 49-63: - 1227 | (try Some (p1 bp a strm) with Stream.Failure -> None) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1230, characters 34-46: - 1230 | | None -> raise (Stream.Error (tree_failed entry a s son)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1237, characters 4-18: - 1237 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1265, characters 66-80: - 1265 | (match (try Some (tematch (LStream.peek_nth n strm)) with Stream.Failure -> None) with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1267, characters 44-58: - 1267 | (match try Some (p1 a strm) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1271, characters 42-56: - 1271 | | DeadEnd -> fun last_a strm -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1277, characters 35-49: - 1277 | try Some (ps strm) with Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1279, characters 87-101: - 1279 | try Some (parser_of_tree entry nlevn alevn (top_tree entry tree) strm) with Stream.Failure -> None - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1282, characters 26-38: - 1282 | | None -> raise (Stream.Error (tree_failed entry last_a (Stoken last_tok) tree)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1289, characters 20-34: - 1289 | | None -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1297, characters 43-57: - 1297 | match try Some (ps al strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1307, characters 40-54: - 1307 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1311, characters 16-30: - 1311 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1312, characters 25-37: - 1312 | raise (Stream.Error (symb_failed entry v sep symb)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1318, characters 44-58: - 1318 | match try Some (ps [] strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1325, characters 40-54: - 1325 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1328, characters 44-58: - 1328 | (try Some (ps al strm__) with Stream.Failure -> None) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1336, characters 44-58: - 1336 | match try Some (ps [] strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1342, characters 43-57: - 1342 | match try Some (ps al strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1353, characters 40-54: - 1353 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1357, characters 16-30: - 1357 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1360, characters 22-36: - 1360 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1361, characters 31-43: - 1361 | raise (Stream.Error (symb_failed entry v sep symb)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1375, characters 40-54: - 1375 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1378, characters 44-58: - 1378 | (try Some (ps al strm__) with Stream.Failure -> None) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1384, characters 20-34: - 1384 | Stream.Failure -> None - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1397, characters 41-55: - 1397 | match try Some (ps strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1421, characters 20-34: - 1421 | | None -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1466, characters 52-66: - 1466 | [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1502, characters 50-64: - 1502 | match try Some (p2 strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1523, characters 57-71: - 1523 | [] -> (fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1542, characters 16-30: - 1542 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1553, characters 37-51: - 1553 | try p levn bp a strm__ with Stream.Failure -> a) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1554, characters 63-77: - 1554 | | Dparser p -> fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1557, characters 9-21: - 1557 | raise (Stream.Error ("entry [" ^ ename ^ "] is empty")) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1622, characters 6-20: - 1622 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1625, characters 6-18: - 1625 | | Stream.Error _ as exc -> - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1624, characters 22-34: - 1624 | Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1662, characters 51-65: - 1662 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1675, characters 51-65: - 1675 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1763, characters 55-69: - 1763 | e.estart <- (fun _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1764, characters 62-76: - 1764 | e.econtinue <- (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -no-alias-deps -o interp/.interp.objs/byte/numTok.cmi -c -intf interp/numTok.mli) - File "interp/numTok.mli", line 85, characters 19-27: - 85 | val parse : char Stream.t -> t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -no-alias-deps -o parsing/.parsing.objs/byte/g_constr.cmo -c -impl parsing/g_constr.ml) - File "parsing/g_constr.mlg", line 46, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 -Wall -Wno-unused -g -O2 -msse2 -mfpmath=sse -g -I /home/opam/.opam/4.14/lib/ocaml -o coq_interp.o -c coq_interp.c) - coq_interp.c: In function 'coq_interprete': - coq_interp.c:301:20: warning: storing the address of local variable 'coq_lbl_ACC0' in 'coq_instr_base' [-Wdangling-pointer=] - 301 | coq_instr_base = coq_Jumptbl_base; - | ^ - coq_interp.c:74:26: note: 'coq_lbl_ACC0' declared here - 74 | # define Instruct(name) coq_lbl_##name: - | ^~~~~~~~ - coq_interp.c:325:7: note: in expansion of macro 'Instruct' - 325 | Instruct(ACC0){ - | ^~~~~~~~ - In file included from coq_interp.c:28: - coq_fix_code.h:20:15: note: 'coq_instr_base' declared here - 20 | extern char * coq_instr_base; - | ^~~~~~~~~~~~~~ - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -o toplevel/.toplevel.objs/byte/g_toplevel.cmo -c -impl toplevel/g_toplevel.ml) - File "toplevel/g_toplevel.mlg", line 34, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/native/numTok.cmx -c -impl interp/numTok.ml) - File "interp/numTok.ml", line 124, characters 33-44: - 124 | let rec number len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 125, characters 32-43: - 125 | | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 126, characters 40-51: - 126 | | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 129, characters 37-48: - 129 | let rec hex_number len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 131, characters 9-20: - 131 | Stream.junk s; hex_number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 133, characters 9-20: - 133 | Stream.junk s; hex_number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 137, characters 12-24: - 137 | match Stream.npeek 3 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 139, characters 9-20: - 139 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 139, characters 24-35: - 139 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 139, characters 39-50: - 139 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 144, characters 17-29: - 144 | match hex, Stream.npeek 2 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 146, characters 9-20: - 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 146, characters 24-35: - 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 148, characters 9-20: - 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 148, characters 24-35: - 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 151, characters 17-29: - 151 | match hex, Stream.npeek 2 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 154, characters 9-20: - 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 154, characters 24-35: - 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 157, characters 21-33: - 157 | begin match Stream.npeek 3 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 159, characters 12-23: - 159 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 159, characters 27-38: - 159 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 159, characters 42-53: - 159 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 174, characters 17-33: - 174 | let strm = Stream.of_string (s ^ " ") in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 176, characters 9-21: - 176 | if Stream.count strm >= String.length s then Some n else None - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 260, characters 17-33: - 260 | let strm = Stream.of_string (s ^ " ") in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 262, characters 18-29: - 262 | | '-' -> (Stream.junk strm; SMinus) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 263, characters 18-29: - 263 | | '+' -> (Stream.junk strm; SPlus) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 266, characters 9-21: - 266 | if Stream.count strm >= String.length s then Some (sign,n) else None - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/native/constrexpr_ops.cmx -c -impl interp/constrexpr_ops.ml) - File "interp/constrexpr_ops.ml", line 575, characters 24-36: - 575 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/native/constrintern.cmx -c -impl interp/constrintern.ml) - File "interp/constrintern.ml", line 584, characters 22-34: - 584 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/tok.cmx -c -impl parsing/tok.ml) - File "parsing/tok.ml", line 144, characters 21-35: - 144 | let err () = raise Stream.Failure in - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/cLexer.cmx -c -impl parsing/cLexer.ml) - File "parsing/cLexer.ml", line 162, characters 11-23: - 162 | let bp = Stream.count cs in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 163, characters 2-13: - 163 | Stream.junk cs; (* consume the char to avoid read it and fail again *) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 175, characters 28-39: - 175 | let njunk n = Util.repeat n Stream.junk - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 188, characters 12-24: - 188 | match Stream.npeek 2 cs with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 194, characters 12-24: - 194 | match Stream.npeek 3 cs with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 201, characters 17-29: - 201 | else match Stream.npeek 4 cs with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 213, characters 8-19: - 213 | match Stream.peek cs with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 225, characters 30-41: - 225 | let rec loop_symb s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 227, characters 8-19: - 227 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 232, characters 23-34: - 232 | | AsciiChar -> Stream.junk s; loop_symb s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 235, characters 13-29: - 235 | loop_symb (Stream.of_string str) - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 238, characters 35-46: - 238 | let rec loop_id intail s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 240, characters 8-19: - 240 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 243, characters 8-19: - 243 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 254, characters 17-33: - 254 | loop_id false (Stream.of_string str) - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 296, characters 39-50: - 296 | if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 308, characters 37-48: - 308 | let rec ident_tail loc len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 310, characters 6-17: - 310 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 318, characters 62-74: - 318 | let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 332, characters 48-59: - 332 | let rec string loc ~comm_level bp len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 334, characters 6-17: - 334 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 336, characters 14-25: - 336 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 337, characters 22-33: - 337 | Some '"' -> Stream.junk s; true - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 342, characters 6-17: - 342 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 343, characters 22-33: - 343 | (fun s -> match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 345, characters 8-19: - 345 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 353, characters 6-17: - 353 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 354, characters 22-33: - 354 | (fun s -> match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 356, characters 12-23: - 356 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 367, characters 4-15: - 367 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 368, characters 13-25: - 368 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 378, characters 6-17: - 378 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 381, characters 14-26: - 381 | let _ = Stream.empty s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 382, characters 15-27: - 382 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 435, characters 12-24: - 435 | let bp2 = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 436, characters 8-19: - 436 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 438, characters 6-17: - 438 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 441, characters 16-27: - 441 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 443, characters 14-25: - 443 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 446, characters 13-27: - 446 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 446, characters 38-50: - 446 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 450, characters 6-17: - 450 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 452, characters 14-25: - 452 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 453, characters 22-33: - 453 | Some ')' -> Stream.junk s; push_string "*)"; loc - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 455, characters 11-25: - 455 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 455, characters 36-48: - 455 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 458, characters 6-17: - 458 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 463, characters 20-32: - 463 | match try Some (Stream.empty s) with Stream.Failure -> None with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 463, characters 41-55: - 463 | match try Some (Stream.empty s) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 465, characters 15-27: - 465 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 469, characters 16-27: - 469 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 471, characters 14-25: - 471 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 472, characters 23-35: - 472 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 475, characters 14-25: - 475 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 477, characters 23-37: - 477 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 484, characters 54-66: - 484 | try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 503, characters 36-48: - 503 | match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 517, characters 8-19: - 517 | match Stream.peek cs with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 528, characters 16-30: - 528 | | exception Stream.Failure -> n, List.make n b, List.make n e - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 531, characters 24-38: - 531 | if len = 0 then raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 540, characters 17-31: - 540 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 545, characters 14-25: - 545 | let c = Stream.next s in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 548, characters 10-24: - 548 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 548, characters 35-47: - 548 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 550, characters 40-52: - 550 | get_buff len, set_loc_pos loc bp (Stream.count s) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 558, characters 43-54: - 558 | let commit1 c = Buffer.add_char b c; Stream.junk s in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 561, characters 14-26: - 561 | match Stream.npeek lenmarker s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 570, characters 48-60: - 570 | let loc = bump_loc_line_last loc (Stream.count s) in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 574, characters 63-77: - 574 | if not dot_gobbling && blank_or_eof s then raise Stream.Failure; - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 579, characters 22-36: - 579 | | [] -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 582, characters 45-57: - 582 | Buffer.contents b, set_loc_pos loc bp (Stream.count s) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 589, characters 15-27: - 589 | let l' = Stream.npeek (i + 1) s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 599, characters 6-17: - 599 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 608, characters 15-27: - 608 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 616, characters 10-21: - 616 | match Stream.peek cs with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 617, characters 30-41: - 617 | | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 618, characters 57-69: - 618 | | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 625, characters 11-23: - 625 | let ep = Stream.count cs in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 646, characters 50-61: - 646 | let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 648, characters 6-17: - 648 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 651, characters 10-24: - 651 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 651, characters 35-47: - 651 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 656, characters 17-29: - 656 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 665, characters 21-33: - 665 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 673, characters 8-19: - 673 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 685, characters 11-23: - 685 | let bp = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 686, characters 8-19: - 686 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 688, characters 6-17: - 688 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 689, characters 15-27: - 689 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 692, characters 6-17: - 692 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 695, characters 6-17: - 695 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 698, characters 10-24: - 698 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 698, characters 35-47: - 698 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 706, characters 21-33: - 706 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 714, characters 6-17: - 714 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 721, characters 6-17: - 721 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 722, characters 15-27: - 722 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 726, characters 6-17: - 726 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 729, characters 10-24: - 729 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 729, characters 35-47: - 729 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 735, characters 17-29: - 735 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 742, characters 17-29: - 742 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 745, characters 6-17: - 745 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 748, characters 10-24: - 748 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 748, characters 35-47: - 748 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 750, characters 15-27: - 750 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 754, characters 6-17: - 754 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 756, characters 14-25: - 756 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 758, characters 12-23: - 758 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 759, characters 21-33: - 759 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 762, characters 12-23: - 762 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 767, characters 11-25: - 767 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 767, characters 36-48: - 767 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 770, characters 6-17: - 770 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 771, characters 15-27: - 771 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 785, characters 23-35: - 785 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 788, characters 53-64: - 788 | let t = process_chars ~diff_mode loc bp (Stream.next s) s in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/pcoq.cmx -c -impl parsing/pcoq.ml) - File "parsing/pcoq.ml", line 22, characters 21-35: - 22 | let err () = raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/pcoq.ml", line 199, characters 13-29: - 199 | let strm = Stream.of_string x in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/g_constr.cmx -c -impl parsing/g_constr.ml) - File "parsing/g_constr.mlg", line 46, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I printing/.printing.objs/byte -I printing/.printing.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -intf-suffix .ml -no-alias-deps -o printing/.printing.objs/native/proof_diffs.cmx -c -impl printing/proof_diffs.ml) - File "printing/proof_diffs.ml", line 102, characters 15-31: - 102 | let istr = Stream.of_string s in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/himsg.cmx -c -impl vernac/himsg.ml) - File "vernac/himsg.ml", line 1439, characters 4-16: - 1439 | | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/proof_using.cmx -c -impl vernac/proof_using.ml) - File "vernac/proof_using.ml", line 212, characters 25-41: - 212 | (Pcoq.Parsable.make (Stream.of_string ("( "^us^" )"))) - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/comInductive.cmx -c -impl vernac/comInductive.ml) - File "vernac/comInductive.ml", line 416, characters 20-32: - 416 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "vernac/comInductive.ml", line 718, characters 20-32: - 718 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/record.cmx -c -impl vernac/record.ml) - File "vernac/record.ml", line 103, characters 20-32: - 103 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/vernacinterp.cmx -c -impl vernac/vernacinterp.ml) - File "vernac/vernacinterp.ml", line 176, characters 9-26: - 176 | (Stream.of_channel in_chan) in - ^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/native/g_toplevel.cmx -c -impl toplevel/g_toplevel.ml) - File "toplevel/g_toplevel.mlg", line 34, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/native/vernac.cmx -c -impl toplevel/vernac.ml) - File "toplevel/vernac.ml", line 93, characters 7-24: - 93 | (Stream.of_channel in_chan) in - ^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/native/coqloop.cmx -c -impl toplevel/coqloop.ml) - File "toplevel/coqloop.ml", line 79, characters 37-48: - 79 | ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "toplevel/coqloop.ml", line 233, characters 33-47: - 233 | tokens = Pcoq.Parsable.make (Stream.of_list []); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - COQCBOOT theories/Init/Notations.v - Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins - [cannot-open-dir,filesystem] - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I plugins/ltac/.ltac_plugin.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -open Ltac_plugin -o plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_tactic.cmo -c -impl plugins/ltac/g_tactic.ml) - File "plugins/ltac/g_tactic.mlg", line 33, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I plugins/ltac/.ltac_plugin.objs/byte -I plugins/ltac/.ltac_plugin.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -open Ltac_plugin -o plugins/ltac/.ltac_plugin.objs/native/ltac_plugin__G_tactic.cmx -c -impl plugins/ltac/g_tactic.ml) - File "plugins/ltac/g_tactic.mlg", line 33, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -open Gramlib -g -O3 -unbox-closures -I plugins/ssr/.ssreflect_plugin.objs/byte -I plugins/ssr/.ssreflect_plugin.objs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I plugins/ltac/.ltac_plugin.objs/byte -I plugins/ltac/.ltac_plugin.objs/native -I plugins/ssrmatching/.ssrmatching_plugin.objs/byte -I plugins/ssrmatching/.ssrmatching_plugin.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -open Ssreflect_plugin -o plugins/ssr/.ssreflect_plugin.objs/native/ssreflect_plugin__Ssrparser.cmx -c -impl plugins/ssr/ssrparser.ml) - File "plugins/ssr/ssrparser.mlg", line 263, characters 28-42: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 265, characters 22-36: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 272, characters 24-38: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 274, characters 22-36: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 276, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 283, characters 24-38: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 285, characters 22-36: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 286, characters 15-29: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 294, characters 31-45: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 297, characters 20-34: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 845, characters 33-47: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 854, characters 9-23: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 859, characters 12-26: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 860, characters 55-69: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 861, characters 45-59: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 2417, characters 37-51: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 2421, characters 17-31: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I checker/.coq_checklib.objs/byte -I checker/.coq_checklib.objs/native -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Coq_checklib -o checker/.coq_checklib.objs/native/coq_checklib__Checker.cmx -c -impl checker/checker.ml) - File "checker/checker.ml", line 226, characters 4-18: - 226 | | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "checker/checker.ml", line 228, characters 4-16: - 228 | | Stream.Error txt -> - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/byte/lStream.cmo -c -impl lib/lStream.ml) - File "lib/lStream.ml", line 14, characters 12-20: - 14 | strm : 'a Stream.t; - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 26, characters 4-15: - 26 | Stream.from - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 35, characters 17-29: - 35 | let count strm = Stream.count strm.strm - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 38, characters 16-28: - 38 | strm.fun_loc (Stream.count strm.strm) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 57, characters 10-21: - 57 | let a = Stream.peek strm.strm in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 58, characters 22-33: - 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 58, characters 72-84: - 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek; - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 62, characters 10-22: - 62 | let l = Stream.npeek n strm.strm in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 63, characters 24-36: - 63 | strm.max_peek <- max (Stream.count strm.strm + List.length l) strm.max_peek; - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 67, characters 13-25: - 67 | let list = Stream.npeek (n + 1) strm.strm in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 70, characters 36-48: - 70 | x :: _, 0 -> strm.max_peek <- Stream.count strm.strm + n + 1; x - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 72, characters 32-44: - 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 72, characters 72-86: - 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 76, characters 16-27: - 76 | let junk strm = Stream.junk strm.strm - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/lStream.ml", line 78, characters 16-27: - 78 | let next strm = Stream.next strm.strm - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Plexing.cmo -c -impl gramlib/plexing.ml) - File "gramlib/plexing.ml", line 5, characters 41-49: - 5 | type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/byte/coqProject_file.cmo -c -impl lib/coqProject_file.ml) - File "lib/coqProject_file.ml", line 86, characters 35-46: - 86 | let rec parse_string buf s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 94, characters 12-26: - 94 | | exception Stream.Failure -> buffer buf - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 96, characters 32-43: - 96 | and parse_string2 buf s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 101, characters 12-26: - 101 | | exception Stream.Failure -> raise (Parsing_error "unterminated string") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 103, characters 33-44: - 103 | and parse_skip_comment s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 106, characters 12-26: - 106 | | exception Stream.Failure -> () - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 108, characters 34-45: - 108 | and parse_args buf accu s = match Stream.next s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 120, characters 12-26: - 120 | | exception Stream.Failure -> accu - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/coqProject_file.ml", line 127, characters 31-48: - 127 | let res = parse_args buf [] (Stream.of_channel c) in - ^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/byte/util.cmo -c -impl lib/util.ml) - File "lib/util.ml", line 126, characters 16-28: - 126 | try List.nth (Stream.npeek (n+1) st) n - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/util.ml", line 127, characters 26-40: - 127 | with Failure _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "lib/util.ml", line 130, characters 11-22: - 130 | repeat n Stream.junk st - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Grammar.cmo -c -impl gramlib/grammar.ml) - File "gramlib/grammar.ml", line 21, characters 34-42: - 21 | val make : ?loc:Loc.t -> char Stream.t -> t - ^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1093, characters 15-29: - 1093 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1102, characters 15-29: - 1102 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1111, characters 27-41: - 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1111, characters 61-75: - 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1115, characters 13-27: - 1115 | else raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1121, characters 6-20: - 1121 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son)) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1121, characters 31-43: - 1121 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1140, characters 4-18: - 1140 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1147, characters 62-76: - 1147 | skip_if_empty bp (fun (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1149, characters 11-25: - 1149 | with Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1182, characters 52-66: - 1182 | DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1193, characters 53-67: - 1193 | try Some (entry.estart alevn strm__) with Stream.Failure -> None - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1203, characters 31-45: - 1203 | try p1 strm__ with Stream.Failure -> p2 strm__) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1213, characters 17-31: - 1213 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1214, characters 26-38: - 1214 | raise (Stream.Error (tree_failed entry a s son)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1224, characters 43-57: - 1224 | match try Some (ps strm) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1227, characters 49-63: - 1227 | (try Some (p1 bp a strm) with Stream.Failure -> None) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1230, characters 34-46: - 1230 | | None -> raise (Stream.Error (tree_failed entry a s son)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1237, characters 4-18: - 1237 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1265, characters 66-80: - 1265 | (match (try Some (tematch (LStream.peek_nth n strm)) with Stream.Failure -> None) with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1267, characters 44-58: - 1267 | (match try Some (p1 a strm) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1271, characters 42-56: - 1271 | | DeadEnd -> fun last_a strm -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1277, characters 35-49: - 1277 | try Some (ps strm) with Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1279, characters 87-101: - 1279 | try Some (parser_of_tree entry nlevn alevn (top_tree entry tree) strm) with Stream.Failure -> None - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1282, characters 26-38: - 1282 | | None -> raise (Stream.Error (tree_failed entry last_a (Stoken last_tok) tree)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1289, characters 20-34: - 1289 | | None -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1297, characters 43-57: - 1297 | match try Some (ps al strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1307, characters 40-54: - 1307 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1311, characters 16-30: - 1311 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1312, characters 25-37: - 1312 | raise (Stream.Error (symb_failed entry v sep symb)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1318, characters 44-58: - 1318 | match try Some (ps [] strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1325, characters 40-54: - 1325 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1328, characters 44-58: - 1328 | (try Some (ps al strm__) with Stream.Failure -> None) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1336, characters 44-58: - 1336 | match try Some (ps [] strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1342, characters 43-57: - 1342 | match try Some (ps al strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1353, characters 40-54: - 1353 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1357, characters 16-30: - 1357 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1360, characters 22-36: - 1360 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1361, characters 31-43: - 1361 | raise (Stream.Error (symb_failed entry v sep symb)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1375, characters 40-54: - 1375 | match try Some (pt strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1378, characters 44-58: - 1378 | (try Some (ps al strm__) with Stream.Failure -> None) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1384, characters 20-34: - 1384 | Stream.Failure -> None - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1397, characters 41-55: - 1397 | match try Some (ps strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1421, characters 20-34: - 1421 | | None -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1466, characters 52-66: - 1466 | [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1502, characters 50-64: - 1502 | match try Some (p2 strm__) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1523, characters 57-71: - 1523 | [] -> (fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1542, characters 16-30: - 1542 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1553, characters 37-51: - 1553 | try p levn bp a strm__ with Stream.Failure -> a) - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1554, characters 63-77: - 1554 | | Dparser p -> fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1557, characters 9-21: - 1557 | raise (Stream.Error ("entry [" ^ ename ^ "] is empty")) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1622, characters 6-20: - 1622 | Stream.Failure -> - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1625, characters 6-18: - 1625 | | Stream.Error _ as exc -> - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1624, characters 22-34: - 1624 | Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename)) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1662, characters 51-65: - 1662 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1675, characters 51-65: - 1675 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1763, characters 55-69: - 1763 | e.estart <- (fun _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "gramlib/grammar.ml", line 1764, characters 62-76: - 1764 | e.econtinue <- (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/byte/numTok.cmo -c -impl interp/numTok.ml) - File "interp/numTok.ml", line 124, characters 33-44: - 124 | let rec number len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 125, characters 32-43: - 125 | | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 126, characters 40-51: - 126 | | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 129, characters 37-48: - 129 | let rec hex_number len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 131, characters 9-20: - 131 | Stream.junk s; hex_number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 133, characters 9-20: - 133 | Stream.junk s; hex_number (store len c) s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 137, characters 12-24: - 137 | match Stream.npeek 3 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 139, characters 9-20: - 139 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 139, characters 24-35: - 139 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 139, characters 39-50: - 139 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 144, characters 17-29: - 144 | match hex, Stream.npeek 2 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 146, characters 9-20: - 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 146, characters 24-35: - 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 148, characters 9-20: - 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 148, characters 24-35: - 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 151, characters 17-29: - 151 | match hex, Stream.npeek 2 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 154, characters 9-20: - 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 154, characters 24-35: - 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 157, characters 21-33: - 157 | begin match Stream.npeek 3 s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 159, characters 12-23: - 159 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 159, characters 27-38: - 159 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 159, characters 42-53: - 159 | Stream.junk s; Stream.junk s; Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 174, characters 17-33: - 174 | let strm = Stream.of_string (s ^ " ") in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 176, characters 9-21: - 176 | if Stream.count strm >= String.length s then Some n else None - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 260, characters 17-33: - 260 | let strm = Stream.of_string (s ^ " ") in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 262, characters 18-29: - 262 | | '-' -> (Stream.junk strm; SMinus) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 263, characters 18-29: - 263 | | '+' -> (Stream.junk strm; SPlus) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "interp/numTok.ml", line 266, characters 9-21: - 266 | if Stream.count strm >= String.length s then Some (sign,n) else None - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/byte/tok.cmo -c -impl parsing/tok.ml) - File "parsing/tok.ml", line 144, characters 21-35: - 144 | let err () = raise Stream.Failure in - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/byte/pcoq.cmo -c -impl parsing/pcoq.ml) - File "parsing/pcoq.ml", line 22, characters 21-35: - 22 | let err () = raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/pcoq.ml", line 199, characters 13-29: - 199 | let strm = Stream.of_string x in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I printing/.printing.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I proofs/.proofs.objs/byte -intf-suffix .ml -no-alias-deps -o printing/.printing.objs/byte/proof_diffs.cmo -c -impl printing/proof_diffs.ml) - File "printing/proof_diffs.ml", line 102, characters 15-31: - 102 | let istr = Stream.of_string s in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/byte/constrexpr_ops.cmo -c -impl interp/constrexpr_ops.ml) - File "interp/constrexpr_ops.ml", line 575, characters 24-36: - 575 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/byte/cLexer.cmo -c -impl parsing/cLexer.ml) - File "parsing/cLexer.ml", line 162, characters 11-23: - 162 | let bp = Stream.count cs in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 163, characters 2-13: - 163 | Stream.junk cs; (* consume the char to avoid read it and fail again *) - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 175, characters 28-39: - 175 | let njunk n = Util.repeat n Stream.junk - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 188, characters 12-24: - 188 | match Stream.npeek 2 cs with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 194, characters 12-24: - 194 | match Stream.npeek 3 cs with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 201, characters 17-29: - 201 | else match Stream.npeek 4 cs with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 213, characters 8-19: - 213 | match Stream.peek cs with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 225, characters 30-41: - 225 | let rec loop_symb s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 227, characters 8-19: - 227 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 232, characters 23-34: - 232 | | AsciiChar -> Stream.junk s; loop_symb s - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 235, characters 13-29: - 235 | loop_symb (Stream.of_string str) - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 238, characters 35-46: - 238 | let rec loop_id intail s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 240, characters 8-19: - 240 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 243, characters 8-19: - 243 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 254, characters 17-33: - 254 | loop_id false (Stream.of_string str) - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 296, characters 39-50: - 296 | if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 308, characters 37-48: - 308 | let rec ident_tail loc len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 310, characters 6-17: - 310 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 318, characters 62-74: - 318 | let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 332, characters 48-59: - 332 | let rec string loc ~comm_level bp len s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 334, characters 6-17: - 334 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 336, characters 14-25: - 336 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 337, characters 22-33: - 337 | Some '"' -> Stream.junk s; true - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 342, characters 6-17: - 342 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 343, characters 22-33: - 343 | (fun s -> match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 345, characters 8-19: - 345 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 353, characters 6-17: - 353 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 354, characters 22-33: - 354 | (fun s -> match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 356, characters 12-23: - 356 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 367, characters 4-15: - 367 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 368, characters 13-25: - 368 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 378, characters 6-17: - 378 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 381, characters 14-26: - 381 | let _ = Stream.empty s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 382, characters 15-27: - 382 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 435, characters 12-24: - 435 | let bp2 = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 436, characters 8-19: - 436 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 438, characters 6-17: - 438 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 441, characters 16-27: - 441 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 443, characters 14-25: - 443 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 446, characters 13-27: - 446 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 446, characters 38-50: - 446 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 450, characters 6-17: - 450 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 452, characters 14-25: - 452 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 453, characters 22-33: - 453 | Some ')' -> Stream.junk s; push_string "*)"; loc - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 455, characters 11-25: - 455 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 455, characters 36-48: - 455 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 458, characters 6-17: - 458 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 463, characters 20-32: - 463 | match try Some (Stream.empty s) with Stream.Failure -> None with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 463, characters 41-55: - 463 | match try Some (Stream.empty s) with Stream.Failure -> None with - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 465, characters 15-27: - 465 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 469, characters 16-27: - 469 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 471, characters 14-25: - 471 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 472, characters 23-35: - 472 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 475, characters 14-25: - 475 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 477, characters 23-37: - 477 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 484, characters 54-66: - 484 | try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 503, characters 36-48: - 503 | match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 517, characters 8-19: - 517 | match Stream.peek cs with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 528, characters 16-30: - 528 | | exception Stream.Failure -> n, List.make n b, List.make n e - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 531, characters 24-38: - 531 | if len = 0 then raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 540, characters 17-31: - 540 | | _ -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 545, characters 14-25: - 545 | let c = Stream.next s in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 548, characters 10-24: - 548 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 548, characters 35-47: - 548 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 550, characters 40-52: - 550 | get_buff len, set_loc_pos loc bp (Stream.count s) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 558, characters 43-54: - 558 | let commit1 c = Buffer.add_char b c; Stream.junk s in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 561, characters 14-26: - 561 | match Stream.npeek lenmarker s with - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 570, characters 48-60: - 570 | let loc = bump_loc_line_last loc (Stream.count s) in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 574, characters 63-77: - 574 | if not dot_gobbling && blank_or_eof s then raise Stream.Failure; - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 579, characters 22-36: - 579 | | [] -> raise Stream.Failure - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 582, characters 45-57: - 582 | Buffer.contents b, set_loc_pos loc bp (Stream.count s) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 589, characters 15-27: - 589 | let l' = Stream.npeek (i + 1) s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 599, characters 6-17: - 599 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 608, characters 15-27: - 608 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 616, characters 10-21: - 616 | match Stream.peek cs with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 617, characters 30-41: - 617 | | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 618, characters 57-69: - 618 | | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 625, characters 11-23: - 625 | let ep = Stream.count cs in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 646, characters 50-61: - 646 | let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 648, characters 6-17: - 648 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 651, characters 10-24: - 651 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 651, characters 35-47: - 651 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 656, characters 17-29: - 656 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 665, characters 21-33: - 665 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 673, characters 8-19: - 673 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 685, characters 11-23: - 685 | let bp = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 686, characters 8-19: - 686 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 688, characters 6-17: - 688 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 689, characters 15-27: - 689 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 692, characters 6-17: - 692 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 695, characters 6-17: - 695 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 698, characters 10-24: - 698 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 698, characters 35-47: - 698 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 706, characters 21-33: - 706 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 714, characters 6-17: - 714 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 721, characters 6-17: - 721 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 722, characters 15-27: - 722 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 726, characters 6-17: - 726 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 729, characters 10-24: - 729 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 729, characters 35-47: - 729 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 735, characters 17-29: - 735 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 742, characters 17-29: - 742 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 745, characters 6-17: - 745 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 748, characters 10-24: - 748 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 748, characters 35-47: - 748 | Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 750, characters 15-27: - 750 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 754, characters 6-17: - 754 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 756, characters 14-25: - 756 | match Stream.peek s with - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 758, characters 12-23: - 758 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 759, characters 21-33: - 759 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 762, characters 12-23: - 762 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 767, characters 11-25: - 767 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 767, characters 36-48: - 767 | with Stream.Failure -> raise (Stream.Error "") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 770, characters 6-17: - 770 | Stream.junk s; - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 771, characters 15-27: - 771 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 785, characters 23-35: - 785 | let ep = Stream.count s in - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "parsing/cLexer.ml", line 788, characters 53-64: - 788 | let t = process_chars ~diff_mode loc bp (Stream.next s) s in - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/vernacinterp.cmo -c -impl vernac/vernacinterp.ml) - File "vernac/vernacinterp.ml", line 176, characters 9-26: - 176 | (Stream.of_channel in_chan) in - ^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/proof_using.cmo -c -impl vernac/proof_using.ml) - File "vernac/proof_using.ml", line 212, characters 25-41: - 212 | (Pcoq.Parsable.make (Stream.of_string ("( "^us^" )"))) - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/byte/vernac.cmo -c -impl toplevel/vernac.ml) - File "toplevel/vernac.ml", line 93, characters 7-24: - 93 | (Stream.of_channel in_chan) in - ^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/comInductive.cmo -c -impl vernac/comInductive.ml) - File "vernac/comInductive.ml", line 416, characters 20-32: - 416 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "vernac/comInductive.ml", line 718, characters 20-32: - 718 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/record.cmo -c -impl vernac/record.ml) - File "vernac/record.ml", line 103, characters 20-32: - 103 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/byte/coqloop.cmo -c -impl toplevel/coqloop.ml) - File "toplevel/coqloop.ml", line 79, characters 37-48: - 79 | ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); - ^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "toplevel/coqloop.ml", line 233, characters 33-47: - 233 | tokens = Pcoq.Parsable.make (Stream.of_list []); - ^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/himsg.cmo -c -impl vernac/himsg.ml) - File "vernac/himsg.ml", line 1439, characters 4-16: - 1439 | | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/byte/constrintern.cmo -c -impl interp/constrintern.ml) - File "interp/constrintern.ml", line 584, characters 22-34: - 584 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") - ^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -open Gramlib -g -bin-annot -I plugins/ssr/.ssreflect_plugin.objs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I plugins/ltac/.ltac_plugin.objs/byte -I plugins/ssrmatching/.ssrmatching_plugin.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -intf-suffix .ml -no-alias-deps -open Ssreflect_plugin -o plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrparser.cmo -c -impl plugins/ssr/ssrparser.ml) - File "plugins/ssr/ssrparser.mlg", line 263, characters 28-42: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 265, characters 22-36: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 272, characters 24-38: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 274, characters 22-36: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 276, characters 19-33: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 283, characters 24-38: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 285, characters 22-36: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 286, characters 15-29: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 294, characters 31-45: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 297, characters 20-34: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 845, characters 33-47: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 854, characters 9-23: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 859, characters 12-26: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 860, characters 55-69: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 861, characters 45-59: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 2417, characters 37-51: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "plugins/ssr/ssrparser.mlg", line 2421, characters 17-31: - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I ide/coqide/.idetop.eobjs/byte -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I ide/coqide/.platform_specific.objs/byte -I ide/coqide/protocol/.protocol.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I toplevel/.toplevel.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -o ide/coqide/.idetop.eobjs/byte/dune__exe__Idetop.cmo -c -impl ide/coqide/idetop.ml) - File "ide/coqide/idetop.ml", line 96, characters 36-52: - 96 | let pa = Pcoq.Parsable.make ~loc (Stream.of_string s) in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "ide/coqide/idetop.ml", line 123, characters 31-47: - 123 | let pa = Pcoq.Parsable.make (Stream.of_string s) in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "ide/coqide/idetop.ml", line 129, characters 31-47: - 129 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I ide/coqide/.idetop.eobjs/byte -I ide/coqide/.idetop.eobjs/native -I /home/opam/.opam/4.14/lib/findlib -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I ide/coqide/.platform_specific.objs/byte -I ide/coqide/.platform_specific.objs/native -I ide/coqide/protocol/.protocol.objs/byte -I ide/coqide/protocol/.protocol.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o ide/coqide/.idetop.eobjs/native/dune__exe__Idetop.cmx -c -impl ide/coqide/idetop.ml) - File "ide/coqide/idetop.ml", line 96, characters 36-52: - 96 | let pa = Pcoq.Parsable.make ~loc (Stream.of_string s) in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "ide/coqide/idetop.ml", line 123, characters 31-47: - 123 | let pa = Pcoq.Parsable.make (Stream.of_string s) in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - File "ide/coqide/idetop.ml", line 129, characters 31-47: - 129 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in - ^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Stream - Use the camlp-streams library instead. - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQCBOOT theories/Init/Ltac.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQCBOOT theories/Init/Logic.v - COQCBOOT theories/Init/Datatypes.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQCBOOT theories/Init/Specif.v - COQCBOOT theories/Init/Wf.v - COQCBOOT theories/Init/Tauto.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQCBOOT theories/Init/Decimal.v - COQCBOOT theories/Init/Tactics.v - COQCBOOT theories/Init/Hexadecimal.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQCBOOT theories/Init/Number.v - COQCBOOT theories/Init/Nat.v - COQCBOOT theories/Init/Byte.v - COQCBOOT theories/Init/Peano.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQCBOOT theories/Init/Prelude.v - COQC theories/ssrmatching/ssrmatching.v - COQC theories/ssr/ssrclasses.v - COQC theories/Program/Basics.v - COQC theories/Program/Tactics.v - COQC theories/Relations/Relation_Definitions.v - COQC theories/Bool/Bool.v - COQC theories/Numbers/BinNums.v - COQC theories/Logic/EqdepFacts.v - COQC theories/Logic/Decidable.v - COQC theories/Bool/Sumbool.v - COQC theories/setoid_ring/Algebra_syntax.v - COQC theories/micromega/ZifyClasses.v - COQC theories/Logic/FunctionalExtensionality.v - COQC theories/Logic/PropExtensionalityFacts.v - COQC theories/Logic/Hurkens.v - COQC theories/Unicode/Utf8_core.v - COQC theories/Numbers/Cyclic/Abstract/CarryType.v - COQC theories/Floats/FloatClass.v - COQC theories/Wellfounded/Inverse_Image.v - COQC theories/Sets/Relations_1.v - COQC theories/Sets/Permut.v - COQC theories/Sets/Ensembles.v - COQC theories/Logic/StrictProp.v - COQC theories/Logic/RelationalChoice.v - COQC theories/Logic/ExtensionalFunctionRepresentative.v - COQC theories/Logic/SetIsType.v - COQC theories/Logic/PropFacts.v - COQC theories/Logic/ExtensionalityFacts.v - COQC theories/Logic/Berardi.v - COQC theories/Logic/Adjointification.v - COQC theories/Lists/Streams.v - COQC theories/Compat/Coq816.v - COQC theories/Compat/AdmitAxiom.v - COQC theories/Bool/DecBool.v - COQC theories/ssr/ssrunder.v - COQC theories/Classes/Init.v - COQC theories/Relations/Relation_Operators.v - COQC theories/PArith/BinPosDef.v - COQC theories/Unicode/Utf8.v - COQC theories/Numbers/Cyclic/Int63/PrimInt63.v - COQC theories/Wellfounded/Inclusion.v - COQC theories/Sets/Relations_1_facts.v - COQC theories/Sets/Relations_2.v - COQC theories/Sets/Constructive_sets.v - COQC theories/Sets/Partial_Order.v - COQC theories/Program/Utils.v - COQC theories/Numbers/AltBinNotations.v - COQC theories/Logic/HLevels.v - COQC theories/Program/Combinators.v - COQC theories/Compat/Coq815.v - COQC theories/Classes/RelationClasses.v - COQC theories/Classes/CRelationClasses.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/Logic/Eqdep_dec.v - COQC theories/Wellfounded/Well_Ordering.v - COQC theories/Logic/Eqdep.v - COQC theories/Logic/ProofIrrelevanceFacts.v - COQC theories/Floats/PrimFloat.v - COQC theories/Sets/Relations_3.v - COQC theories/Sets/Relations_2_facts.v - COQC theories/Compat/Coq814.v - COQC theories/Sets/Finite_sets.v - COQC theories/Sets/Cpo.v - COQC theories/Relations/Operators_Properties.v - COQC theories/Wellfounded/Disjoint_Union.v - COQC theories/Wellfounded/Transitive_Closure.v - COQC theories/Logic/JMeq.v - COQC theories/Logic/ProofIrrelevance.v - COQC theories/Sets/Powerset.v - COQC theories/Sets/Relations_3_facts.v - COQC theories/Lists/StreamMemo.v - COQC theories/Wellfounded/Lexicographic_Product.v - COQC theories/Wellfounded/Union.v - COQC theories/Program/Equality.v - COQC theories/Classes/CMorphisms.v - COQC theories/ssr/ssreflect.v - COQC theories/Sets/Uniset.v - COQC theories/Bool/IfProp.v - COQC theories/Bool/BoolEq.v - COQC theories/Relations/Relations.v - COQC theories/Sets/Powerset_facts.v - COQC theories/Program/Subset.v - COQC theories/ssr/ssrsetoid.v - COQC theories/Classes/Morphisms.v - COQC theories/ssr/ssrfun.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/ssr/ssrbool.v - COQC theories/Classes/CEquivalence.v - COQC theories/Classes/Morphisms_Prop.v - COQC theories/Classes/Equivalence.v - COQC theories/Classes/SetoidTactics.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/Setoids/Setoid.v - COQC theories/Structures/Equalities.v - COQC theories/Numbers/NumPrelude.v - COQC theories/Structures/Orders.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/Structures/OrdersTac.v - COQC theories/Bool/BoolOrder.v - COQC theories/Structures/OrdersFacts.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/Structures/GenericMinMax.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/extraction/Extraction.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/extraction/ExtrOcamlBasic.v - COQC theories/extraction/ExtrHaskellBasic.v - COQC theories/Program/Wf.v - COQC theories/Numbers/NatInt/NZAxioms.v - COQC theories/Numbers/NatInt/NZBase.v - COQC theories/Numbers/NatInt/NZAdd.v - COQC theories/Numbers/NatInt/NZOrder.v - COQC theories/funind/FunInd.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/Numbers/NatInt/NZMul.v - COQC theories/Numbers/NatInt/NZAddOrder.v - COQC theories/derive/Derive.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC theories/Numbers/NatInt/NZMulOrder.v - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - COQC user-contrib/Ltac2/Init.v - COQC theories/Numbers/NatInt/NZParity.v - COQC theories/Numbers/NatInt/NZPow.v - COQC theories/Numbers/NatInt/NZSqrt.v - COQC theories/Numbers/NatInt/NZDiv.v - COQC theories/Numbers/NatInt/NZGcd.v - COQC theories/Numbers/NatInt/NZProperties.v - COQC user-contrib/Ltac2/String.v - COQC user-contrib/Ltac2/Std.v - COQC user-contrib/Ltac2/Message.v - COQC user-contrib/Ltac2/Int.v - COQC user-contrib/Ltac2/Bool.v - COQC user-contrib/Ltac2/Char.v - COQC user-contrib/Ltac2/Constr.v - COQC user-contrib/Ltac2/Ident.v - COQC user-contrib/Ltac2/Ind.v - COQC user-contrib/Ltac2/Ltac1.v - COQC user-contrib/Ltac2/Printf.v - COQC user-contrib/Ltac2/Control.v - COQC user-contrib/Ltac2/Env.v - COQC user-contrib/Ltac2/Pattern.v - COQC user-contrib/Ltac2/Option.v - COQC user-contrib/Ltac2/Array.v - COQC user-contrib/Ltac2/List.v - COQC user-contrib/Ltac2/Fresh.v - COQC user-contrib/Ltac2/Notations.v - COQC user-contrib/Ltac2/Ltac2.v - COQC theories/Numbers/NatInt/NZLog.v - COQC theories/Numbers/NatInt/NZBits.v - COQC theories/Numbers/Natural/Abstract/NAxioms.v - COQC theories/Numbers/Integer/Abstract/ZAxioms.v - COQC theories/Numbers/Natural/Abstract/NBase.v - COQC theories/Numbers/Integer/Abstract/ZBase.v - COQC theories/Numbers/Integer/Abstract/ZAdd.v - COQC theories/Numbers/Natural/Abstract/NAdd.v - COQC theories/Numbers/Natural/Abstract/NIso.v - COQC theories/Numbers/Natural/Abstract/NOrder.v - COQC theories/Numbers/Integer/Abstract/ZMul.v - COQC theories/Numbers/Integer/Abstract/ZLt.v - COQC theories/Numbers/Natural/Abstract/NAddOrder.v - COQC theories/Numbers/Integer/Abstract/ZAddOrder.v - COQC theories/Numbers/Natural/Abstract/NMulOrder.v - COQC theories/Numbers/Natural/Abstract/NSub.v - COQC theories/Numbers/Integer/Abstract/ZMulOrder.v - COQC theories/Numbers/Natural/Abstract/NMaxMin.v - COQC theories/Numbers/Natural/Abstract/NParity.v - COQC theories/Numbers/Natural/Abstract/NSqrt.v - COQC theories/Numbers/Natural/Abstract/NDiv.v - COQC theories/Numbers/Natural/Abstract/NGcd.v - COQC theories/Numbers/Natural/Abstract/NStrongRec.v - COQC theories/Numbers/Integer/Abstract/ZMaxMin.v - COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v - COQC theories/Numbers/Integer/Abstract/ZParity.v - COQC theories/Numbers/Natural/Abstract/NPow.v - COQC theories/Numbers/Natural/Abstract/NLog.v - COQC theories/Numbers/Natural/Abstract/NBits.v - COQC theories/Numbers/Natural/Abstract/NLcm.v - COQC theories/Numbers/Integer/Abstract/ZPow.v - COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v - COQC theories/Numbers/Integer/Abstract/ZDivFloor.v - COQC theories/Numbers/Integer/Abstract/ZGcd.v - COQC theories/Numbers/Integer/Abstract/ZDivEucl.v - COQC theories/Numbers/Integer/Abstract/ZBits.v - COQC theories/Numbers/Integer/Abstract/ZLcm.v - COQC theories/Numbers/Natural/Abstract/NProperties.v - COQC theories/Arith/PeanoNat.v - COQC theories/Arith/Arith_prebase.v - COQC theories/Lists/List.v - COQC theories/Arith/EqNat.v - COQC theories/Arith/Max.v - COQC theories/Arith/Min.v - COQC theories/Arith/Even.v - COQC theories/Arith/Le.v - COQC theories/Arith/Lt.v - COQC theories/Arith/Plus.v - COQC theories/Arith/Minus.v - COQC theories/Arith/Between.v - COQC theories/Arith/Peano_dec.v - COQC theories/PArith/BinPos.v - COQC theories/Arith/Gt.v - COQC theories/Sets/Multiset.v - COQC theories/Numbers/NatInt/NZDomain.v - COQC theories/Arith/Mult.v - COQC theories/Numbers/Integer/Abstract/ZProperties.v - COQC theories/Arith/Compare_dec.v - COQC theories/Arith/Div2.v - COQC theories/Numbers/Natural/Peano/NPeano.v - COQC theories/Arith/Factorial.v - COQC theories/Arith/Wf_nat.v - COQC theories/Arith/Bool_nat.v - COQC theories/Arith/Arith_base.v - COQC theories/Logic/ClassicalFacts.v - COQC theories/funind/Recdef.v - COQC theories/Arith/Euclid.v - COQC theories/Vectors/Fin.v - COQC theories/Arith/Compare.v - COQC theories/Logic/Classical_Prop.v - COQC theories/Logic/PropExtensionality.v - COQC theories/Logic/Classical_Pred_Type.v - COQC theories/Vectors/VectorDef.v - COQC theories/Logic/Classical.v - COQC theories/Sets/Classical_sets.v - COQC theories/Logic/ClassicalUniqueChoice.v - COQC theories/NArith/BinNatDef.v - COQC theories/PArith/Pnat.v - COQC theories/PArith/POrderedType.v - COQC theories/Sets/Powerset_Classical_facts.v - COQC theories/NArith/BinNat.v - COQC theories/setoid_ring/BinList.v - COQC theories/Lists/ListTactics.v - COQC theories/Vectors/VectorSpec.v - COQC theories/micromega/Refl.v - COQC theories/rtauto/Bintree.v - COQC theories/Wellfounded/Lexicographic_Exponentiation.v - COQC theories/Sorting/Sorted.v - COQC theories/Lists/ListDec.v - COQC theories/Numbers/NaryFunctions.v - COQC theories/Logic/WeakFan.v - COQC theories/Lists/ListSet.v - COQC theories/Lists/SetoidList.v - COQC theories/PArith/PArith.v - COQC theories/Logic/FinFun.v - COQC theories/Sets/Finite_sets_facts.v - COQC theories/micromega/Tauto.v - COQC theories/Wellfounded/Wellfounded.v - COQC theories/rtauto/Rtauto.v - COQC theories/Vectors/VectorEq.v - COQC theories/Sorting/Permutation.v - COQC theories/Sets/Image.v - COQC theories/Vectors/Vector.v - COQC theories/setoid_ring/Ring_theory.v - COQC theories/ZArith/BinIntDef.v - COQC theories/NArith/Nnat.v - COQC theories/NArith/Ndiv_def.v - COQC theories/NArith/Nsqrt_def.v - COQC theories/NArith/Ngcd_def.v - COQC theories/Numbers/Natural/Binary/NBinary.v - COQC theories/Bool/Bvector.v - COQC theories/Sets/Infinite_sets.v - COQC theories/Program/Syntax.v - COQC theories/ZArith/BinInt.v - COQC theories/Program/Program.v - COQC theories/Sets/Integers.v - COQC theories/Classes/SetoidClass.v - COQC theories/Classes/Morphisms_Relations.v - COQC theories/Classes/EquivDec.v - COQC theories/Strings/Byte.v - COQC theories/Sorting/Mergesort.v - COQC theories/Sorting/CPermutation.v - COQC theories/Sorting/Sorting.v - COQC theories/Classes/RelationPairs.v - COQC theories/Structures/OrderedType.v - COQC theories/Structures/DecidableType.v - COQC theories/Lists/SetoidPermutation.v - COQC theories/Structures/EqualitiesFacts.v - COQC theories/Numbers/Natural/Abstract/NDefOps.v - COQC theories/MSets/MSetInterface.v - COQC theories/Structures/OrdersAlt.v - COQC theories/Structures/OrderedTypeAlt.v - COQC theories/FSets/FSetInterface.v - COQC theories/FSets/FMapInterface.v - COQC theories/FSets/FMapWeakList.v - COQC theories/FSets/FMapList.v - COQC theories/FSets/FSetBridge.v - COQC theories/setoid_ring/Ring_polynom.v - COQC theories/ZArith/Zeven.v - COQC theories/ZArith/Zcompare.v - COQC theories/ZArith/Znat.v - COQC theories/ZArith/Zpow_def.v - COQC theories/micromega/Env.v - COQC theories/Numbers/Cyclic/Abstract/DoubleType.v - COQC theories/ZArith/Zpow_alt.v - COQC theories/ZArith/Zeuclid.v - COQC theories/ZArith/Int.v - COQC theories/Numbers/Integer/Binary/ZBinary.v - COQC theories/Structures/OrdersLists.v - COQC theories/micromega/EnvRing.v - COQC theories/ZArith/Zorder.v - COQC theories/MSets/MSetWeakList.v - COQC theories/MSets/MSetList.v - COQC theories/omega/OmegaLemmas.v - COQC theories/ZArith/ZArith_dec.v - COQC theories/ZArith/Zminmax.v - COQC theories/ZArith/Zmin.v - COQC theories/ZArith/Zmax.v - COQC theories/ZArith/auxiliary.v - COQC theories/ZArith/Zmisc.v - COQC theories/ZArith/Wf_Z.v - COQC theories/ZArith/Zbool.v - COQC theories/ZArith/Zabs.v - COQC theories/ZArith/Zhints.v - COQC theories/ZArith/ZArith_base.v - COQC theories/setoid_ring/Ncring.v - COQC theories/micromega/VarMap.v - COQC theories/setoid_ring/InitialRing.v - COQC theories/setoid_ring/Ncring_polynom.v - COQC theories/setoid_ring/Ring_tac.v - COQC theories/setoid_ring/Ring_base.v - COQC theories/setoid_ring/Ring.v - COQC theories/setoid_ring/ZArithRing.v - COQC theories/setoid_ring/ArithRing.v - COQC theories/micromega/OrderedRing.v - COQC theories/setoid_ring/NArithRing.v - COQC theories/setoid_ring/Field_theory.v - COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v - COQC theories/Arith/Arith.v - COQC theories/ZArith/Zcomplements.v - COQC theories/micromega/Ztac.v - COQC theories/QArith/QArith_base.v - COQC theories/micromega/ZifyInst.v - COQC theories/Logic/ConstructiveEpsilon.v - COQC theories/extraction/ExtrOcamlNatInt.v - COQC theories/extraction/ExtrOcamlNatBigInt.v - COQC theories/extraction/ExtrHaskellNatNum.v - COQC theories/Bool/Zerob.v - COQC theories/MSets/MSetGenTree.v - COQC theories/Logic/WKL.v - COQC theories/Logic/ChoiceFacts.v - COQC theories/Classes/SetoidDec.v - COQC theories/Strings/Ascii.v - COQC theories/ZArith/Zdiv.v - COQC theories/ZArith/Zpower.v - COQC theories/extraction/ExtrHaskellNatInteger.v - COQC theories/extraction/ExtrHaskellNatInt.v - COQC theories/micromega/Zify.v - COQC theories/micromega/ZifyPow.v - COQC theories/omega/PreOmega.v - COQC theories/ZArith/Znumtheory.v - COQC theories/micromega/ZifyNat.v - COQC theories/micromega/ZifyN.v - COQC theories/micromega/DeclConstant.v - COQC theories/QArith/QOrderedType.v - COQC theories/QArith/Qminmax.v - COQC theories/Logic/ClassicalChoice.v - COQC theories/Logic/IndefiniteDescription.v - COQC theories/Logic/Epsilon.v - COQC theories/Logic/Diaconescu.v - COQC theories/Logic/Description.v - COQC theories/Logic/ClassicalEpsilon.v - COQC theories/Logic/SetoidChoice.v - COQC theories/Logic/ClassicalDescription.v - COQC theories/Strings/String.v - COQC theories/MSets/MSetAVL.v - COQC theories/MSets/MSetRBT.v - COQC theories/Strings/ByteVector.v - COQC theories/extraction/ExtrOcamlChar.v - COQC theories/extraction/ExtrHaskellString.v - COQC theories/Structures/OrdersEx.v - COQC theories/Strings/OctalString.v - COQC theories/Strings/HexString.v - COQC theories/Strings/BinaryString.v - COQC theories/Numbers/HexadecimalString.v - COQC theories/Numbers/DecimalString.v - COQC theories/extraction/ExtrOcamlString.v - COQC theories/extraction/ExtrOcamlNativeString.v - COQC theories/NArith/Ndigits.v - COQC theories/QArith/Qreduction.v - COQC theories/NArith/NArith.v - COQC theories/NArith/Ndec.v - COQC theories/NArith/Ndist.v - COQC theories/MSets/MSetPositive.v - COQC theories/micromega/RingMicromega.v - COQC theories/Structures/OrderedTypeEx.v - COQC theories/setoid_ring/Field_tac.v - COQC theories/setoid_ring/Field.v - COQC theories/Structures/DecidableTypeEx.v - COQC theories/FSets/FSetPositive.v - COQC theories/QArith/Qfield.v - COQC theories/MSets/MSetFacts.v - COQC theories/FSets/FSetFacts.v - COQC theories/FSets/FMapFacts.v - COQC theories/micromega/ZCoeff.v - COQC theories/QArith/Qring.v - COQC theories/QArith/QArith.v - COQC theories/micromega/ZMicromega.v - COQC theories/QArith/Qabs.v - COQC theories/QArith/Qround.v - COQC theories/micromega/QMicromega.v - COQC theories/QArith/Qcanon.v - COQC theories/FSets/FSetDecide.v - COQC theories/Reals/Abstract/ConstructiveReals.v - COQC theories/micromega/Lqa.v - COQC theories/MSets/MSetDecide.v - COQC theories/FSets/FSetCompat.v - COQC theories/QArith/Qcabs.v - COQC theories/FSets/FSetWeakList.v - COQC theories/FSets/FSetList.v - COQC theories/FSets/FSetProperties.v - COQC theories/micromega/Lia.v - COQC theories/MSets/MSetProperties.v - COQC theories/micromega/ZArith_hints.v - COQC theories/ZArith/Zpow_facts.v - COQC theories/ZArith/Zgcd_alt.v - COQC theories/ZArith/Zwf.v - COQC theories/ZArith/Zquot.v - COQC theories/Sorting/PermutSetoid.v - COQC theories/Arith/Cantor.v - COQC theories/ZArith/ZArith.v - COQC theories/QArith/Qpower.v - COQC theories/Reals/Cauchy/PosExtra.v - COQC theories/Reals/Cauchy/ConstructiveExtra.v - COQC theories/micromega/ZifyBool.v - COQC theories/micromega/ZifyComparison.v - COQC theories/extraction/ExtrOcamlZInt.v - COQC theories/extraction/ExtrOcamlZBigInt.v - COQC theories/extraction/ExtrOcamlIntConv.v - COQC theories/Floats/SpecFloat.v - COQC theories/extraction/ExtrHaskellZNum.v - COQC theories/Classes/DecidableClass.v - COQC theories/ZArith/Zdigits.v - COQC theories/Numbers/HexadecimalFacts.v - COQC theories/Numbers/DecimalFacts.v - COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v - COQC theories/Numbers/Cyclic/Int31/Int31.v - COQC theories/FSets/FSetAVL.v - COQC theories/FSets/FMapPositive.v - COQC theories/FSets/FMapAVL.v - COQC theories/Numbers/Cyclic/Int63/Uint63.v - COQC theories/Sorting/PermutEq.v - COQC theories/Sorting/Heap.v - COQC theories/extraction/ExtrHaskellZInteger.v - COQC theories/extraction/ExtrHaskellZInt.v - COQC theories/btauto/Algebra.v - COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v - COQC theories/Numbers/Cyclic/Int31/Cyclic31.v - COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v - COQC theories/Reals/Abstract/ConstructiveAbs.v - COQC theories/Reals/Cauchy/QExtra.v - COQC theories/Reals/Cauchy/ConstructiveCauchyReals.v - COQC theories/FSets/FMaps.v - COQC theories/btauto/Reflect.v - COQC theories/FSets/FSetEqProperties.v - COQC theories/FSets/FSetToFiniteSet.v - COQC theories/btauto/Btauto.v - COQC theories/Reals/Abstract/ConstructiveLimits.v - COQC theories/MSets/MSetToFiniteSet.v - COQC theories/Numbers/DecimalPos.v - COQC theories/Numbers/DecimalNat.v - COQC theories/MSets/MSetEqProperties.v - COQC theories/FSets/FSets.v - COQC theories/Numbers/DecimalN.v - COQC theories/MSets/MSets.v - COQC theories/Numbers/DecimalZ.v - COQC theories/setoid_ring/Ncring_initial.v - COQC theories/Numbers/DecimalQ.v - COQC theories/micromega/ZifyUint63.v - COQC theories/Numbers/Cyclic/Int63/Sint63.v - COQC theories/Array/PArray.v - COQC theories/Floats/FloatOps.v - COQC theories/Numbers/Cyclic/Int63/Cyclic63.v - COQC theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v - COQC theories/Numbers/HexadecimalPos.v - COQC theories/Numbers/HexadecimalNat.v - COQC theories/Floats/FloatAxioms.v - COQC theories/extraction/ExtrOCamlPArray.v - COQC theories/Numbers/Cyclic/Int31/Ring31.v - COQC theories/Reals/Abstract/ConstructiveLUB.v - COQC theories/Reals/Abstract/ConstructiveRealsMorphisms.v - COQC theories/Numbers/Cyclic/Int63/Ring63.v - COQC theories/micromega/ZifySint63.v - COQC theories/extraction/ExtrOCamlInt63.v - COQC theories/Reals/Abstract/ConstructiveSum.v - COQC theories/Reals/Abstract/ConstructiveMinMax.v - COQC theories/Reals/Abstract/ConstructivePower.v - COQC theories/setoid_ring/Ncring_tac.v - COQC theories/FSets/FMapFullAVL.v - COQC theories/Numbers/HexadecimalN.v - COQC theories/Numbers/HexadecimalZ.v - COQC theories/setoid_ring/Cring.v - COQC theories/Reals/Cauchy/ConstructiveCauchyAbs.v - COQC theories/Numbers/HexadecimalQ.v - COQC theories/setoid_ring/Integral_domain.v - COQC theories/setoid_ring/Rings_Z.v - COQC theories/setoid_ring/Rings_Q.v - COQC theories/nsatz/NsatzTactic.v - COQC theories/Reals/Cauchy/ConstructiveRcomplete.v - COQC theories/Reals/ClassicalDedekindReals.v - COQC theories/Reals/Rdefinitions.v - COQC theories/Reals/Raxioms.v - COQC theories/Reals/Rpow_def.v - COQC theories/Numbers/HexadecimalR.v - COQC theories/Numbers/DecimalR.v - COQC theories/setoid_ring/RealField.v - COQC theories/Reals/ClassicalConstructiveReals.v - COQC theories/Reals/RIneq.v - COQC theories/Reals/DiscrR.v - COQC theories/Reals/R_Ifp.v - COQC theories/Reals/SplitRmult.v - COQC theories/QArith/Qreals.v - COQC theories/Reals/Rlogic.v - COQC theories/Reals/Rbase.v - COQC theories/Reals/ROrderedType.v - COQC theories/Reals/Rbasic_fun.v - COQC theories/Reals/R_sqr.v - COQC theories/Reals/SplitAbsolu.v - COQC theories/Reals/ArithProp.v - COQC theories/Reals/Rminmax.v - COQC theories/Reals/Rfunctions.v - COQC theories/Reals/Rseries.v - COQC theories/micromega/RMicromega.v - COQC theories/Reals/Rregisternames.v - COQC theories/Reals/RList.v - COQC theories/Reals/Runcountable.v - COQC theories/Reals/SeqProp.v - COQC theories/micromega/Lra.v - COQC theories/micromega/MExtraction.v - COQC theories/Reals/Rlimit.v - COQC theories/micromega/Fourier_util.v - COQC theories/micromega/Psatz.v - COQC theories/micromega/Fourier.v - COQC theories/Reals/Rcomplete.v - COQC theories/Floats/FloatLemmas.v - COQC theories/Reals/Rderiv.v - COQC theories/Reals/PartSum.v - COQC theories/Reals/Ranalysis1.v - COQC theories/Floats/Floats.v - COQC theories/Reals/AltSeries.v - COQC theories/Reals/Binomial.v - COQC theories/Reals/Rsigma.v - COQC theories/Reals/Cauchy_prod.v - COQC theories/Reals/Alembert.v - COQC theories/extraction/ExtrOCamlFloats.v - COQC theories/Reals/Rtopology.v - COQC theories/Reals/Ranalysis2.v - COQC theories/Reals/Rprod.v - COQC theories/Reals/Ranalysis3.v - COQC theories/Reals/SeqSeries.v - COQC theories/Reals/MVT.v - COQC theories/Reals/Rtrigo_fun.v - COQC theories/Reals/Rsqrt_def.v - COQC theories/Reals/PSeries_reg.v - COQC theories/Reals/Rtrigo_def.v - COQC theories/Reals/R_sqrt.v - COQC theories/Reals/Rtrigo_alt.v - COQC theories/Reals/Cos_rel.v - COQC theories/Reals/Sqrt_reg.v - COQC theories/Reals/Cos_plus.v - COQC theories/Reals/Rtrigo1.v - COQC theories/Reals/Exp_prop.v - COQC theories/Reals/Rtrigo_reg.v - COQC theories/Reals/Rtrigo_calc.v - COQC theories/Reals/Rgeom.v - COQC theories/Reals/Ranalysis4.v - COQC theories/Reals/Rpower.v - COQC theories/Reals/Ranalysis_reg.v - COQC theories/Reals/Rtrigo_facts.v - COQC theories/Reals/RiemannInt_SF.v - COQC theories/Reals/RiemannInt.v - COQC theories/Reals/Ranalysis5.v - COQC theories/Reals/Ratan.v - COQC theories/Reals/Machin.v - COQC theories/Reals/Rtrigo.v - COQC theories/Reals/Ranalysis.v - COQC theories/Reals/NewtonInt.v - COQC theories/Reals/Integration.v - COQC theories/Reals/Reals.v - COQC theories/setoid_ring/Rings_R.v - COQC theories/nsatz/Nsatz.v - make[1]: Leaving directory '/home/opam/.opam/4.14/.opam-switch/build/coq.8.16.1' -> compiled coq.8.16.1 Processing 83/87: [coq: make install] + /usr/bin/make "COQ_USE_DUNE=" "install" (CWD=/home/opam/.opam/4.14/.opam-switch/build/coq.8.16.1) - /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build install - make[1]: Entering directory '/home/opam/.opam/4.14/.opam-switch/build/coq.8.16.1' - DUNE sources - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - dune install --display=quiet --release --mandir=""/home/opam/.opam/4.14/man"" --prefix=""/home/opam/.opam/4.14"" --etcdir=""/home/opam/.opam/4.14/lib/coq/config"" --docdir=""/home/opam/.opam/4.14/doc/coq"" coq-core - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - dune install --display=quiet --release --mandir=""/home/opam/.opam/4.14/man"" --prefix=""/home/opam/.opam/4.14"" --etcdir=""/home/opam/.opam/4.14/lib/coq/config"" --docdir=""/home/opam/.opam/4.14/doc/coq"" coqide-server - Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune - 3.8 and will be removed in an upcoming Dune version. - Hint: To disable this warning, add the following to your dune-project file: - (warnings (deprecated_coq_lang_lt_08 disabled)) - INSTALL VOFILES - make[1]: Leaving directory '/home/opam/.opam/4.14/.opam-switch/build/coq.8.16.1' -> installed coq.8.16.1 Processing 84/87: [coq-serapi: dune build] + /home/opam/.opam/4.14/bin/dune "build" "-p" "coq-serapi" "-j" "255" (CWD=/home/opam/.opam/4.14/.opam-switch/build/coq-serapi.8.16.0+0.16.3) -> compiled coq-serapi.8.16.0+0.16.3 -> installed coq-serapi.8.16.0+0.16.3 Processing 86/87: [coq-lsp: dune build] + /home/opam/.opam/4.14/bin/dune "build" "-p" "coq-lsp" "-j" "255" (CWD=/home/opam/.opam/4.14/.opam-switch/build/coq-lsp.0.1.3+v8.16) -> compiled coq-lsp.0.1.3+v8.16 -> installed coq-lsp.0.1.3+v8.16 Done. # Run eval $(opam env) to update the current shell environment 2024-01-29 18:47.46 ---> saved as "4c2bdaf094ce557842c6b70fde72613ae96ea73dd45958cd83d2fb94d21ee42b" /home/opam: (run (shell "opam exec -- ~/voodoo-prep -u coq-lsp:8d2b270a4ae7c5bd7b16c79259f1b7a9")) 2024-01-29 18:47.48 ---> saved as "3eb2c2293c261571e1ee490e8885d72162fd7d4ff5929b59c0f0dc932216a512" /home/opam: (run (network host) (secrets (ssh_privkey (target /home/opam/.ssh/id_rsa)) (ssh_pubkey (target /home/opam/.ssh/id_rsa.pub)) (ssh_config (target /home/opam/.ssh/config))) (shell "(echo '0.242925') && (for DATA in prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16,coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9,coq-lsp.0.1.3+v8.16; do IFS=\",\"; set -- $DATA; ([ -d $1 ] || (echo \"FAILED:$2\" && mkdir -p $1 && cp ~/opam.err.log $1 && opam show $3 --raw > $1/opam)) && (shopt -s nullglob && ((tar -cvf $1.tar $1/* && rm -R $1/* && mv $1.tar $1/content.tar) || (echo 'Empty directory'))) done) && (for DATA in prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16,coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9,coq-lsp.0.1.3+v8.16; do IFS=\",\"; set -- $DATA; rsync -aR --no-p ./$1 docs.ci.ocaml.org:/data/.; done) && (for DATA in prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16,coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9,coq-lsp.0.1.3+v8.16; do IFS=\",\"; set -- $DATA; HASH=$((sha256sum $1/content.tar | cut -d \" \" -f 1) || echo -n 'empty'); printf \"HASHES:$2:$HASH\\n\"; done)")) 0.242925 prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/doc/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/doc/coq-lsp/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/doc/coq-lsp/CHANGES.md prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/doc/coq-lsp/LICENSE prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/doc/coq-lsp/README.md prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/META prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq.ocamlobjinfo prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Ast.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Ast.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Ast.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Goals.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Goals.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Goals.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Init.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Init.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Init.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Interp.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Interp.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Interp.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Loader.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Loader.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Loader.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Message.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Message.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Message.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Parsing.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Parsing.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Parsing.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Print.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Print.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Print.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Protect.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Protect.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Protect.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__State.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__State.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__State.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Workspace.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Workspace.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/coq/coq__Workspace.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/dune-package prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche.ocamlobjinfo prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Config.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Config.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Debug.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Debug.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Doc.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Doc.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Doc.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Info.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Info.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Info.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Io.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Io.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Io.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Memo.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Memo.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Memo.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Stats.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Stats.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Stats.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Types.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Types.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/fleche/fleche__Types.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/ prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp.ocamlobjinfo prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp__Base.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp__Base.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp__Base.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp__Io.cmi prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp__Io.cmt prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/lib/coq-lsp/lsp/lsp__Io.cmti prep/universes/8d2b270a4ae7c5bd7b16c79259f1b7a9/coq-lsp/0.1.3+v8.16/opam Warning: Permanently added '[docs.ci.ocaml.org]:2222' (ED25519) to the list of known hosts. HASHES:coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9:6055a5d3dbadcefef6445831be1d2a83f1a627ec10887e0c17fba756ed30145c 2024-01-29 18:47.49 ---> saved as "f1133455d3decad79a6aac2d69b22a7eca9a449b73d1dcea1bb552ef6fbfefd1" Job succeeded 2024-01-29 18:53.18: coq-lsp.0.1.3+v8.16-8d2b270a4ae7c5bd7b16c79259f1b7a9 -> 6055a5d3dbadcefef6445831be1d2a83f1a627ec10887e0c17fba756ed30145c 2024-01-29 18:53.18: Job succeeded