CODEWITHSUNDEEP
makefilecoqocamlbuild
Quyen
Quyen

Reputation: 1373

Makefile with coqtop -R coqdir

I have a makefile:

Add the command: coqtop -R coqdir I have to give a physical path in my computer, but this directory depends on user directory. (~/color/trunk/color/devel/gwen Devel and ~/color/trunk/color CoLoR).

Is there another way to call and combine a program without given the physical path?

tmp/rainbow.native: tmp
coqtop -q -R ~/color/trunk/color/devel/gwen Devel -R ~/color/trunk/color CoLoR 
-batch -load-vernac-source extraction.v && 
(cd tmp && ocamlbuild -j 3 rainbow.native)

tmp:
    mkdir -p $@

Upvotes: 1

Views: 422

Answers (2)

Tom Prince
Tom Prince

Reputation: 682

With coq v8.4, you can set the environment variable COQPATH to a colon separated path (probably semi-colon separated on windows), and coq will treat those directories as if it was passed -R <directory> ''. In other words, it will recursively add all files, with a null prefix.

Also by default, coq v8.4 will automatically treat ~/.local/share/coq (technically ${XDG_DATA_HOME}/coq) the same way. Thus, you could just link the appropriate directories there, with the appropriate names (i.e. Devel and CoLoR).

Upvotes: 0

MadScientist
MadScientist

Reputation: 100836

This is what the $PATH environment variable is for: you add directories to it where programs you want to be run will be found. Basically there's no way make, or your makefile, can search the entire computer for the coqtop program so the person invoking the makefile has to know where it is and inform the makefile.

Usually this is done by the person who knows where the program is, adding the directory containing the program to their $PATH environment variable before they invoke make.

If you don't want to go that way, then they will need to set a variable on the make command line that points to the location: make DEVEL=$HOME/color/trunk/color/devel or similar. Or they can set the path in an environment variable (make always imports all environment variables as makefile macros).

As another option, you can use (assuming you're using GNU make or a make that supports it) -include local.mk then have them create a file local.mk in their directory that sets this variable before they run make; this way they can create that file with the proper path one time and be done with it.

These are about your only options, unless there is some way you can algorithmically determine the path you want based on, for example, the current directory or the directory containing the makefile (which you seem to be saying there isn't).

Upvotes: 1

Related Questions