AUTOSAR CountdownAdvent Calendar 2022Day 24

MacintoshでCoq(6)ide

Last updated at 2024-10-27Posted at 2018-01-20

名古屋のProof Cafeで永らくCoqを利用してきた。
http://proofcafe.org/wiki/

持っていく機材が毎回違うと、毎回Coqを入れ直しをしていた。

導入済みの道具類によって、導入方法が違うと面倒である。

最近ではbrew cask install coqide"で導入している。

道具の導入の仕方が良くないと、うまく過去のプログラムを読み込まず、最初からファイルを読み込みながらやっていた。

資料

proofcafa
http://proofcafe.org/sf/
Software Foundation(ソフトウェアの基礎)　
Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey

Software Foundation Volume 1 Logical Foundations
https://softwarefoundations.cis.upenn.edu/lf-current/index.html
https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz

Software Foundation Volume 2 Programming Language Foundations
https://softwarefoundations.cis.upenn.edu/plf-current/index.html
https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz

Software Foundation Volume 3 Verified Functional Algorithms
https://softwarefoundations.cis.upenn.edu/vfa-current/index.html
https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz

1. coqide

1.1 導入

$ brew cask install coqide

* snip *

==> Moving App 'CoqIDE_8.7.1.app' to '/Applications/CoqIDE_8.7.1.app'.
  coqide was successfully installed!

アプリケーションフォルダに

ができていた。

ダブルクリックすると

おかしいことが２点。
ダウンロードしたのは2018年1月9日になっているが、2018年1月21日（日本時間）。
ダウンロードしたのはSafariではなくbrew(ruby)のはず。
<この事項は継続調査します。>

「開く」を選ぶと

一度もOpenしていないのに、Reopenとは如何なものか。
「Don’t Reopen」を選ぶ。

画面が開く。

1.2 ソースダウンロード

ProofCafeにある Software Foundation（ソフトウェアの基礎）をダウンロード
sfja.tarというファイルがダウンロードできる。

$ cd ~/Downloads
$ mkdir sfja
$ mv sfja.tar sfja
$ cd sfja
$ tar -xf sfja.tar

1.3 読み込み

coq ideで読み込み
「ファイル」メニューを選ぶ。

自分のユーザ名のDownloadフォルダのsfjaフォルダを開くと、ファイル一覧が出る。

最初の章はBasics_J

Basics_J.vを選択して「open」を選ぶ

(で始まって)で終わるのが註釈(comment)

1.4 実行

ファイルとシステムの導入がうまくいっているかを確かめるため

「Navigation」メニューの「end」アイコンをおす。アイコンリスト上の同じアイコンも同じ機能。

を押すと先頭に戻る。

１行づつ確かめる時には

１行戻るときは

次に List_J.vを読み込む。
「end」を実行すると

Unable to locate library Basics_J.

これは厄介な難事件。ネットで検索しても、Load Pathの表現が、/ではなくて.を使えということはわかっても、現在のフォルダ名をBasics_Jの前に

Users.ogawakiyoshi.Downloads.sfja.Basics_J.
としても同じエラー。

さらに検索すると、coqのlibの下にあるものはうまく動作するらしい。そこで

cd /usr/local/Cellar/coq/8.7.1/lib/
mv /Users/ogawakiyoshi.Downloads/sfja .

ここに、sfjaを移動してきたらうまく行った。
ここには、coqというフォルダがある。coqのフォルダの下ではなければ、混在することはないはず。

しかし、「Compile」メニューの「Compile buffer」を実行すると、インタプリタでは実行するものの、

Unable to locate library Basics_J.

これでは、さっぱりわからない。coqcコマンドを実行してみた。
Basics_Jがコンパイルしていないと上記のエラー、コンパイルしてBasics_J.voがあると下記のエラー。

coqc Lists_J.v
File "./Lists_J.v", line 10, characters 0-24:
Error:
Compiled library Basics_J (in file /usr/local/Cellar/coq/8.7.1/lib/sfja/Basics_J.vo) makes inconsistent assumptions over library Coq.Init.Logic

Software Foundation Volume 1 Logical Foundations

ファイルは、Basic.v <- Induction.v <- List.v
という構造になっている。
https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz

Basic.v は実行、コンパイルともOK
Induction.vは実行はOK, コンパイルで次のエラーが出る。

coqc induction.v
Compilation output:
File "/Users/ogawakiyoshi/Downloads/lf/Induction.v", line 184, characters 2-7:
Error: The reference evenb was not found in the current environment.

2 coq導入

すでに導入済みのソフトウェアによって導入時間が異なる。

brew install coq
==> Installing dependencies for coq: ocaml, camlp5, ocaml-num
==> Installing coq dependency: ocaml
  /usr/local/Cellar/ocaml/4.06.0: 1,989 files, 225.7MB, built in 7 
==> Installing coq dependency: camlp5
  /usr/local/Cellar/camlp5/7.03_1: 213 files, 25.4MB
==> Installing coq dependency: ocaml-num
  /usr/local/Cellar/ocaml-num/1.1_1: 44 files, 1.1MB
Emacs Lisp files have been installed to:
  /usr/local/share/emacs/site-lisp/coq
==> Summary
  /usr/local/Cellar/coq/8.7.1: 4,288 files, 217.3MB

2018年1月20日現在、8.7.1が導入できる。
資料によっては、古いCoqを使う必要があるかもしれない。

High sierraでocamlのバイナリ導入に失敗したが、ソースから導入してくれた。

==> Downloading https://homebrew.bintray.com/bottles/ocaml-4.06.0.high_sierra.
curl: (18) transfer closed with 78162040 bytes remaining to read
Error: Failed to download resource "ocaml"
Download failed: https://homebrew.bintray.com/bottles/ocaml-4.06.0.high_sierra.bottle.tar.gz
Warning: Bottle installation failed: building from source.
==> Downloading https://caml.inria.fr/pub/distrib/ocaml-4.06/ocaml-4.06.0.tar.
######################################################################## 100.0%
==> ./configure -prefix /usr/local -with-debug-runtime -mandir /usr/local/Cell
==> make world.opt
==> make install PREFIX=/usr/local/Cellar/ocaml/4.06.0
 /usr/local/Cellar/ocaml/4.06.0: 1,989 files, 225.7MB, built in 7 minutes 35 seconds

この作業に７分ちょっとかかったので、全体で１０分を超えた。エラーがなければ３分以内で終わる場合もある。

アプリケーションホルダを見ると、何もない。

opam導入

$ brew install opam
Updating Homebrew...
==> Installing dependencies for opam: ocamlbuild, camlp4, clingo, aspcud
==> Installing opam dependency: ocamlbuild
==> Downloading https://homebrew.bintray.com/bottles/ocamlbuild-0.12.0.high_sierra.bottle.tar.gz
######################################################################## 100.0%
==> Pouring ocamlbuild-0.12.0.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/ocamlbuild/0.12.0: 30 files, 7.5MB
==> Installing opam dependency: camlp4
==> Downloading https://homebrew.bintray.com/bottles/camlp4-4.06+1.high_sierra.bottle.tar.gz
######################################################################## 100.0%
==> Pouring camlp4-4.06+1.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/camlp4/4.06+1: 165 files, 147.9MB
==> Installing opam dependency: clingo
==> Downloading https://homebrew.bintray.com/bottles/clingo-5.2.2.high_sierra.bottle.1.tar.gz
######################################################################## 100.0%
==> Pouring clingo-5.2.2.high_sierra.bottle.1.tar.gz
🍺  /usr/local/Cellar/clingo/5.2.2: 18 files, 6.2MB
==> Installing opam dependency: aspcud
==> Downloading https://homebrew.bintray.com/bottles/aspcud-1.9.4_1.high_sierra.bottle.tar.gz
######################################################################## 100.0%
==> Pouring aspcud-1.9.4_1.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/aspcud/1.9.4_1: 11 files, 445.5KB
==> Installing opam
==> Downloading https://homebrew.bintray.com/bottles/opam-1.2.2_4.high_sierra.bottle.tar.gz
######################################################################## 100.0%
==> Pouring opam-1.2.2_4.high_sierra.bottle.tar.gz
==> Caveats
OPAM uses ~/.opam by default for its package database, so you need to
initialize it first by running (as a normal user):

$  opam init

Run the following to initialize your environment variables:

$  eval `opam config env`

To export the needed variables every time, add them to your dotfiles.
  * On Bash, add them to `~/.bash_profile`.
  * On Zsh, add them to `~/.zprofile` or `~/.zshrc` instead.

Documentation and tutorials are available at https://opam.ocaml.org, or
via "man opam" and "opam --help".

Bash completion has been installed to:
  /usr/local/etc/bash_completion.d

zsh completions have been installed to:
  /usr/local/share/zsh/site-functions
==> Summary
🍺  /usr/local/Cellar/opam/1.2.2_4: 31 files, 16.3MB

opamは、Ocaml PAckage Manager

 opam init
OPAM has already been initialized.Your system compiler has been changed. Do you want to upgrade your OPAM installation ? [Y/n] y

=-=- Upgrading system -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

System update successful. Go on with "opam init" ? [Y/n] y

In normal operation, OPAM only alters files within ~/.opam.

During this initialisation, you can allow OPAM to add information to two
other files for best results. You can also make these additions manually
if you wish.

If you agree, OPAM will modify:

  - ~/.bash_profile (or a file you specify) to set the right environment
    variables and to load the auto-completion scripts for your shell (bash)
    on startup. Specifically, it checks for and appends the following line:

    . /Users/ogawakiyoshi/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true


  - ~/.ocamlinit to ensure that non-system installations of `ocamlfind`
    (i.e. those installed by OPAM) will work correctly when running the
    OCaml toplevel. It does this by adding $OCAML_TOPLEVEL_PATH to the list
    of include directories.

If you choose to not configure your system now, you can either configure
OPAM manually (instructions will be displayed) or launch the automatic setup
later by running:

   opam config setup -a


Do you want OPAM to modify ~/.bash_profile and ~/.ocamlinit?
(default is 'no', use 'f' to name a file other than ~/.bash_profile)
    [N/y/f] 

Global configuration:
  ~/.opam/opam-init/init.sh is already up-to-date.
  ~/.opam/opam-init/init.zsh is already up-to-date.
  ~/.opam/opam-init/init.csh is already up-to-date.
  ~/.opam/opam-init/init.fish is already up-to-date.

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

1. To configure OPAM in the current shell session, you need to run:

      eval `opam config env`

2. To correctly configure OPAM for subsequent use, add the following
   line to your profile file (for instance ~/.bash_profile):

      . /Users/ogawakiyoshi/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

3. To avoid issues related to non-system installations of `ocamlfind`
   add the following lines to ~/.ocamlinit (create it if necessary):

      let () =
        try Topdirs.dir_directory (Sys.getenv "OCAML_TOPLEVEL_PATH")
        with Not_found -> ()
      ;;

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

ssreflect導入

http://ssr.msr-inria.inria.fr
Documentationを押すと、
Mathematical Components
のページになる。

＜メニューの作り方がよろしくない。選んだ言葉と、出てくる言葉は同じにするのがメニューの基本。＞

all_ssrefrectだからAを選択。

all_ssreflectを選択。

mathcomp.ssreflect.all_ssreflect.v

Require Export ssreflect.
Require Export ssrbool.
Require Export ssrfun.
Require Export eqtype.
Require Export ssrnat.
Require Export seq.
Require Export choice.
Require Export path.
Require Export div.
Require Export fintype.
Require Export fingraph.
Require Export tuple.
Require Export finfun.
Require Export bigop.
Require Export prime.
Require Export finset.
Require Export binomial.
Require Export generic_quotient.

個別にダウンロードするのは無理と判断。

http://ssr.msr-inria.inria.fr
で
「The homepaged of the Mathematical Components library moved to github.」
を押す。

「downloaded from github.」
を押す。

The Mathematical Components library 1.6.4
@CohenCyril CohenCyril released this on 7 Nov 2017 · 265 commits to master since this release

Assets
ssreflect-mathcomp-installer-1.6.4-8.7.0-win32.exe 22.5 MB 
ssreflect-mathcomp-installer-1.6.4-8.7.0-win64.exe 22.5 MB 
 Source code (zip)
 Source code (tar.gz)

Source code (zip)

ここで大事なのは、
「removes compatibility with Coq 8.4.*; supported Coq versions are 8.5, 8.6 and 8.7」

Coqの版の確認はCoq IDEでは、「Help」メニューの「About」を押すと表示する。

Coq 8.4以下であれば、更新してください。Macintoshなら、

$ brew cask upgrade coqide

SSreflect解凍　

INSTALLファイルを読む。

# INSTALLATION PROCEDURE

Users familiar with OPAM can use such tool to install Coq and the Mathematical Components library with commands like

    opam repo add coq-released http://coq.inria.fr/opam/released
    opam install coq-mathcomp-fingroup

This document is for users that installed Coq in another way, for example
compiling it from sources.

## REQUIREMENTS

Coq version 8.5 to 8.7.0

## BUILDING

The Mathematical Components library is divided into various installation
units.  On can install the entire library (compilation time is around 35 minutes) or only some of its units.

In both cases, if Coq is not installed such that its binaries like `coqc`
and `coq_makefile` are in the PATH, then the COQBIN environment variable
must be set to point to the directory containing such binaries.
For example:

    export COQBIN=/home/user/coq/bin/

Now, to install the entire library, including the SSReflect proof language:

    cd mathcomp-1.6/mathcomp
    make -j2 && make install

If one wants to only install a few modules he should instead run make
inside the modules he wants to install *in the following order*:

  1. ssreflect
  2. fingroup
  3. algebra
  4. solvable
  5. field
  6. character

This means that one cannot install, say, algebra without having already
installed fingroup. An example:

    cd mathcomp-1.6/mathcomp
    cd ssreflect && make -j2 && make install
    cd ../fingroup && make -j2 && make install

## CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE

The `mathcomp/ssreflect/` directory comes with a small configuration file
`pg-ssr.el` to extend ProofGeneral (PG), a generic interface for
proof assistants based on the customizable text editor Emacs, to the
syntax of ssreflect.

The >= 3.7 versions of ProofGeneral support this extension.

- Following the installation instructions, unpack the sources of PG in
a directory, for instance <my-pgssr-location>/ProofGeneral-3.7, and add
the following line to your .emacs file.
Under Unix/MacOS:

    (load-file
      "<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" )
    (load-file "<my-pgssr-location>/pg-ssr.el")

Under Windows+Cygwin:

    (load-file
      "C:\\<my-pg-location>\\ProofGeneral-3.7\\generic\\proof-site.el")
    (load-file "<my-pgssr-location>\\pg-ssr.el")

Where <my-pg-location> is the location of your own ProofGeneral
directory, and where <my-pgssr-location> is the location of your pg-ssr.el
file.

Coq sources have a .v extension. Opening any .v file should
automatically launch ProofGeneral.

＜この項は書きかけです。＞

Macintosh High Sierraの日本語入力機能が、画面の操作の仕方によって入力した文字を、頻出文字に変換して保存することがある。そのため、誤植が現在多発しています。誤字、脱字等がありましたら、ご指摘くださると幸いです。

自己参照

「coq入門」の入門
https://qiita.com/kaizen_nagoya/items/13566f0b2083ea8d4998

「Coqで証明書いてみた」の１行づつの実行を記録してみた。
https://qiita.com/kaizen_nagoya/items/6b8398bf6980315945c6

coq(ide)を使おう　または　初めてのcop(ide) mac編
https://qiita.com/kaizen_nagoya/items/a236dfbfaa4f946b4f8d

Godel’s Incompleteness Theorem in coq 壁いくつ、今壁4つ
https://qiita.com/kaizen_nagoya/items/181cb3dae504f64d0619

「Coqの余帰納法でハマってしまった」を記録
https://qiita.com/kaizen_nagoya/items/7c9e32a024aeaf7b5658

MacintoshでCoqide
https://qiita.com/kaizen_nagoya/items/0314ca15130bdfa9dce2

<この項は書きかけです。順次追記します。>
This article is not completed. I will add some words and/or centences in order.

自己記事一覧

Qiitaで逆リンクを表示しなくなったような気がする。時々、スマフォで表示するとあらわっることがあり、完全に削除したのではなさそう。

４月以降、せっせとリンクリストを作り、統計を取って確率を説明しようとしている。
2025年２月末を目標にしている。

一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39

仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df

Qiita(0)Qiita関連記事一覧（自分）
https://qiita.com/kaizen_nagoya/items/58db5fbf036b28e9dfa6

Error一覧 error(0)
https://qiita.com/kaizen_nagoya/items/48b6cbc8d68eae2c42b8

C++ Support(0)　
https://qiita.com/kaizen_nagoya/items/8720d26f762369a80514

Coding(0) Rules, C, Secure, MISRA and so on
https://qiita.com/kaizen_nagoya/items/400725644a8a0e90fbb0

Ethernet 記事一覧　Ethernet(0)
https://qiita.com/kaizen_nagoya/items/88d35e99f74aefc98794

Wireshark 一覧 wireshark(0)、Ethernet(48)
https://qiita.com/kaizen_nagoya/items/fbed841f61875c4731d0

線網（Wi-Fi）空中線(antenna)(0) 記事一覧(118/300目標)
https://qiita.com/kaizen_nagoya/items/5e5464ac2b24bd4cd001

なぜdockerで機械学習するか書籍・ソース一覧作成中 (目標100)
https://qiita.com/kaizen_nagoya/items/ddd12477544bf5ba85e2

プログラムちょい替え（0）一覧:4件
https://qiita.com/kaizen_nagoya/items/296d87ef4bfd516bc394

言語処理100本ノックをdockerで。python覚えるのに最適。:10+12
https://qiita.com/kaizen_nagoya/items/7e7eb7c543e0c18438c4

Python(0)記事をまとめたい。
https://qiita.com/kaizen_nagoya/items/088c57d70ab6904ebb53

安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409

プログラマによる、プログラマのための、統計(0)と確率のプログラミングとその後
https://qiita.com/kaizen_nagoya/items/6e9897eb641268766909

転職(0)一覧
https://qiita.com/kaizen_nagoya/items/f77520d378d33451d6fe

物理記事　上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff

量子(0) 計算機, 量子力学
https://qiita.com/kaizen_nagoya/items/1cd954cb0eed92879fd4

数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d

統計(0)一覧
https://qiita.com/kaizen_nagoya/items/80d3b221807e53e88aba

図(0) state, sequence and timing. UML and お絵描き
https://qiita.com/kaizen_nagoya/items/60440a882146aeee9e8f

品質一覧
https://qiita.com/kaizen_nagoya/items/2b99b8e9db6d94b2e971

言語・文学記事　１００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6

医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82

自動車　記事　１００
https://qiita.com/kaizen_nagoya/items/f7f0b9ab36569ad409c5

通信記事１００
https://qiita.com/kaizen_nagoya/items/1d67de5e1cd207b05ef7

日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68

英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d

音楽　一覧(0)
https://qiita.com/kaizen_nagoya/items/b6e5f42bbfe3bbe40f5d

「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b

鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/faa4ea03d91d901a618a

OSEK OS設計の基礎　OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3

coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68

官公庁・学校・公的団体（NPOを含む）システムの課題、官（０）
https://qiita.com/kaizen_nagoya/items/04ee6eaf7ec13d3af4c3

「はじめての」シリーズ　ベクタージャパン　
https://qiita.com/kaizen_nagoya/items/2e41634f6e21a3cf74eb

AUTOSAR(0)Qiita記事一覧, OSEK(75)
https://qiita.com/kaizen_nagoya/items/89c07961b59a8754c869

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

LaTeX(0) 一覧　
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792

自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b

Rust(0) 一覧　
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927