---
# System prepended metadata

title: Cameleer

---

# 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)