Stream: Dune devs & users

Topic: dune, theories composition and several package


view this post on Zulip 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.

view this post on Zulip Thomas Letan (Dec 15 2020 at 14:57):

do you have any suggestion?

view this post on Zulip Thomas Letan (Dec 15 2020 at 14:57):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:24):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:24):

but instead they are resolved using the installed versions

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:26):

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

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:27):

but it feels fragile

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:27):

or maybe I am missing something?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:27):

Oh indeed, that is broken

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:27):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:27):

it is part of the inter-scope patch

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

so indeed your setup is not yet usable, sorry

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:28):

so theories are resolved similarly as they are in OCaml:

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2020 at 15:29):

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:37):

don't worry

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:37):

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

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:37):

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

view this post on Zulip 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

view this post on Zulip Thomas Letan (Dec 15 2020 at 15:41):

Thanks for the quick answer btw!

view this post on Zulip Karl Palmskog (Dec 15 2020 at 17:57):

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

view this post on Zulip 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

view this post on Zulip Thomas Letan (Dec 15 2020 at 18:36):

Oups, sorry about the wrong chan


Last updated: Oct 16 2021 at 09:07 UTC