4

標準ライブラリを使用するAgdaプログラムをコンパイルすると、コンパイラは次のような行を出力するのに長い時間を費やします。

Skipping Relation.Binary.Consequences (/home/owen/install/lib-0.6/src/Relation/Binary/Consequences.agdai).
Skipping Relation.Binary.Indexed.Core (/home/owen/install/lib-0.6/src/Relation/Binary/Indexed/Core.agdai).
Skipping Relation.Binary (/home/owen/install/lib-0.6/src/Relation/Binary.agdai).

それらを安全に「スキップ」する理由は、それらがすでにコンパイルされているためだと思います（ディレクトリにはすでに.agdaiファイルがあります）。しかし、それでもそれらをスキップするのに多くの時間を費やし、コンパイルには1分以上かかります。

すべてのコンパイルでこの余分な作業をすべて回避する方法はありますか？

4

2 に答える 2

1

Agda は、これらの .agdai ファイルの少なくとも一部をメモリにロードして、独自のコードを型チェックできるようにする必要があります。そのため、これらのモジュールのチェックがスキップされたとしても、まだ時間がかかる可能性があります。

于 2012-10-21T01:18:58.837 に答える
0

Agda や coq などの他の同様のソフトウェア システムには、通常は emacs にインストールされている Proof General を介して利用できるインタラクティブなインターフェイスがあります。

プログラミング言語は外部シンボルの浅い名前チェックに依存する傾向があるため、モジュラー コンパイルは他のコンテキストで機能します。Agda は証明システムであるため、機能を果たすには、毎回ゼロから始めて、証明全体を詳細に検証する必要があります。

于 2012-09-16T21:41:46.017 に答える