No Such Blog or Diary
Coq の副作用に泣く
- 2012-11-08 (Thu)
- 一般
正しく証明できた定理の上部で後から必要になったライブラリのモジュールをインポートしたら証明が破綻した.原因はライブラリ内で Obligation Tactic が上書きされててそれがグローバルに影響をもたらしてくれてるからで…… 副作用ありまくりだなぁ.デフォルトが何なのかわからんが Show Obligation tactic で見る限り "Obligation Tactic := unfold complement, equiv; program_simpl." あたりっぽい?
モジュールを読み込んで泣く別のパターンとしては型クラスのインスタンスの優先度が変わってしまって implicit な引数に思ったものがハマってくれなくなるという現象が起きる.使って欲しいインスタンスを Existing Instance でトップに持ってきておけばなんとか大丈夫っぽいけれど.
色々と副作用がありまくりなので透明なライブラリとか頑健なライブラリとか気をつけないと書くことができないと理解した.
- Comments: 0
- TrackBack (Close): -
作業途中で追い出される
- 2012-11-07 (Wed)
- 一般
20時過ぎに作業してたら19:30で建物閉めるんだからさっさと出てけクソがと警備の人たちに追い出された.なんでやねん.カードキー持っとるので幾らでも出入りできるのに……
どうも時間外に作業するには向いていない環境な気がする.
- Comments: 0
- TrackBack (Close): -
また時間が……
- 2012-11-06 (Tue)
- 一般
サーチがお馬鹿すぎる.あさっての方向を向いてどんどん突き進んでいく……
どうも引数の構造が「沢山の単純なインスタンス+それらの関係を示すインスタンス」になっていると単純な方を先にサーチしに行ってどんどんアホになるらしい.まあ,そりゃそうだろうけど.
とりあえず,単純なインスタンスを関係を示すインスタンスの奥底においてやったら頭良くなった.
閑話休題.
どっかにサーチのアルゴリズムを詳細に述べたものとかないんかな? C++のテンプレートのサーチの方がまだ分かりやすい挙動をしてくれる気が……
- Comments: 0
- TrackBack (Close): -
コードを綺麗にしたら、Coq が全力で3時間走るようになった!
- 2012-11-05 (Mon)
- 一般
なんでやねん.どうも型クラスのリゾルバが正しいインスタンスを探すのにアホなサーチをしてる気がするのだけど…… コードを綺麗にしてより般化されたのでサーチにさらに時間がかかるようになってしまった.とりあえず,型クラスのリゾルバを3時間も待った人間はそうはいまい.
余計な引数を渡すようにして無駄なサーチが走らないように縛りを入れないとダメかなぁ.ぶっちゃけ型クラスの使い方間違ってるかもね.
閑話休題.
ネタとしては笑いを取れた.
閑話休題.
お菓子の買いだめが切れたので何となく作業しづらい.スーパーはもう閉まっとるし,自販機はあるけど高いし.
そして角砂糖をそのまま食べるという手段に出る.
閑話休題.
無駄なサーチが走らないように型にタグを付けてみたり無駄なインスタンスを省いてみたりしたら15秒に縮んだ.ばんざい.
それにしても狙ったところに行かせるにはなかなか苦労するなぁ.コードも汚くなっちまうし.自由度高いので自動でやらせるのは色々としんどいのね……
- Comments: 0
- TrackBack (Close): -
Coq の Definision の評価にCPUが全力で6分間働きづつけるとか
- 2012-11-04 (Sun)
- 一般
ふつうのコトなのか頭おかしいのかよくわからん.Typeclass 使いまくりなのが原因だけど.i5-2540M なのでそんなに頭悪くないと思うのだけど…… まあ,C++でも template でメタプログラミングすればコンパイルに時間かかるから普通かね.
だがしかし,その定義の上部に行って何かを修正して帰ってくると泣ける.
閑話休題.
Let'snote の排熱が熱すぎるんだけど大丈夫かなぁ.
- Comments: 0
- TrackBack (Close): -
はぢめてのパスワード寄越せメール
- 2012-11-04 (Sun)
- 一般
「Notification: Re-validate your email」とかいうタイトルでスパム判定もされずに下記の内容のメールが届いた.パスワード送れ系の詐欺メールは初めて受信した.
To increase your storage capacity and the functions, you are required to reply to this mail and enter your Login ID and Password in the space provided below due to the fact that we are about to carry out maintenance and increment of storage capacity on our web-mail services/account within the next 72 hours. nbsp; Failure to do this within 72hours will immediately render your email account deactivated from our database. nbsp; FULL NAME: E-MAIL ADDRESS: USERNAME: PASSWORD: CONFIRM PASSWORD: nbsp; Your Account can also be verified via our Web-mail Link before the information are sent.
送り主は「hogehoge.ac.jp E-mail Services <acct.auth@ hogehoge.ac.jp>」とかなってるのに,送り元IPはトルコ.ヘッダを見みたらトルコの大学か何かの誰かのアカウントから送られてるようなので乗っ取られたのかね.
つか,平文でパスワード書くのに confirm password のフィールドは必要なのか?
閑話休題.
何となく最近銀行とかのログイン画面のところに「うちのページでは乱数表を全入力させるとかないから気をつけて!」とかあるのが印象に残ってるのだけど,オンラインバンキングをターゲットにしたトロイの木馬とか流行ってるのか?
閑話休題.
他のプログラムに寄生して頑張るコンピュータウイルスって未だいるのかね? ○○日に発病するまで潜伏してるとか,寄生してもファイルサイズ増やさないように巧妙にできてるとか,自己複製を頑張るとか,昔のウイルスは面白みがあった気がするのだけど…… 最近ウイルスと呼ばれいている悪意あるソフトウェアは技術的にもやってる事的にもつまらん気がする.ただの詐欺ツールだったりするのだから,ウイルス以外の名前で読んでほしい.
- Comments: 0
- TrackBack (Close): -