人力検索はてな
モバイル版を表示しています。PC版はこちら
i-mobile

libcvc3.so.3ファイルについて入手方法、または代用についてご存知の方はいらっしゃいませんか?

js-symbolic-executorという既製品(フリー)の環境構築をを行なっています。

==質問内容==
libcvc3.so.3の入手方法についてご存知の方はいらっしゃいませんか?
libcvc3.so.5やlibcvc3.so.2などで代用は可能でしょうか?


==質問の経緯==
補足に要点をまとめたものを記述させて頂きます。

(詳細な経緯は:http://ruzxa.hatenablog.com/entry/2014/11/22/014638より。あまり纏まっておらず申し訳ありません。)

●質問者: ruzxa
●カテゴリ:コンピュータ
○ 状態 :終了
└ 回答数 : 2/2件

▽最新の回答へ

質問者から

make実行時に下記のエラーが出ました。

make終了間際のログ**


Unpacking parser
Unpacking translator
Unpacking vcl
Unpacking c_interface
cat UNPACKED | xargs g++ -shared -m64 -fPIC \
 -Wl,-soname,libcvc3.so.3 -o '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0' `` -lgmp 
/sbin/ldconfig -nv /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu
/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu:
<span style="color: #cc0000">libcvc3.so.3 -> libcvc3.so.3.0.0/sbin/ldconfig.real: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3 から libcvc3.so.3.0.0 へリンクできません</span>
 (スキップされました)
ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0
<span style="color: #cc0000">ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです</span>
<span style="color: #cc0000">make[2]: *** [/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0] エラー 1
</span>
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make[1]: *** [build] エラー 2
make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make: *** [build] エラー 2


libcvc3.so.3からlibcvc3.so.3.0.0へリンクが出来ておらず、libcvc3.so.3ファイルがないのがそもそもの問題かと思われます。


名前の少々似たファイルとしては、libcvc3.soに関する記述があり(探しているのはlibcvc3.so.3ファイル)
cvc/java/READMEのヘルプ
http://js-symbolic-executor.googlecode.com/svn/trunk/cvc3/java/READMEより抜粋

3.4 Installation
----------------

"make install" copies libcvc3jni.so into the same directory as
libcvc3.so (by default, /usr/local/lib) and the Java library into
the directory specified by javadir (by default, /usr/local/java).

そこで上記より、js-symbolic-executoe既成品の中や、/usr/lib/bin、JAVA_HOME(jdk1.8.0_40)内を探したのですが見つかりませんでした。
また、windows上のjdkにおいてもJdk 1.9.0,1.8_25,1.8.0_20にはありませんでした。

ネット上にはlibcvc3.so.2やlibcvc3.so.5などがあったり、
apt-getコマンドにて
maru@marU:/$ sudo apt-get install libcvc3-
libcvc3-5 libcvc3-5-java libcvc3-5-jni libcvc3-dev
と出るなど似たような名前のファイルは公開されており、ネット上から拾ってくるような種類のものに感じています。


1 ● tea_cup

後半の質問は、答えられます。
Linux共有ライブラリの簡単なまとめ - wagavulinの日記を読むと、soの後の数字が変わるとインタフェース非互換とあるので、http://www.cs.nyu.edu/acsys/cvc3-releases/current/ とかからファイルを持ってきても動かないでしょう。


ruzxaさんのコメント
>|| Linuxで共有ライブラリ(*.so) ライブラリを作るときは.c -> .o -> .soの順に作るが -Wl,-soname=libhoge.so.1 -o libhoge.so.1.0 といったコマンドはmakeで見かけました。 呼び方 意味 例 soname lib + ライブラリ名 + .so + バージョン libhoge.so.1 real name sonameにマイナー番号、リリース番号を付けたもの libhoge.so.1.0.0 real nameに付くマイナー番号やリリース番号は互換性のある変更を行ったときに上げる。公開インターフェースは変えず、内部のバグフィックスのみなどのときである。また、関数の追加だけの場合も互換性は保たれる。 sonameに付くバージョンは、インターフェース非互換になったときに上げる。つまり、既存の関数の引数を変えた場合や、公開している構造体のメンバ変数を変えた場合などである(構造体の末尾に追加するだけなら互換らしい)。 ||< libcvc3.so.3がどういった種類のファイルかということすら知らなかったのでとても勉強になります! ご回答頂き、本当にありがとうございました。 ==以下、個人的な思考です!== >|| maru@marU:/$ find -name libcvc3.so* find: `./lost+found': 許可がありません ?省略? ./usr/lib/libcvc3.so ?省略? ||< >|| /usrには、読み出し可能かつ共有可能なファイルを配置 /usr/lib以下はライブラリファイル(必須) /libは Linuxでは早くからシェアドライブラリを使ったダイナミックリンク機能が提供されていました。シェアドライブラリは、実行時、必要になった時点で初めてHDからメモリに読み込まれます。そのイメージを保存しておくディレクトリが/libです。カーネルのブート時に必要なものと、/ファイルシステムにあるコマンド(/binや/sbin内のコマンド)を実行するのに必要なライブラリはここにあります。 なお、FHS 2.2では複数の実行形式バイナリをサポートするシステムのために、/libという形式のディレクトリもオプションとして既定されています。 ||< ・今後 libcvc3.soファイルがあるならリンク元もあるはず?出てこない理由は不明だが、一端整理してみる。 /usr/lib以下にgccやsslなどがあるので、libcvc3.soファイルもどこかからもって来れるかも?そのようなライブラリの一般的にもってくる場所を調べる。 もう一度読み直してヒントがないか探る または別のうまいやり方?を探す。(エラー無視?環境を新たに別のOSで構築?UBUNTUのOSファイルの中にあったりしないかなあ。。

2 ● a-kuma3
ベストアンサー

分かりませぬ。
とりあえず、ヒントになればと思って、分かったことをずらずらと書きます。

cvc3 の make が失敗する理由

libcvc3.so.3からlibcvc3.so.3.0.0へリンクが出来ておらず、libcvc3.so.3ファイルがないのがそもそもの問題かと思われます。

だいたいその通りだと思います。
ldconfig は libcvc3.so.3.0.0 から libcvc3.so.3 を作ろうとしているし、ln は libcvc3.so.3.0.0 から libcvc3.so.3.0 を作ろうとしています。
libcvc.so.3 がないから、ln に失敗しているわけではありません。

気になるのは、このメッセージ。

ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0
ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです

ディレクトリ /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/ の権限ってどうなってます?
まさか、書き込み権限が無いとか?
make の途中で作られる(ぽい)ディレクトリだから、そんなはずはないかな、と思いつつも、メッセージを信じてみる。

libcvc3.so.3.0.0 の在処

http://www.cs.nyu.edu/acsys/cvc3/oldversions.html
↑に、過去のバージョンがありますが、
CVC3 2.4 → libcvc.so.4.0.0
CVC3 2.2 → libcvc.so.2.1.1
だと思うので、番号が飛んでますね。
cvc3/VERSION というファイルは、公開されているものだとバージョンが書かれているのですが、js-symbolic-executor に同梱されているファイルには日付が書かれています。
日付的には 2.3 くらいなのでしょうけれど、公開されてないのだと思います。

他のバージョンは使えない?

js-symbolic-executor の方でビルドを通すのが良いと思いますが、他のバージョンの libcvc3.so が使えないだろうか、ということについて。
CVC3 を作ってる人がどう考えているか分かりませんが、普通はライブラリって、下位互換を保つように作ります。少なくともインターフェースは。
もちろん機能を変更するケースはありますから、新しいライブラリを使うと動きが違ってる、ということはあります。
でも、普通は新しいインターフェースを増やすことがあっても、インターフェースを変えることは、まずやりません。

なので、最新の CVC3 2.4.1 (libcvc3.so.5) や、ひとつ前の CVC3 2.4 (libcvc3.so.4) では、動く可能性が高いと思います。

はてなブログに書いてある find のこと

maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ find -name libcvc3.so.3*
./lib/x86_64-linux-gnu/libcvc3.so.3.0.0

ファイルは見当たらず、エラーもまだわからない

Windows のコマンドと違って、* はシェルが展開します。
find を使うには、こうです。

$ find -name "libcvc3.so.3*"



魔法使いへの道のりは長いようです ><。


ruzxaさんのコメント
お調べ頂きありがとうございます。 libcvc3の説明がどうにも見当たらず、何を変数として試せばいいのかどうにもわからないので OSのバージョンを変えてみたり、JDKを変えてみる、svnを導入して直にファイルを落としてみるなどを試しております。 ふと思ったのですが、下記のエラー libcvc3-3.0.0.jarとlibcvc3.so.3(libcvc3.so.2などであればlibcvc3-2-....とネットに記載されてあるので)が関係がありかもと思ったのですが、一般にsoファイルは.c→.o→.soという作成手順に則っているためjarファイルからlibcvc3.soファイルは関係のないものなのかな。とどちらなのか迷っております。 ネット上にないものは、普通に考えればパッケージによって作られている可能性があるのかなと思いましたので。 >|| cvc3: [exec] Makefile:1: Makefile.local: そのようなファイルやディレクトリはありません [exec] make: *** ターゲット `Makefile.local' を make するルールがありません. 中止. [exec] Result: 2 BUILD FAILED /home/maru/js-symbolic-executor.orig/js-symbolic-executor/build.xml:116: Warning: Could not find file /home/maru/js-symbolic-executor.orig/cvc3/java/lib/libcvc3-3.0.0.jar to copy. Total time: 2 seconds ||< この後 ./configureの実行やmakeをしたのですが、今現在、libcvc3-3.0.0.jarファイルは見当たりませんでした。 libcvc.3.3.0.0.jar(ファイル無、どこかで消された?) → libcvc3.so.3.0.0(ファイル有) →libcvc3.so.3(ファイル有) こういうパターンもあり得るのでしょうか。 ==ご質問頂いた事== 書き込み権限はいずれにおいても問題なさそうです。 >|| maru@marU:/home$ ls -l /mnt/sharefolder/js-symbolic-executor/cvc3/lib/ 合計 8 drwxrwxrwx 1 root root 8192 11月 22 02:40 x86_64-linux-gnu maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu$ ls -l /home/maru/ ?省略? drwxr-xr-x 2 maru maru 4096 11月 23 14:37 デスクトップ ?省略? maru@marU:/home$ ls -l /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu 合計 22566 ?関係ないと思いますが、念のため? -rwxrwxrwx 1 root root 358216 11月 22 02:40 libc_interface.a -rwxrwxrwx 1 root root 61340 11月 22 02:33 libcontext.a -rwxrwxrwx 1 root root 6989255 11月 22 02:40 libcvc3.so.3.0.0 -rwxrwxrwx 1 root root 89322 11月 22 02:33 libcvc_util.a -rwxrwxrwx 1 root root 526716 11月 22 02:33 libexpr.a -rwxrwxrwx 1 root root 1068350 11月 22 02:40 libparser.a -rwxrwxrwx 1 root root 695742 11月 22 02:34 libsat.a -rwxrwxrwx 1 root root 2406788 11月 22 02:40 libsearch.a -rwxrwxrwx 1 root root 614158 11月 22 02:33 libtheorem.a -rwxrwxrwx 1 root root 3868682 11月 22 02:36 libtheory_arith.a -rwxrwxrwx 1 root root 394188 11月 22 02:36 libtheory_array.a -rwxrwxrwx 1 root root 1671136 11月 22 02:36 libtheory_bitvector.a -rwxrwxrwx 1 root root 1210398 11月 22 02:34 libtheory_core.a -rwxrwxrwx 1 root root 620690 11月 22 02:37 libtheory_datatype.a -rwxrwxrwx 1 root root 955198 11月 22 02:38 libtheory_quant.a -rwxrwxrwx 1 root root 252300 11月 22 02:38 libtheory_records.a -rwxrwxrwx 1 root root 125578 11月 22 02:38 libtheory_simulate.a -rwxrwxrwx 1 root root 298872 11月 22 02:38 libtheory_uf.a -rwxrwxrwx 1 root root 216092 11月 22 02:40 libtranslator.a -rwxrwxrwx 1 root root 680284 11月 22 02:40 libvcl.a ||< >気になるのは、このメッセージ。 >ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0 >ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです デスクトップフォルダになら普通にリンクはできました。ただ、書き込み権限には変わりはないはずですが、sudoを付けてみてもx86-linux-gnu以下には同じエラーが出てきました。 原因対処については探せばありそうな気もしましたが、これ以上は設定であったり泥沼になってしまうのかな。リンクをコピーで解決できないかなど手軽な方法を探してみます。 >|| maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu$ ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0 ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu$ ln -sf libcvc3.so.3.0.0 /home/maru/デスクトップ/libcvc3.so.3.0 maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu$ ls /home/maru/デスクトップ/ libcvc3.so.3.0 libcvc3.so.3.0.0 ||< ldconfigなどご指摘いただいたお蔭で、調べなおすきっかけとなりました。 わからない時に、パッとみて知っている知識だけで判断し、その中身の意味を調べない癖は直さなければですね。 どこかで見た事のあるワードでしたが、正しく問題を把握するうえで知っておかなければならない知識でした。 最終的にはこの二つの事について解決すべきですね。問題整理できました!ありがとうございます。 >ldconfig は libcvc3.so.3.0.0 から libcvc3.so.3 を作ろうとしているし、ln は libcvc3.so.3.0.0 から libcvc3.so.3.0 を作ろうとしています。 libcvcについては試させて頂きます! ==以下余談です== 魔法使いでふと思ったことです。。(若輩者の私がふと感じた事です。読み流して頂けると幸いです。 昨夜いつもご飯を作ってくださる料理長の方(師匠が有名な方らしく、その方はその師匠より評価されていたようですが)とお話しした内容です。 その師匠の方に料理を出す前夜にお酒を飲んでいたのですが、料理を出すとその師匠の方は味を見るなりすぐに「酒を飲んだだろ!」と怒られた様なのです。世の中には耳かき一杯分の塩の量を見分けられる方がいらっしゃるとか。 そんな凄い師匠についていた料理長は包丁を持って2?30年立たれたようなのですが、それでも、ようやく料理人のスタートに立ったとおっしゃられるのです。 食材の特性や作る量、また料理は食材による所も大きく色々な変数のあるなかで、どうすると美味しくなるのか使い分けができるようになったと自負を持たれたのかなと感じられていたと思います。 その料理長は、お店の外観や香り、お客さんの声など何によるものなのかわかりませんが、おいしい料理屋さんをパッっと見分ける事ができるようなのです。それにはたくさんのお金を使ったとおっしゃっていました。 お婆ちゃんなどはもうあまり味覚を感じないというのですが、それでもとても美味しい料理を作ってくれます。 何もない時代に試行錯誤してきた結果なのでしょうか。 そんなシックスセンスみたいなものが、魔法使いのスキルなのかなとふと思いました。 また、細かい所まで手を抜かず、ほんとに良いものを作れるようになるのには それこそ十年などでは到底足らず、何十年も時を重ねて腕を磨いていかなければならないんだなあと感じました。 10年我武者羅に頑張り続ければ(それでもかなり難しい事ですが)魔法使いになれるかな(笑)と思っておりましたが、 そんなに簡単な話ではないんだろうなあと実感し、少し悲しくもなりました。 そんな自分は今、包丁の持ち方を習っている所で、道のりはもっともっと長いようです。

ruzxaさんのコメント
svnよりダウンロードして、chownでグループはそのままrootでユーザだけmaruに変更してmaru rootで試しにantを実行したら一発でなぜか通りました! 少し府に落ちない事がいっぱいあるので、今から整理してみます。 お手数おかけしました。 ご相談に乗って頂きありがとうございました。 質問の答えとしては、ネット上には存在せず、cvc3より作られるというのが正しい答えの様です。

a-kuma3さんのコメント
んー、owner が root でも、others は +w になってるのに... ぼくも腑に落ちない感じですが、上手くいって良かった <tt>:-)</tt>

ruzxaさんのコメント
遠回りはしてしまいましたが、エラーを読み解く自信の一切なかった自分が 頑張ればエラー読めるんだぞと実感できたとてもいい経験でした。 ありがとうございます! なんとなく原因がわかったのでご報告させて頂きます。 svnは関係ありませんでした。 ./cvc3/config.status実行時にoperation not permitted というエラーが原因のようでした。 このファイルだけhttp://blog.popowa.com/2013/11/phpchmod-operation-not-permitted.htmlより chown maru config.status としてしまえば、libcvc3.so.3などのファイルはできていました。 ちなみにconfig.status は事前にchmod 777としていたので実行されるはずでしたがどうにも違うみたいです。 config.statusだけではうまくいかなかったのでcvc3以下を chown -R maru cvc3 としてあげたら、build.xmlを読んで手作業も必要でしたが入りました! 全ファイルのユーザーを変更してしまえばant一発でした。

a-kuma3さんのコメント
メキメキという音が聞こえてきそう <tt>:-)</tt> CVC3 は、情報が少なそうですし、一通り上手くいったら、はてなブログにでも敬意を残しておくと、後続のためになりそうに思います。
関連質問

●質問をもっと探す●



0.人力検索はてなトップ
8.このページを友達に紹介
9.このページの先頭へ
対応機種一覧
お問い合わせ
ヘルプ/お知らせ
ログイン
無料ユーザー登録
はてなトップ