Stream: Dune devs & users

Topic: dune, theories composition and several package

Thomas Letan (Dec 15 2020 at 14:56):

Hi. I am currently working on packaging FreeSpec, which provides three theories in the same repository, in three Opam packages. I can mention FreeSpec.Core (from coq-freespec-core) in the dune file of FreeSpec.FFI (from coq-freespec-ffi). dune build works, but dune build -p coq-freespec-ffi does not work.

Thomas Letan (Dec 15 2020 at 14:57):

do you have any suggestion?

Thomas Letan (Dec 15 2020 at 14:57):

Have you any idea, @Emilio Jesús Gallego Arias?

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:24):

Likely you have to do dune build -p coq-freespec-core,coq-freespec-ffi

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:24):

With -p, local packages are not taken into account [as per docs]

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:24):

but instead they are resolved using the installed versions

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:25):

so for example, opam files should mention only one package in -p , as the build should happen w.r.t. the opam-resolved version

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:25):

but if you wanna do a joint build with -p you need to specify both

Thomas Letan (Dec 15 2020 at 15:26):

the issue with having opam to use only one package in -p is that it will complain for the theories arguments it does not know

Thomas Letan (Dec 15 2020 at 15:26):

I guess I could have a way to patch dune files for standalone build

Thomas Letan (Dec 15 2020 at 15:27):

but it feels fragile

Thomas Letan (Dec 15 2020 at 15:27):

or maybe I am missing something?

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:27):

Oh indeed, that is broken

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:27):

sorry I forgot, that is broken I need to fix ASAP

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:27):

it is part of the inter-scope patch

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

as of dune master, (theories ...) are not resolved w.r.t. installed theories

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

so indeed your setup is not yet usable, sorry

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

I have been promising to fix this for months, I'm really sorry

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

I have a tree but actually the last part missing is scanning of user-contrib

Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

so theories are resolved similarly as they are in OCaml:

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

• first dune computes the list of installed theories [basically the file-tree / scope of user-contrib + COQPATH]
• then dune computes the list of visible public theories coming from other scopes / vendored libs, etc...
• then dune computes the list of in scope both private and public theories

Thomas Letan (Dec 15 2020 at 15:37):

don't worry

Thomas Letan (Dec 15 2020 at 15:37):

I will do just like I did with supporting several version of OCaml for coqffi

Thomas Letan (Dec 15 2020 at 15:37):

i.e., proviing patches to accomodate with the different use cases

Thomas Letan (Dec 15 2020 at 15:37):

and the opam repository will just apply the patch that removes the theories line to the dune files

Thomas Letan (Dec 15 2020 at 15:41):

Thanks for the quick answer btw!

Karl Palmskog (Dec 15 2020 at 17:57):

@Théo Zimmermann move this to the Dune stream please

Notification Bot (Dec 15 2020 at 17:59):

This topic was moved here from #Coq users > dune, theories composition and several package by Théo Zimmermann

Thomas Letan (Dec 15 2020 at 18:36):

Oups, sorry about the wrong chan

Last updated: Jun 04 2023 at 23:30 UTC