# Cameleer [TOC] ## URL - https://github.com/yuyaha/cameleer ## install ### opam - [2019年度「プログラミング言語」配布資料](https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/pl/setup.html) - 手元の opam の version は 2.1.2 ### cameleer - レポジトリをクローン ``` $ git clone https://github.com/yuyaha/cameleer.git ``` - ocaml をインストール - option は 全て yes でよい（？） - うまくいかない時は、opam を 最新 version に ``` $ cd cameleer $ opam switch create . ``` - solver をインストール - `cvc4` は Homebrew で install 可能 - `coq` の使い方はいまいちわからない ``` $ opam install alt-ergo altgr-ergo $ opam install z3 $ opam install why3-coq ``` - solver を why3 に追加 ``` $ why3 config detect ``` - 実行コマンド - why3-ide が開くので、Theories/Goals を右クリックして solver を選択 ``` $ cameleer smartcontracts/boomerang.ml ``` ## edit - 新しいライブラリを実装する - `src/ocamlstdlib.mlw` ## build - `Makefile` に書いてあるとおり - `make install` ## reference - [icfp21](https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/13/Cameleer-a-Deductive-Verification-Tool-for-OCaml) - [arxiv](https://arxiv.org/abs/2104.11050)