エンジニアですよ!

頑張れ俺くん、巨匠と呼ばれるその日まで

cabal install conduitに失敗してた

環境とか色々忘れたけどmacでcabalでconduit入れようとしたら失敗した。 The Glasgow Haskell Compiler (GHC) on OS X 10.9... これ参考にやっていけた 以上 ついでにすごいHaskell学ぼう!

Coq入門 - 4.1

coq

https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。 https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由が…

Coq入門 - 4

coq

進捗あまりない。 update · 702639b · totem3/coq-prac · GitHub 全然わからんのでもうImportしたのを使って証明せずに進めているw できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。 こう…

Coq入門 - 3

coq

Coq入門 - 2.1 - エンジニアですよ! に追記したが、Lemma le_n_0_eqが証明できた あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。 False_indやFalseの証明の仕方が少しわかった。 しかし、その後も証明ははかどら…

emacsのauto-completeでCoqの補完が効いてなかった

題名の通り。 効いてなかった。 よくわからんのでスルーしていたが、ストレスフルなので治すことにした。 Auto Complete Modeユーザーマニュアル auto-completeの情報は↑に素晴らしくまとまっていて、簡単に対応はわかった。 ダウンロードしたauto-complete…

Coq入門 - 2.1

coq

進捗ありません。 疑問メモ 矛盾を示すのが難しい forall n:nat, S n <= 0 と forall n:nat, S n > 0 があれば矛盾を示すのは簡単に見える けど、どうやるのかわからない forall n: nat, S n <= 0 はPropということでいいんだよな・・ CheckしてみるとPropと…

Coq入門 - 2

coq

totem3/coq-prac こういうのをやることにした。 ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。 こんな初歩的なものなら簡単に証明できるだろ\(^o^)/ と思っていたら、いきなりできない・・・w Lemma le_n_0_eq n : n <= 0 -> 0 = n. …

Coq入門 - 1

coq

Agda入門にまんまと失敗して、Coqを入門してみることにした。 プログラミング Coq このチュートリアルをやっている。 色々調べてみると結構他にも入門はあって、先に調べるべきだったと思ったりした。 で、このチュートリアルは、とりあえず手を動かしてみる…

『関数プログラミング 珠玉のアルゴリズムデザイン』買ってきた

Amazonが届けてくれないっていうから買ってきた 人気なのか、そもそもちょっとしか入荷してないのか・・・ でもこれおもしろい! アルゴリズムっていうと手続き型のものが多くて関数型のってそんなにない(気がするだけ)から、うれしい。 値段の割りに薄く…

coq環境作って使う emacs + ProofGeneral

そもそもはProofGeneralが使いたいがためにEmacsを使い始めたが、とりあえずAgdaをやめてCoqをいじるようになった今、vimscripts/coq_IDEというやつでもいいかもしれないと思い始めているが・・・ Macでの導入は簡単。 homebrewを使う.もう何でもこれに頼っ…

emacs不満集

ProofGeneralが使いたいがために使い始めたが、やはりvimに慣れているのでなかなかemacsの操作は難しいところがある。 うまくいかないところを書いて解消できたら更新していく。 text objectがないのは辛い → thingoptでそれっぽい操作を http://dev.ariel-n…

既に時代遅れだったemacsのパッケージ管理

Getting Started Emacs - エンジニアですよ! でpackage.elを使ってパッケージ管理を始めた。 しかし!! 時代は既に先に進んでいた。 Cask, Palletなるものが現れていた OMG https://github.com/cask/cask あのnaoya-itoも既に乗り換えているではないか htt…

Getting Started Emacs

agdaに挑戦して即死した話 - エンジニアですよ! で書いたように、emacsが必要になった そこで、emacsを入門することにした。 vimに慣れすぎて頭がvimベースになっているが、emacsはemacs. 別のエディタなので別の考え方をしないといけなそう。 やってみてと…

agdaに挑戦して即死した話

agdaに挑戦し、即死した話 agdaは公式のチュートリアル(http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)に日本語の記事があったので、それをやることにした http://ocvs.cfv.jp/tr-data/PS2008-014.pdf こいつだ。 その前にまずagda…

HAX is not installed on this machine と言われてエミュレータが起動しないやつ

Android Studioでエミュレータを起動しようと思った時に、 emulator: ERROR: x86 emulation currently requires hardware acceleration! Please ensure Intel HAXM is properly installed and usable. CPU acceleration status: HAX is not installed on thi…

laravelのmodelのhook

最近rubyを書くようになってrakeが便利すぎてPHPで書いてることを後悔している今日このごろだけど、相変わらずlaravel. laravelでArdentを使うと便利、が・・ - エンジニアですよ! で、Ardentのフックを使おうと思ったんだけどArdentがダメっぽいというのを…

Laravelで複数カラムのvalidation

LaravelのValidationは便利。 http://laravel.com/docs/4.2/validation#basic-usage にある例を引用すると $validator = Validator::make( array( 'name' => 'Dayle', 'password' => 'lamepassword', 'email' => 'email@example.com' ), array( 'name' => 'r…

laravelでArdentを使うと便利、が・・

laravel - Model で Validation したい? それならば Ardent だ! - Qiita こういう記事を読んだり、削除する前のvalidationをcontrollerに書きまくるのが嫌だったのでhookを削除前のvalidationもsaveの時と同じように簡単にやりたいなぁなどと思っていて、Ar…

コンパイラつくろー - 2

コンパイラつくろー - エンジニアですよ!で書いたように、コンパイラを作っている。 まぁまだ難しいのでコンパイラというか単に数式をパースして計算するというのを作っている。。 アセンブリコードを出力しようとして色々試していたら、パーサー部分がまだ…

ELFがどう実行されるか調べる - 2

難しいのでこれとかを読みまくる以上のことはできない(;´Д`) プログラムはどう動くのか? 〜 ELFの黒魔術をかいまみる kernelかー。触れたことがない領域。

ELFがどう実行されるか調べる

コンパイラつくろー - エンジニアですよ!で書いたようにコンパイラを作っている。 フロントエンドもさることながらバックエンドの難しさは自分の理解できる範囲を余裕で超えている。 気になることを調べながら地道に進めていく。 ELFヘッダーについて調べつ…

コンパイラつくろー

最近は前に比べてちょっとレイヤーが低めな仕事をするようになり、わからないことが増えた。 中でもc言語やメモリのこと、cpuのことなどなどは全くもってわからない。 ミドルウェアはcで書かれていることが多かったり、ハード的な制約に影響されることが出て…

chefを入門するなどしていた

(laravelのコードを読んでいたけど、ドキュメントまず読めという電波を受信してせっせとドキュメントを読んでいたら、色々勉強する必要に迫られて別のことやっている。) 例えばchef。 chefとかcookbookとかrecipeとかknifeとか、無知なのでネーミングにイ…

Laravel Reading ServiceProvider Register

ルーティング周りを読んでいて気になった内部的なローディングのことを少し確認しておく。 laravelはたくさんのServiceProviderが提供するサービスを利用して動いている(?) ServiceProviderをregisterすることで、色々なところから使える状態になる https://…

Laravel Reading Routing

Modelで引っかかったところがあって先に読んだけどまず気になるのはやはりルーティング周りになるよね。 読んでみる プロジェクトを作ると、app/routes.phpが作られる 初期状態だと Route::get('/', function() { return View::make('hello'); }); となって…

Laravel Reading Alias

プロジェクトを作った時に作られるファイルを眺めていて、モデルを見ていると class User extends Eloquent implements UserInterface, RemindableInterface ですと。 Eloquentってなんだ。 laravelが独自のORMのことをEloquent ORMって呼んでいるのはわかる…

Laravel Reading

導入 最近はやりのPHPのWeb Application Framework, Laravelを使うことにした laravel自体の勉強と、色んなコード読んで設計や実装について学ぼう月間の一環として、実装中に気になったところのコードをちょいちょい読んでくことにする。 読むのはLaravel ve…

Facebook APIのcallbackで(指定されたURLは、アプリケーションの設定で許可されていません。)になってドはまりした

Facebookのアプリなんて今更誰が作るのかというのはおいといて、facebook apiを野暮用で使うことになったが、このcallbackで苦労した・・。 php-sdk-4を使ってfacebook loginを使おうとしていたけど、ちゃんと実装はできていてfacebookに遷移まではするが、…

unite-outlineが動いてなかった(?)

いつからかuniteのバージョン上げてからか、unite-outlineが動かなくなってた。 使おうとするとエラーが出る Error detected while processing ~/.vim/bundle/unite-outline/autoload/unite/sources/outline.vim: line 52: E121: Undefined variable: g:unit…

scala で型のところに出てくる #

# というのはこういうやつ → ({type λ[α]=State[S, α]})#λ 先日のscalaz勉強会でも質問があって触れられていましたが(↓) http://t.co/GoCDB4TGVu "Scalaにおける型パラメータの部分適用 [({type F[X] = G[A,X]})# F] について" #scalaz— Kenji Yoshida (@x…