Build:
- 0
2026-06-24 11:28.34: New job: build coq-core.8.17.0 (6b58e3f58ed8)
2026-06-24 11:28.34: Waiting for resource in pool day11-builds
2026-06-24 12:16.09: Got resource from pool day11-builds
2026-06-24 12:16.09: [profile full] build coq-core.8.17.0
2026-06-24 12:16.09: build coq-core.8.17.0 (6b58e3f58ed8)
=== DEPENDENCIES (11 transitive) ===
base-threads.base c9e7bdbf5823
base-unix.base 7d1428be9ddb
compiler-cloning.enabled 439a1fc77aa6
conf-gmp.5 be11edf77089
conf-pkg-config.5 d5de2c6a88f9
dune.3.23.1 a59dd9b14fe3
ocaml.5.5.0 383268832c4b
ocaml-base-compiler.5.5.0 522c248944c8
ocaml-compiler.5.5.0 eb1a8babf54c
ocamlfind.1.9.8 b506a15fcd6c
zarith.1.14 c48bd7ff5430
=== STDOUT ===
Processing: [default: loading data]
[coq-core.8.17.0: dl]
[coq-core.8.17.0: extract]
-> retrieved coq-core.8.17.0 (https://opam.ocaml.org/cache)
[coq-core: ./configure no]
+ /home/opam/.opam/default/.opam-switch/build/coq-core.8.17.0/./configure "-prefix" "/home/opam/.opam/default" "-mandir" "/home/opam/.opam/default/man" "-libdir" "/home/opam/.opam/default/lib/coq" "-native-compiler" "no" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-core.8.17.0)
- ocamlfind: [WARNING] Cannot read directory ../stublibs which is mentioned in ld.conf
- ocamlfind: [WARNING] Cannot read directory ./stublibs which is mentioned in ld.conf
- You have OCaml 5.5.0. Good!
- You have OCamlfind 1.9.8. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.14 installed. Good!
-
- Architecture : Linux
- Sys.os_type : Unix
- OCaml version : 5.5.0
- OCaml binaries in : /home/opam/.opam/default/bin/
- OCaml library in : /home/opam/.opam/default/lib/ocaml
- 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 where installation is expected by Coq Makefile:
- - Coq is expected in /home/opam/.opam/default
- - the Coq library is expected in /home/opam/.opam/default/lib/coq
- - the Coqide configuration files is expected in /home/opam/.opam/default/etc/xdg/coq
- - the Coqide data files is expected in /home/opam/.opam/default/share/coq
- - the Coq man pages is expected in /home/opam/.opam/default/man
- - documentation prefix path for all Coq packages is expected in /home/opam/.opam/default/share/doc
-
- 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'.
[coq-core: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "coq-core" "-j" "39" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/coq-core.8.17.0)
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/float64.cmi -c -intf kernel/float64.mli)
- File "kernel/float64.mli", line 60, characters 3-15:
- 60 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 66, characters 3-15:
- 66 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 80, characters 3-15:
- 80 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 83, characters 3-15:
- 83 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 89, characters 3-15:
- 89 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 92, characters 3-15:
- 92 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 101, characters 3-15:
- 101 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64.mli", line 109, characters 3-15:
- 109 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/float64_common.cmi -c -intf kernel/float64_common.mli)
- File "kernel/float64_common.mli", line 60, characters 3-15:
- 60 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 66, characters 3-15:
- 66 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 70, characters 3-15:
- 70 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 73, characters 3-15:
- 73 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 79, characters 3-15:
- 79 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 82, characters 3-15:
- 82 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 91, characters 3-15:
- 91 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/float64_common.mli", line 99, characters 3-15:
- 99 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -cmi-file kernel/.kernel.objs/byte/uGraph.cmi -no-alias-deps -o kernel/.kernel.objs/byte/uGraph.cmo -c -impl kernel/uGraph.ml)
- File "kernel/uGraph.ml", line 22, characters 10-17:
- 22 | end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *)
- ^^^^^^^
- Warning 53 [misplaced-attribute]: the inlined attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I kernel/.kernel.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -no-alias-deps -o kernel/.kernel.objs/byte/nativevalues.cmi -c -intf kernel/nativevalues.mli)
- File "kernel/nativevalues.mli", line 104, characters 3-15:
- 104 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 107, characters 3-15:
- 107 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 110, characters 3-15:
- 110 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 113, characters 3-15:
- 113 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 124, characters 3-15:
- 124 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 148, characters 3-15:
- 148 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 192, characters 3-15:
- 192 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 195, characters 3-15:
- 195 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 198, characters 3-15:
- 198 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 201, characters 3-15:
- 201 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 204, characters 3-15:
- 204 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 207, characters 3-15:
- 207 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 210, characters 3-15:
- 210 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 213, characters 3-15:
- 213 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 216, characters 3-15:
- 216 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 219, characters 3-15:
- 219 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 222, characters 3-15:
- 222 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 225, characters 3-15:
- 225 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 228, characters 3-15:
- 228 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 231, characters 3-15:
- 231 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 234, characters 3-15:
- 234 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 237, characters 3-15:
- 237 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 240, characters 3-15:
- 240 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 243, characters 3-15:
- 243 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 246, characters 3-15:
- 246 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 249, characters 3-15:
- 249 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 252, characters 3-15:
- 252 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 255, characters 3-15:
- 255 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 258, characters 3-15:
- 258 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 261, characters 3-15:
- 261 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 264, characters 3-15:
- 264 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 267, characters 3-15:
- 267 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 270, characters 3-15:
- 270 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 273, characters 3-15:
- 273 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 282, characters 3-15:
- 282 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 306, characters 3-15:
- 306 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 309, characters 3-15:
- 309 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 312, characters 3-15:
- 312 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 315, characters 3-15:
- 315 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 318, characters 3-15:
- 318 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 321, characters 3-15:
- 321 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 324, characters 3-15:
- 324 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 327, characters 3-15:
- 327 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 330, characters 3-15:
- 330 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 333, characters 3-15:
- 333 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 336, characters 3-15:
- 336 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 339, characters 3-15:
- 339 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 342, characters 3-15:
- 342 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 345, characters 3-15:
- 345 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 348, characters 3-15:
- 348 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 351, characters 3-15:
- 351 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 354, characters 3-15:
- 354 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 357, characters 3-15:
- 357 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 360, characters 3-15:
- 360 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 375, characters 3-15:
- 375 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 378, characters 3-15:
- 378 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 381, characters 3-15:
- 381 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 384, characters 3-15:
- 384 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 387, characters 3-15:
- 387 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
-
- File "kernel/nativevalues.mli", line 390, characters 3-15:
- 390 | [@@ocaml.inline always]
- ^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.inline attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -cmi-file gramlib/.gramlib.objs/byte/gramlib__Grammar.cmi -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Grammar.cmo -c -impl gramlib/grammar.ml)
- File "gramlib/grammar.ml", lines 323-324, characters 7-48:
- 323 | .......let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in
- 324 | Belast (NoRec2, TNext (NoRec2, r, s), s')
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Belast (MayRec2, TStop, Stoken _)
-
- File "gramlib/grammar.ml", lines 319-327, characters 18-50:
- 319 | ..................match ar, r with
- 320 | | NoRec2, TStop -> Belast (NoRec2, TStop, s)
- 321 | | MayRec2, TStop -> Belast (MayRec2, TStop, s)
- 322 | | NoRec2, TNext (NoRec2, r, s') ->
- 323 | let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in
- 324 | Belast (NoRec2, TNext (NoRec2, r, s), s')
- 325 | | MayRec2, TNext (_, r, s') ->
- 326 | let Belast (_, r, s') = belast_rule MayRec2 r s' in
- 327 | Belast (MayRec2, TNext (MayRec2, r, s), s')...
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NoRec2, TNext (MayRec2, _, _))
-
- File "gramlib/grammar.ml", lines 331-333, characters 5-41:
- 331 | .....let Belast (MayRec2, r, s) = belast_rule MayRec2 r s in
- 332 | let AnyS (r, pf) = get_symbols r in
- 333 | AnyS (TCns (MayRec2, s, r), RelS pf)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Belast (NoRec2, TStop, Stoken _)
-
- File "gramlib/grammar.ml", lines 335-337, characters 5-40:
- 335 | .....let Belast (NoRec2, r, s) = belast_rule NoRec2 r s in
- 336 | let AnyS (r, pf) = get_symbols r in
- 337 | AnyS (TCns (NoRec2, s, r), RelS pf)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Belast (MayRec2, TStop, Stoken _)
-
- File "gramlib/grammar.ml", lines 353-355, characters 2-35:
- 353 | ..match ar, arn, get_rec_tree t with
- 354 | | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2
- 355 | | NoRec2, NoRec3, NoRec -> NoRec2
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NoRec2, NoRec3, MayRec)
-
- File "gramlib/grammar.ml", lines 370-384, characters 8-46:
- 370 | ........match ar, tree with
- 371 | | NR10, Node (_, n) -> Node (MayRec3, node n)
- 372 | | NR11, Node (NoRec3, n) -> Node (NoRec3, node n)
- 373 | | NR11, LocAct (old_action, action_list) ->
- 374 | (* What to do about this warning? For now it is disabled *)
- ...
- 381 | Feedback.msg_warning (Pp.str msg)
- 382 | end;
- 383 | LocAct (action, old_action :: action_list)
- 384 | | NR11, DeadEnd -> LocAct (action, [])
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NR10, DeadEnd)
-
- File "gramlib/grammar.ml", lines 394-397, characters 7-58:
- 394 | .......match ar, ars, get_rec_symbols sl with
- 395 | | MayRec2, MayRec2, MayRec -> Node (MayRec3, node NR01)
- 396 | | MayRec2, _, NoRec -> Node (MayRec3, node NR11)
- 397 | | NoRec2, NoRec2, NoRec -> Node (NoRec3, node NR11)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (MayRec2, NoRec2, MayRec)
-
- File "gramlib/grammar.ml", lines 410-412, characters 10-74:
- 410 | ..........begin match ar, ars, arn, arss with
- 411 | | MayRec2, _, _, _ -> Some (Node (MayRec3, node))
- 412 | | NoRec2, NoRec2, NoRec3, NR11 -> Some (Node (NoRec3, node)) end
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NoRec2, NoRec2, NoRec3, NR00)
-
- File "gramlib/grammar.ml", lines 428-430, characters 16-69:
- 428 | ................match ar, ars, arn, arss with
- 429 | | MayRec2, _, _, _ -> Node (MayRec3, node)
- 430 | | NoRec2, NoRec2, NoRec3, NR11 -> Node (NoRec3, node)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NoRec2, NoRec2, NoRec3, NR00)
-
- File "gramlib/grammar.ml", lines 434-436, characters 10-58:
- 434 | ..........match ar, arn with
- 435 | | MayRec2, _ -> Some (Node (MayRec3, node))
- 436 | | NoRec2, NoRec3 -> Some (Node (NoRec3, node))
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NoRec2, MayRec3)
-
- File "gramlib/grammar.ml", lines 443-445, characters 14-66:
- 443 | ..............begin match ar, arn with
- 444 | | MayRec2, _ -> Some (Node (MayRec3, node))
- 445 | | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) end
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NoRec2, MayRec3)
-
- File "gramlib/grammar.ml", lines 463-467, characters 4-24:
- 463 | ....function
- 464 | | Node (NoRec3, {node = s; son = son; brother = bro}) ->
- 465 | Node (NoRec3, {node = retype_symbol s; son = retype_tree son; brother = retype_tree bro})
- 466 | | LocAct (k, kl) -> LocAct (k, kl)
- 467 | | DeadEnd -> DeadEnd
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Node (MayRec3, _)
-
- File "gramlib/grammar.ml", lines 469-479, characters 4-38:
- 469 | ....function
- 470 | | Stoken p -> Stoken p
- 471 | | Stokens l -> Stokens l
- 472 | | Slist1 s -> Slist1 (retype_symbol s)
- 473 | | Slist1sep (s, sep, b) -> Slist1sep (retype_symbol s, retype_symbol sep, b)
- ...
- 476 | | Sopt s -> Sopt (retype_symbol s)
- 477 | | Snterm e -> Snterm e
- 478 | | Snterml (e, l) -> Snterml (e, l)
- 479 | | Stree t -> Stree (retype_tree t)...
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Sself
-
- File "gramlib/grammar.ml", lines 481-483, characters 4-76:
- 481 | ....function
- 482 | | TStop -> TStop
- 483 | | TNext (NoRec2, r, s) -> TNext (NoRec2, retype_rule r, retype_symbol s)...
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: TNext (MayRec2, _, _)
- (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -fPIC -pthread -D_FILE_OFFSET_BITS=64 -O2 -fno-strict-aliasing -fwrapv -fPIC -pthread -Wall -Wno-unused -g -O2 -msse2 -mfpmath=sse -g -I /home/opam/.opam/default/lib/ocaml -o coq_interp.o -c coq_interp.c)
- coq_interp.c: In function 'coq_interprete':
- coq_interp.c:817:11: warning: assignment discards 'volatile' qualifier from pointer target type [-Wdiscarded-qualifiers]
- 817 | p = &Field(accu, 0);
- | ^
- coq_interp.c:305:20: warning: storing the address of local variable 'coq_lbl_ACC0' in 'coq_instr_base' [-Wdangling-pointer=]
- 305 | 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:329:7: note: in expansion of macro 'Instruct'
- 329 | 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/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -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 -cmi-file gramlib/.gramlib.objs/byte/gramlib__Grammar.cmi -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/native/gramlib__Grammar.cmx -c -impl gramlib/grammar.ml)
- File "gramlib/grammar.ml", lines 323-324, characters 7-48:
- 323 | .......let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in
- 324 | Belast (NoRec2, TNext (NoRec2, r, s), s')
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Belast (MayRec2, TStop, Stoken _)
-
- File "gramlib/grammar.ml", lines 319-327, characters 18-50:
- 319 | ..................match ar, r with
- 320 | | NoRec2, TStop -> Belast (NoRec2, TStop, s)
- 321 | | MayRec2, TStop -> Belast (MayRec2, TStop, s)
- 322 | | NoRec2, TNext (NoRec2, r, s') ->
- 323 | let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in
- 324 | Belast (NoRec2, TNext (NoRec2, r, s), s')
- 325 | | MayRec2, TNext (_, r, s') ->
- 326 | let Belast (_, r, s') = belast_rule MayRec2 r s' in
- 327 | Belast (MayRec2, TNext (MayRec2, r, s), s')...
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NoRec2, TNext (MayRec2, _, _))
-
- File "gramlib/grammar.ml", lines 331-333, characters 5-41:
- 331 | .....let Belast (MayRec2, r, s) = belast_rule MayRec2 r s in
- 332 | let AnyS (r, pf) = get_symbols r in
- 333 | AnyS (TCns (MayRec2, s, r), RelS pf)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Belast (NoRec2, TStop, Stoken _)
-
- File "gramlib/grammar.ml", lines 335-337, characters 5-40:
- 335 | .....let Belast (NoRec2, r, s) = belast_rule NoRec2 r s in
- 336 | let AnyS (r, pf) = get_symbols r in
- 337 | AnyS (TCns (NoRec2, s, r), RelS pf)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Belast (MayRec2, TStop, Stoken _)
-
- File "gramlib/grammar.ml", lines 353-355, characters 2-35:
- 353 | ..match ar, arn, get_rec_tree t with
- 354 | | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2
- 355 | | NoRec2, NoRec3, NoRec -> NoRec2
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NoRec2, NoRec3, MayRec)
-
- File "gramlib/grammar.ml", lines 370-384, characters 8-46:
- 370 | ........match ar, tree with
- 371 | | NR10, Node (_, n) -> Node (MayRec3, node n)
- 372 | | NR11, Node (NoRec3, n) -> Node (NoRec3, node n)
- 373 | | NR11, LocAct (old_action, action_list) ->
- 374 | (* What to do about this warning? For now it is disabled *)
- ...
- 381 | Feedback.msg_warning (Pp.str msg)
- 382 | end;
- 383 | LocAct (action, old_action :: action_list)
- 384 | | NR11, DeadEnd -> LocAct (action, [])
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NR10, DeadEnd)
-
- File "gramlib/grammar.ml", lines 394-397, characters 7-58:
- 394 | .......match ar, ars, get_rec_symbols sl with
- 395 | | MayRec2, MayRec2, MayRec -> Node (MayRec3, node NR01)
- 396 | | MayRec2, _, NoRec -> Node (MayRec3, node NR11)
- 397 | | NoRec2, NoRec2, NoRec -> Node (NoRec3, node NR11)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (MayRec2, NoRec2, MayRec)
-
- File "gramlib/grammar.ml", lines 410-412, characters 10-74:
- 410 | ..........begin match ar, ars, arn, arss with
- 411 | | MayRec2, _, _, _ -> Some (Node (MayRec3, node))
- 412 | | NoRec2, NoRec2, NoRec3, NR11 -> Some (Node (NoRec3, node)) end
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NoRec2, NoRec2, NoRec3, NR00)
-
- File "gramlib/grammar.ml", lines 428-430, characters 16-69:
- 428 | ................match ar, ars, arn, arss with
- 429 | | MayRec2, _, _, _ -> Node (MayRec3, node)
- 430 | | NoRec2, NoRec2, NoRec3, NR11 -> Node (NoRec3, node)
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NoRec2, NoRec2, NoRec3, NR00)
-
- File "gramlib/grammar.ml", lines 434-436, characters 10-58:
- 434 | ..........match ar, arn with
- 435 | | MayRec2, _ -> Some (Node (MayRec3, node))
- 436 | | NoRec2, NoRec3 -> Some (Node (NoRec3, node))
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NoRec2, MayRec3)
-
- File "gramlib/grammar.ml", lines 443-445, characters 14-66:
- 443 | ..............begin match ar, arn with
- 444 | | MayRec2, _ -> Some (Node (MayRec3, node))
- 445 | | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) end
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: (NoRec2, MayRec3)
-
- File "gramlib/grammar.ml", lines 463-467, characters 4-24:
- 463 | ....function
- 464 | | Node (NoRec3, {node = s; son = son; brother = bro}) ->
- 465 | Node (NoRec3, {node = retype_symbol s; son = retype_tree son; brother = retype_tree bro})
- 466 | | LocAct (k, kl) -> LocAct (k, kl)
- 467 | | DeadEnd -> DeadEnd
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Node (MayRec3, _)
-
- File "gramlib/grammar.ml", lines 469-479, characters 4-38:
- 469 | ....function
- 470 | | Stoken p -> Stoken p
- 471 | | Stokens l -> Stokens l
- 472 | | Slist1 s -> Slist1 (retype_symbol s)
- 473 | | Slist1sep (s, sep, b) -> Slist1sep (retype_symbol s, retype_symbol sep, b)
- ...
- 476 | | Sopt s -> Sopt (retype_symbol s)
- 477 | | Snterm e -> Snterm e
- 478 | | Snterml (e, l) -> Snterml (e, l)
- 479 | | Stree t -> Stree (retype_tree t)...
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: Sself
-
- File "gramlib/grammar.ml", lines 481-483, characters 4-76:
- 481 | ....function
- 482 | | TStop -> TStop
- 483 | | TNext (NoRec2, r, s) -> TNext (NoRec2, retype_rule r, retype_symbol s)...
- Warning 8 [partial-match]: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched: TNext (MayRec2, _, _)
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I engine/.engine.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I boot/.boot.objs/byte -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -cmi-file engine/.engine.objs/byte/proofview_monad.cmi -no-alias-deps -o engine/.engine.objs/byte/proofview_monad.cmo -c -impl engine/proofview_monad.ml)
- File "engine/proofview_monad.ml", line 151, characters 31-41:
- 151 | module StateStore = Store.Make(struct end)
- ^^^^^^^^^^
- Warning 73 [generative-application-expects-unit]: A generative functor
- should be applied to (); using (struct end) is deprecated.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -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/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -cmi-file kernel/.kernel.objs/byte/uGraph.cmi -no-alias-deps -o kernel/.kernel.objs/native/uGraph.cmx -c -impl kernel/uGraph.ml)
- File "kernel/uGraph.ml", line 22, characters 10-17:
- 22 | end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *)
- ^^^^^^^
- Warning 53 [misplaced-attribute]: the inlined attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I pretyping/.pretyping.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -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 -cmi-file pretyping/.pretyping.objs/byte/inductiveops.cmi -no-alias-deps -o pretyping/.pretyping.objs/byte/inductiveops.cmo -c -impl pretyping/inductiveops.ml)
- File "pretyping/inductiveops.ml", line 119, characters 3-19:
- 119 | [@@ocaml.deprecated "Alias for Inductiveops.nconstructors"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 128, characters 3-19:
- 128 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 137, characters 3-19:
- 137 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 146, characters 3-19:
- 146 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 155, characters 3-19:
- 155 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 164, characters 3-19:
- 164 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 173, characters 3-19:
- 173 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 182, characters 3-19:
- 182 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 191, characters 3-19:
- 191 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 200, characters 3-19:
- 200 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 209, characters 3-19:
- 209 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 218, characters 3-19:
- 218 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 227, characters 3-19:
- 227 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 236, characters 3-19:
- 236 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 243, characters 3-19:
- 243 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I tactics/.tactics.objs/byte -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/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 -no-alias-deps -o tactics/.tactics.objs/byte/hints.cmi -c -intf tactics/hints.mli)
- File "tactics/hints.mli", line 200, characters 2-18:
- 200 | [@ocaml.deprecated "Declare a hint constant instead"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -bin-annot-occurrences -I plugins/ltac2/.ltac2_plugin.objs/byte -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/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 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 tools/coqworkmgr/.coqworkmgrapi.objs/byte -I vernac/.vernac.objs/byte -cmi-file plugins/ltac2/.ltac2_plugin.objs/byte/ltac2_plugin__Tac2dyn.cmi -no-alias-deps -open Ltac2_plugin -o plugins/ltac2/.ltac2_plugin.objs/byte/ltac2_plugin__Tac2dyn.cmo -c -impl plugins/ltac2/tac2dyn.ml)
- File "plugins/ltac2/tac2dyn.ml", line 13, characters 24-34:
- 13 | module DYN = Dyn.Make(struct end)
- ^^^^^^^^^^
- Warning 73 [generative-application-expects-unit]: A generative functor
- should be applied to (); using (struct end) is deprecated.
-
- File "plugins/ltac2/tac2dyn.ml", line 29, characters 22-32:
- 29 | module Val = Dyn.Make(struct end)
- ^^^^^^^^^^
- Warning 73 [generative-application-expects-unit]: A generative functor
- should be applied to (); using (struct end) is deprecated.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I engine/.engine.objs/byte -I engine/.engine.objs/native -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -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 -I library/.library.objs/byte -I library/.library.objs/native -cmi-file engine/.engine.objs/byte/proofview_monad.cmi -no-alias-deps -o engine/.engine.objs/native/proofview_monad.cmx -c -impl engine/proofview_monad.ml)
- File "engine/proofview_monad.ml", line 151, characters 31-41:
- 151 | module StateStore = Store.Make(struct end)
- ^^^^^^^^^^
- Warning 73 [generative-application-expects-unit]: A generative functor
- should be applied to (); using (struct end) is deprecated.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -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 -cmi-file pretyping/.pretyping.objs/byte/inductiveops.cmi -no-alias-deps -o pretyping/.pretyping.objs/native/inductiveops.cmx -c -impl pretyping/inductiveops.ml)
- File "pretyping/inductiveops.ml", line 119, characters 3-19:
- 119 | [@@ocaml.deprecated "Alias for Inductiveops.nconstructors"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 128, characters 3-19:
- 128 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 137, characters 3-19:
- 137 | [@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 146, characters 3-19:
- 146 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 155, characters 3-19:
- 155 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 164, characters 3-19:
- 164 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 173, characters 3-19:
- 173 | [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 182, characters 3-19:
- 182 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 191, characters 3-19:
- 191 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 200, characters 3-19:
- 200 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 209, characters 3-19:
- 209 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 218, characters 3-19:
- 218 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 227, characters 3-19:
- 227 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 236, characters 3-19:
- 236 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
-
- File "pretyping/inductiveops.ml", line 243, characters 3-19:
- 243 | [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
- ^^^^^^^^^^^^^^^^
- Warning 53 [misplaced-attribute]: the ocaml.deprecated attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -unbox-closures -I plugins/ltac2/.ltac2_plugin.objs/byte -I plugins/ltac2/.ltac2_plugin.objs/native -I /home/opam/.opam/default/lib/findlib -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/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 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 tools/coqworkmgr/.coqworkmgrapi.objs/byte -I tools/coqworkmgr/.coqworkmgrapi.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -cmi-file plugins/ltac2/.ltac2_plugin.objs/byte/ltac2_plugin__Tac2dyn.cmi -no-alias-deps -open Ltac2_plugin -o plugins/ltac2/.ltac2_plugin.objs/native/ltac2_plugin__Tac2dyn.cmx -c -impl plugins/ltac2/tac2dyn.ml)
- File "plugins/ltac2/tac2dyn.ml", line 13, characters 24-34:
- 13 | module DYN = Dyn.Make(struct end)
- ^^^^^^^^^^
- Warning 73 [generative-application-expects-unit]: A generative functor
- should be applied to (); using (struct end) is deprecated.
-
- File "plugins/ltac2/tac2dyn.ml", line 29, characters 22-32:
- 29 | module Val = Dyn.Make(struct end)
- ^^^^^^^^^^
- Warning 73 [generative-application-expects-unit]: A generative functor
- should be applied to (); using (struct end) is deprecated.
-> compiled coq-core.8.17.0
-> installed coq-core.8.17.0
[WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config
=== STDERR ===
2026-06-24 12:19.49: OK: build coq-core.8.17.0 (runc: 180.8s, disk: 60KB)
2026-06-24 12:19.49: Job succeeded