The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Hi everyone,

Have you had a look at using Dune for your Coq projects? Coq support
in Dune is still alpha but already used in more and more projects and
it has the major advantage of producing hygienic builds.

This is not to say that hygienic builds couldn't be added to
coq_makefile as well, but with Dune on the horizon, I don't think you
can count on any of the main developers to fulfill this request.

Some references on Dune:

https://coq.github.io/doc/v8.12/refman/practical-tools/utilities.html#building-a-coq-project-with-dune
https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory
https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20
https://coq.discourse.group/t/compilation-output-files/734
https://github.com/coq-community/templates (can generate basic Dune
files if you add "dune: true" to your meta.yml)

Cheers,
Théo

Le lun. 13 juil. 2020 à 10:41, Ralf Jung <jung AT mpi-sws.org> a écrit :
>
> Hi,
>
> unless that has already been done, IMO it is reasonable to report this as a
> feature request against coq_makefile.  I'd also prefer the Coq build to not
> clobber the source directory.
>
> Kind regards,
> Ralf
>
> On 13.07.20 06:42, Chris Dams wrote:
> > Hello Erkki,
> >
> > I have a Makefile for this purpose. The files that are build end up in the
> > 'build' directory. Contents is below. Coqide does not always work 
> > optimally with
> > this, though. It seems to like the aux files in the same directory 
> > sometimes.
> > But it does not prevent you from editing with coqide. Sometimes one just 
> > has to
> > press the down error twice to make it start compiling.
> >
> > Good luck,
> > Chris
> >
> > target: build/redblack/redblack.vo
> >
> > SRC = $(shell ls */*.v)
> >
> > ifneq ($(MAKECMDGOALS), clean)
> > -include $(addprefix build/,$(SRC:.v=.d))
> > endif
> >
> > target:
> >    @echo succeeded building $^
> >
> > build/%.d: %.v
> >    @echo coqdep $<
> >    @coqdep -R . Lib $< | sed 's/\([a-zA-Z0-9\/_]*.vo\)/build\/\1/g' > $@
> >
> > build/%.vo: %.v
> >    @echo coqc $<
> >    @coqc -R . Lib -o $@ $<
> >
> > clean:
> >    rm -f build/*/*.vo build/*/*.glob build/*/*.d build/*/.*.aux
> >
>
> --
> Website: https://people.mpi-sws.org/~jung/