1

私はメイクファイルを持っています：

コマンドを追加しcoqtop -R coqdirます。コンピューターに物理パスを指定する必要がありますが、このディレクトリはユーザー ディレクトリに依存します。( ~/color/trunk/color/devel/gwen Devel and ~/color/trunk/color CoLoR)。

物理パスを指定せずにプログラムを呼び出して結合する別の方法はありますか?

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 $@
4

2 に答える 2

1

これが$PATH環境変数の目的です。実行したいプログラムが見つかるディレクトリをそれに追加します。基本的にmake、またはメイクファイルがコンピューター全体でcoqtopプログラムを検索できる方法はないため、メイクファイルを呼び出す人は、それがどこにあるかを知り、メイクファイルに通知する必要があります。

通常、これは、プログラムの場所を知っている人が実行し、プログラムを含むディレクトリを$PATH環境変数に追加してから、 を呼び出しmakeます。

そのようにしたくない場合は、makeコマンド ラインで場所を指す変数を設定する必要がありmake DEVEL=$HOME/color/trunk/color/develます。または、環境変数にパスを設定することもできます (make常にすべての環境変数を makefile マクロとしてインポートします)。

別のオプションとして、(GNU make またはそれをサポートする make を使用していると仮定して) を使用して、実行前にこの変数を設定-include local.mkするファイルをディレクトリに作成させることができます。このようにして、適切なパスでそのファイルを一度作成すれば、それで完了することができます。local.mkmake

これらは、現在のディレクトリやmakefileを含むディレクトリなどに基づいて、必要なパスをアルゴリズムで決定できる方法がない限り、唯一のオプションに関するものです(そうではないと言っているようです)。

于 2012-03-20T14:53:09.687 に答える
0

coq v8.4 では、環境変数COQPATHをコロンで区切られたパス (Windows ではセミコロンで区切られている可能性があります) に設定でき、coq はそれらのディレクトリを渡されたかのように扱い-R <directory> ''ます。つまり、null プレフィックスを付けて、すべてのファイルを再帰的に追加します。

また、デフォルトでは、coq v8.4 は自動的に~/.local/share/coq(技術的${XDG_DATA_HOME}/coqに) 同じように扱います。Develしたがって、そこにある適切なディレクトリを適切な名前 (つまりと)でリンクするだけですCoLoR。

于 2012-03-31T05:27:33.033 に答える