No Such Blog or Diary

«Prev || 1 | 2 | 3 |...| 713 | 714 | 715 |...| 1110 | 1111 | 1112 || Next»

コードを綺麗にしたら、Coq が全力で3時間走るようになった!

なんでやねん.どうも型クラスのリゾルバが正しいインスタンスを探すのにアホなサーチをしてる気がするのだけど…… コードを綺麗にしてより般化されたのでサーチにさらに時間がかかるようになってしまった.とりあえず,型クラスのリゾルバを3時間も待った人間はそうはいまい.

余計な引数を渡すようにして無駄なサーチが走らないように縛りを入れないとダメかなぁ.ぶっちゃけ型クラスの使い方間違ってるかもね.

閑話休題.

ネタとしては笑いを取れた.

閑話休題.

お菓子の買いだめが切れたので何となく作業しづらい.スーパーはもう閉まっとるし,自販機はあるけど高いし.

そして角砂糖をそのまま食べるという手段に出る.

閑話休題.

無駄なサーチが走らないように型にタグを付けてみたり無駄なインスタンスを省いてみたりしたら15秒に縮んだ.ばんざい.

それにしても狙ったところに行かせるにはなかなか苦労するなぁ.コードも汚くなっちまうし.自由度高いので自動でやらせるのは色々としんどいのね……

Coq の Definision の評価にCPUが全力で6分間働きづつけるとか

ふつうのコトなのか頭おかしいのかよくわからん.Typeclass 使いまくりなのが原因だけど.i5-2540M なのでそんなに頭悪くないと思うのだけど…… まあ,C++でも template でメタプログラミングすればコンパイルに時間かかるから普通かね.

だがしかし,その定義の上部に行って何かを修正して帰ってくると泣ける.

閑話休題.

Let'snote の排熱が熱すぎるんだけど大丈夫かなぁ.

はぢめてのパスワード寄越せメール

「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 のフィールドは必要なのか?

閑話休題.

何となく最近銀行とかのログイン画面のところに「うちのページでは乱数表を全入力させるとかないから気をつけて!」とかあるのが印象に残ってるのだけど,オンラインバンキングをターゲットにしたトロイの木馬とか流行ってるのか?

閑話休題.

他のプログラムに寄生して頑張るコンピュータウイルスって未だいるのかね? ○○日に発病するまで潜伏してるとか,寄生してもファイルサイズ増やさないように巧妙にできてるとか,自己複製を頑張るとか,昔のウイルスは面白みがあった気がするのだけど…… 最近ウイルスと呼ばれいている悪意あるソフトウェアは技術的にもやってる事的にもつまらん気がする.ただの詐欺ツールだったりするのだから,ウイルス以外の名前で読んでほしい.

雲がはえぇなぁ

何となく低めの位置の雲の動きが速い時が多いようなきがするのだけど,山とかがない平坦な土地だからなのか? 季節的なものなのか? 日本だとそんなに頻繁に見ない気がするのだけど.よくわからん.

とりあえず天気の悪い週末が多い気がするぞ.

式が展開されず困る罠

証明というか項というか,その構成途中に展開できないものを使ってしまうと Eval で評価して動作確認ができなくなる.んで,どの場所が展開不能なのか探り当ててそれを使わない方向で証明を書きなおし…… とかいう作業がちらほら.XX_dec 系のは動くプログラムとして使いたいけど直接プログラム書くのが面倒だから証明しちゃえとかやるとこうなる.

折衷案としては危なそうな部分は手で書いておいて細かい部分を個々に証明して埋めるってのかね.

そして締切伸びる

必要最低ラインまで突貫工事で直し終えたら締切伸びた.まあ,時間に余裕が出来たことは良いことだ.……あと2日早く宣言して欲しかったなぁ.

さて,これで実装を覗く時間が出来たのでチェックを入れよう.

«Prev || 1 | 2 | 3 |...| 713 | 714 | 715 |...| 1110 | 1111 | 1112 || Next»
Search
Feeds

Page Top