Hatena::ブログ(Diary)

::Eldesh a b = LEFT a | RIGHT b このページをアンテナに追加 RSSフィード Twitter

2014-09-14

SML/NJのCygwin上でビルドに失敗するバグが修正された

私が以前パッチを書いて報告していた SML/NJのCygwin上でのインストールに失敗するバグ が 110.77(08/22/14) で修正されています。

Here is a list of tracked bugs fixed (or closed) with this release, please see the bug tracker for more details.

..

125 build script is broken on Cygwin-x86

..

http://www.smlnj.org/dist/working/110.77/110.77-README.html

実際のファイルには以下のように記述されてますので、*1

Older versions of Cygwin had a file /usr/include/exceptions.h, but this

file has disappeared in more recent versions. Here is the key bits

taken from ftp://ftp.com.univ-mrs.fr/pub/cygwin/usr/include/exceptions.h

やっぱり古いCygwinでは exceptions.h が存在したようなんですが、Cygwinはどれが本家のソースコードかよく分からないんですよねぇ(^^;;

とりあえずexceptions.hの内容は特にひねりも無く、でっち上げたパッチで正解だったことが分かって良かったです。

2014-09-12

ProofSummit2014とJSSST2014に参加

f:id:eldesh:20140910094313j:image:w300:right

遅めの夏休みを使ってProofSummit2014JSSST2014に行ってきました。

Coqチュートリアルとサマースクール(スパコンの話)に参加し、火曜日のPPLとその他セッションをふらふらしてた感じ。


Coqチュートリアルが主目的で参加したハズなんですが、謎の強烈な眠気であんまり覚えてません…。ひどい。

ssreflectのタクティックはかなりゴルフ的な方針で証明を短くしている感じを受けた気がします。

あとはかなり所謂工数を気にかけてCoq採用事例が解説されていたのが印象的でした。まだ開発で採用されるには時間がかかると思っているのですが、気づいたら証明も出来ない奴は人権が無い世界になるかも知れません。コワイ。


スパコンのサマースクールでは学部の授業を大急ぎでなぞった感じであまりテクニカル(に最新)な話は出ませんでした。

20年後でも使える言語じゃ無いとダメだそうですが、20年前に出来たソフトを使い続けてるんでしょうか。


他で印象に残ってるのは筑波の方のrefinement typeの拡張(?)とガリグ先生の型エイリアスでしょうか。PPL4

前者は自分で質問したのでやはり覚えてますね。

提案手法(述語を何回か展開して近似)では SMTソルバのfixpoint operatorより一般的なケースを扱えるようです。オフラインで教えて頂いたのですが、使ってるのはまさに質問で持ち出したZ3だったようで発表者の方にはその場で答えて欲しかった内容ですね(笑

それはともかくSMTソルバ流行ってますねぇ。


後者はOCamlモジュールの代入は通常定義をコピーするのに対して、名前を追跡するようになるものと理解しました。

アプリカティブファンクタに有用とのことですが、SMLにあっても嬉しいような気がします。どうなんでしょう?

あとNJ(というかCM)がさりげなく槍玉に上げられていたのでOCamlにだって仕様は無いじゃないか ( ー`дー´)と言っておきます(笑


FTDが初日のチュートリアルと被ってたので今回は会場で観られませんでした。

ちょっと残念でしたね。youtubeで公開してるので一応リンク貼っておきます。

2014-07-08

PolyMLの依存関係管理

Poly/MLREPLとしてもコンパイラとしても使うことのできるSML処理系です。

64bit環境に対応した処理系でもあるので、そういった意味でお手軽な場合も多そうですね。


ここではPolyMLのREPLでコードを読み込む方法を紹介します。

use

とりあえず use は備えています。指定したファイルの内容を直接replに入力したように動きます。

> val use;
val it = fn : use : string -> unit
> use "Sample1.sml";
structure Sample1 : sig val f : unit -> unit end
val it = (): unit
>

PolyML.make

本題。必要なデータ/ファイルだけを(再)読み込みする機能。

SML/NJのCM*1(の一分)に相当する機能がREPLに組み込まれています。

単一ファイルから成るオブジェクト

まず Sample1.sml というファイルがある場合、

$ ls
Sample1.sml
$ cat Sample1.sml
structure Sample1 =
struct
  fun f () = print "Sample1.f\n"
end

以下のように PolyML.make "structure/signature/functor名" を評価すると、対応するファイルを読み込みます。

> PolyML.make "Sample1"; (* structure名を指定 *)
Making Sample1
Created structure Sample1
structure Sample1 : sig val f : unit -> unit end
val it = (): unit
> Sample1.f();           (* 読み込まれている *)
Sample1.f
val it = (): unit
> PolyML.make "Sample1"; (* もう一度評価しても *)
val it = (): unit        (* 必要無いのでリコンパイルされない *)

前回の評価以降に変更されたファイルのみ読み込むので、二度連続でmakeしても余計なコンパイルは発生しません。

また、指定したファイルから公開される他の名前のオブジェクト*2も同時に公開されます。


複数ファイルから成るオブジェクト

以下のように structure Sample2 が Sample3 に依存している場合、

structure Sample2 =
struct
  fun f () = Sample3.f "Sample2.f"
end

structure名に対応したディレクトリ内に ml_bind.ML*3 というファイル名で実装を提供します。

$ ls Sample2/
ml_bind.ML  Sample3.sml # ml_bind.ML 内で Sample2 が定義されている

実際に読み込む場合は Sample1 の時と同じくstructure名を指定するだけです。

> PolyML.make "Sample2";
Making Sample2
Making Sample3
Created structure Sample3
structure Sample3 : sig val f : string -> unit end
Created structure Sample2
structure Sample2 : sig val f : unit -> unit end
val it = (): unit

出典

Chapter 7: The Poly/ML Make System

公式ドキュメントですが、上で紹介した機能以外はもう提供されていないみたいです。


メモ

ビルドに際して複雑なことは出来なさそうですが、CMやMLBasisより覚えることが少なくお手軽なので64bit環境しか手元に無い人はPolyMLに堕とすをお勧めするのもいいかも知れません(^^)

*1CompileManager

*2:structure/signature/functor

*3:なんだこの名前…

2014-06-10

GeSHiにSMLのsyntax highlightがマージされた

だいぶ前に書いてpull reqestしておいた、SMLコードのGeSHi用syntax highlight設定が本家にマージされてました。やったー。

support StandardML syntax #6


GeSHiはphpで書かれた汎用syntax highlighterで、言語毎に正規表現(のキモイ拡張)の塊を持っています。

各言語の設定は言語要素(文字列とかキーワードとか)毎に、それを切り出すための正規表現を持ちます。

今回StandardML用のファイルを書き、それが取り込まれました。


以下のように読み込んで表示すると…、

<?php
$src = file_get_contents('sample.sml');
$language = 'standardml';
$geshi = new GeSHi($src, $language);
$geshi->enable_line_numbers(GESHI_NORMAL_LINE_NUMBERS);
$geshi->set_line_style('background: #fcfcfc;', true);
$geshi->set_tab_width(4);
echo $geshi->parse_code();
?>

こんな感じになります。

f:id:eldesh:20140610114742p:image

(レコードとかラムダとか使うともうちょっとカラフルになります)


真面目にパースしているわけではないのでそもそも仕組みから怪しいわけですが、手元ではそれなりに動いているようです。文字リテラルが怪しかった気がする。(もう忘れた)

とりあえず全てのキーワードとBasisのモジュールは拾ってあるはず。


ところでSMLは中置演算子を好きに導入できるので…。まぁその辺はカンベンして下さい(^^;;

2014-06-04

SMLの規格書が公開されていた

気付いてなかったのですが、いつの間にか StandardML'97 の規格書がgithubで公開されています*1

SMLFamily/sml97


手元のCentOSビルドところ、ちゃんとroot.pdfが生成されました。

(app (yum install) ["texinfo", "texinfo-tex"]; latexmk(unzip _; install latexmk.pl ~/bin/latexml; latexmk -pdf root))


以前はMIT Pressから販売されているものを買うしかありませんでしたが、これで手軽に規格を読むことができますね(?)

*1:というか誰が気付くんだこれ…