Dune hierarchical

Ecosystem
1

I had this working with earlier version of jubuilder before but now could not make it work with dune-1.2.1:

I have the following directory structure:

ml/
   dune
   test.ml
   extracted/
                 dune
                 _(lot of .ml files)_

The ml/dune:

(executables_
 (names test)_
 (libraries extracted))

ml/extracted/dune:

(library
 (name extracted)
 (wrapped false)
 (flags (:standard -w -39-33-20-50))
 (synopsis "ML code extracted from Coq"))

All I want to do dune build test.ext under ml and get everything compiled.
Now it complains: Error: Library “extracted” not found.

2

Do you have any .opam files in your project?

3

No.
As workaround I switched back to jbuilder (tweaking syntax a bit) and it works there. I thought dune is backward compatible with jbuilder?

4

It is. Do you have the project lying around somewhere? I’d like to reproduce this.

5

Sure. Here it is https://github.com/digamma-ai/asn1fpcoq/tree/master/ml
You can see our failed dune attempts in the history.

6

Weird, I brought back your dune files and the jbuild files and I get this error:

      ocamlc .test.eobjs/OcamlFPBER.{cmi,cmti} (exit 2)
(cd _build/default && /Users/rgrinberg/.opam/4.06.1/bin/ocamlc.opt -w @a-4-29-40-41-42-44-45-48-58-59-60-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I .test.eobjs -no-alias-deps -opaque -o .test.eobjs/OcamlFPBER.cmi -c -intf OcamlFPBER.mli)
File "OcamlFPBER.mli", line 1, characters 5-12:
Error: Unbound module FullBin

Which seems reasonable as I can’t find FullBin defined anywhere.

I’m using dune 1.3.0 however, perhaps you can try upgrading to that?

7

I am sorry, but to try it you need to run make from the top directory of the project. This will genrate ML files I am trying to compile. For that you may need to install some dependencies (via OPAM) per README.md.

8

I tried with 1.3 and how it does not build with jbuilder anymore. It is building OK with 1.2.1. Looks like regression. It will probably break some my older projects…

9

Okay, well I’m getting somewhere:

dune build ml/test.exe --profile release
    ocamlopt ml/.test.eobjs/OcamlFPBER.{cmx,o} (exit 2)
(cd _build/default && /Users/rgrinberg/.opam/4.06.1/bin/ocamlopt.opt -w -40 -g -I ml/.test.eobjs -I ml/extracted/.extracted.objs -intf-suffix .ml -no-alias-deps -o ml/.test.eobjs/OcamlFPBER.cmx -c -impl ml/OcamlFPBER.ml)
File "ml/OcamlFPBER.ml", line 2, characters 5-9:
Error: Unbound module Core
      ocamlc ml/.test.eobjs/test.{cmi,cmo,cmt} (exit 2)
(cd _build/default && /Users/rgrinberg/.opam/4.06.1/bin/ocamlc.opt -w -40 -g -bin-annot -I ml/.test.eobjs -I ml/extracted/.extracted.objs -no-alias-deps -o ml/.test.eobjs/test.cmo -c -impl ml/test.ml)
File "ml/test.ml", line 17, characters 25-43:
Error: Unbound module Float

I still cannot reproduce your error btw. dune is able to see the extracted library just fine.

Here are the dune files I’m working with:

diff --git a/ml/dune b/ml/dune
new file mode 100644
index 0000000..9bd1bcd
--- /dev/null
+++ b/ml/dune
@@ -0,0 +1,3 @@
+(executables
+ (names test)
+ (libraries extracted))
\ No newline at end of file
diff --git a/ml/extracted/dune b/ml/extracted/dune
new file mode 100644
index 0000000..47254a3
--- /dev/null
+++ b/ml/extracted/dune
@@ -0,0 +1,6 @@
+(library
+ (name extracted)
+ (wrapped false)
+ (flags (:standard -w -39-33-20-50))
+ (synopsis "ML code extracted from Coq")
+ )

PS, there’s no need to cd to ml to build with dune. $ dune build ml/test.exe works just fine as well.

10

Hmm, it looks like I’ve introduced Core dependency. You need opam install core as well. Thanks for the hint with cd.

I want to say that I really appreciate you looking into that, because right now with dune upgrade to 1.3 I am stuck as my old jbuilder workaround no longer working :frowning: I hope we can figure it out soon.

11

And yes, you need (libraries (extracted core num))

12

No problem, btw I’ll give that a try as well. Btw, you’ll need to add num to your extracted library as well. Doing that and attempting to load extracted in the repl with:

$ [rgrinberg:~/tmp/ml/asn1fpcoq] master(+0/-15) 1 ± dune utop ml/extracted
Fatal error: exception Failure("AXIOM TO BE REALIZED")

I get a result (not sure if it’s expected?), so it seems like dune is able to load this module.

Give $ dune utop in the extracted dir a try and see if it manages to load the library for you. Do you have any dune-project files lying around somewhere, btw?

PS, dune 1.3 includes a jbuilder compatibility mode in the form of the jbuilder executable. So if things work for you using $ jbuilder but not with $ dune (with version 1.3) then it would narrow things down for me.

13

yes, the AXIOM TO BE REALIZED error is expected. But to get to it I need first to be able to compile it all with dune. It looks like you succeeded doing so. What dune files you used? I assume you are using 1.3.

14

I’ve made a clean branch for experimenting with dune1.3. GitHub - digamma-ai/asn1fpcoq at dune13-coq882-opam2

It still gives me the same error:

$ dune build test.exe 14:40:05
File “dune”, line 3, characters 13-22:
3 | (libraries extracted core num)
^^^^^^^^^
Error: Library “extracted” not found.
Hint: try: dune external-lib-deps --missing test.exe

15

After much debugging with 2 versions of dune and 2 versions of opam, looking at dune sources and running strace, the problem turns out to be in presence of dune-project under extracted. Once removed it worked nicely! Problem solved!

2 Likes
16

Based on this thread I’ve opened an issue: https://github.com/ocaml/dune/issues/1439

1 Like