Ali Caglayan (Jul 19 2021 at 16:50): Ali Caglayan (Jul 19 2021 at 16:50):When I build with Makefile.dune I get this warning:
Warning 58 [no-cmx-file]: no cmx file was found in path for module Zarith_version, and its interface was not compiled with -opaque
How do we fix it?
Gaëtan Gilbert (Jul 19 2021 at 16:52):ocaml version, zarith version, dune version? how were they installed (opam?)?
Ali Caglayan (Jul 19 2021 at 16:53):zarith 1.12 Implements arithmetic and logical ope
dune 2.9.0 Fast, portable, and opinionated build
ocaml 4.12.0 The OCaml compiler (virtual package)
ocaml-option-flambda 1 Set OCaml to be compiled with flambda
all with opam
Gaëtan Gilbert (Jul 19 2021 at 16:55):is the warning located? what produces it?
Ali Caglayan (Jul 19 2021 at 16:58):This is where it appears in dune verbose:
Running[3093]: (cd _build/default && /mnt/sdd1/.opam/dev/bin/ocamlc.opt -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -g -bin-annot -I plugins/micromega/.micromega_plugin.objs/byte -I /mnt/sdd1/.opam/dev/lib/ocaml/threads -I /mnt/sdd1/.opam/dev/lib/zarith -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/public_cmi -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/public_cmi -I vernac/.vernac.objs/public_cmi -no-alias-deps -opaque -open Micromega_plugin -o plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Mutils.cmi -c -intf plugins/micromega/mutils.mli)
Output[3084]:
File "_none_", line 1:
Warning 58 [no-cmx-file]: no cmx file was found in path for module Zarith_version, and its interface was not compiled with -opaque
Whoops wrong one
Ali Caglayan (Jul 19 2021 at 16:59):Running[3084]: (cd _build/default && /mnt/sdd1/.opam/dev/bin/ocamlopt.opt -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -g -I plugins/micromega/.micromega_plugin.objs/byte -I plugins/micromega/.micromega_plugin.objs/native -I /mnt/sdd1/.opam/dev/lib/ocaml/threads -I /mnt/sdd1/.opam/dev/lib/zarith -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/native -I stm/.stm.objs/public_cmi -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/native -I tactics/.tactics.objs/public_cmi -I vernac/.vernac.objs/native -I vernac/.vernac.objs/public_cmi -intf-suffix .ml -no-alias-deps -opaque -open Micromega_plugin -o plugins/micromega/.micromega_plugin.objs/native/micromega_plugin__NumCompat.cmx -c -impl plugins/micromega/numCompat.ml)
So something is going on in plugins/micromega/numCompat.ml
Gaëtan Gilbert (Jul 19 2021 at 17:05):what does ocamlfind query zarith say and what files does the returned path contain?
Ali Caglayan (Jul 19 2021 at 17:06):/mnt/sdd1/.opam/dev/lib/zarith
Ali Caglayan (Jul 19 2021 at 17:06):which is correct
Ali Caglayan (Jul 19 2021 at 17:06):It's just my dev switch
Ali Caglayan (Jul 19 2021 at 17:07):big_int_Z.cmi libzarith.a q.cmx zarith.cmxa z.cmi
big_int_Z.cmti META q.mli zarith.cmxs z.cmti
big_int_Z.cmx q.cmi zarith.a zarith.h z.cmx
big_int_Z.mli q.cmti zarith.cma zarith_top.cma z.mli
drwxrwxr-x 2 ali ali 4096 Jul 6 17:05 .
drwxr-xr-x 29 ali ali 4096 Jul 14 15:22 ..
-rw-rw-r-- 1 ali ali 6945 Jul 6 17:05 big_int_Z.cmi
-rw-rw-r-- 1 ali ali 29076 Jul 6 17:05 big_int_Z.cmti
-rw-rw-r-- 1 ali ali 18930 Jul 6 17:05 big_int_Z.cmx
-rw-rw-r-- 1 ali ali 2730 Mar 3 09:00 big_int_Z.mli
-rw-rw-r-- 1 ali ali 101812 Jul 6 17:05 libzarith.a
-rw-rw-r-- 1 ali ali 414 Mar 3 09:00 META
-rw-rw-r-- 1 ali ali 7957 Jul 6 17:05 q.cmi
-rw-rw-r-- 1 ali ali 47803 Jul 6 17:05 q.cmti
-rw-rw-r-- 1 ali ali 65591 Jul 6 17:05 q.cmx
-rw-rw-r-- 1 ali ali 7306 Mar 3 09:00 q.mli
-rw-rw-r-- 1 ali ali 120434 Jul 6 17:05 zarith.a
-rw-rw-r-- 1 ali ali 27859 Jul 6 17:05 zarith.cma
-rw-rw-r-- 1 ali ali 1881 Jul 6 17:05 zarith.cmxa
-rwxrwxr-x 1 ali ali 214488 Jul 6 17:05 zarith.cmxs
-rw-rw-r-- 1 ali ali 1168 Mar 3 09:00 zarith.h
-rw-rw-r-- 1 ali ali 2165 Jul 6 17:05 zarith_top.cma
-rw-rw-r-- 1 ali ali 17730 Jul 6 17:05 z.cmi
-rw-rw-r-- 1 ali ali 110788 Jul 6 17:05 z.cmti
-rw-rw-r-- 1 ali ali 40719 Jul 6 17:05 z.cmx
-rw-rw-r-- 1 ali ali 22184 Mar 3 09:00 z.mli
It only seems to happen when I have flambda enabled. See this related issue: https://github.com/ocaml/num/issues/9
Ali Caglayan (Jul 19 2021 at 17:41):I'm not sure why enabling flambda would give out extra warnings tho?
Emilio Jesús Gallego Arias (Jul 19 2021 at 18:12):That's a known issue, I suggest disabling the warning, it is quite harmless
Emilio Jesús Gallego Arias (Jul 19 2021 at 18:12):Indeed it is a flambda specific warning
Last updated: Nov 29 2023 at 06:01 UTC