ocaml / ocaml/dune

Bug when linking ocaml with a dune package including a static library

Open
#6,844 8 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

rocq
Dominant language
OCaml
Stars
1.9k
Forks
500
Avg merge
15h 21m
Merged PRs (30d)
277

Description

Expected Behavior

I wanted to call Rust from COQ via OCaml, using ocaml-interop for Rust <-> OCaml FFI. The project structure is as follows:

├── dune-project
├── src
│   ├── dune
│   ├── hello_world.ml
│   ├── my_plugin.mlpack
│   └── syntax.mlg
├── rust-lib
│   ├── dune
│   ├── Cargo.toml
│   └── src/
└── theories
    ├── dune
    └── UsingMyPlugin.v

The dune file in the rust_lib:

(rule
 (targets libcallable_rust.a dllcallable_rust.so)
 (deps Cargo.toml dune (source_tree ./src))
 (action
  (no-infer
   (progn
    (run cargo build)
    (run sh -c
      "cp target/debug/libcallable_rust.so ./dllcallable_rust.so 2> /dev/null || \
       cp target/debug/libcallable_rust.dylib ./dllcallable_rust.so")
    (run cp target/debug/libcallable_rust.a ./libcallable_rust.a)
   ))))

(library
 (name callable_rust)
 (public_name my-coq-plugin.callable_rust)
 (c_library_flags -lpthread -lc -lm)
 (foreign_archives callable_rust))

The dune file in the src dir:

(library
 (name my_plugin)
 (public_name my-coq-plugin.plugin)
 (synopsis "My Coq Plugin")
 (flags :standard -rectypes -w -27)
 (libraries my-coq-plugin.callable_rust coq-core.vernac threads.posix))

(coq.pp
 (modules syntax))

And the dune file in the theories dir:

(coq.theory
 (name MyPlugin)
 (package my-coq-plugin)
 (plugins my-coq-plugin.plugin))

I am compiling a Rust library and copying the archive of object files. I am creating a dune library with it for a later use in OCaml. The problem is that when setting it all up and doing dune build. I expect this to be compiled correctly.

Actual Behavior

I am having some weird behaviour:

File "./theories/UsingMyPlugin.v", line 1, characters 0-51:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"dlopen(/Users/andrei/Documents/COQ/PluginUsingDune/_build/default/src/my_plugin.cmxs, 0x000A): symbol not found in flat namespace (_rust_twice)\")")

    Updating crates.io index                 
   Compiling cc v1.0.78
   Compiling ocaml-sys v0.22.3
   Compiling cty v0.2.2
   Compiling ocaml-interop v0.8.8
   Compiling static_assertions v1.1.0
   Compiling ocaml-boxroot-sys v0.2.0
   Compiling callable_rust v0.1.0 (/Users/andrei/Documents/COQ/PluginUsingDune/_build/default/rust_lib)
    Finished dev [unoptimized + debuginfo] target(s) in 4.03s

I assume that the compilation of the OCaml library happens before the compilation of the Rust and a linking error occurs. It is possible that the output is shown in an incorrect order, but the dynlink error is thrown out immediately, but the compilation process of Rust takes about 3 seconds.

Moreover, when doing dune build two times, the problem remains, even tho it should've been gone, if it occurs only due to incorrect compilation order.

Reproduction

I am attaching a minimal reproducible example. It also contains directory test, which shows that when trying to call the created dune library from an OCaml executable, but not COQ, everything seems to work as expected. You can compile the project using dune build and see that ./_build/default/test/test1.exe is an executable with expected behaviour. It seems that the compilation processes for coq plugins and ordinary Ocaml executables vary and there is a problem in the first one.

Specifications

  • Version of dune: 3.6.1
  • Version of ocaml: 4.14.0
  • Operating system: macOS Monterey 12.5.1

Additional information

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with the linked minimal reproducible example and run dune build on macOS, comparing rust-lib/dune with the src and theories dune files. Contrast the failing Coq plugin load with the working test/test1.exe case; the issue is resolved when the Coq plugin loads the Rust symbol without the Dynlink error.

Written by the indexing model from the issue text.

Assessment

Tech stack
ocaml, rust
Domain
build-system
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
38/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.