I have a repo containing two packages
B depending on
A. I see two ways to set it up:
(theories A). This makes
Bdepend on the local build of
dune buildbuilds everything. Con: this doesn't allow
Bto depend on a global installation of
A. The build of
Bhas to build
(theories A). Pro: I can build and install
Bseparately, after installing
dune builddoesn't work when
Aisn't already installed.
Can I get the best of both worlds?
Yes soon hopefully. I am in fact working on theories being able to use externally defined installations of theories.
@Li-yao there's now a PR up if you want to help test
@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
I think you mean: "Dune now has support for composition with user-contrib-installed Coq libraries"?
@Karl Palmskog I think he meant extraction, we didn't support user-contrib yet.
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.
I am in favor of supporting an output directory for extraction in Coq.
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.
We could instead ask for an env var
or absorb extraction as core coq finally and support it from the cli
On the dune side, we can support directory targets for extraction
So you just have to say: my extracted code will go in this dir.
Dune will be able to use all the ml files that get generated in there
Last updated: Feb 04 2023 at 02:03 UTC