問題タブ [opam]

coq HelloWorld チュートリアル(以下のコード) に従っていましたが、プログラムをコンパイルできませんでした。インストール手順に従って、インストールしopam install coq:io:systemました。私の opam インストールはデフォルトの場所にあります~/.opam。それでも、エラーが発生しました

これは、emacs/proofgeneral または coqide (8.4pl6、ubuntu 14.04) のいずれかです。問題を解決する方法を知っている人はいますか?

hello_world.v以下は、 emacs/coqideという名前のファイルにコピーしてロードしたコードです。

- アップデート - -

@gtzinos、https://github.com/clarus/coq-hello-worldの readme に従いました。今回は についてのクレームはありませんでしたが、見つからないSystem.effectsという新たなエラーが発生しました。Extraction.launch私は試した：

そして得た：

フォルダにも入れようとしmakeましたextractionが、成功しませんでした。ポインタはありますか？

opamをインストールし、uint パッケージをインストールしました。しかし、私がこのようなことをしようとすると

エラーが発生します

私が見逃している可能性があるものについて何か提案はありますか? 私はOCamlとopamが初めてです

次のステートメントを使用して、OSX ターミナルでコードをコンパイルしました。

opam list -aOPAMで現在利用可能なすべてのパッケージをリストしますが、opam list --help出力に従って、現在インストールされていないパッケージのバージョン番号は表示しません:

(...) 出力形式では 1 行に 1 つのパッケージが表示され、各行にはパッケージの名前、インストールされているバージョン、または -- パッケージがインストールされていない場合は (...)

バージョン番号を含むすべてのパッケージを一覧表示するにはどうすればよいですか?

コンパイラのバグ (LLVM IR をビルドするときのセグメンテーション違反) を追跡するためにアサーションを有効にして LLVM 3.6 をローカルで再コンパイルする必要がありますが、いくつかのエラーが発生します。

1: opam が LLVM ライブラリを見つけられません:

しかし

libllvm の特定のディレクトリを調べるように opam に指示するにはどうすればよいですか?

編集：LLVMのコンパイル時にこの構成を使用して解決しました：

opam updateその後、 OPAMopam upgradeは 10 個のパッケージをより新しいバージョンにアップグレードしたいと考えています。

ただし、うっかり何かを壊してしまうことを恐れて、他のパッケージには触れずに、 1 つのパッケージだけをアップグレードしたいと考えています。このパッケージには依存関係がなく、他のパッケージは依存していないようです。

ただし、これを実行opam upgrade <package>すると と同じ結果になりopam upgradeます。つまり、OPAM は、必要なパッケージだけでなく、10 個のパッケージすべてをアップグレードしようとします。

も試しopam install <package>.<new version>ましたが、一度にすべてをアップグレードしたいと考えています。

他のパッケージに触れずに、この 1 つのパッケージだけをアップグレードする方法はありますか? 理論的には壊れてはいけませんが、実際には壊れることがよくあります...

opam を使用してロープをインストールし、使用できることを確認しました。

rope 0.5 Ropes ("heavyweight strings")

しかし、それをロードする方法?? ドキュメントには使用する必要があると記載され#load "rope.cma";;ていますが、これによりメッセージが表示されますCannot find file rope.cma.

誰かがそれをロードするための呪文を教えてもらえますか??