プログラミングなどなど

プログラミングに関係しそうな内容を

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手順で解消しました。

  1. コンパイル時のQオプション指定
  2. 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」指定の効果なのだと思います。