問題タブ [coqide]
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.
windows - CoqIDE Make on Windows
GnuWin32 MakeとGnuWin32 Coreutilsがインストールされており、PATH. これは機能します：
しかしFrap.v、CoqIDE で開いてCompile > Make を実行すると、次のような出力しか表示されません。
これは期待されていますか？Coqにこれをビルドさせるにはどうすればよいですか?
coq - Coq コードを分割して Coq ideslave (XML プロトコル) にフィードする方法は?
Coq ideslave (Coq XML プロトコルとしても知られる) の "Add" 呼び出しは、一度に 1 つのコードのチャンクをピリオド ( .) で分割する必要があると思いました。私は今でも、ほとんどの場合、これが真実であると信じています。例えば、
このコード ブロックには複数の行がありますが、最後の行だけにピリオドがあるため、1 回の "Add" 呼び出しで入力する必要があります。
+ただし、箇条書き ( 、-、*、{、および}) がある場合は、この限りではありません。例えば、
2 つの「追加」呼び出しによって入力する必要があります-。intros [H _]; exact H.別のケースでは、
{、destruct Hl; [ right | destruct Fl | ]; assumption.、およびの 3 つの部分として供給する必要があり}ます。Coq IDE でこれらの動作を観察しましたが、これは内部で Coq ideslave を使用していると思います。
私の最初の質問: これらは、「追加」呼び出しを使用するために .v ファイルをチャンクに分割するための完全な規則ですか? いいえの場合、完全なルールは何ですか?
2 番目の質問: "partitioned-by-period" ルールのみを使用する場合、たとえば{ destruct Hl; [ right | destruct Fl | ]; assumption. }、3 回ではなく 1 回の "Add" 呼び出しとしてフィードしようとすると、XML はすぐにエラーを発生させません。ただし、いくつかの証明手順の後This proof is focused, but cannot be unfocused this way、Coq IDE には表示されないエラー ( ) が発生する可能性があり、エラーを元に戻すことはできません。
エラーを元に戻そうとすると、Coq XML で同じエラー メッセージが表示されます。このエラーは、弾丸を 1 つのチャンクとして供給することに関連していますか? はいの場合、チャンクをフィードすると、Coq XML がこれについて文句を言わないのはなぜですか?
追加の質問: 近い将来、SerAPI を試してみたいと思います。SerAPI は、コード チャンクの供給に関して同じルールを共有していますか?
助けてくれてありがとう！
coq - CoqIDE のインストール - jhbuild の更新に失敗しました
Coq は既にインストールされていますが、Mac に CoqIDE をインストールしようとしています。Coq wikiをフォローしています。ビルドは 2 番目のステップで失敗します。私が走るとき
sh gtk-osx-build-setup.sh
これは私が得るエラーです:
助けていただければ幸いです。