Add COQBIN to configure.ac

[Villetaneuse]

• A COQBIN variable, if set and non-null is prepended to the PATH in configure.ac. The variables COQC, COQDOC and COQTOP now contain an absolute path.
• I have also changed BINDIR so that it remains the parent directory of whatever is COQC.
• In this case, if the OCAMLPATH variable is not set, a warning is emitted during ./configure (because the user probably wants the coq ml libs to be those corresponding to its current coq build)
• Other cleaning made in Makefile.in, using variables COQC COQTOP and COQDOC rather than fixed commands.
• make archi_clean now cleans more
• small addition in .gitignore (swap files for vim)

closes #127

[Villetaneuse]

As a side remark, I tested that without COQBIN set it does indeed use the usual PATH search. But, I never had a build which builds and passes the tests other than Coq master, because I suspect some recent change makes your coq-master branch incompatible with even coq-8.18.

However, since you have regular tags for coq-versions, this seems ok. If that's intended, maybe this could be written somewhere that your coq-master branch is only meant to be compatible with coq's master branch.

[ybertot]

Yes, PR requests merged as soon as mid august make coq-master incompatible with coq-V8.18.

[ybertot]

Will this work as expected when users set COQBIN to the empty string (which I assume should have the same meaning as having COQBIN not set).

I believe something like test "a$COQBIN" != "a" is more resilient.

[Villetaneuse]

Will this work as expected when users set COQBIN to the empty string (which I assume should have the same meaning as having COQBIN not set).

I believe something like test "a$COQBIN" != "a" is more resilient.

In today's POSIX shell this is usually all right. But you are right, I would not bet on it with m4sh... I force-pushed your suggestion (did so with OCAMLPATH too).