yoshihiro503

Require Export ExtrOcamlBasic.
Require Import SCaml.

Extract Inlined Constant int => "SCaml.int".
Extract Inlined Constant operation => "Scaml.operation".

Extract Inlined Constant int_plus => "SCaml.(+)".
Extract Inlined Constant int_sub => "SCaml.(-)".

yoshihiro503

module OrderedTree

type elem = int

type tree =
  | Leaf
  | Node of (tree * elem * tree)

let rec all_tree pred t =
  match t with

yoshihiro503

gh_pages の設定方法

• githubプロジェクト作成
• circleci プロジェクト登録
• $ ssh-keygen -m PEM -t rsa -C "[email protected]" -f ./id_rsa_circleci
• githubのプロジェクト設定画面のDeploy keys項目にAllow write accessをONにして↑の公開鍵 id_rsa_circleci.pub を登録する
  • https://github.com/proof-ninja/proof-ninja.github.io/settings/keys/new
• circleciのプロジェクト設定でSSH permissions項目でAdd SSH Key する(秘密鍵登録), ホスト名はgithub.comにする

yoshihiro503

通常盤tezos node (mainnnet) の実行

mainnetブランチのtezosソースコード

実行準備

export PATH=~/tezos:$PATH
source ./src/bin_client/bash-completion.sh
export TEZOS_CLIENT_UNSAFE_DISABLE_DISCLAIMER=Y

yoshihiro503

必要用件

Ubuntuの場合

sudo apt -y install libev-dev libhidapi-dev

MacOSの場合

yoshihiro503

module Fact

open FStar.Mul

val factorial : x:int{x>=0} -> Tot int
let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)

val fact_tlrec_aux : int -> x:int{x>=0} -> Tot int (decreases x)

yoshihiro503

前提

• opam 2.0.4

インストール手順

z3のインストール　

brew install z3

yoshihiro503

Coqのプロジェクトを新規作成する方法

https://github.com/yoshihiro503/coq_template を参考にプロジェクトディレクトリを作成する

Coqソースファイル

Coqのソースファイルは .v 拡張子で src/ ディレクトリに追加する。そして _CoqProject に追加したファイルを列挙する。 *.ml ファイルも同じで大丈夫。

ビルド方法

yoshihiro503

let number_of_modules =
  if Array.length Sys.argv <= 1 then 100
  else Sys.argv.(1) |> int_of_string

let create_module_succ index =
  Printf.sprintf {|
-module(mod_%d).
-export([f/1]).

-spec f(input_%n) -> ok.

yoshihiro503

My Environment

• MacOS 10.12.6
• opam 2.0.0
• ocaml 4.07

Console

yoshihiro_imai:~ $ opam install --debug obeam.0.1.4