このたびAgdaを最新の2.5.1にバージョンアップしたので、手順を記録しておく。 特に、新しくなったライブラリ管理の設定方法がややこしかった。手順は主に以下に従った。 http://hackage.haskell.org/package/Agda-2.5.1/changelog 何にせよ、ようやくまとも…

以前、2.4.2.2のインストールでだいぶ手こずった話を書いて、Agdaをやってみようという方の気をそいだ感があるのだが、このたびリリースされた2.4.2.4へは素直にバージョンアップできた。cabalを叩くだけで。ちなみに、次のリリースは2.4.4で、ライブラリの…

去年のProofsummitのときに、Agdaという言語はなぜそういう名前なのかという話を飲み会でしたら結構好評だったので、あらためて調べたことも含めて。Agdaとは何かというと、これのことみたい。 実際、Agda the henでググってみると http://bit.ly/1aBKbbH と…

http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ でポスター発表してきました。ポスター（実態はスライド）も http://www.slideshare.net/ShujiKinoshita/ppl2015-uivalidationfull に置いてますが、それだけだと何のことかわからない部分も多いので補足しときま…

2016-05-30追記 Agda2.5.1は割と素直にインストールできるようになりました。先週うまくいかないと書いていたAgda新バージョンのインストールの話。改めて同僚Tさん*1にエラーについて聞いてみたら、原因が判明し、そしてインストールもできたので以下展開。…

最近の修正で、ロケールをなおす必要はなくなって、普通に cabal install agda -f -cpphs と同僚Tさんから聞いてやってみたのだが、失敗。以下ログ。またあとでやってみる。cabalが古いかも。 C:\Windows\system32>cabal install agda -f -cpphs Resolving d…

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.WindowsNotes-2-4-2 きのう同僚Tさんから聞いて驚いたのだが、一度ロケールを英語にしないとインストールできないというcabalのバグ？らしい。すごいな。自分のバージョンはまだ2.3.2だった。

本日Agda-MLに流れてきた話によると、Aaron Stumpさんという型方*1がAgda本を執筆中で、出版社とも交渉中とのこと。現在のドラフト版が https://svn.divms.uiowa.edu/repos/clc/projects/agda/book/ にあります。興味がある方はご一読を。ドラフトを15年春ま…

Ubuntu（正確にはXubuntu14.02）にAgda2.4.2をインストールしようとして（cabal install agda）、なんかHaskellのあたりでうまくいかなくて困った。が、 http://stackoverflow.com/questions/25104367/ghc-incompatibility-installing-haskell-src-exts-via-…

とりあえず、LuaLaTeX上でLuaTeX-jaパッケージを動かして、日本語表示とunicodeのマニアックな記号表示を両立されるところまではできたぞ。環境はWindows7上のTeXWorks。 成果物はGithubに https://github.com/kino3/luatex-ja フォントの制御はまだうまくで…

今日から1日3コマ×3週間でAgdaを使った定理証明実習という講義がはじまる。ぼくはTAとして参加予定で現在インストール手順など作っています。思ったこと。 やっぱり日本語文献を書かねば・・・ WebでAgdaができる環境があればインストールしなくてもいいのに…

Agdaをさわりはじめてかれこれ2年ぐらいになる。最近ようやく、Agdaの面白さがわかってきて、それを広めたいという気持ちになってきたのでこうしていろいろ書いている。Agdaについてまとまった日本語の情報はあまりに少なく、まとまった日本語の情報がないと…

Agdaではじめてコンパイルしてみたので、そのやり方メモ。環境はWindows7。 emacs上でコードを書く module HelloAgdaWorld where open import IO.Primitive open import Foreign.Haskell open import Data.String main : IO Unit main = putStrLn (toCostrin…

構成的型理論についての代表著作「Programming in Martin-Löf's Type Theory」をAgdaで書きながら勉強するgithubリポジトリを作成しました。 https://github.com/kino3/PiMLTT元論文PDF http://www.cse.chalmers.se/research/group/logic/book/ぼちぼち更新…