opam switchのエクスポート・インポート

文脈としては前回の続き。

opam switchとは、node.jsでいうところのasdf-vmやnodenvのような、OCamlコンパイラのバージョンを切り替えられる、opamの機能である。opam installでインストールしたパッケージたちも、各switchに保存されるため、開発環境を切り替えるのにとても便利だ。

camlspotter.gitlab.io

さて、ローカルで作ったswitchを他の人に共有したいことがある。たとえば研究の実験環境を保存したいときだ。
こういうときにはopam switch exportを使う。インポートしたいときはopam switch importで可能になる。

https://opam.ocaml.org/doc/FAQ.html#Can-I-get-a-new-switch-with-the-same-packages-installed

emacsとevilと

背景

EasyCryptの証明のためには、ProofGeneralが必須であり、それを動かすためにはEmacsを使わなければならない。一方で、私は昔からVimを使っているので、Emacsキーバインドはほとんど知らない。そこで、以前からSpacemacsのevilモードを使っていた。

ところが、opam switchによって実行するEasyCryptを変更しようとしたとき、Spacemacsで読んでいる$PATHにすべてのswitchのbinディレクトリが追加されており、うまくいかなかったため、Emacsで環境を作り直すことにした。

できたもの

evilプラグインとopam-user-setupを使って.emacsを作った。

また、undo-redoを使うため、Emacs28以降で動作する。

gist.github.com

FastifyのヘッダーをHooksで共通化する

問題

Fastifyで書かれたAPIサーバにて、以下のようなルートハンドラがあるとする。

getHelloHandler (request: FastifyRequest, reply: FastifyReply) {
    reply.header('Content-Type', 'application/json').code(200);
    reply.send({ hello: 'world' });
}

上記に出てくるreply.header('Content-Type', 'application/json')は、レスポンスヘッダにContent-Type: application/jsonを追加するコードである。
レスポンスをJSONで返すことが決まっている場合、このように毎回書くのは面倒くさい。これをHooksを使って共通化する。

ソリューション

Fastifyには、リクエスト/レスポンス、およびアプリケーションのライフサイクル*1に準じた複数のイベントトリガが設定されている。

www.fastify.io

これらのイベントトリガが発火したときに実行するフックを定義しておくことで、パケットに対して柔軟な制御ができる。

今回は上記のようなユーザ定義のルートハンドラを実行する前にヘッダを追加しておきたい。そこで、preHandlerフックを使う。

const serer = Fastify();
server.addHook("preHandler", (request, reply, done) => {
      reply.header("Content-Type", "application/json");
      done();
});

これによって、すべてのレスポンスパケットにContent-Type: application/jsonが付与されるようになる。

課題点

以下の場合は実行時に"Reply already sent"なるエラーが発生する。

  1. Content-Typeとしてapplication/jsonまたはtext/plain以外を指定したとき
  2. Content-Typeとしてtext/plainを指定しているにもかかわらず、オブジェクト型をreply.sendの引数に与えたとき

1は、Fastifyがデフォルトでapplication/jsonとtext/plain以外をサポートしていないためである。それ以外のContent-Typeヘッダーを追加したい場合は、以下の方法でパーサーを追加しなければならない。

www.fastify.io

Fastifyはreply.send()の引数のパースを、Content-Typeヘッダーの有無と、その種類を手がかりに行っている*2。したがって、2はtext/plainのパーサーがオブジェクト型を予期しておらず、パースに失敗した時点で処理を停止するのが原因と考えられる。

注意すべきなのは、このエラーで処理が失敗した際には、エラーメッセージのわりに、クライアント側にはレスポンスが返らないことだ。何らかのエラーハンドリングを必要とするが、個人的にはonErrorフックでレスポンスを返すのが良いと思う。

まとめ

FastifyのHooksの一例を紹介した。Fastify自体は理路整然と作ってあるものの、日本語の文献が少なく若干とっつきづらいところがある。今後も便利な機能があれば紹介していきたい。

*1:ライフサイクルはここを参照: https://www.fastify.io/docs/latest/Lifecycle/

*2:lib/reply.jsのReply.prototype.send参照

EasyCryptとProofgeneralのインストール

EasyCryptという暗号系の形式検証支援系をインストールしようとしたところ、詰まったところがたくさんあったので備忘録。
2019/11/12追記 ここを読まずに公式のGithubリポジトリの手順を読みましょう。

EasyCryptインストールまで

公式Githubを参考にインストールする。手順をおおまかに書くと、

  1. opam入れる
  2. opamにEasyCryptのリポジトリを追加する
  3. opam install depextしてopam depext easycryptする
  4. opam install --deps-only easycryptしてopam install ec-proversする
    ここまでしか書いていない資料があるが、これだけだとメタパッケージまでしか入っていないので、
  5. opam install easycryptする
  6. why3 config --detectする

5をしないと次のproofgeneralのインストールで詰まる。
なお親切な人がdockerイメージを配布しているので、4まではこれをつかって省略できる。

Proofgeneralのインストール

Coq等でおなじみProofgeneralは、公式でEasyCryptに対応している。

  1. opam install proofgeneralする
  2. emacsのパッケージアーカイブにMELPAを追加する。ここ参照
  3. package-install でexec-path-from-shellとopamをインストールする
  4. init.elに次を書き込む
(when (memq window-system '(mac ns))
  (exec-path-from-shell-initialize))

(opam-init) 

そのあと.emacsに次を書き込む

(load-file "$proof-general-home/generic/proof-site.el")

ただし $proof-general-home には opam config var prefixで出力されたパスを入れる。

emacsもopamもほぼ全く使ったことがなかったのでめちゃくちゃ大変だった