So-net無料ブログ作成
前の10件 | -

JIRAやConfluenceのアドオンをGoogle App Engineで動かす [Java]

JIRAやConfluenceのクラウド版のアドオンを作ってGoogle App Engineで動かすためのMavenアーキタイプを作成しました。

https://bitbucket.org/tkob/acspring-gcloud-quickstart

いまAtlassianのクラウド製品のアドオンを作るときはAtlassian Connectという作法に従って、Webアプリケーション(Atlassian製品の外で動作する)をアドオンとしてつくって製品と連携するということになっています。それをJavaで作るときはAtlassian Connect Spring BootというSpring BootベースのフレームワークがAtlassian公式として公開されています。

https://bitbucket.org/atlassian/atlassian-connect-spring-boot

JIRAアドオンを気軽に作ろうと思うとこれを動かすためのサーバーを見つけないといけません。ここで無料のサーバーで動かしたい…と思うと、今だとGCPのフリーティアーが候補になると思います。

1つの候補はCompute Engineのf1-microインスタンスを使うことですが、ここで問題になるのはAtlassian ConnectではHTTPS通信を必須としていることで、GCEの場合だと追加でドメイン取得が必要となります。

もう1つの可能性はApp Engineのスタンダード環境を使うことですが、(1) Spring BootはJava8以降が要件であること (2) フリーティアーで使えるストレージはCloud Datastoreしかない(Atlassian Connect Spring BootはSpring Dataを使ってインストール先ホストを保存するのだが、Cloud Datastore用のSpring Dataがない)という点が問題でした(appspot.comドメインはHTTPSが使えます)。

(1)については最近までGAEスタンダード環境ではJava7のみだったのが最近Java8対応したことで解消されました。(2)については自分で作ることで解消しました。1つ前の記事のSpring Data Google Cloud Datastoreがそれです。

手順にしたがってMavenアーキタイプからプロジェクトを作るとサンプルアプリが動くようになっていて、このアプリはJIRAから課題を取得してDatastoreに保存し、それを集計して表示するということをやっています(なお、Datastoreは集約関数が利用できないため本来こうした集計には向いていません。使い方の例としてそのようにしています)。
nice!(0)  コメント(0) 

Spring Data Google Cloud Datastoreを作った。 [Java]

Spring Data Google Cloud DatastoreというJavaのライブラリを開発しました。

https://github.com/tkob/spring-data-gclouddatastore

その名の通りSpring Dataの作法でGoogle Cloud DatastoreのデータをCRUDするものです。クエリメソッド(インターフェイスにfindByFooOrderByBarなどメソッド定義するとそのメソッド名に従った実装を提供する機能)にも対応しています。
nice!(1)  コメント(0) 

Isabelleの練習 - 命題論理の自然演繹 [Isabelle]

「PPLサマースクール2017 Isabelle/HOL による証明とプログラミング」 http://ppl.jssst.or.jp/index.php?ss2017 を受講しに行っていた。結果として自分がIsabelleを咀嚼するのはまだかかりそうだという感想だったが、もっと初歩的なことをやって練習していくことにしたい。

題材としては論理学の教科書に出てくるような自然演繹による証明をIsabelleでやってみることにする。

自然演繹というのは、命題論理の証明を「P,Q... |- R」のように前提P,Q,...から帰結Rが出てくるものとするとP,Q,...に対してあらかじめ用意されたルールを適用して変形することで最終的にRが出てくれば証明完了というものだ。

Isabellの証明はtheoryという構造の中に書く。jEditで次のようなファイルを作ってNaturalDeduction.thyというファイル名で保存する。

theory NaturalDeduction
  imports Main
begin
  (* ... *)
end

ファイル名とtheoryの名前は一致しなければならない。また、jEditは特に拡張子を自動でつけてくれないが、拡張子がないと証明ファイルとして認識されないので注意しなければならない。

"imports Main"とは何か、はよくわかっていないが気にしないことにする。#include <stdio.h>のようなものだろう。

コメントはMLスタイルで、「(*」と「*)」で囲む。

1つ目の例題として、"P∩Q, R |- Q∩R"を証明してみよう。なお、この記事で使う例題はすべてHuth and Ryan (2004) "Logic in Computer Science"から採っている。

これを証明するにはまずP∩QからQを取り出し(P∩Qが成立するということはQ単独でも成立する)、QとRからQ∩Rを作る(QとRが成立するということはQ∩Rも成立する)必要がある。

問題はIsabelleでそのようなルールが何という名前で提供されているかだが、既存の定理を探すにはfind_theoremsというコマンド(?)を使う。

find_theorems "_ ∧ _ ⟹ _"
find_theorems "_ ⟹ _ ∧ _"

このように書くと検索結果の最初のほうに出てくるconunct2とconjIが求めているものだとわかる。

  HOL.conjunct2: ?P ∧ ?Q ⟹ ?Q
  HOL.conjI: ?P ⟹ ?Q ⟹ ?P ∧ ?Q

さて、"P∩Q, R |- Q∩R"という定理を表明するにはこのように書けばいいようだ。

theorem Example_1_4:
  (*fixes P Q*)
  assumes 1: "P ∧ Q"
  assumes 2: "R"
  shows "Q ∧ R"

つまり前提をassumes、帰結をshowsのところに書く。前提はassumes 1: "P ∧ Q" and 2: "R"と書いてもいいようだ。

コメントアウトしているfixes P Qは「任意のPとQをとった時に」という意味だがこれは書かなくても暗黙の裡にそうなるそうだ。

「1:」とかいうのは前提などに後で使うための名前を付けている。

これだけだと問題を表現しただけで、証明ではない。証明は続けて書くのだが、こうなる。

proof-
  have 3: "Q" using 1 by (rule conjunct2)
  show 4: "Q ∧ R" using 3 2 by (rule conjI)
qed

proofのあとにハイフンをつけるのは…なんだっけ。セミナーで説明してもらったと思うのだがあまり理解できず、忘れてしまった。ともかくこの例ではハイフンを消すとエラーになる。

前提からこういう事実が導けますというのをhaveとかshowで宣言する。haveとshowの違いは、途中に来るのがhaveで最後に来る(証明したかった)ものがshowだと考えればよいようだ。

1から3はconjunct2で変形できるのでby (rule conunct2)になる。usingがIsabelle的にどういう機能なのかきちんと理解していないのだが、とりあえずこの例ではルールの引数を指定するようなイメージのものだと解釈できる。3と2を使ってconjIを使うと4が出せる。

なお、jEditのOutputパネルでProof stateを表示しておくとproofの先頭にカーソルを置くと

proof (state)
goal (1 subgoal):
 1. Q ∧ R

と表示され、show 4:...の行末では

goal:
No subgoals!

となる。「No subgoals!になったらそこにqedと書く」と思っておけばよいようだ。

次に二重否定の除去(~~PからPを導く)と導入(Pから~~Pを導く)を扱う例を書きたい。

find_theorems "¬¬ _ ⟹ _"
theorem notnotI: "P ⟹ ¬¬P" by auto

検索により二重否定の除去はnotnotDが使えるとわかる。二重否定の導入は見つからなかったので独自に定理として作る。by autoで自動的に証明できてしまうのだが、それがなぜかは気にしないことにする。

これらを使うと"P, ~~(Q∩R) |- ~~P∩R"の証明が書ける。

theorem Example_1_5:
  assumes 1: "P"
  assumes 2: "¬¬(Q∧R)"
  shows "¬¬P∧R"
proof-
  have 3: "¬¬P" using 1 by (rule notnotI)
  have 4: "Q∧R" using 2 by (rule notnotD)
  have 5: "R" using 4 by (rule conjunct2)
  show 6: "¬¬P∧R" using 3 5 by (rule conjI)
qed

次にmodus ponensとmodus tollensを使った証明をしたい。いずれもそのものはIsabelleの中にないようなので定理として作っておく。

theorem  mp: "(P⟹Q) ⟹ P ⟹ Q" by auto
theorem  mt: "(P⟹Q) ⟹ ¬Q ⟹ ¬P" by auto
"P⇒(Q⇒R), P, ~R |- ~Q"はMPとMTを順に適用することで証明できる。
theorem Example_1_7:
  assumes 1: "P⟹(Q⟹R)"
  assumes 2: "P"
  assumes 3: "¬R"
  shows "¬Q"
proof-
  have 4: "Q⟹R" using 1 2 by (rule mp)
  show 5: "¬Q" using 4 3 by (rule mt)
qed

次は==>を導入するような式変形ルールを使う。これはいままでのルールとはちょっと違って「Pを仮定したときにQが導けるならばP==>Qを導いてよい」というものだ。これをIsabelle上で行うには、"P==>Q"の証明の中でassume Pを使って最後にshow Qを行えばよい。

"~Q⇒P |- P⇒~~Q"を証明する例が次のものだ。

theorem Example_1_9:
  assumes 1: "¬Q⟹¬P"
  shows "P⟹¬¬Q"
proof-
  assume 2: "P"
  have 3: "¬¬P" using 2 by (rule notnotI)
  show 4: "¬¬Q" using 1 3 by (rule mt)
qed

==>がいくつもあるような証明を行うときは入れ子構造になる。

theorem Example_1_11:
  shows "(Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"
proof-
  assume 1: "Q⟹R"
  show "(¬Q⟹¬P) ⟹(P⟹R)"
    proof-
      assume 2: "¬Q⟹¬P"
      show "P⟹R"
        proof-
          assume 3: "P"
          have 4: "¬¬P" using 3 by (rule notnotI)
          have 5: "¬¬Q" using 2 4 by (rule mt)
          have 6: "Q" using 5 by (rule notnotD)
          show 7: "R" using 1 6 by (rule mp)
        qed
    qed
qed

これは前提がないので"|- (Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"ということである。いままでhaveやshowで宣言した式の証明をするのにbyを使ってきたが、ここではbyの代わりに入れ子のproofを書いている。

ただし上の例はフラットに書いても同じことができる。

theorem Example_1_11':
  shows "(Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"
proof-
  assume 1: "Q⟹R"
  assume 2: "¬Q⟹¬P"
  assume 3: "P"
  have 4: "¬¬P" using 3 by (rule notnotI)
  have 5: "¬¬Q" using 2 4 by (rule mt)
  have 6: "Q" using 5 by (rule notnotD)
  show 7: "R" using 1 6 by (rule mp)
qed

連言、二重否定、条件とやったので今度は選言を使う。選言には「PがいえるならばP∪Qも言える」というもの(導入)と、「P∪Qが言えて、Pの場合とQの場合でいずれもRが導けるならば、Rを導いてよい」(除去)の2つがある。

前者はIsabelleに既にあり、後者はなかったので独自の定理を作る。

find_theorems "_ ⟹ _ ∨ _"
theorem disjE: "P∨Q ⟹ (P⟹R) ⟹ (Q⟹R) ⟹ R" by auto

これらを両方使うと"Q⇒R |- P∪Q ⟹ P∪R"の証明が書ける。

theorem Example_1_16:
  assumes 1: "Q⟹R"
  shows "P∨Q ⟹ P∨R"
proof-
  assume 2: "P∨Q"
  show "P∨R"
  proof-
    have 34: "P⟹(P∨R)"
    proof-
      assume 3: "P"
      show 4: "P∨R" using 3 by (rule disjI1)
    qed
    have 57: "Q⟹(P∨R)"
    proof-
      assume 5: "Q"
      have 6: "R" using 1 5 by (rule mp)
      show 7: "P∨R" using 6 by (rule disjI2)
    qed
    show "P∨R" using 2 34 57 by (rule disjE)
  qed
qed

次に"P⟹(Q⟹P)"を証明することを考えてみる。この場合Pは前提としているんだからQは関係なくPを前提しているということからそのままPが出てくるはずだ。Huth and Ryan (2004)ではこのルールをcopyと呼んでいる。適当に入力してあたりをつけてみたところ、Isabelleでは「by assupmtion」と書けばいいようだ。

theorem Example_copy:
  shows "P⟹(Q⟹P)"
proof-
  assume 1: "P"
  show "Q⟹P"
  proof-
    assume 2: "Q"
    show 3: "P" using 1 by assumption
  qed
qed

次の証明では「Pと~Pが両方出てきたら矛盾している」と例の「矛盾からは何でも出てくる」を使う。前者はnotE、後者はFalseEとしてIsabelleで用意されている。

theorem Example_1_20:
  assumes 1:"¬P∨Q"
  shows "P⟹Q"
proof-
  have a: "¬P⟹(P⟹Q)"
  proof-
    assume a2: "¬P"
    show "P⟹Q"
    proof-
      assume a3: "P"
      have a4: "False" using a2 a3 by (rule notE)
      show "Q" using a4 by (rule FalseE)
    qed
  qed
  have b: "Q⟹(P⟹Q)"
  proof-
    assume b2: "Q"
    show "P⟹Q"
    proof-
      assume b3: "P"
      show "Q" using b2 by assumption
    qed
  qed
  show "P⟹Q" using 1 a b by (rule disjE)
qed

最後に「Pと仮定して矛盾が導かれるならばPではない(~Pを導ける)」を使う。これはIsabelleではnotIという名前である。

theorem Example_1_21:
  assumes 1: "P⟹Q"
  assumes 2: "P⟹¬Q"
  shows "¬P"
proof-
  have 36: "P⟹False"
  proof-
    assume 3: "P"
    have 4: "Q" using 1 3 by (rule mp)
    have 5: "¬Q" using 2 3 by (rule mp)
    show 6: "False" using 5 4 by (rule notE)
  qed
  show "¬P" using 36 by (rule notI)
qed
以上Isabelleで命題論理の自然演繹の証明をいくつか書いてみた。「~のようだ」が多い記事になったことは申し訳なく思う。


nice!(1)  コメント(0) 

CSV parsing for Standard ML [SML]

ありそうでなかった(と思う)、Standard ML用のCSV読み込みライブラリを作りました。

CSV parsing for Standard ML

単純な使い方はテストケースを見るとすぐわかると思います。


Standard ML用の新しいXMLパーサー [SML]

Standard ML用のXMLパーサーを作った。

UXML

SMLの世界にはSMLで書かれたXMLパーサーが(知っている範囲では)すでに2つある。 1つはfxpという、かなり昔からあるもので、これはDTDの検証も行うフルセットのXML1.0準拠もの、 もう1つはSMLNJ-LIBの中にあるXMLストラクチャで、これはかなり非力なものだ。

UXMLは非検証のXMLプロセッサーとしてXML1.0になるべく準拠しようとしている。 現段階ではUTF-8しか受け入れない点と&#x10000;以上の文字を受け入れない点 (これはUXMLが依存しているSMLNJ-LIBのUTF8ストラクチャの制約)、 そしてXML1.0の整形条件違反のかなりの部分を報告しない(受け入れてしまう)点が 非準拠であるが、現実的な処理では十分に使える状態になっていると思う。

他の2つのXMLプロセッサーにない点として、 名前空間をサポートしている点と、XPathライクなナビゲーションAPIを持つ点がある。

使用するにはタグv.0.1.0を取得するか、Smackageから利用してほしい。 Smackageを使う場合、.smackage/sources.localにuxml git git://github.com/tkob/uxml.gitという行を追加し、SML/NJのCMファイルからは`$SMACKAGE/uxml/v0.1.0/uxml.cmのように参照する。


REPLのセッションをそのまま単体テストにする [Rehearsal]

REPLを持ったプログラミング言語処理系における原始的かつボトムアップな開発手順について考えよう。

まず小さな関数(だとか)を書く。 思った通りにかけているだろうか? そこでREPLを起動してソースをロードし、関数に対して入力を与え、結果を見る。 正常系は問題ない。 そこで異常な入力に対するハンドリングを関数内に追加して、異常処理がうまくいくことを見る。 でもさっきの正常系の処理が変わったりしていないだろうか。 そこでESCに続けてkを何度か押して(またはCtrl+Pを何度か押して)履歴から正常系の入力の式を復元してもう1回確認してみる。 関数の実装がちょっと気に入らないので変更する。 さっきまで動いていた分はまだ正しく動くだろうか。 そこでまた履歴から入力式を復元して叩いてみる。

この試行錯誤の中には「テスト」をしている箇所がある。 でもそれは揮発的だ。 REPLの履歴とプログラマの短期記憶の中だけにあって、しばらくすると消えてしまう。

テスト駆動開発、あるいは単に「単体テストを書く」ことは不揮発なテストによってコードの品質を保とうとする習慣である。 そこではREPLでアドホックにテストをするのではなくてテスティングフレームワークの定める形でテストコードを書く。 テストはことあるごとに自動で繰り返し実行される。 コードの変更が何かを壊していたらすぐにわかるし、いま現在のコードがすべてのテストを通過しているという確証を得ることができる。

では我々はそもそも最初からREPLなんて使うべきではなかったのだろうか。

長期的に見てテスティングフレームワークを使用すべきことは明らかだ。 でもREPLにも良い点はある。敷居の低さだ。 REPL上の作業ではプログラム実行とプログラマの頭の中は実際には 「とにかく入力を与えてみて、結果を見る。その次に結果が妥当かどうかを考え、妥当であればよしとする」 という関係になっている場合が多い。 これはある種の教義を信奉する人にとっては悪い習慣とみなされるだろうが、 ともかく「良い習慣」より敷居が低いことは事実だ。

問題はREPL上の作業とテスティングフレームワークで単体テストを書くこととの間の距離だ。 敷居の低いREPLで行った「テスト」を不揮発にしたくなった段階で、その距離が問題になる。 さっきまでのREPLに打っていた式ではなくて、テスティングフレームワーク上のアサーションを書かなければならなくなるのだ。

Rehearsal は、ここにフィットするテスティングフレームワークだ。 Rehearsalにおける単体テストはREPLのセッションそのものである。 例えばSML/NJでgreet.smlというテスト対象のプログラムを作り、次のようなREPLセッションを行ったとする。

- use "greet.sml";
[opening greet.sml]
val greet = fn : unit -> unit
val it = () : unit
- greet ();
hello!
val it = () : unit

このセッションを不揮発にするには、コピーアンドペーストで次のファイルを作る。

# greet function prints "hello!" to the console
 
```
use "greet.sml";
[opening greet.sml]
val greet = fn : unit -> unit
val it = () : unit
- greet ();
hello!
val it = () : unit
```

これを t/greet.t というファイル名で保存したとすると、テストを再実行するには次のコマンドを打つ。 このコマンドはもちろんMakefileなどに書いておけばよい。

$ rehearsal -command sml -ps1 '- ' -ps2 '= ' t/greet.t
1..1
ok 1 greet function prints "hello!" to the console

RehearsalはREPLがなんであるかは問わない。シェルでもよいしPythonでもScalaでもよい。 出力はPerlのTAPという形式に従っているが、JUnit XML形式の出力ができるのでJenkinsなどに集計させることもできる。

Reharsalのテストスクリプトの文法はMarkdownに合わせている。 だからドキュメントとしてのテストを書いて読みやすい形式に変換することもできるし、 「Markdownで書かれたその言語のチュートリアル」をそのままテストとして実行することもできる。 (例: Ruby, Python

REPLをそのままテストにすることの良い副作用として、プリティプリンタが得られる点がある。 例えばSMLでは(Javaのような言語とは違って)値を文字列に変換する関数は一般的には手に入らず、自分で書かなければならない。 また、SMLのテスティングフレームワークであるSMLUnitでは、 テストが失敗した場合の表示のためにアサートする値に対してプリティプリンタをセットで与えなければならない (期待値と実際の値の比較をエラーメッセージの中に含むために使われる)。 これは合理的ではあるもののREPLと単体テストの間の距離を一層離すことにつながっている。

一方でSMLでもREPLを使うならばそのような面倒くささはない。 REPLは自身のプリティプリンタによって値を表示していて、 プログラマがREPLでテストをするときはREPLが出してくれたものを目で見て妥当性を判断しているからだ。

このようにRehearsalのアプローチはREPLの気軽さを損ねずに自動的な回帰テストの利点を取り入れることができる。 こうした方法が「とにかく自動的な回帰テストを回し始める最初の一歩」を容易にすると考えている。


YokohamaUnit 0.3.0 の新機能 [YokohamaUnit]

YokohamaUnit の 0.3.0 をリリースした。

https://github.com/tkob/yokohamaunit/releases/tag/v0.3.0

このリリースには次の2つの新機能が含まれる。

リソース式

Javaのユニットテストではテストデータをクラスパス上に配置して(リソース)読み込むことがよくある。

Let url = `getClass().getResource("text1.txt")`.

この書き方は面倒くさい。そこでリソースのための特別な文法を用意した。

Let url = resource "text1.txt".

次のようにも書ける。それぞれリソースをInputStream, File, URIとして返す。

Let ins = resource "text1.txt" as `java.io.InputStream`.
Let file = resource "text1.txt" as `java.io.File`.
Let uri = resource "text1.txt" as `java.net.URI`.

一時ファイル式

一時ファイルを作成するための式を追加した。

Let tempFile = a temporary file.
Let tempFile = a temp file.

作られたファイルに対しては自動的にdeleteOnExitが呼ばれる。

その他

内部的にJavaslangを使うことにした。 Javaでタプルや関数的リストなどを使うのにこれまでは独自に実装したものを使っていて、自分で書くのも何だなと思っていた。 Functional Javaを検討したこともあったが、 いまいちJavaの中になじんでくれないAPIだったのでやめていた。 Javaslangのほうが比較的使いやすいように感じる。

使用例

nbmtoolsのテストで、上述の新機能を使っているので参考にしてほしい。

https://github.com/tkob/nbmtools/tree/f0cd916a7fa5d28228d6e05a37144413ea808c18/src/test/docy/nbmtools


リモート参照を含むNetBeansのnbmファイルをオフライン化するツール [Java]

NetBeansのプラグインモジュールをオフライン環境下でインストールするには nbmファイルをダウンロードしてくればよいが、 このnbmファイルがリモートのファイルへの参照を含んでいる場合、 単独ではインストールに失敗する。

nbmファイルは実態としてはZIPファイルだが、 その中に.externalというファイルが含まれている場合、 NetBeansが.externalの中に書かれたURLからダウンロードして置き換える仕組みになっているからだ。

一方で、この.externalを置き換えたZIPファイルをあらかじめ用意しておけば、 そのようなnbmファイルでもオフラインでインストールできる。 例えば下記のサイトでそのような方法が紹介されている。

NetBeans80にofflineでJUnitをインストール

しかしこれを手動で行うのは面倒だ。ということで自動で行うツールを作った。

nbmtools: https://github.com/tkob/nbmtools

これを使うと上掲の記事の作業は次のようにすればよい。

なお作ってはみたものの.externalを含むnbmファイルはあまり多くない気もしている。

技術的に特筆すべきことはないが、ScalaとJavaの半々でコーディングし、 テストのためにYokohamaUnitをドッグフーディングしている。 とてもひさしぶりにScalaを書いた。


YokohamaUnit 0.2.0 の新機能 [YokohamaUnit]

YokohamaUnit の 0.2.0 をリリースした。

https://github.com/tkob/yokohamaunit/releases/tag/v0.2.1 (バグフィックスの0.2.1に更新)

このリリースには次の2つの新機能が含まれる。

データ変換

テストを書いていると「フィクスチャをテスト可能なデータ型まで変換する」といった、 テストそのものには本質的でない処理がテストコード中にいくつも紛れ込んでしまうことがある。 例えば resources ディレクトリに配置したデータを InputStream から何らかのデータに変換したりといったようなことだ。

そうするとユーティリティメソッドを使って IOUtils.toString(is) のように書くことになるのだが、 あまり美しくない。

0.2.0 導入された機能を使うと is as InputStream と書けるようになる。 まずユーティリティメソッドを Java か何かで書いて、次のようにアノテーションをつける。

@As
public class DataConverters {
    @As
    @SneakyThrows(IOException.class)
    public static String inputStreamAsString(InputStream is) {
        return IOUtils.toString(is, "UTF-8");
    }
}

そうすると YokohamaUnit のテストからは次のように使えるようになる。

Assert `bais as String` is "hello"
where bais = `new ByteArrayInputStream("hello".getBytes("UTF-8"))`.

これを使うためには YokohamaUnit のオプションで -converter <base-package> と指定すると、指定したパッケージ以下(カンマ区切りで複数指定できる)から変換メソッドを見つけてくれる。

不変条件チェック

テスト対象に下記のように Invariant アノテーションをつける。

@lombok.AllArgsConstructor
@Invariant("({ it.count >= 0 })")
@Invariant("({ it.count < 10})")
public class DummyCounter {
    @Getter
    private int count;
 
    public void increment() {
        count++;
    }
}

そうすると YokohamaUnit の4フェーズテストの Setup と Exercise の後に、 テスト内容にかからわず常にこの不変条件をチェックし、満たされないとテストが失敗するようになる。

この機能を有効にするには -contract のオプションを指定する。


SMLZIP: Standard ML用のZIPファイル読み込みライブラリ [SML]

Standard MLからZIPファイルの読み込み・解凍をするためのライブラリを作った。

SMLZIP https://github.com/tkob/smlzip

特徴はPure-SMLである(Cバインディングではない)という点である。 機能は読み込みのみで、現状は最低限のことができる程度だ。 PKZIP形式から読み込みたい場合と、Deflate形式を直接扱いたい場合で 異なるMLB/CMを選択できるようになっている。 Smackage から利用できるようにするためのファイルも配置してみた。

バグ等をみつけたらGithubのissueに報告してほしい。


前の10件 | -

この広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。