Stream: Coq devs & plugin devs

Topic: Unbound module Mltop


view this post on Zulip Andrej Dudenhefner (May 19 2021 at 09:54):

During the past month there seem to be some changes when running ci projects locally. After ./configure -local and make if I now run make ci-bignums I get the error

CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
File "plugin/bignums_syntax.ml", line 11, characters 9-31:
11 | let () = Mltop.add_known_module __coq_plugin_name
              ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Mltop

upon manual compilation I get the error

File "./BigNumPrelude.v", line 28, characters 0-42:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/user/stdlib/bignums/plugin/bignums_syntax_plugin.cmxs: undefined symbol: camlNotation__declare_numeral_interpreter_inner_10205\")")

Am I missing some new flag?
(A month ago both workflows were fine.)
(ocamlc --version = 4.10.1)

view this post on Zulip Gaëtan Gilbert (May 19 2021 at 10:41):

what coq commit?

view this post on Zulip Andrej Dudenhefner (May 19 2021 at 10:42):

Gaëtan Gilbert said:

what coq commit?

current master

view this post on Zulip Andrej Dudenhefner (May 19 2021 at 10:58):

So to reproduce the error from fresh master clone:

./configure -local
make world
make ci-bignums

Probably I'm missing some flag.

view this post on Zulip Gaëtan Gilbert (May 19 2021 at 11:12):

try https://github.com/coq/coq/pull/14340

view this post on Zulip Andrej Dudenhefner (May 19 2021 at 11:20):

Gaëtan Gilbert said:

try https://github.com/coq/coq/pull/14340

Yes, this works.

view this post on Zulip Gaëtan Gilbert (May 19 2021 at 15:04):

it broke other stuff so I gave up
for development I recommend giving up on the legacy build mode

view this post on Zulip Andrej Dudenhefner (May 19 2021 at 17:36):

What would be the current alternative to the above

./configure -local
make world
make ci-bignums

in the dev/doc/build-system.dune.md there is no mention on how to locally build ci targets.

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

make -f Makefile.dune world; make -f Makefile.ci ci-bignums

view this post on Zulip Andrej Dudenhefner (Jul 12 2021 at 14:41):

Now (current master) ./configure -local and then make -f Makefile.dune world; make -f Makefile.ci ci-bignums once again gives me the error

File "plugin/bignums_syntax.ml", line 11, characters 9-31:
11 | let () = Mltop.add_known_module __coq_plugin_name
              ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Mltop

What would now be the correct command to locally build ci targets?

view this post on Zulip Gaëtan Gilbert (Jul 12 2021 at 15:01):

stop using configure with dune

view this post on Zulip Gaëtan Gilbert (Jul 12 2021 at 15:01):

delete _build_vo if it exists
then try again

view this post on Zulip Gaëtan Gilbert (Jul 12 2021 at 15:01):

you can also try make -f Makefile.dune ci-bignums


Last updated: Oct 15 2021 at 21:02 UTC