小粒なうぇっぶあぷりを作ってて、 Vue.js を使いたいなと思ってる（使ってる） 小さいしドキュメントも充実しているので、ちょっとガイド読めば使えるのであんまり把握せずに使ってるけど、それはよくないよねということでコード読むところから始めようと思…

最近家のmacのターミナルの起動が超遅くてストレスを感じてた きっとzshrcにいろいろ書きまくっているからだろうとそろそろ治すか・・と思ってたら、どうもターミナルの起動時とかタブを新しく開いた時によく見てみると遅いのは login だった。 login が遅い…

まだ3章までしか読んでないけど、『ハロー "Hello, World"』がおもしろい 最近はLinux Kernelのコード読んだりしてみたいな〜と思って読んだりしてたんだけど、やっぱ膨大なのでとっつきにくい。 そこでこんな本を見かけたものだから、"OSと標準ライブラリの…

第3回 ソース内のシステム・コールを確認するitpro.nikkeibp.co.jp を読んでgrepしたり、http://lxr.free-electrons.com/ident?i= で検索してもなかなかシステムコールを定義してる箇所が見つからないなーと思ってたら、 SYSCALL_DEFINEx っていうマクロを使…

rustのenumを定数を列挙するためだけに使いたいということもありますね？（ないですか？） そういう時、数値からenumに変換したいということがありますね？（ないですか？） rustのenumはこんなふうに定義します。 rustのenumはだいぶ高機能なのでいろんなこ…

chef/mixlib-cligithub.com mixlib-cli、便利ですよね。 この option で同じオプションで複数の値を渡したい時はどうすればいいか 例えば --hosts で複数のホストの情報を渡したいとか。 ぱっと調べた感じ＆動作を見た感じでは、 cmd --hosts host1 --hosts …

なんて言ったらいいかよくわからないけどタイトルみたいなことがしたいときどうするか テーブルのデータそのものじゃなくてテーブルのデータから計算できるデータがあったとして、それをクライアントに計算させるんじゃなくてレスポンスに入れて返したいとか…

php artisan migrate PHP Fatal error: Class 'Doctrine\DBAL\Driver\PDOMySql\Driver' not found in .../vendor/laravel/framework/src/Illuminate/Database/MySqlConnection.php on line 59 みたいなエラーが出てなんぞ、と思っていたところ Schema Builde…

いつからかtmuxを起動すると Not privileged to set domain environment. Not privileged to set domain environment. とエラーが出るようになった。 なんだこれは。 調べるとどうも .zshrc で launchctl setenv とかいじってるのが問題らしい。 何してたか…

前回うまくできなかったけどやってみたらうまくいったという、それだけ。 前回試した時はopenの戻り値の型が c_int だから kevent struct の ident の型も無理矢理 c_int にしてたから、 Invalid Argumentのエラーが出てたんだけど、last_os_error()とか見て…

rustがそろそろ1.0出るってことでしばらく前からいじり始めた。 entrをgoでcloneしたgotrを見てちょっといいお題かも？とか思って書いてみようと思った。 totem3/rustr · GitHub 結果 今んとこできたこと イベント検知して渡されたコマンドを実行できるよう…

前回 Docker のイメージから ACI を作り、 Rocket で動かすということをやってみた。 今回は仕様を見ながらイメージを作ってみる。 appc の仕様はここにまとまっている。（リンクはこれを書いてる時点で見てたバージョン。v0.4.1） https://github.com/appc/…

CoreOSでRocketを動かしてみよう $ git clone https://github.com/coreos/coreos-vagrant/ [~/sandbox] Cloning into 'coreos-vagrant'... remote: Counting objects: 351, done. remote: Compressing objects: 100% (5/5), done. remote: Total 351 (delta …

stackoverflowに回答があった。 types - Difference between `data` and `newtype` in Haskell - Stack Overflow 使いドコロがわからなくて使ってなかったしこれ読んでも使いどころは特にわかってはいないんだけど、とりあえず違いについてはわかった気がす…

githubのフィードをtwitterに投げ続けるだけのbotをherokuで作った Procfileは↓というだけの簡単なもので、構成もGemfileとProcfileとbot.rbだけのシンプルなもの cat Procfile worker: bundle exec ruby bot.rb herokuにログイン https://dashboard.heroku.…

メモ テーブルは list series カラムはぱっと見つかったのだとこれ influxdb does not list all column names · Issue #514 · influxdb/influxdb · GitHub select * from /.*/ limit 1 とか

Macというのはダメな奴なので、ubuntuとかが欲しくなる。 というわけでとりあえず作業用にVMを立ち上げたりよくするんだけど、適当にVagrantfileを作って起動するものだから、しばらくするとどこで立ち上げたやつだかわからなくなる。 Vagrantfileどこだっけ…

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

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

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

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

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

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

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

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

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

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

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

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

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