META.pkg is illformed

[gares]

Expected Behavior

The file is placed at the toot of the build tree and findlib can parse it

Actual Behavior

Findlib cannot parse it since it lacks the directory stanza. The file is only accepted when symlinked in _build/install/...lib/pkg/META since there it does not need the directory stanza.

My suggestion is to create two meta files, one good for installation, and another one good for using uninstalled. The former shall be "hidden".

[rgrinberg]

My suggestion is to create two meta files, one good for installation, and another one good for using uninstalled. The former shall be "hidden".

What prevents you from wanting to use the installed META? Is it because you want to load a private library with findlib?

[ejgallego]

@rgrinberg it is because we've been told that depending on things in _install is not good practice.

However I'm not sure that advice is correct.

[rgrinberg]

You can depend on things being in _build/install if you depend on (package ..) or the @install alias.

[ejgallego]

I mean, why the rule for pkg.install can depend on things there but our Coq rules cannot?

[rgrinberg]

Although we never intended this to be user facing, you most certainly can. And we are not planning to shift the location of this directory around just to spite our users :)

But let me try to convince to why you should think twice before doing it. When we load the rules for _build/install, recall that we need to scan the entire workspace to determine all files that might be installable (install stanzas, public libraries, executables, etc). Doing this work requires us to load certain user rules. While we try to load as little rules as possible, it's not something that we ever guarantee to be stable between versions of dune. This means that you might get cycles in future versions of dune if we decide to force the rules in the directory that's using %{workspace_root}../install/%{context_name}. If that risk is acceptable to you, feel free and depend on things inside _install/%{context_name}

[ejgallego]

@rgrinberg I'm fine not depending on _install, as long as we agree on a general method to provide runtime deps.

For example, I'd be fine emulating (env (bin ...)) and thus creating a _build/$context/.lib and extending OCAMLPATH properly, what do you think?

That would also be the most useful thing to do I think as would provide convenient support for other people using OCaml plugins.

Maybe I'm just not respecting some API boundaries, but for me, morally having (deps (package foo)) is the same than writing a rule which directly depends on something in _install/$context

[ejgallego]

We could implement this feature as a new (runtime-libraries ...) field (which could just set a boolean), or we could unconditionally make them available, I don't know.

This provides an alternative to some functionality present in the dune sites plugin, but seems much lighter to me.

[rgrinberg]

Sure, I have nothing against in generating rules that will help you with runtime deps. I'd like to hear more about your use case however. How are you using the runtime deps? Are you building something with them? Are you dynlinking?

For example, I'd be fine emulating (env (bin ...)) and thus creating a _build/$context/.lib and extending OCAMLPATH properly, what do you think?

I would like something simpler than this. There are also some related use cases in dune that we might be able to unify.

We could implement this feature as a new (runtime-libraries ...) field (which could just set a boolean), or we could unconditionally make them available, I don't know.

Could you describe this a bit more?

[gares]

Coq projects are sometimes made of both .v files .ml files. The latter constitutes a plugin coqc must load in order to compile the .v files.
Recently coq switched from a home baked, broken, loading mechanism to findlib. This, for example, makes it possible for plugins to use ocaml libraries.

Now, dune builds a META file and a cmxs but that seems only to be properly after the fact. During the build process the META file is illformed hence unusable.

Emilio proposes to make the file usable while building the package.

Splitting each Coq projects with a plugin into two packages (an ocaml library and a pure .v one) and use a package dependency seems to the Coq devs a bit too much to ask to our users. There are a few PR out there doing that, and they are too large to be considered reasonable, IMO.

Hope it helps.

[ejgallego]

Are you dynlinking?

Yes, we are dynlinking, and we use Fl_dynload because we need to be able to pull deps when dynlinking, and also we need to support quite a bit of 3rd party systems that still don't use Dune, so we rely on the dep info on META.

We could make things work by depending on the (installed) cmxs and the META file, but as you mentioned, it'd be better to have more constrained rules similarly to what is done for _build/$context/.bin

[ejgallego]

This was discussed and a few points where made:

• there are two ways to make Fl_dynload work for build (run ...) actions:
  • depend on the required files on _build/install, as Dune already extends OCAMLPATH to point there
  • extend OCAMLPATH to point to a _build/%{context}/.lib directory, and add rules for META and the .cmxs.
• first option is easy, but loads more rules; second option would allow to make private plugins available as (env (bin ...)) does with binaries
• there is a question of how this overlaps with Dune sites? Dune sites is morally option 1, but with less granularity than what we want here. I dont' know what more special stuff does the Dune sites setup do.

I guess for now the easiest thing to do , but as Rudi points out, we need to be beware of cycles, user messages may not be the best.

[paurkedal]

I have a similar need when running the testsuite for Caqti, which also uses Fl_dynload. I had a look at dune-site, but as far as I can tell it has the same limitation, that the test suite will need to depend on the full @install target. Would it be feasible to have more precise dependencies, like having individual @pkg/install aliases which could be referred from deps stanzas, or even more precisely (deps ...(plugin <dir>/<plugin-name>)...) for the dune-site.plugins-based solution? [Update: @pkg/install is available as the already mentioned (package pkg) dependency specification.]

(My current solution has been to rewrite the META files, prepending a directory directive. With sublibraries that becomes more tricky, unless the libraries are rearranged in the source code so that the META.pkg can be copied into pkg/META.)

[ejgallego]

In src/coq/coq_rules.ml we just depend on the META install location, that works, and IMHO should be better supported in the stanzas.

When we generate dune files, we use a very ugly hack which is to emit (deps ../../../install/default/lib/coq-core/foo/META) etc....