Dune hierarchical

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:

                 _(lot of .ml files)_

The ml/dune:

 (names test)_
 (libraries extracted))


 (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.

Do you have any .opam files in your project?

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

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

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

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?

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.

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…

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 @@
+ (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 @@
+ (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.

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.

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

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.

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.

I’ve made a clean branch for experimenting with dune1.3. https://github.com/digamma-ai/asn1fpcoq/tree/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

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!


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

1 Like