coqdocを使った

coqdocを初めて使ってみました。はじめは company-coq のスタイルに合わせて見出しとか書いてましたが、なんとなく気が向いたので公式(documenting-coq-files-with-coqdoc )の方を確認してみたのでした。目的はcoqスクリプトの(主にコメントの)整形スタイル…

静的コード解析の会#9

(会場と日程を変更しました) #静的コード解析の会 第9回 - connpass に行ってきました。今回も何らかの発表は出来ず。 どこかで宣伝したらしく、前回から人数が大幅に増えて14~5人くらいの参加者でした。参加者の傾向としては: なぜかIsabelle使いが多い。 …

RustでマルチスレッドWebサーバを作る例を写経

Final Project: Building a Multithreaded Web Server - The Rust Programming Languageを写経した。 標準ライブラリのみを使って簡単なマルチスレッドWebサーバを書く例。 スレッドプールを作ってacceptするたびに「htmlを応答する関数」をJobとしてチャン…

ブログ引っ越し完了

滑り込みではてなダイアリーから引っ越し完了しました。 移行が簡単に出来るのは素晴らしいですね。デザインはこれから横幅がいっぱいに使えるヤツをゆっくり探します。

歯が痛くて倒れていた

8月中旬頃、突然奥歯(の中の神経)に激痛が起こりました(結局明確な原因は不明)。 2週間くらいしてようやく普通の生活が出来るようになりました。あまりに酷い状態だったので書き留めておきます。 どんな状態だったかというと: 常に痛い。何もして無くても神…

terraformのチュートリアルを読んだ

terraformのチュートリアルを一通り読んで実行した。 チュートリアルを実行するのに必要な知識が全てチュートリアル内にあり、かなり分かりよい ほぼ写経で動く(1度AWSのよく分からないエラーが出たけど) 記述が古い箇所がある(動きはする) その時点でのconf…

静的コード解析の会#6で発表してきた

静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…) 前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。 が、今回の発表では多重集合、整礎関係、実際の処理系で検査でき…

SMLでSHA2アルゴリズムを実装しました

SML

SMLでSHA2(Secure Hash Algorithm)というハッシュアルゴリズムを実装しました。 https://github.com/eldesh/sha2_sml.gitに公開してあります。現在のところSML/NJで動作を確認しています。 #こういう基本的な部品から実装して行くのが重要です。たぶん。 実…

定理証明支援系 matita のdockerイメージを作った

Matitaという定理証明系のdockerイメージを作りました。 MatitaはBologna(ボローニャ)大学で作られた、OCaml(+lablgtk)製の、依存型に基づく定理証明器です。 Leanの論文から参照されていたので知りました。 定理証明器の研究用途に作成されたようなので実用…

SMLUnitのインストールを通してSML/NJ向けのライブラリのインストール方法を解説する

SML/NJにはCM(CompilationManager)というビルドツールが付いてきます。 以前は基本的な使い方を書きました>CompileManager(SML用make)の使い方。今回の記事ではSMLUnitというユニットテストライブラリを例にCMで管理するライブラリのインストール方法を説明…

MLtonのdockerイメージを作りました

SMLの最適化コンパイラであるMLtonのDockerイメージを作りました。MLtonは開発は行われているのですが、長らくリリースが出ていないため使いづらい状態です。あとなぜか私の手元だとビルドに失敗したりします*1。 そこで現状の開発ヘッドをビルドしたイメー…

VeriFastのDockerイメージを作りました

C言語/Java検証器であるVeriFastのDockerイメージを公開しました。 > https://hub.docker.com/r/eldesh/verifast/ 現時点(2017/8/24)での開発ヘッドをビルドしてあります*1。リリース版は公式サイトでバイナリが配布されているのでそちらを使いましょう。こ…

SML#3.3.0のDockerイメージを作った

Dockerの練習として SML#3.3.0 の入ったDockerイメージを作ってみました。> https://hub.docker.com/r/eldesh/smlsharp/ $ docker pull eldesh/smlsharp:3.3.0 とやれば使えるはず。ベースイメージは centos:centos7.3.1611 です。 LLVMのサイズが強敵でした…

Dockerイメージのアップロードが謎の失敗

VMware Player上のCentOSからDockerHubへのDockerイメージのアップロードが謎の理由で失敗する。 当然 docker login 済み。 以下のようになる。 smlsharp-3.3.0$ sudo docker push eldesh/smlsharp:3.3.0 The push refers to a repository [docker.io/eldesh…

ML勉強会#2 と ProofSummit2017 に参加した

ProofSummit2017とML勉強会#2に参加してきました。 とりあえず二日連続はつらいものがあった。 個々の感想 SML#の話は良かった。言語や処理系の機能が列挙されていると個人的に楽しい。そういう意味ではATSも楽しいんだけど、機能(のアップデート)が少なかっ…

ゼロから作るDeep Learningを読んだ

ゼロから作るDeep Learningを読み終わりました。おおよそ一ヶ月くらいかかりました。機械学習自体(とpython)の全くの素人状態から読みましたが、とりあえず、単独で読み切れる本です。 その点は良いですね。 本全体を通して、MNISTと言われる手書き数字のデ…

静的コード解析の会で停止性検証について発表してきた

静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました http://d.hatena.ne.jp/eldesh/20161121/1479703222">*1。 本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込ん…

静的コード解析の会 第0回 でVeriFastについて発表してきた

#静的コード解析の会 第0回でC言語(とJava)の検証器であるVeriFastについて発表してきました。資料は公開してあるので興味ある人は見てください。動画もあります。 > https://metasepi.connpass.com/event/42141/presentation/ 結構(私の理解が)きわどい質問…

古の商用SML処理系MLWorksを動かす

2016年現在SMLの処理系はいくつもありますが、昔はMLWorksという商用の処理系がありました。MLWorksは開発元のHarlequinが潰れて2000年くらいに姿を消していたのですが、突然2013年にオープンソースになりgithub上に公開されました。 実働していた頃は様々な…

MLKitの謎のバグを修正してaobenchが動くようにした

SML

AObench-SMLがSMLの処理系の一つであるMLKitに対応しました。これまではMLKitにバグがあり、実数の指数表現リテラルのうち小文字の'e'を使ったもの(e.g. 2e3 10e~5 など)が使えませんでした。 単にレキサの規則が足りてなかっただけなんですが(基本的過ぎて)…

QCheckをSML#に対応させた

以前紹介したSML版QuickCheckであるところの QCheck を SML#3.0.1で動作できるようにしてマージされましたヽ(゚ー゚*ヽ)(ノ*゚ー゚)ノ*1!! そのマージに続いていくつか変更があって現在バージョンが v1.2 に上がっていますので今後はこれを使いましょう。 #どうで…

Infer Introduction

C言語の静的自動検証器である Infer の使い方がある程度分かってきたので紹介します。 Infer Infer は、C言語(or [C++, Obj-C, Java])の検証器で、 自動で特定の種類のバグを発見してくれます。発見できるバグとして分かり易い例ではリソースリークを発見で…

z3sml リリース!

この記事は MLアドベントカレンダー 12日目の記事です。 SML# 向けに Z3 というライブラリのバインディングライブラリ z3sml をリリースしました。 Z3 は SMT*1ソルバ(もしくは単にSMT) と呼ばれる種類のソフトウェアで、ある種類の制約充足問題を自動で解く…

PolyMLのpretty printerをユーザ定義する

Poly/MLというStandardMLの処理系があります。 このPoly/MLの提供するREPLでは、入力した式の値をエコーバックする際に使用するプリンタ(REPLの'P')をSML自身のコード内で指定することができます。 この記事では Poly/ML のREPLのpretty printerを部分的に上…

Cygwin/X 1.17に繋げない

新たにCygwinをインストールしたマシン(win7 64bit)上で、Cygwinの提供するXサーバが使えなかった。 より正確には、XWin.exeは起動しているのにxterm等のクライアントが接続できない。 $ xterm xterm: Xt erorr: Can't open display: 192.168. ... またこの…

改訂新版C++ポケットリファレンスレビュー

前回のBoost.勉強会でいただいた 改訂新版C++ポケットリファレンス を一通りさらったのでレビュー(というか紹介)を書いておきます。 どんな本? この本は、目的から探せる形式でC++の(主に)標準ライブラリを解説した逆引きリファレンスです。 今回私が読んだ…

Boost.勉強会 #17 東京に参加

先日(2015/05/30)行われたBoost.勉強会 #17 東京に久々に参加してきました。 IIJ新社屋がめっちゃ綺麗でビビりつつ滑り込みセーフ(アウト)で会場着。 セッション資料は以下にまとまってます。 Boost.勉強会 #17 東京 タイムテーブル C++は適用ドメインがまっ…

firefoxの更新をキャンセルする

firefoxというブラウザでは [ソフトウェアの更新を確認] すると手元のソフトウェアが最新バージョンに更新される。 中断は(少なくとも素の状態では)出来ない。*1 何を言っているのか分からないと思うが事実だ。 ちなみにこの「ソフトウェアの更新」ボタンは…

random_rは使ってはいけない

random_r 関数は glibc が提供しているリエントラントな擬似乱数生成APIです。 複数のスレッドで乱数を使いたい場合はこれを使うべきらしい。*1 複数のスレッドが random() を使うような状況では、この関数を使用すべきではない。 その場合には random_r(3) …

XtoWに期待

Cygwin/Xの起動方法の変化を調べていて知ったのだけど、cygwinではXtoWという、よりネイティブ環境と密に連携できるWindow Managerが使える。 これを使うには startxtow というコマンドで X を起動すればよい。 プロトタイプらしく実際そういう品質のようで…