Andrej Dudenhefner (May 19 2021 at 09:54): 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)
Gaëtan Gilbert (May 19 2021 at 10:41):what coq commit?
Andrej Dudenhefner (May 19 2021 at 10:42):Gaëtan Gilbert said:
what coq commit?
current master
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.
Gaëtan Gilbert (May 19 2021 at 11:12):try https://github.com/coq/coq/pull/14340
Andrej Dudenhefner (May 19 2021 at 11:20):Gaëtan Gilbert said:
Yes, this works.
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
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.
Gaëtan Gilbert (May 19 2021 at 17:50):make -f Makefile.dune world; make -f Makefile.ci ci-bignums
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?
Gaëtan Gilbert (Jul 12 2021 at 15:01):stop using configure with dune
Gaëtan Gilbert (Jul 12 2021 at 15:01):delete _build_vo if it exists
then try again
Gaëtan Gilbert (Jul 12 2021 at 15:01):you can also try make -f Makefile.dune ci-bignums
Last updated: Oct 13 2024 at 01:02 UTC