Li-yao (May 24 2022 at 22:06): 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:
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.(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?
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.
Rudi Grinberg (May 27 2022 at 18:34):@Li-yao there's now a PR up if you want to help test
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
Karl Palmskog (May 31 2022 at 16:39):I think you mean: "Dune now has support for composition with user-contrib-installed Coq libraries"?
Ali Caglayan (May 31 2022 at 17:49):@Karl Palmskog I think he meant extraction, we didn't support user-contrib yet.
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.
Ali Caglayan (May 31 2022 at 19:36):I am in favor of supporting an output directory for extraction in Coq.
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.
Ali Caglayan (May 31 2022 at 19:37):We could instead ask for an env var
Ali Caglayan (May 31 2022 at 19:37):or absorb extraction as core coq finally and support it from the cli
Ali Caglayan (May 31 2022 at 19:38):On the dune side, we can support directory targets for extraction
Ali Caglayan (May 31 2022 at 19:38):So you just have to say: my extracted code will go in this dir.
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