Stream: Dune devs & users

Topic: Extraction and dune build -p

Karl Palmskog (May 30 2020 at 17:33):

so I have the following under an ocaml directory:

(coq.extraction
 (prelude fitch_decidable_extrocaml)
 (extracted_modules fitch_system)
 (theories Fitch))
...
(executable
 (name checker)
 (public_name fitch-checker)
 (libraries util fitch_system)
 (package fitch-checkers))

and the following under a coq sibling directory:

(coq.theory
 (name Fitch)
 (package coq-fitch)
 (synopsis "Sound Fitch-style proof system in Coq for propositional logic"))

Yet, when I try to build the executable as a standalone package (dune build -p fitch-checkers), I get the following error:

File "ocaml/dune", line 4, characters 11-16:
4 |  (theories Fitch))
               ^^^^^
Error: Theory Fitch not found

Karl Palmskog (May 30 2020 at 17:34):

everything works great with just dune build (this succesfully generates both all .vo files and compiles the OCaml executable), and dune build -p works fine for the Coq theory package alone. Am I missing some annotation/option?

Karl Palmskog (May 30 2020 at 17:42):

to replicate, one can simply clone https://github.com/palmskog/fitch.git and do dune build -p fitch-checkers

Emilio Jesús Gallego Arias (May 30 2020 at 18:30):

Yup, Coq mode for Dune doesn't support yet composing with libraries coming from different packages, this is one of the reasons I'm holding off the call for beta testers

Emilio Jesús Gallego Arias (May 30 2020 at 18:31):

In regular setup that should not work anyways, unless you install the other package first

Emilio Jesús Gallego Arias (May 30 2020 at 18:31):

does dune build -p pkg1,pkg2 work?

Emilio Jesús Gallego Arias (May 30 2020 at 18:32):

but indeed it should not, but I'd have to see the concrete setup

Emilio Jesús Gallego Arias (May 30 2020 at 18:32):

hopefully we fix this soon, but we were having some discussion upstream w.r.t. lbis

Emilio Jesús Gallego Arias (May 30 2020 at 18:32):

Indeed I didn't fully settle on how to interpret (theory foo) when theory is not present in the workspace

Karl Palmskog (May 30 2020 at 21:55):

dune build -p coq-fitch,fitch-checkers actually works. These packages live in the same dune-project, I guess this is why?

Karl Palmskog (May 30 2020 at 22:00):

at least according to the manual, projects in the scope of the same dune-projectshould be composable? Composition at that level would solve 90+% of my use cases.

Emilio Jesús Gallego Arias (May 31 2020 at 15:02):

Still the case where you install coq-fitch and build fitch-checkers from the workspace should work; I hope to fix this soon.

Karl Palmskog (May 31 2020 at 17:19):

The problem with this case is that one gets a forced dependency in fitch-checkers on having installedcoq-fitch, when the sources live in the same tarball. None of the Coq files are actually needed in the checkers, they are just build dependencies.

Karl Palmskog (Jun 02 2020 at 08:13):

ah, basically one ends up in a catch-22 with theories: if Coq dependencies are listed there, you can build compositionally locally, but can't have the dependencies installed. If you don't list any dependencies, you can use installed dependencies, but local builds don't work properly.

Emilio Jesús Gallego Arias (Jun 02 2020 at 11:36):

Yup, this needs to be solved; theories deps needs to be resolved as in OCaml, first installed theories, second public but out-of-scope, then in-scope. There are some proposals to unify this in Dune so I've been having a look on how to do that without duplicating a lot of code.

Karl Palmskog (Jun 02 2020 at 14:59):

sounds good. In any case, I've found that using dune opens up many possibilities for slicing a repo up into multiple projects/packages, which should help CI/maintenance and downstream use. For example, our mutation analysis tool (mCoq) doesn't deal well at all with plugins, but with dune I could slice up projects into pure Coq and other parts.

Emilio Jesús Gallego Arias (Jun 02 2020 at 15:12):

Yup, tho the current library / interface capabilities of Coq are quite limited IMO in the sense of what we can do; for example, the current install scenario has no prevision for installing any package meta-data, which is usually needed. Handling this scenario properly is what is making me spend so much time to support (theories ) for installed libs.

We will have to break backwards compat with coq-makefile at some point, so indeed your experiments are essential to see what we can do

Karl Palmskog (Jun 02 2020 at 15:19):

Emilio Jesús Gallego Arias said:

We will have to break backwards compat with coq-makefile at some point

What I settled for with one project was having the pure Coq part be buildable with coq_makefile, and dune for the rest (but still dune in CI/opam for everything). This seems reasonable, and keeps an important use case (editing Coq files with old VSCoq/ProofGeneral). For the plugin, there was just no way I could figure out how to keep it buildable with coq_makefile without terrible things like checking in extracted code into version control.

Théo Zimmermann (Jun 02 2020 at 15:21):

When Emilio talks about breaking backward-compatibility, he generally means something much more radical: packages built with Dune/coq-makefile wouldn't be compatible with each other anymore (after being installed).

Karl Palmskog (Jun 02 2020 at 15:22):

ah, so you can't even Require stuff installed with dune? That's indeed radical, and I think that change has to be carefully coordinated across key Coq packages.

Théo Zimmermann (Jun 02 2020 at 15:24):

Yep, that's why this is something the Emilio is considering for version 2 of the Dune language, while we haven't even reached version 1 yet.

Théo Zimmermann (Jun 02 2020 at 15:25):

But the goal will be to have the ability to specify exactly on which libraries you depend on (like in OCaml) instead of loading everything that has been installed.

Théo Zimmermann (Jun 02 2020 at 15:25):

Maybe a solution for better compatibility will simply be to patch coq_makefile as well to be compatible with the new model...

Karl Palmskog (Jun 02 2020 at 15:26):

Théo Zimmermann said:

But the goal will be to have the ability to specify exactly on which libraries you depend on (like in OCaml) instead of loading everything that has been installed.

so one might say we move from large monolithic packages to more NodeJS style, where one can have hundreds of small deps?

Emilio Jesús Gallego Arias (Jun 02 2020 at 15:29):

I think we can keep some good amount of compatibility in the install sense, but at some point some advanced features may be disabled if you didn't build your dependencies with dune, to that extent we can introduce (v1_theories ...) to signal dependencies into stuff that installs with coq_makefile

Emilio Jesús Gallego Arias (Jun 02 2020 at 15:29):

main compat breaker is not installing everything under user-contrib anymore

Emilio Jesús Gallego Arias (Jun 02 2020 at 15:30):

but I'm convinced we can keep a good amount of compatibility, so hopefully the change should not be very "radical"

Emilio Jesús Gallego Arias (Jun 02 2020 at 15:30):

will depend on what features Coq users need

Théo Zimmermann (Jun 02 2020 at 15:40):

Karl Palmskog

so one might say we move from large monolithic packages to more NodeJS style, where one can have hundreds of small deps?

I don't think that it's related. This is more a question of style.

Last updated: Jun 03 2023 at 18:01 UTC