この記事は SATySFi Advent Calendar 2020 の13日目の記事です。 SATySFi ユーザのみなさま今年も amutake/satysfi (以降 docker-satysfi) をご利用いただきありがとうございました (docker-satysfi は SATySFi と Satyrographos (SATySFi のパッケージマネ…

これは SATySFi Advent Calendar 23 日目の記事です (なぜか12月12日付の記事になっていますが23日目の記事です…)。 22日目は zr_tex8r さんの徹底検証！ SATySFiはLaTeXの代わりになるかでした。 24日目は monaqa さんの予定です。 私は進捗大陸という技術…

この記事は SATySFi Advent Calendar 2020 8日目の記事です。7日目は abenori さんによるSATySFiで可換図式でした。9日目は fiveseven さんの予定です。 表題の通り、SATySFi で書かれた本などのまとめを作ってみました。こちらのリンクにあります。 最新の…

(これは主に自分の備忘のための記事です) 最近出た opam-bin を使って、opam で satysfi パッケージをインストールできる小さい docker image を作りました。satysfi-docker の opam-slim タグです (experimental 扱い)。 satysfi-docker については satysfi…

これは SATySFi Advent Calendar 2019 6日目の記事です。 5日目はzr_tex8rさんによるSATySFiコード中で整数を16進数で書きたいでした。 3日目の記事では satysfi-docker の紹介をしましたが、今回は satysfi-docker と GitHub Actions を使って SATySFi パッ…

この記事は SATySFi Advent Calendar 2019 3日目の記事です。 2日目はSATySFiの作者であるgfngfnさんによるSATySFiの2段組機能でした。 追記 2020/12/08: satysfi-docker から docker-satysfi に名前を変更しました。以降の文章は面倒なので satysfi-docker …

尊敬している先輩が毎年の年末に一年の総括を書いているので、自分も真似してやってみる。 仕事 今年の半分は sluicegate という、メディアストリームを fan-out させるシステムを作っていた。これに関しては Erlang & Elixir Fest. 2018 で発表しているので…

finagle の finch を触っています。 現時点での最新版は0.9.2なのですが、0.9.2には RequestReaders.bodyOption: RequestReader[Option[String]] とこれを使っている RequestReaders.body: RequestReader[String] にバグがあります。0.9.3-SNAPSHOT では直っ…

前回 dotfiles を大幅にアップデートしたのがちょうど2013年の10月だったので、約2年ぶりの更新です。 以下変えた部分。 Emacs el-get をアップデートした init-loader を使うようにしたい el-get-lock を使うようにした 新しいマシンに .emacs.d を持ってく…

最近 Rust に再入門しています。 言語初心者によくある問題として、良い (信頼できる) ライブラリがどれかわからないというものがあります。 Rust の中央パッケージリポジトリである crates.io は各パッケージのダウンロード数が書かれていて、 良さそうなラ…

表題のとおり、mbed という自分のような初心者にも優しいマイコンで PS2 を操作するなにかを、研究室の同期3人で作りました。 これは個人の日記ですのであとで3人でもう少し詳しい解説記事を書くかもしれませんが、とりあえず簡単に言うと、 こんなので、 こ…

PBLというチーム開発の授業でうちのチームはこんなの作ったり使ったりしたよという記事です。 成果発表会や展覧会では技術的なことの説明はほとんどしなかったように思うので、せっかくなので公開しておきます。 来年以降この授業を取る人の参考になればと思…

個人的に更新を楽しみにしているWeb漫画10の2回目です。前回と被っているものもあります。 Web漫画とは言えないものもありますが、とりあえず2015年2月3日現在Webで読めればよしとします。 (順不同) NOBELU-演- 一番楽しみにしてる 宇宙大恋愛 マイアニマル …

utop のバグっぽいものを見つけたので、それを issue に書くために GIF のツールを使ってみた。 keycastr/keycastr · GitHub Gifzo - 宇宙一簡単なスクリーンキャスト共有 Keycastr はキーストロークを画面に表示してくれるツールで、Gifzo はスクリーンショ…

環境: OSX Yosemite パッケージマネージャ: homebrew, homebrew-cask, opam コンパイラ: ocaml4.01.0+clang-fix brew cask install xquartz これを入れないと pkg-config でコケる (X が入ってないというエラーはでない) 普通に XQuartz.dmg を入れた状態だ…

プログラミングの勉強を本気でWebゲーム化した「CodinGame」が時間泥棒確定！ 面白そうなのでやってみました。 いくつか解いてみた感想 ただのプログラミングコンテストの問題 標準入力から情報を受け取って、なんらかの計算をして標準出力に計算結果を出力…

チャット上で証明が書けたら面白そうだなと思ったので、ProveEverywhere のサーバを使う hubot スクリプトを書きました。 こんなかんじ。 導入方法 (hubot 自体の導入方法については他の記事に任せます) 適当なサーバに Coq 8.4 以上をインストールします。 …

夏休みです。 Coq Summer School 8月の終わりに NII Shonan School on Coq に行ってきました。 一週間みっちりCoq漬けでした。楽しかった。でも英語ができればもっと……。 夏ゼミ Coq合宿が終わった3日後から2泊3日の研究室合宿がありました。千葉の館山に行…

追記 2015/11/11 今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。 opam repo add coq-released https://coq.inria.fr/opam/released # opam に Coq 関連のライブラリを追加 opam install -j4 coq.8.4.6 …

プロンプトについて ProofGeneral や、coqtop-vim は裏で coqtop -emacs というコマンドを実行して、そこと通信しています。 coqtop -emacs を実行すると、標準エラー出力に <prompt>Coq < 1 || 0 < </prompt> というのが出てきます。ここを見ると現在の coqtop の状態がわか…

下のようなエラーが出たとき <command line>: can't load .so/.DLL for: /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib (dlopen(/Users/amutake/work/jype/jype-doc/. cabal-sandbox/lib/x86_64-</command>…

cabal-install の bootstrap.sh で module ‘stm-2.4.3:Main’ is defined in multiple files: ... みたいなエラーが出てコケたときは、 % cd stm-2.4.3 % ./Setup install % cd ../ % ./bootstrap.sh とやればよい。仕組みは不明。

golang の GOPATH について。 昨日まで GOPATH で指定したディレクトリは、Haskell の .cabal ディレクトリみたいにパッケージがインストールされるだけの場所だと思ってたけど、自分でコードを書くときもこの中で作業をするということを知った。 研究室の先…

個人的に更新を楽しみにしているWeb漫画10選です。順不同。 パペラキュウ All You Need Is Kill 市場クロガネは稼ぎたい はるこ少女期 徒然チルドレン 働かないふたり 俺とヒーローと魔法少女 T.Yめもり～ず アクアの魔法 裏ジャック

Why3 で遊んでみたのでメモ．インストールで手間取った．環境は Mac OS X 10.9.1 です． Why3 のインストール ※この方法は Mac OS X かつ Homebrew 専用です．Linux や MacPorts でのインストールはわかりません． ソースからは面倒なので，OCaml のパッケー…

idris-0.9.10 がリリースされたのでちょっと触ってみた。http://www.idris-lang.org/idris-0-9-10-released/ 証明付き型クラス 以前の idris では下のツイートのようなことはできなかったのですが、できるようになっていました。 型クラスを実装するときに、…

最近巷で話題の Idris (依存型を持つ純粋関数型言語)ですが、この Idris にも vim と emacs のプラグインがあります。 idris-vim vim の idris-mode です。Idris のメイン開発者である Edwin Brady さんも開発に加わっています。 リポジトリ Edwin Brady さ…

参照: http://cp.reddit.com/r/haskell/comments/1ozukp/anyone_running_ghc_763_on_osx_mavericks/ Xcode 5 が clang を使っていて gcc4.2 を提供しなくなったせいらしい。 clang に対応している GHC7.8 が出るまで待つか GHC HEAD を使えばいいらしいけど…