You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
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.
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 :
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
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:
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
The text was updated successfully, but these errors were encountered: