Recommended Project Structure with local library · coq-community devs & users

Hey everyone. I am historically phobic of Makefiles and such, and am trying to cure myself. Setting up a new project Today, the "Recommended Project Structure" has been of great help to start clean rather than paste and patch an old Makefile I don't understand (thanks @Karl Palmskog !). So here comes a trivial question, apologies in advance for that -.-
I have compared to the coq-community example a local library, with its own Makefile, that I have setup as a git submodule and lives in a ./lib folder. I therefore added -R ./lib/InteractionTrees/theories ITree to my _CoqProject. I now want the Makefile to run make -C ./lib/InteractionTrees first: what would be the simplest way to extend the existing Makefile to this end?

Karl Palmskog (Dec 23 2020 at 14:21):

@Yannick Zakowski are you sure you want to run make -C at all? Maybe it would be easier to just add all .v files from ITree to your toplevel _CoqProject

Karl Palmskog (Dec 23 2020 at 14:22):

also for the record, I think Anton Trunov wrote most of the "Rec project structure", I just added some small parts

Yannick Zakowski (Dec 23 2020 at 14:22):

I see. I guess I don't really mind either way, it just felt more natural to reuse the Makefile of the library.

Karl Palmskog (Dec 23 2020 at 14:23):

the problem with reusing the library Makefile is that you will have to make sure that the make -C is run before everything and is kept up to date, and this may be a chore, if you add stuff to your own _CoqProject this is handled without further effort.

Karl Palmskog (Dec 23 2020 at 14:24):

normally, I would recommend depending on ITree via opam instead, there are both released and dev packages

Yannick Zakowski (Dec 23 2020 at 14:25):

It's kinda convenient for me to have a local submodule as I dev itrees in parallel by need of features, but yes I should depend on opam simply eventually I agree

Yannick Zakowski (Dec 23 2020 at 14:26):

I guess I'll just add the ITree files directly to the _CoqProject for now then.
Just to be sure, there's no way to just recursively add the folder?

Karl Palmskog (Dec 23 2020 at 14:27):

I'm not sure what "recursively add the folder" would mean exactly, but you can for sure get your make -C into the makefile in multiple ways as well

Karl Palmskog (Dec 23 2020 at 14:29):

for example, if you use a delegating Makefile like the one in coq-community, you could do:

all: Makefile.coq itree
        @+$(MAKE) -f Makefile.coq all

itree:
        @+$(MAKE) -C path/to/itree

clean: Makefile.coq
        @+$(MAKE) -f Makefile.coq cleanall
        @rm -f Makefile.coq Makefile.coq.conf

Makefile.coq: _CoqProject
        $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq

force _CoqProject Makefile: ;

%: Makefile.coq force
        @+$(MAKE) -f Makefile.coq $@

.PHONY: all clean force itree

Yannick Zakowski (Dec 23 2020 at 14:32):

Karl Palmskog (Dec 23 2020 at 14:33):

a third option is to use Dune, which would not require Makefiles at all, but you would need to add some Dune boilerplate to Itree

Karl Palmskog (Dec 23 2020 at 14:35):

Paolo Giarrusso (Dec 23 2020 at 17:00):

Does that Makefile let the main library depend on itree? I’d either add the .v files to the main _CoqProject, use find to list them on the command line of the parent makefile, or let Makefile.coq depend on itree.

Paolo Giarrusso (Dec 23 2020 at 17:02):

And if you’re developing both libraries together, you probably really want a “merged incremental build”, with either dune or all files into the same _CoqProject

Christian Doczkal (Jan 05 2021 at 15:43):

I just had a look at the aforementioned Recommended Project Structure and I noticed that the section "Makefile and Makefile.coq.local" talks about CoqMakefile.local and CoqMakefile rather than the more customary Makefile.coq[.local] If there is an attempt at changing the names used, this should probably be said, otherwise, the names should probably be fixed. @Karl Palmskog @Anton Trunov

Karl Palmskog (Jan 05 2021 at 15:52):

@Christian Doczkal I think this is due to Anton and I using different conventions over time. I edited the wiki page to make Makefile.coq the canonical name. Thanks for pointing this out.

Stream: coq-community devs & users

Topic: Recommended Project Structure with local library

Yannick Zakowski (Dec 23 2020 at 14:11):