Hi. I am currently working on packaging FreeSpec, which provides three theories in the same repository, in three Opam packages. I can mention
coq-freespec-core) in the
dune file of
dune build works, but
dune build -p coq-freespec-ffi does not work.
do you have any suggestion?
Have you any idea, @Emilio Jesús Gallego Arias?
Likely you have to do
dune build -p coq-freespec-core,coq-freespec-ffi
-p, local packages are not taken into account [as per docs]
but instead they are resolved using the installed versions
so for example, opam files should mention only one package in
-p , as the build should happen w.r.t. the opam-resolved version
but if you wanna do a joint build with
-p you need to specify both
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
I guess I could have a way to patch
dune files for standalone build
but it feels fragile
or maybe I am missing something?
Oh indeed, that is broken
sorry I forgot, that is broken I need to fix ASAP
it is part of the inter-scope patch
as of dune master,
(theories ...) are not resolved w.r.t. installed theories
so indeed your setup is not yet usable, sorry
I have been promising to fix this for months, I'm really sorry
I have a tree but actually the last part missing is scanning of
so theories are resolved similarly as they are in OCaml:
I will do just like I did with supporting several version of OCaml for coqffi
i.e., proviing patches to accomodate with the different use cases
and the opam repository will just apply the patch that removes the
theories line to the
Thanks for the quick answer btw!
@Théo Zimmermann move this to the Dune stream please
This topic was moved here from #Coq users > dune, theories composition and several package by Théo Zimmermann
Oups, sorry about the wrong chan
Last updated: Oct 16 2021 at 09:07 UTC