問題タブ [coqide]

I want to retrieve the result of the compilation of a file. v from coqide or coqc for treated with java, rather I have treatment of an automaton and I want to build a graphical interface of this automaton in java.

Thanks for your response.

このページで見つけた CoqIDE for vim プラグインを使用しようとしています。

~/.vim/ftplugin フォルダに coq_IDE.vim ファイルを置きます。私の現在の .vimrc ファイルは次のとおりです。

しかし、vim を起動しても、CoqIDE は自動的にロードされません (通常の vim と比べてまったく変化が見られないので、そうではないと思います)。コマンドで手動でロードしようとすると:source coq_IDE.vim、次のエラーメッセージが表示されます。

このエラーの原因は何ですか?

関連する可能性のある追加情報を次に示します。

1) Ubuntu 14.04 を実行しています。

:version2) vim shows で確認しました+perl。

2) gvim ではなく、端末から vim を実行しています。

3）異なるバージョンのvim（vim、vim-gtk、vim-gnome）を削除して再インストールしようとしました

4) CoqIDE インストール ガイドには、変数coqtop.optを介してアクセスできる必要があると記載されています。PATHこれが何を意味するのかさえわからないので、これがここでの問題かもしれませんが、そうではないようです。私が理解していることから、 vim を読み取ろうとするとエラーが発生するcoq_IDE.vimため、探している部分に到達することさえできませんcoqtop.opt。

5) Ubuntu Software Center から CoqIDE をインストールしました。

6）:echo &runtimepath私は得る：~/.vim,/var/lib/vim/addons,/usr/share/vim/vimfiles,/usr/share/vim/vim74,/usr/share/vim/vimfiles/after,/var/lib/vim/addons/after,~/.vim/after

Coq ファイルを編集するために、Linux マシンでVim 用の CoqIDE プラグインを使用しています。今、私はそれを Windows 8 にインストールしようとしています。しかし、プラグインを入手しようとすると、

これは奇妙なこと:versionです+perl/dyn。これは私が必要とするものとは異なり+perlますか?

Perl対応のVimを入手するには、Vimの前にPerlをインストールする必要があるとどこかで聞いたので、それも試しました。Vim をアンインストールし、Strawberry Perl 5.18.2.2 (64bit)をインストールして、Vim を再インストールしました。それでも同じ問題です。

解決策にバイナリを手動でコンパイルすることが含まれる場合、経験がないため、詳細な手順をいただければ幸いです。

CoqIDE Vim プラグインを Windows 8.1 で動作させようとしています。Vim からプラグインを入手すると、次のエラー メッセージが表示されます。

そこで、プラグインのドキュメントを調べたところ、関連していると思われる部分が見つかりました。

これが何を意味するのかはわかりcoqtopませんが、vim から見えるようにする必要がある名前のファイルまたはディレクトリがあると推測しています。そこで、Coq インストール ディレクトリを開いて を検索しましたcoqtop。検索ヒットは次のとおりです。

ここで明らかな最初の候補は ですcoqtop。クリックすると、インタラクティブな Coq コンソールが開きます。しかし、let CoqIDE_coqtopコマンドを使用してこのファイルを Vim にリンクし、プラグインを再度ロードすると、次のようになります。

問題があると思われるもう 1 つの点は、ファイルの種類です。上記のエラー メッセージからわかるように、coqtopファイルには.exeMS-DOS および Windows に固有の拡張子が付いています。.exeしかし、プラグインがファイルで動作するように書かれているとは思いません...

また、他のすべての検索ヒットを として使用しようとしましたcoqtopが、役に立ちませんでした。

これは、プラグインが Windows では役に立たないということですか? 誰かが確認できれば、あきらめて他の IDE を使用します。でも、できればVimを使い続けたいです。

rlwrapREPLループ内で矢印キーを処理する優れたプログラムです。ほとんどの場合、それは機能します。たとえば、、などrlwrap sbclですrlwrap sml。しかし、 になるrlwrap coqtopと失敗します。エラー情報は以下です。 rlwrap: error: Couldn't read completions from /usr/local/Cellar/rlwrap/0.41/share/rlwrap/completions/coqtop: No such file or directory

coqidecoq の Web サイトからダウンロードrlwrapし、 homebrew. ファイル/usr/local/Cellar/rlwrap/0.41/share/rlwrap/completions/coqtopは適切な場所にあります。それで、これを修正する方法の手がかりはありますか？それとも代わりになるソフトはありますか？

私は Coq 初心者なので、プルーフ チェックの理解を深めるために、Ssreflect ライブラリを使用しようとしています。

ターミナルで動作する Mac OS v 10.10.3 ( Yosemite ) に Ssreflect v 1.5 をインストールしました。

ただし、次を使用してライブラリを CoqIDE 8.4p15 にロードしようとしたとき:

エラーが発生します：

私は使用してみました：

SSRCOQ_LIB は現在設定されていますが、次のエラーが表示されます。

CoqIDE 内から ssreflect ライブラリをロードする際の助けに感謝します。

ほとんどの IDE またはテキスト エディターでは、用語を右クリックすると、その用語が定義されているファイルに移動できます。CoqIDE にはそれがないようなので、私は を実行coqdoc myfile.v --htmlしてから、生成された HTML ドキュメントに移動しました。しかし、そのファイルでクリックできる用語は、Coq 標準ライブラリに関するものだけです。ssreflect で定義された用語 (たとえば) はクリックできません。

Coqファイルで、用語/識別子が定義されている場所(およびそのソースコード)をすばやく検索できる標準的な方法はありますか? CoqIDE または emacs + ProofGeneral (私は CoqIDE を使用していますが、emacs/ProofGeneral にこの機能があれば切り替えます)。

それとも、使用するすべての Coq プロジェクトと依存関係のドキュメントを生成する標準的な方法ですか?

CoqIDE 内で次のコマンドを実行すると:

次のエラーが表示されます。

代わりに試してみると：

エラーが発生します：

MacOSX 用の CoqIDE 8.5beta3 を使用しています。

どうすればこれを修正できますか? 権限の問題なしに CoqIDE を介して抽出を行うにはどうすればよいですか?