SPIN:-o2オプションを使用して書き込みだけの変数も検証させる
spinのヘルプを見ているときに-o2オプションが気になりました。
-o2オプションのヘルプの説明を読むと書き込みだけの変数も隠さずに検証するような記述になっています。このオプションの説明から、もしかすると「SPINモデル検査入門」で紹介されている8クイーン問題の解を書き込み用のダミー変数(_)を使うことなく全て列挙できるのではないかと思い試してみました。
-o2オプションを試した結果、ダミー変数(_)を使用せずに状態で全ての解である92個が列挙されました。
ソース 8qeen.pml
使用したソースは「SPINモデル検査入門」のp.192(ソースコード 11.5)のものとなります。
-o2オプション無しでの実行
本のとおり86個の解が検出されます。
$ spin -run -E -c0 8qeen.pml
pan:1: assertion violated 0 (at depth 104)
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by -E flag)
State-vector 56 byte, depth reached 106, errors: 86
39249 states, stored
788 states, matched
40037 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
3.144 equivalent memory usage for states (stored*(State-vector + overhead))
2.923 actual memory usage for states (compression: 92.98%)
state-vector as stored = 50 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
131.366 total actual memory usage
unreached in proctype Queens
(0 of 41 states)
pan: elapsed time 0.02 seconds
pan: rate 1962450 states/second
-o2オプション有りでの実行
書き込みダミー(_)を使用していませんが92個の解が検出されます。
$ spin -o2 -run -E -c0 8qeen.pml
pan:1: assertion violated 0 (at depth 104)
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by -E flag)
State-vector 64 byte, depth reached 106, errors: 92
41433 states, stored
0 states, matched
41433 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
3.635 equivalent memory usage for states (stored*(State-vector + overhead))
3.411 actual memory usage for states (compression: 93.84%)
state-vector as stored = 58 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
131.855 total actual memory usage
unreached in proctype Queens
(0 of 41 states)
pan: elapsed time 0.02 seconds
pan: rate 2071650 states/second
spinヘルプ -o2オプション
-o2オプションを見ると書き込みだけが行われた変数を
隠さずに検証器が処理するような記述が有ります。
$ spin --help
use: spin [-option] ... [-option] file
Note: file must always be the last argument
-A apply slicing algorithm
:
(省略)
:
-o1 turn off dataflow-optimizations in verifier
-o2 don't hide write-only variables in verifier
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-o3 turn off statement merging in verifier
:
SPIN:順次の実行と値
これまで読んだSPIN本のどこかに書かれているかもしれませんが完全にスルーしていた内容を紹介します。(SPINモデル検査入門の8クイーン問題で知りました。)
以下の見出しでわかってしまいますが、以下のモデルを実行した際に
Hello, world!は出力されるでしょうか。
timeoutになる例
seq-stop.pml
byte b = 0; active proctype p() { b; printf("Hello, world!\n"); }
timeoutになる
$ spin seq-stop.pml
timeout
#processes: 1
b = 0
0: proc 0 (p:1) seq-stop.pml:5 (state 1)
1 process createdなんとtimeoutになり、Hello, world!は出力されません。
通過する例
bの初期値を変更すると今度はprintfまで進みます。
seq-pass.pml
byte b = 1; active proctype p() { b; printf("Hello, world!\n"); }
通過する
$ spin seq-pass.pml
Hello, world!
1 process created知ってました?
SPIN:3x3の魔法陣の数値選択部分にselectを使用してみる
3x3の魔法陣の解をSPINで求める記事をアップロードした後に、マニュアル(http://spinroot.com/spin/Man)を見ていると、たまたまselectというものがあるのを知りました。
selectを使用すると数値を非決定的に選択する部分を簡単に記述できそうでしたので、magicSquare.pmlをselectを使用して書き直してみます。
作成したソースは以下のとおりです。
ソース magicSquare.pml
#define SIZE 3 /* ------------------------- 魔法陣ms 1列目 2列目 3列目 1行目 ms[0] ms[1] ms[2] 2行目 ms[3] ms[4] ms[5] 3行目 ms[6] ms[7] ms[8] -------------------------- */ byte ms[SIZE*SIZE]; /* ------------------------- 使用済みの数値判定用 例 used[0] == true <- 数値1使用済み used[1] == false <- 数値2未使用 : used[8] == true <- 数値9使用済み -------------------------- */ bool used[SIZE*SIZE]; active proctype p() { /* 魔法陣に1から9の数値を非決定的に設定していく */ byte a; byte i = 0 do :: i < (SIZE*SIZE) -> /* 数値を非決定的に選ぶ */ select(a : 1..9); if /* 選んだ数値が未使用の場合 */ :: used[a-1] != true -> ms[i] = a; used[a-1] = true i++ /* 選んだ数値が使用済みの場合 */ :: else -> skip fi /* 魔法陣に数値を入れきったらループを抜ける */ :: i == SIZE*SIZE -> break od /* 魔法陣 */ printf("\nMS : %d %d %d\nMS : %d %d %d\nMS : %d %d %d\n", ms[0],ms[1],ms[2],ms[3],ms[4],ms[5],ms[6],ms[7],ms[8]); /* 魔法陣の和を確認する */ bool check = true; if :: /* 各行のチェック */ (ms[0] + ms[1] + ms[2] == 15) && (ms[3] + ms[4] + ms[5] == 15) && (ms[6] + ms[7] + ms[8] == 15) && /* 各列のチェック */ (ms[0] + ms[3] + ms[6] == 15) && (ms[1] + ms[4] + ms[7] == 15) && (ms[2] + ms[5] + ms[8] == 15) && /* 対角線のチェック */ (ms[0] + ms[4] + ms[8] == 15) && (ms[6] + ms[4] + ms[2] == 15) -> check = true :: else -> check = false fi /* 検証により検出させるため check == false を検査式にする */ assert(check == false); }
検証器を作成しての確認
検証時の生成からエラートレイルの列挙
$ spin -run -e magicSquare.pml : 省略 : $ for i in $(seq 1 8); do echo magicSquare.pml$i.trail; spin -t$i -B magicSquare.pml | grep MS; done magicSquare.pml1.trail MS : 2 7 6 MS : 9 5 1 MS : 4 3 8 magicSquare.pml2.trail MS : 2 9 4 MS : 7 5 3 MS : 6 1 8 magicSquare.pml3.trail MS : 4 3 8 MS : 9 5 1 MS : 2 7 6 magicSquare.pml4.trail MS : 4 9 2 MS : 3 5 7 MS : 8 1 6 magicSquare.pml5.trail MS : 6 1 8 MS : 7 5 3 MS : 2 9 4 magicSquare.pml6.trail MS : 6 7 2 MS : 1 5 9 MS : 8 3 4 magicSquare.pml7.trail MS : 8 1 6 MS : 3 5 7 MS : 4 9 2 magicSquare.pml8.trail MS : 8 3 4 MS : 1 5 9 MS : 6 7 2
同じ結果になっていそうです。
マニュアルにあたると色々と発見があります。
SPIN:3x3の魔法陣の解を求める
「SPINモデル検査入門」という本の11章ケーススタディに8クイーン問題の解を求めるサンプルがあったので、自身の練習として3x3の魔法陣の解を求めてみたいと思います。
作成したソースは以下のとおりです。
ソース magicSquare.pml
#define SIZE 3 /* ------------------------- 魔法陣ms 1列目 2列目 3列目 1行目 ms[0] ms[1] ms[2] 2行目 ms[3] ms[4] ms[5] 3行目 ms[6] ms[7] ms[8] -------------------------- */ byte ms[SIZE*SIZE]; /* ------------------------- 使用済みの数値判定用 例 used[0] == true <- 数値1使用済み used[1] == false <- 数値2未使用 : used[8] == true <- 数値9使用済み -------------------------- */ bool used[SIZE*SIZE]; active proctype p() { /* 魔法陣に1から9の数値を非決定的に設定していく */ byte a; byte i = 0 do :: i < (SIZE*SIZE) -> /* 数値を非決定的に選ぶ */ if :: a = 1 :: a = 2 :: a = 3 :: a = 4 :: a = 5 :: a = 6 :: a = 7 :: a = 8 :: a = 9 fi if /* 選んだ数値が未使用の場合 */ :: used[a-1] != true -> ms[i] = a; used[a-1] = true i++ /* 選んだ数値が使用済みの場合 */ :: else -> skip fi /* 魔法陣に数値を入れきったらループを抜ける */ :: i == SIZE*SIZE -> break od /* 魔法陣 */ printf("\nMS : %d %d %d\nMS : %d %d %d\nMS : %d %d %d\n", ms[0],ms[1],ms[2],ms[3],ms[4],ms[5],ms[6],ms[7],ms[8]); /* 魔法陣の和を確認する */ bool check = true; if :: /* 各行のチェック */ (ms[0] + ms[1] + ms[2] == 15) && (ms[3] + ms[4] + ms[5] == 15) && (ms[6] + ms[7] + ms[8] == 15) && /* 各列のチェック */ (ms[0] + ms[3] + ms[6] == 15) && (ms[1] + ms[4] + ms[7] == 15) && (ms[2] + ms[5] + ms[8] == 15) && /* 対角線のチェック */ (ms[0] + ms[4] + ms[8] == 15) && (ms[6] + ms[4] + ms[2] == 15) -> check = true :: else -> check = false fi /* 検証により検出させるため check == false を検査式にする */ assert(check == false); }
手動シミュレーションでの簡易動作確認
手動シミュレーションで検証エラーになる場合とならない場合を簡易的に確認します。
魔法陣が成立しない(検証エラーにならない)場合
手動で何度も入力するのが面倒なので入力データを作成しました。
入力データ in01
$ cat in01 1 2 3 4 5 6 7 8 9
シミュレーション
作成したデータをリダイレクトで入力します。
$ spin -i magicSquare.pml < in01
Select stmnt (proc 0 (p:1) )
choice 1: ((i<(3*3)))
:
(略)
:
Select stmnt (proc 0 (p:1) )
choice 2: ((i==(3*3)))
MS : 1 2 3
MS : 4 5 6
MS : 7 8 9
Select stmnt (proc 0 (p:1) )
choice 2: (else)
1 process created魔法陣が成立していないので、検証エラーも出ていません。
魔法陣が成立する(検証エラーになる)場合
入力データ in02
$ cat in02 2 7 6 9 5 1 4 3 8
シミュレーション
$ spin -i magicSquare.pml < in02 Select stmnt (proc 0 (p:1) ) choice 1: ((i<(3*3))) : (略) : spin: magicSquare.pml:78, Error: assertion violated spin: text of failed assertion: assert((check==0)) #processes: 1 ms[0] = 2 ms[1] = 7 ms[2] = 6 ms[3] = 9 ms[4] = 5 ms[5] = 1 ms[6] = 4 ms[7] = 3 ms[8] = 8 used[0] = 1 used[1] = 1 used[2] = 1 used[3] = 1 used[4] = 1 used[5] = 1 used[6] = 1 used[7] = 1 used[8] = 1 89: proc 0 (p:1) magicSquare.pml:78 (state 34) 1 process created
魔法陣が成立しているので、検証エラーとなっています。
検証器を作成しての確認
検証時の生成から実行
$ spin -run -e magicSquare.pml
Depth= 172 States= 1e+06 Transitions= 2.47e+06 Memory= 181.952 t= 0.51 R= 2e+06
Depth= 172 States= 2e+06 Transitions= 4.93e+06 Memory= 235.272 t= 1.04 R= 2e+06
Depth= 172 States= 3e+06 Transitions= 7.4e+06 Memory= 288.593 t= 1.59 R= 2e+06
Depth= 172 States= 4e+06 Transitions= 9.87e+06 Memory= 341.913 t= 2.15 R= 2e+06
pan:1: assertion violated (check==0) (at depth 110)
pan: wrote magicSquare.pml1.trail
Depth= 172 States= 5e+06 Transitions= 1.23e+07 Memory= 395.233 t= 2.78 R= 2e+06
pan: wrote magicSquare.pml2.trail
Depth= 172 States= 6e+06 Transitions= 1.48e+07 Memory= 448.554 t= 3.47 R= 2e+06
Depth= 172 States= 7e+06 Transitions= 1.73e+07 Memory= 501.776 t= 4.18 R= 2e+06
Depth= 172 States= 8e+06 Transitions= 1.97e+07 Memory= 555.097 t= 4.83 R= 2e+06
Depth= 172 States= 9e+06 Transitions= 2.22e+07 Memory= 608.417 t= 5.47 R= 2e+06
pan: wrote magicSquare.pml3.trail
Depth= 172 States= 1e+07 Transitions= 2.47e+07 Memory= 661.737 t= 6.15 R= 2e+06
pan: wrote magicSquare.pml4.trail
Depth= 172 States= 1.1e+07 Transitions= 2.71e+07 Memory= 715.058 t= 6.84 R= 2e+06
Depth= 172 States= 1.2e+07 Transitions= 2.96e+07 Memory= 768.378 t= 7.56 R= 2e+06
Depth= 172 States= 1.3e+07 Transitions= 3.21e+07 Memory= 821.698 t= 8.39 R= 2e+06
Depth= 172 States= 1.4e+07 Transitions= 3.45e+07 Memory= 874.921 t= 9.22 R= 2e+06
pan: wrote magicSquare.pml5.trail
Depth= 172 States= 1.5e+07 Transitions= 3.7e+07 Memory= 928.241 t= 10.1 R= 1e+06
pan: wrote magicSquare.pml6.trail
Depth= 172 States= 1.6e+07 Transitions= 3.95e+07 Memory= 981.562 t= 10.9 R= 1e+06
Depth= 172 States= 1.7e+07 Transitions= 4.19e+07 Memory= 1034.882 t= 11.9 R= 1e+06
Depth= 172 States= 1.8e+07 Transitions= 4.44e+07 Memory= 1088.202 t= 13 R= 1e+06
Depth= 172 States= 1.9e+07 Transitions= 4.69e+07 Memory= 1141.522 t= 13.9 R= 1e+06
pan: wrote magicSquare.pml7.trail
Depth= 172 States= 2e+07 Transitions= 4.93e+07 Memory= 1194.843 t= 14.8 R= 1e+06
pan: wrote magicSquare.pml8.trail
Depth= 172 States= 2.1e+07 Transitions= 5.18e+07 Memory= 1248.065 t= 15.7 R= 1e+06
Depth= 172 States= 2.2e+07 Transitions= 5.43e+07 Memory= 1301.386 t= 16.7 R= 1e+06
Depth= 172 States= 2.3e+07 Transitions= 5.67e+07 Memory= 1354.706 t= 17.9 R= 1e+06
Depth= 172 States= 2.4e+07 Transitions= 5.92e+07 Memory= 1408.026 t= 18.9 R= 1e+06
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 32 byte, depth reached 172, errors: 8
24987242 states, stored
36640017 states, matched
61627259 transitions (= stored+matched)
0 atomic steps
hash conflicts: 19533061 (resolved)
Stats on memory usage (in Megabytes):
1429.781 equivalent memory usage for states (stored*(State-vector + overhead))
1332.493 actual memory usage for states (compression: 93.20%)
state-vector as stored = 28 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1460.663 total actual memory usage
unreached in proctype p
(0 of 35 states)
pan: elapsed time 19.8 seconds
pan: rate 1263257.9 states/second8パターンのエラーが検出されています。
エラートレイルの列挙
8パターンあるので魔法陣出力部分を抜き出して出力させます。
$ for i in $(seq 1 8); do echo magicSquare.pml$i.trail; spin -t$i -B magicSquare.pml | grep MS; done magicSquare.pml1.trail MS : 2 7 6 MS : 9 5 1 MS : 4 3 8 magicSquare.pml2.trail MS : 2 9 4 MS : 7 5 3 MS : 6 1 8 magicSquare.pml3.trail MS : 4 3 8 MS : 9 5 1 MS : 2 7 6 magicSquare.pml4.trail MS : 4 9 2 MS : 3 5 7 MS : 8 1 6 magicSquare.pml5.trail MS : 6 1 8 MS : 7 5 3 MS : 2 9 4 magicSquare.pml6.trail MS : 6 7 2 MS : 1 5 9 MS : 8 3 4 magicSquare.pml7.trail MS : 8 1 6 MS : 3 5 7 MS : 4 9 2 magicSquare.pml8.trail MS : 8 3 4 MS : 1 5 9 MS : 6 7 2
確かに魔法陣になっていそうです。
spin, panコマンドのヘルプとページャ(less)
SPINを勉強しているのですが、spin, 検証器(pan)コマンドのオプションが覚えられずに頻繁にヘルプを参照しています。
私の環境ではヘルプを出力すると作業ターミナルの画面から溢れるのでページャを通して確認することが多いです。ページャを通すと検索機能を使えるため個人的にはとても気に入って使っています。
今回は以下の2つを紹介したいと思います。
- spinのヘルプ(標準出力)をページャを通して見る
- pan のヘルプ(標準エラー出力)をページを通して見る
使用しているページャはlessです。
使用しているシェルの確認
$ echo $SHELL /bin/bash
spinコマンドのヘルプ
$ spin --help | less
検証器(pan)のヘルプ
適当なモデルを記述して検証の生成からコンパイルを行います。
$ cat p.pml
bool b = true;
active proctype p()
{
if
:: b = true
:: b = false
fi
}
$ spin -a p.pml
$ gcc -w pan.c -o pan
spinと同じように試す
以下のようにヘルプを見ようとしても画面出力が流れます。
$ ./pan -h | less
これはヘルプの標準エラーに出力されているためです。
標準エラー出力を含めてパイプに流す
$ ./pan -h |& less
おわりに
ページャに慣れておくと1画面を超える出力をゆっくり確認したい場合に役立ちますので、個人的にはおすすめです。以下のようなケースでよく使用します。
$ cat *.log | less <-- ログファイルをまとめて確認 $ cat *.log | 各種フィルタコマンド | less <-- 出力結果を1画面ずつ確認
SPIN:-searchオプションを指定した場合の動きについて
PROMELAで記述したモデルから検証器を生成する際にnever claimが2つ以上になると、どれか一つを選択して欲しい旨と-searchオプションを指定する例が出力されます。
本などには以下の流れで記載されていますが、何か違いがあったりするのでしょうか。
- 検証器の生成
- 検証器のコンパイル
- 検証器の実行
straceコマンドを利用して見てみたいと思います。
サンプルソース : sample.pml
byte b = 0; active proctype p() { if :: b = 1; :: b = 2; fi } ltl l01 { <>(b == 1) }
検証器の生成
$ spin -a sample.pml ltl l01: <> ((b==1))
コンパイルと実行
$ gcc -w pan.c -o pan
$ ./pan -a
pan:1: acceptance cycle (at depth 4)
pan: wrote sample.pml.trail
(Spin Version 6.4.9 -- 17 December 2018)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (l01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 5, errors: 1
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
ltlの追加
サンプルソース(ltl追加) : sample.pml
以下のようにltlを追加します。
byte b = 0; active proctype p() { if :: b = 1; :: b = 2; fi } ltl l01 { <>(b == 1) } ltl l01n { !(<>(b == 1)) }
検証器の生成(ltl追加後)
検証器を生成しようとすると1つの場合とは異なりオプションの説明が出力されます。
$ spin -a sample.pml ltl l01: <> ((b==1)) ltl l01n: ! (<> ((b==1))) the model contains 2 never claims: l01n, l01 only one claim is used in a verification run choose which one with ./pan -a -N name (defaults to -N l01) or use e.g.: spin -search -ltl l01 sample.pml
検証器の生成からコンパイル、実行
例に習って-searchオプションを指定してみます。
$ spin -search -ltl l01 sample.pml
ltl l01: <> ((b==1))
ltl l01n: ! (<> ((b==1)))
the model contains 2 never claims: l01n, l01
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N l01)
or use e.g.: spin -search -ltl l01 sample.pml
pan: ltl formula l01
pan:1: acceptance cycle (at depth 4)
pan: wrote sample.pml.trail
(Spin Version 6.4.9 -- 17 December 2018)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (l01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 5, errors: 1
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.290 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
-searchオプションを指定した際の動作を追う
-searchオプションを使用した場合のspinコマンドの動作をstraceコマンドを使用して追ってみます。
straceによるシステムコールのトレース取得
$ strace -o sout -f spin -search -ltl l01 sample.pml
トレース確認
以下はトレースの抜粋です。
コンパイル時のオプションが手動で実行した場合と異なりますが、生成、コンパイル、実行を順に行ってくれていることがわかります。
$ less sout
5255 execve("/home/makoto/bin/spin", ["spin", "-search", "-ltl", "l01", "sample.pml"], 0x7ffeb6c98828 /* 67 vars */) = 0
:
5255 openat(AT_FDCWD, "pan.c", O_WRONLY|O_CREAT|O_TRUNC, 0666) = 3 <-- pan.cの生成部分
:
fd=3についてwriteが呼び出されている。
:
5255 close(3) = 0
:
5260 execve("/usr/bin/gcc", ["gcc", "-std=gnu99", "-O", "-DNOFAIR", "-o", "pan", "pan.c"], 0x5573ac3132d8 /* 67 vars */) = 0 <-- コンパイル部分
;
5265 execve("/bin/sh", ["sh", "-c", "./pan -N l01 -a"], 0x7ffed5d7edc8 /* 67 vars */) = 0 <-- 実行部分
Coq:「Require Import Cpdt.CpdtTactics.」実行時のエラー対処について
この文章について
このページでは Coqで「Require Import Cpdt.CpdtTactics.」を実行した際に出力されたエラー「Error:Cannot find a physical path bound to logical path matching suffix Cpdt.」を解消する方法について紹介したいと思います。
私がCoqの勉強を始めたばかりでわからないことも多く、通常は選択しない解消法かもしれませんが、同じエラーで躓いた方の助けになればと思います。
作業環境など
Coqのバージョンと作業ディレクトリは以下のとおりです。
作業シェル
$ echo $SHELL /bin/bash
Coqバージョン
$ coqtop -v The Coq Proof Assistant, version 8.8.0 (November 2018) compiled on Nov 22 2018 0:16:38 with OCaml 4.07.0
作業ディレクトリ
$ pwd /home/makoto/programming/coq/cpdt
Certified Programming with Dependent Typesのサイトからダウンロードしたcpdtlib.tgzを作業ディレクトリにコピーしtarコマンドで次のように展開しています。
cpdtlib.tgzの展開
$ tar zxvf cpdtlib.tgz cpdtlib/CpdtTactics.v cpdtlib/DepList.v cpdtlib/LICENSE cpdtlib/MoreSpecif.v
エラーまでの流れ
cpdtlib/CpdtTactics.vを次のようにコンパイルしました。
cpdt/CpdtTactics.vのコンパイル
$ coqc cpdtlib/CpdtTactics.v
「Require Imoprt」時のエラー
coqtopを起動し「Require Import Cpdt.CpdtTactics.」を実行したところ次のエラーが出力されました。
$ coqtop Welcome to Coq 8.8.0 (November 2018) Coq < Require Import Cpdt.CpdtTactics. Toplevel input, characters 15-31: > Require Import Cpdt.CpdtTactics. > ^^^^^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path matching suffix Cpdt.
解消方法
色々調べながらトライ&エラーを行っていったところ、以下の2手順で解消しました。
- コンパイル時のQオプション指定
- coqtop実行時のパス指定
1.コンパイル時のQオプション指定
$ coqc -Q cpdtlib Cpdt cpdtlib/CpdtTactics.v
2.coqtop実行時のパス指定
いくつか方法があるので好みの方法で指定すれば良いと思います。
2.1.coqtop起動時のQオプション指定
$ coqtop -Q cpdtlib Cpdt Welcome to Coq 8.8.0 (November 2018) Coq < Require Import Cpdt.CpdtTactics. [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done]
2.2.coqtop実行後の「Add LoadPath」を実行
$ coqtop Welcome to Coq 8.8.0 (November 2018) Coq < Add LoadPath "cpdtlib" as Cpdt. Coq < Require Import Cpdt.CpdtTactics. [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done] Coq <
2.3. _CoqProjectファイルの用意
Proof Generalを使用している方向けです。
$ cat _CoqProject -Q cpdtlib Cpdt
解消までの流れ
解消までの手順が別トラブルの解消に役立つかもしれませんので、流れを記載します。
LoddPathの確認
Coqがパスをどのように認識しているかを「Print LoadPath」で確認しました。
$ coqtop Welcome to Coq 8.8.0 (November 2018) Coq < Print LoadPath. Logical Path / Physical path: <> /home/makoto/programming/coq/cpdt <> /home/makoto/.opam/4.07.0/lib/coq/user-contrib Coq /home/makoto/.opam/4.07.0/lib/coq/plugins Coq.syntax /home/makoto/.opam/4.07.0/lib/coq/plugins/syntax :
「Logical Path」と「Physical Path」の対応が出力されましたが、 ここに、「Logical Path」が「Cpdt」、「Physical Path」が「cpdtlib」となっている行はありませんでした。
そこで、「Add LoadPath」でパスを追加してみました。
「Add LoadPath」によるパスの追加
$ coqtop Welcome to Coq 8.8.0 (November 2018) Coq < Add LoadPath "cpdtlib". Coq < Print LoadPath. Logical Path / Physical path: <> /home/makoto/programming/coq/cpdt/cpdtlib <> /home/makoto/programming/coq/cpdt <> /home/makoto/.opam/4.07.0/lib/coq/user-contrib Coq /home/makoto/.opam/4.07.0/lib/coq/plugins
「Physical Path」に「cpdtlib」が追加されましたが、「Logical Path」が「<>」となっています。「Add LoadPath」を調べると「Logical Path」を指定する方法があったので、指定し「Require Import」を実行してみました。
「Add LoadPath」によるパスの追加(「Logical Path」指定)と「Require Import」の実行
$ coqtop Welcome to Coq 8.8.0 (November 2018) Coq < Add LoadPath "cpdtlib" as Cpdt. Coq < Print LoadPath. Logical Path / Physical path: Cpdt /home/makoto/programming/coq/cpdt/cpdtlib <> /home/makoto/programming/coq/cpdt <> /home/makoto/.opam/4.07.0/lib/coq/user-contrib Coq /home/makoto/.opam/4.07.0/lib/coq/plugins : Coq < Require Import Cpdt.CpdtTactics. Toplevel input, characters 0-32: > Require Import Cpdt.CpdtTactics. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: The file /home/makoto/programming/coq/cpdt/cpdtlib/CpdtTactics.vo contains library CpdtTactics and not library Cpdt.CpdtTactics
エラー情報について、Coqのリファレンスマニュアルを参照したところ、次のような記述がありました。
Coqリファレンスマニュアルからの引用
Error The file `ident.vo` contains library dirpath and not library dirpath’.
The library file dirpath’ is indirectly required by the Require command but it is bound in the current loadpath to the file ident.vo which was bound to a different library name dirpath at the time it was compiled.
どうやら.voを作成するコンパイルの方法に間違いがありそうなことがわかりました。ここからはトライ&エラーでcoqcのオプションを試しQオプションに行き着きました。
コンパイル時にQオプションを付与することで.voファイルがどのように変化するのか(興味)
coqcのQオプションにより.voファイルの内容が変わるはずなので、どのように変化しているかを簡易的に確認してみました。
Qオプショ指定無しコンパイルとバックアップ
$ coqc cpdtlib/CpdtTactics.v $ mv cpdtlib/CpdtTactics.vo cpdtlib/CpdtTactics.vo1
Qオプショ指定有りコンパイル
$ coqc -Q cpdtlib Cpdt cpdtlib/CpdtTactics.v
ファイルの比較1
$ sdiff -w 160 <(hexdump -Cv cpdtlib/CpdtTactics.vo) <(hexdump -Cv cpdtlib/CpdtTactics.vo1 )
00000000 00 00 22 60 00 00 1c 16 84 95 a6 be 00 00 1b fa |.."`............ | 00000000 00 00 22 60 00 00 1c 10 84 95 a6 be 00 00 1b f4 |.."`............
00000010 00 00 05 f9 00 00 13 81 00 00 10 d6 b0 a0 2b 43 |..............+C | 00000010 00 00 05 f7 00 00 13 7b 00 00 10 d1 b0 a0 2b 43 |.......{......+C
00000020 70 64 74 54 61 63 74 69 63 73 a0 24 43 70 64 74 |pdtTactics.$Cpdt | 00000020 70 64 74 54 61 63 74 69 63 73 40 08 00 00 28 00 |pdtTactics@...(.
^^^^この辺りがQオプション指定の効果と思われる。
00000030 40 08 00 00 28 00 a0 29 4e 6f 74 61 74 69 6f 6e |@...(..)Notation | 00000030 a0 29 4e 6f 74 61 74 69 6f 6e 73 a0 24 49 6e 69 |.)Notations.$Ini
ファイルの比較2
$ sdiff <(strings cpdtlib/CpdtTactics.vo) <(strings cpdtlib/CpdtTactics.vo1) +CpdtTactics | +CpdtTactics@ $Cpdt@ < )Notations )Notations $Init $Init #Coq@ #Coq@
Qオプショを指定でコンパイルしたものには、「$Cpdt@」が入っていました。この辺りが「Logical Path」指定の効果なのだと思います。
