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?
@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
also for the record, I think Anton Trunov wrote most of the "Rec project structure", I just added some small parts
I see. I guess I don't really mind either way, it just felt more natural to reuse the Makefile of the library.
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.
normally, I would recommend depending on ITree via opam instead, there are both released and
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
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?
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
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
Oh great, I'll toy with both options then, thanks a lot!
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
I show some Makefile and Dune structure/ideas here: https://github.com/palmskog/coq-program-verification-template
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.
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
I just had a look at the aforementioned Recommended Project Structure and I noticed that the section "
Makefile.coq.local" talks about
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
@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.
Last updated: Feb 04 2023 at 02:03 UTC