search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

Redundancy in _CoqProject #1

Closed palmskog closed 6 years ago

palmskog commented 6 years ago

Why not just have the contents of Make in _CoqProject and use the latter as argument to coq_makefile? This both gives a canonical definition of namespaces/files and allows IDEs like ProofGeneral and coqide to find the files.

anton-trunov commented 6 years ago

It has been modeled after math-comp library as many things in fcsl.

In principle, this separation of concerns between the build system and the IDE support offers finer control.

palmskog commented 6 years ago

While I generally like math-comp conventions, I disagree strongly with this one. The _CoqProject file is the closest Coq has to a build system convention, and is what made our work on incremental proving in CI systems possible. I was hoping to use fcsl-pcm in future proof engineering research, and listing project files in _CoqProject would help a lot.

anton-trunov commented 6 years ago

Oh, so you'd like to use the name _CoqProject as part of the interface to the build system. Yeah, makes sense.

palmskog commented 6 years ago

Thanks!