問題タブ [proof-general]

質問する

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

38 問題
Newest
Active
Bountied
318
Unanswered
0 投票する
1 に答える
121 参照

emacs - 依存型を持つ認定プログラミングをセットアップできません

依存型を使用した認定プログラミングという本を使用していますが、毎回別のエラーが見つかります。このエラーは、Proof General からのコンパイル プロセスと、本のソースの makefile によるコンパイル プロセスとの不一致から発生しているように思えます。

  1. ソースを make でコンパイルし、たとえば Proof-General で Subset.v を実行しようとすると、次のようになります。

エラー: ファイル /home/usuario/Desktop/Coq/cpdt/src/CpdtTactics.vo に不正なマジック番号 81100 (予想される 8600) があります。壊れているか、別のバージョンの Coq でコンパイルされています。

  1. make clean で makefile コンパイル済みファイルを消去し、require の前にオプション Coq -> Auto Compilation -> Compile を続行しようとすると、次の行になります。

抽出が必要です。

それは失敗します。もともとはエラーで失敗しました：

エラー: ライブラリ抽出が見つかりません。

ただし、上記のオプションを有効にすると、次のようになります。

echo "抽出が必要です。" > /tmp/ProofGeneral-coqQPJTf0.v coqdep -Q /home/usuario/Desktop/Coq/cpdt/src/ -R /home/usuario/Desktop/Coq/cpdt/src Cpdt /tmp/ProofGeneral-coqQPJTf0.v ※警告: ファイル /tmp/ProofGeneral-coqQPJTf0.v で、ライブラリの抽出が必要ですが、ロードパスに見つかりませんでした! *警告: ファイル /tmp/ProofGeneral-coqQPJTf0.v で、ライブラリの抽出が必要ですが、ロードパスに見つかりませんでした! /tmp/ProofGeneral-coqQPJTf0.vo /tmp/ProofGeneral-coqQPJTf0.glob /tmp/ProofGeneral-coqQPJTf0.v.beautified: /tmp/ProofGeneral-coqQPJTf0.v /tmp/ProofGeneral-coqQPJTf0.vio: /tmp/ProofGeneral-coqQPJTf0 .v

どうすればこれを解決できますか?


12345678910