Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007876OCamldynlink and natdynlinkpublic2018-11-24 15:072018-12-08 16:19
Reporterejgallego 
Assigned Tolpw25 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformLinuxOSUbuntuOS Version 18.04
Product Version 
Target VersionFixed in Version 
Summary0007876: [dynlink] Error while loading ".../ltac_plugin.cmxs" The module `Ltac_plugin__Tacarg' is not yet initialized.
DescriptionDear OCaml devs,

we are testing Coq with OCaml trunk (https://github.com/coq/coq/pull/8856 [^]) and indeed it seems that in the Dune build with plugins we are finding a linking problem likely related to https://github.com/ocaml/ocaml/pull/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 ReproduceIn a context with OCaml master, checkout https://github.com/coq/coq/pull/8856 [^] and do make -f Makefile.dune trunk
Additional InformationInformation about `ocamlobjinfo` for the ltac_plugin [without wrapping] is at:
https://pastebin.com/nM1XWKVr [^]
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019492)
lpw25 (developer)
2018-11-28 14:30

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.
(0019493)
ejgallego (reporter)
2018-11-29 03:47
edited on: 2018-11-29 03:48

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!

(0019494)
lpw25 (developer)
2018-11-30 11:31

@ejgallego, could you try out:

https://github.com/ocaml/ocaml/pull/2176 [^]
(0019495)
ejgallego (reporter)
2018-11-30 22:53

Thanks a lot Leo, Coq now works fine, I confirm 2176 fixes Coq plugins in both build modes [using -pack and using aliases].
(0019501)
lpw25 (developer)
2018-12-08 16:19

GPR#2176 has now been merged in trunk.

- Issue History
Date Modified Username Field Change
2018-11-24 15:07 ejgallego New Issue
2018-11-28 14:30 lpw25 Note Added: 0019492
2018-11-28 14:30 lpw25 Assigned To => lpw25
2018-11-28 14:30 lpw25 Status new => assigned
2018-11-29 03:47 ejgallego Note Added: 0019493
2018-11-29 03:48 ejgallego Note Edited: 0019493 View Revisions
2018-11-29 03:48 ejgallego Note Edited: 0019493 View Revisions
2018-11-30 11:31 lpw25 Note Added: 0019494
2018-11-30 22:53 ejgallego Note Added: 0019495
2018-12-08 16:19 lpw25 Note Added: 0019501
2018-12-08 16:19 lpw25 Status assigned => resolved
2018-12-08 16:19 lpw25 Resolution open => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker