The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
Sorry for not answering earlier.
The short answer is no.
The longer answer is ask for listing what does it means to put « Foo.v » in a 
_CoqProject file and what you would expect for « TestSuite1.v » or «  
Example1.v ».

- it makes a makefile rule to compile it (make a vo). You would expect a 
makefile rule to load it (be sure it works) Thus rules are annoying to do in 
Makefiles as they do not produce anything but we could imagine generating 
dummy TestSuite1.checked file as a standard workaround.
- it builds up a machinery to install it. You would expect it not to be 
installed.
    So far, it looks like the following lines would be a solution
    -extra '%.checked' '%.v' '$(COQBIN)coqtop $(COQARGS) -load-vernac-source 
$^ && touch $@' 
    -extra-phony 'all' 'TestSuite1.checked' ''
but it also
- asks coqdep for the dependencies of TestSuite.v and include them in the 
makefile in order that make do things in the right order !
    You can do it by hand but this starts to be really annoying and fragile
- coqdoc it and generate an installation rule for this documentation. That 
would be enjoyable to have that fro examples and tests …
Mainly, 
- Coqide and proof general now use the _CoqProject to automatically set the 
arguments of coqtop while it starts to process it (the -R the -Q the -I and 
the args of -arg)
and you won’t simulate that with any -extra dark magic …

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 !

Pierre B.
PS : I’ve voluntary put under the carpet the « files only to produce 
extracted code » part as dependency management in thus place is an 
independent horrible question :-)


> Le 3 janv. 2015 à 17:53, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  a écrit :
> 
> Is there a way to specify that some script files in a _CoqProject file 
> should be put into the Makefile such that they are processed by coqtop 
> instead of coqc?  For instance, I have some scripts that are only used to 
> produce extracted OCaml - and so compiling them is a waste.  Unit test 
> scripts are another example.
> 
> I keep having to re-arrange my Makefile to do this by hand after it is 
> re-generated by coq_makefile.
> 
> -- Jonathan
>