Stream: Coq devs & plugin devs

Topic: no cmx file was found in path for module Zarith_version


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jul 19 2021 at 16:52):

ocaml version, zarith version, dune version? how were they installed (opam?)?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 19 2021 at 16:53):

all with opam

view this post on Zulip Gaëtan Gilbert (Jul 19 2021 at 16:55):

is the warning located? what produces it?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 19 2021 at 16:59):

Whoops wrong one

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:00):

So something is going on in plugins/micromega/numCompat.ml

view this post on Zulip Gaëtan Gilbert (Jul 19 2021 at 17:05):

what does ocamlfind query zarith say and what files does the returned path contain?

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:06):

/mnt/sdd1/.opam/dev/lib/zarith

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:06):

which is correct

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:06):

It's just my dev switch

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:07):

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

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:40):

It only seems to happen when I have flambda enabled. See this related issue: https://github.com/ocaml/num/issues/9

view this post on Zulip Ali Caglayan (Jul 19 2021 at 17:41):

I'm not sure why enabling flambda would give out extra warnings tho?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2021 at 18:12):

Indeed it is a flambda specific warning


Last updated: Oct 16 2021 at 01:03 UTC