Coqの定理の高速計算

Question

非常に単純な場合でもCoqが計算を終了するまで待たなければなりません。

「非同期および並列プルーフ処理」については知っていますが、私のコードには固有の悪意があると思われますので、 ガイドライン/プルーフのスタイリングのベストプラクティスに参考にしてください。 例えば：

1. は、代わりに定理の定義を使用するように

2. 使用コンパイラを試してみてください。 parrallel処理を使用します。より良いハードウェアを使用してください。

3. （@functionname VAR1 ... VARN）

4. セミコロンのように、すべての引数を埋め、プレースホルダを使用しないでください（;）（。）の代わりにピリオドの

5. 使用することがはるかに高速ですセクションの定義を "set（f：= term）"の代わりに使用します。証拠に（おそらくすべての「セット」が印刷されるために余分な時間がかかるからです。）

Coqを加速するには？ （上記の項目に間違いがあるかどうかは、私の実践から得られたものです）

計算の最も重要な段階は何ですか？

Answer 1

聖杯はコードをプロファイルし、ホットスポットを最適化することです。 Coq> = 8.6では、戦術をプロファイルするためにSet Ltac Profiling.とReset Ltac Profile.とShow Ltac Profile.を使用できます。 -time引数を使用してcoqcを呼び出すと、行単位のタイミング情報が取得されます。 sed詐欺のビットは、あなたのための情報をソートすることができます：コックで

coqc -time foo.v | sed s'/^\(.*\) \([0-9\.]\+ secs.*\)$/\2 \1/g' | sort -h 

を> = 8.8、あなたはネイティブコンパイラをプロファイルにSet Native Compute Profilingできるようになります。他のボトルネックに遭遇した場合、推測に熟練していること、デベロッパーにプロファイリングツールを追加すること、実行中のcoqバイナリをプロファイリングすること、コードをプロファイリングする価値があることをdevsに説得することが必要です。 （遅れがCoqの効率バグを指しているときに、Pierre-MariePédrotに自分のコードをプロファイルすることがあります）

1つの有用なプラクティスは、常に1回のコミットごとにコードをプロファイリングすることです。 Coq> = 8.7では、ターゲットmake-pretty-timed-before、make-pretty-timed-after、およびprint-pretty-timed-diffがあり、レポの2つの状態間でのファイルごとのコンパイル時のdiffの素敵なソートテーブルが得られます。 make TIMING=before、make TIMING=after、make all.timing.diffで1行の情報を得ることができます。

あなたはまた、おそらくその紙（pdf）（pptx with presenter notes）のプレゼンテーション用スライドデッキExperience Implementing a Performant Category-Theory Library in Coq（複数のメディアhere）を見に興味がある、とあります。

---

Coqは、いくつかの場所で遅くなる可能性がありますが、あなたが言及するもののほとんどは無関係です。ために、あなたの通って行く：

1. TheoremとDefinitionは同義語であり、唯一の違いは、Definitionが:=をサポートし、Theoremがないということです。
2. Coqの最適化コンパイラはありませんが、ハードウェアは増えますが、RAMが増え、CPUが高速ですが、間違いなく助けになります。並列処理も同様です。このノートでは、ファイルレベルの並列処理は、プルーフレベルの並列処理よりも優れている傾向があります。できるだけファイルを分割し、ライブラリ読み込み時間に問題がないようにきめ細かい読み込みを行い、make -jを使用する傾向があります。
3. すべての引数を埋めることは、助けようとするよりも傷つきやすいでしょう。特にあなたが引数を埋める条件が大きい場合は、追加の統一コストが発生します。あなたが議論を記入することによってあなたがする真のことは、統一に対するエバールの創造を取引することです。通常、統一はより遅い。しかし、標準構造の解決、型クラスの解決、または他のバックトラックやアンフォールディングやユニバース変数のリフレッシュが必要な穴がある場合は、それらを埋めることで多くのことをスピードアップできます。
4. プルーフスクリプトのセミコロンとピリオドの違いは、対話モード（coqtop/CoqIDE/ProofGeneral/etcでは、makeを実行しているときではなく）でのみ重要だと思います。あなたがそれを試して、それ以外のものを発見すれば教えてください。
5. これは非常に真実であり、印刷やその他の作業にも影響します。 set自体は印刷のために遅くなるのではなく、あなたの目標の中にある用語のすべての出現箇所を見つけようとしているからです（愚かなことに、幾分かの減量（ベータイオタ？私は想起できません）構文上の平等よりも高い）、それらを新しい仮説に置き換える。この動作が必要ない場合は、setではなくposeを使用してください。さらに、大きなコンテキスト変数は、コンテキストのサイズに依存する戦術を減速させる可能性があります。そのため、Definitionの方が高速です。私はに実行したもので

その他の思考：

• 良い抽象化障壁を選んで、宗教的にそれらを尊重しています。あなたは抽象的な障壁を破るたびに汗や涙を払います。 （良い抽象化の障壁を選ぶことは信じられないほど難しいですが、通常、私は既存の数学的抽象化または公開された論文をコピーすることでこれを行います。 "Cのようなコードを書くときには、すべての関数が引数として1つのタプルをとり、その結果として1つのタプルを返します。"）
• 反射的な証明を行っているなら良いアルゴリズムを選ぶ。単項自然数を使用するか、アルゴリズムの実行時間が指数関数的に変化する場合、証明は遅くなります。
• Coq < 8.7では、エバールマップの正規化により大規模なオーバーヘッドが発生します。
• スローEnd Section（時には遅いDefined）は、頻繁にrehashconsingの問題が原因で発生します。これは、EConstrブランチでこれを修正するためのProps from Pierre-Marieです。これを解決するには、指を交差させて祈ってください。
• 巨大なボディを持つ裸のfix（おそらく、ベータ - イオタ - ゼータレキシックスの存在下でのみ？）をチェックする際に、守備チェッカーは非常に遅いです。回避策は、ボディを別の定義に抽出することです。例えば、むしろ

 
Fixpoint length A (ls : list A) : nat := 
    match ls with 
    | nil => 0 
    | cons _ xs => S (length _ xs) 
    end. 

を書くよりも、あなたは

 
Definition length_step 
      (length : forall A, list A -> nat) 
      A (ls : list A) 
    : nat 
    := match ls with 
     | nil => 0 
     | cons _ xs => S (length _ xs) 
     end. 
Fixpoint length A (ls : list A) : nat 
    := length_step length A ls. 

• はコックが簡単に指数関数定義内在時間につながることができます自由に（時には一貫性なく）インラインlet x := ... in ...文、ことに注意して書くことができます。
• 標準化の構造は高速ですが読みにくいですが、Ltacは約2倍遅く、typeclassの分解能は2倍遅くなります（またはLtacと同じスピードになります）。うまくいけば、Ltac2が終了したらもっとうまくいくだろう。
• simplは、大規模な用語

私は戻ってくると、後にさらに追加する（と私は追加するためのコメントで物事を示唆して自由に感じる）ことに非常に遅いですが、これは半分まともなスタートです。