Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[dynlink] Error while loading ".../ltac_plugin.cmxs" The module `Ltac_plugin__Tacarg' is not yet initialized. #7876

Closed
vicuna opened this Issue Nov 24, 2018 · 5 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Nov 24, 2018

Original bug ID: 7876
Reporter: @ejgallego
Assigned to: @lpw25
Status: resolved (set by @lpw25 on 2018-12-08T15:19:46Z)
Resolution: fixed
Priority: normal
Severity: major
Platform: Linux
OS: Ubuntu
OS Version: 18.04
Category: dynlink and natdynlink
Monitored by: @nojb

Bug description

Dear OCaml devs,

we are testing Coq with OCaml trunk (coq/coq#8856) and indeed it seems that in the Dune build with plugins we are finding a linking problem likely related to #1063

$ make -f Makefile.dune world
...
(cd _build/default && ../install/default/bin/coqtop -boot -coqlib . -noinit -R theories Coq -compile theories/Init/Notations.v)
File "./theories/Init/Notations.v", line 128, characters 0-32:
Error: while loading
/home/egallego/external/coq-master/_build/default/plugins/ltac/ltac_plugin.cmxs:
error while linking /home/egallego/external/coq-master/_build/default/plugins/ltac/ltac_plugin.cmxs.
The module `Ltac_plugin__Tacarg' is not yet initialized

I've tried to minimize the problem without success so far :(

At the suggestion of the Dune devs I disabled "wrapping" for the Ltac plugin, however the same error persists:

The module Tacarg is not yet initialized

thus this seems unrelated to packing.

See below for ocamlobjinfo information.

Steps to reproduce

In a context with OCaml master, checkout coq/coq#8856 and do make -f Makefile.dune trunk

Additional information

Information about ocamlobjinfo for the ltac_plugin [without wrapping] is at:
https://pastebin.com/nM1XWKVr

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 28, 2018

Comment author: @lpw25

I haven't quite reproduced the error message you're getting, but the new implementation is indeed more restrictive for interface-only modules. I'm going to try to adjust the implementation to explicit support such modules, and hopefully that will fix the particular instance of the problem that you're seeing.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 29, 2018

Comment author: @ejgallego

Hi lpw25, thanks a lot!

Note that the Dune-based build whose instructions I've posted doesn't use interface-only modules, I guess you tried the regular make-based build, which indeed errors with -packs that contain interface-only files.

This seems indeed like a different problem than the one reported here.

In order to reproduce the Dune case [which seems to choke on module aliases] be sure to :

  • have a clean tree [git clean -fxd]
  • latest Coq master,
  • call 'make -f Makefile.dune world'

Thanks again!

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 30, 2018

Comment author: @lpw25

@ejgallego, could you try out:

#2176

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 30, 2018

Comment author: @ejgallego

Thanks a lot Leo, Coq now works fine, I confirm 2176 fixes Coq plugins in both build modes [using -pack and using aliases].

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 8, 2018

Comment author: @lpw25

#2176 has now been merged in trunk.

@vicuna vicuna closed this Dec 8, 2018

@vicuna vicuna added the dynlink label Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.