The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/11/2015 09:50 AM, Pierre Boutillier wrote:
> ...
> Writing email helps to gett idea !
> How geeky adhocky gorky would it be to have a policy like 'a special suffix 
> for such files’ ?
> Let say all files ending by .test.v (I’m not happy by this extension please 
> propose one if you thing the general idea is good) are files not to compile.
> as they are .v files, coqdep, coqide, coqdoc, proof general will behave 
> correctly with them for free.
> Making a rule so that make all « process them instead of compile them » is 
> doable.
> Adding a $(filter-out %.test.v,$(VFILES:.v:=.vo)) in install targets is 
> trivial !

I don't think that deciding what make rule is used for a file based on 
its suffix - even one like .test.v - is "geeky adhocky gorky" at all.  
But, there is always a small chance that such changes would cause 
compatibility problems if such suffixes are already in use.

Would it be much more difficult to add some declarative annotation to 
file lines in _CoqProject?  In other words, for any file on a line with 
no annotation, assume the current coqc rule - but for lines that look like:

foo.v        coqtop

process them with coqtop instead.

One could even extend this syntax further to file-specific options - 
which could also appear on the same line - like:

bar.v        -noinit
baz.v        coqtop -noinit

Or, allow the use of named rules so that common options can be collected 
together:

!rule1        coqtop -noinit
bar.v        rule1
baz.v        rule1

I know this is beginning to sound like it is reconstructing make - but 
it is still leaving out the most fragile and ugly parts of make while 
still giving the user control over how individual files are processed.

-- Jonathan