ブラウザ上でAgdaを試せるサイトを作ってみた

この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です.

Agdaコンパイルできないんだがとか,agda-modeってEmacsだけなんでしょ?とか,そういった話をちょくちょく耳にするし,ProofSummit2014で明日の記事担当のamutakeくんがブラウザからCoq使えるやつを発表してたりしたので,Try Agda というサイトを作ってみた.

リポジトリはここ https://github.com/notogawa/agda-interactive-server

バックエンドはHaskellでwai+warp+websocketでAgdaのライブラリからAgdaを直に利用.フロントはjquery+ACE editor.画面レイアウトはもちろんbiim兄貴リスペクトだ.

サーバ強くないし,あんまりデカい証明に使ったりするとガバガバなリロードのせいで激重になったりするかもしれないので,あくまでもお試し用で.

あと,Agdaやる場合は文字の都合上フォントがとても重要なので,DejaVu Sans Monoフォントを推奨する.フォントによっては,Unicode文字の幅とかがACE上での認識とズレるため,表示位置とカーソル位置が離れているといったことが起こる.

ACEに限らず大体のJavaScript製エディタが持つsyntax highlighting機構は,AgdaTopが提供するsyntax highlighting情報を適切に食ってキープできるカンジじゃなさそうで,編集中はhighlightingが消えてしまうがここは割り切っている*1.代わりに適当なタイミングでサーバ側とWS通信し,リロードが入ってhighlightingを復活させるようにしている.

エディタ上でバックスラッシュ叩くとUnicode文字入力モードになる.agda-modeのやつを移植しているので,大体同じようにUnicode文字入力できるはずだ.モジュールはMainのみ決め打ち.

右上のウィンドウは各ゴールに対する入力窓と,Agdaコマンド,エディタコマンドになっている.プルダウンメニューでゴールを選択すると,Contextが勝手に走ってゴールの型や前提条件の型が確認できる.テキストフィールドに入力してRefineすることで穴埋めが進む.Caseは場合分けの生成だけど,まだ関数ケースのみ対応でラムダケースには非対応.なので,ラムダケースに対して使うと悲しみを背負うと思う.SaveとLoadはlocalStorageへエディタのバッファ内容を保存・読み出しをする.

右のウィンドウは情報表示ウィンドウになっており,型エラーの情報や,Context情報などを表示する.

下のウィンドウはWS通信によるサーバ側のAgdaTop挙動を表示している.あまり気にしなくてよい.

目下一番の問題は,biimシステムなのに左下を担当する適切なキャラクターがいないことだ.

*1:と言いつつ誰かいいものあったら教えて