Stream: Dune devs & users

Topic: Multi-package repo workflow


view this post on Zulip Li-yao (May 24 2022 at 22:06):

I have a repo containing two packages A and B, with B depending on A. I see two ways to set it up:

  1. In B's dune file, have (theories A). This makes B depend on the local build of A. Pro: dune build builds everything. Con: this doesn't allow B to depend on a global installation of A. The build of B has to build A locally.
  2. Don't have (theories A). Pro: I can build and install B separately, after installing A. Con: dune build doesn't work when A isn't already installed.

Can I get the best of both worlds?

view this post on Zulip Ali Caglayan (May 24 2022 at 22:28):

Yes soon hopefully. I am in fact working on theories being able to use externally defined installations of theories.

view this post on Zulip Rudi Grinberg (May 27 2022 at 18:34):

@Li-yao there's now a PR up if you want to help test

view this post on Zulip Rudi Grinberg (May 31 2022 at 16:09):

@Li-yao dune now has support for extraction. I noticed that you extract some tests in InteractionTrees with makefiles, perhaps you can do it in dune now

view this post on Zulip Karl Palmskog (May 31 2022 at 16:39):

I think you mean: "Dune now has support for composition with user-contrib-installed Coq libraries"?

view this post on Zulip Ali Caglayan (May 31 2022 at 17:49):

@Karl Palmskog I think he meant extraction, we didn't support user-contrib yet.

view this post on Zulip Li-yao (May 31 2022 at 19:13):

I already use that part of dune :) There is one annoyance with recursive separate extraction, where all extracted modules have to be listed, but the fault really lies with extraction rather than dune.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:36):

I am in favor of supporting an output directory for extraction in Coq.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:37):

What is dumb today is that we cannot do this since extraction is a plugin and therefore has no business asking for command line args.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:37):

We could instead ask for an env var

view this post on Zulip Ali Caglayan (May 31 2022 at 19:37):

or absorb extraction as core coq finally and support it from the cli

view this post on Zulip Ali Caglayan (May 31 2022 at 19:38):

On the dune side, we can support directory targets for extraction

view this post on Zulip Ali Caglayan (May 31 2022 at 19:38):

So you just have to say: my extracted code will go in this dir.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:38):

Dune will be able to use all the ml files that get generated in there


Last updated: Feb 04 2023 at 02:03 UTC