2023-03
3月も終わりやね
今までずっとGTK_IM_MODULE=fcitxを設定していなかったことが明らかに
嘘だろ？？？
募集しています
あった!!!
今(?)明かされる歴史
定数倍で再帰深度を減速させるmap(count_map)を適用していき，再帰深度が閾値を超えたら末尾再帰版に切り替え
末尾再帰版もオブジェクト確保回数を減らすために9個ずつまとめて処理している
なんで9なんだろう，OCaml の内部表現を知ってるとなるほどみたいになる値なんだろうか？ 真面目に.mliを書いているが，まあ普通にダルい
書かなくてもええ！という向きもあるが，それはそれで全てが公開されるノーガード戦法になってどうなん？という気持ち
なんかこう，pubとか書いたらいい感じに生成してくれたりしませんか？
というか OCaml は全体的にアクセス制御とか無いという感じがする モジュール制約とかはあるので抽象化で困ることはあんまりなさそうだけど
そういう中で.mliは貴重な公開制御の方法であるとは言える
ありえん速い
やはり自分は文献を読み込んでその結果を一気に吐き出すみたいな感じでコードを書いたほうがいいんじゃないかという気がしている
十分に手を動かしてからそれをその通りに実装する
こうしたほうがバグらせにくい
問題が十分に単純で，調べつつやったほうが早いみたいなケースもありはするけど
みた
いい話すぎる
ありえない終わりかた
良すぎる
花粉症なのか睡眠不足なのか体調が破滅していて，↑を確認するくらいしかできなかった
みた
監視リテラルの変数→節の対応を保持する構造をint list arrayからint Queue.t arrayにしてみる
別に速くならなかったしStateful Programmingの度合いが上がるだけだった
監視リテラルにおいて，次に辿る変数の集合をスタックで管理していたのをキューにしてみる
conflict に繋がらない部分をひたすら探索しないようになるので少し速くなるかも？と思ったがあまり変わらず
多くの場合全部辿るので大差ないのかも
監視リテラルの変数→節の対応と節→リテラルの対応の更新が別々になっていて，薄氷を踏むように丁寧に更新していた
最悪状態マシマシプログラミング
遷移をグッと睨むと一般化できたので，監視リテラルを更新する関数を呼ぶだけで構造が更新されるようになった
みた
みた
やばすぎ
4倍速くなって感動
ハチャメチャにバグらせたりした
デバッグモードを用意して適当なステップで冗長なアルゴリズムを使って状態を検査してあげるといい
みた
字幕を読まないと話が全くわからないすごすぎるアニメ
でも面白いんだよな
低予算レヴュースタァライト
みた
そう?
次は劇場版でってことらしい、そんなことある?
昨日に引き続きSATソルバ
「関数型」なデータ構造が使えるか?ということを考えていた
永続な感じのやつ
使う利点としては
バックジャンプが行われるときに少ないコストで戻せる
プログラムが明確(諸説あり)
かなり微妙そう
巻き戻す必要のある状態が少ない
これは逆で、刹那的なデータ構造で状態を持つ場合巻き戻す処理が重く、これを行わないで済むような最適化手法が研究されているということだと思われる
変数の割当を格納する構造くらい
レベル単位でしか巻き戻しが起きない
あらゆる操作のタイミングの状態を記録できる構造はオーバースペックに思える
CDCLアルゴリズムは複数のレベルを跨いたバックジャンプを行うので、各レベルで状態を保存するのも微妙 コストはバックジャンプのタイミングで必要な分だけまとめて払いたい
激しい読み込みが発生する
監視リテラルは新たに割り当てられたリテラルの処理を遅延させる効果を持つので、この手法を導入することを前提にした場合、節を表現する配列を端から読んでいって各変数の割当を確認するという操作が大量に発生する 割当を配列で管理すればこの操作のコストは最小と言える
これにトータルで勝てる気がしない
どうしたらいいんだ?
SATソルバ書いてた
$ \botに向かわないノードを持つ
たぶんこう:
変数の割当を決めるとき、その割当が発生したレベルと割当を発生させた節を覚えておく
割当を発生させる節は複数存在する可能性があるないわ
そんなことある?と思う、もしかしたらないかも
割当が決まったとき、その変数を含む節は全てその変数とは関係のない節になる
充足される or それ以外の未割当の変数を見る
conflict が起きたとき、割当$ a=(x:=t)\in\Lambdaについて次の2つの節が Conflict Graph における$ \botに直接向かう辺になる $ \lnot aを導く「直接の」原因節
$ aを導く原因節
これは前述した部分で覚えている
なんかかなり違う気がしてきたtosuke.icon
この仮定で current level に属さない割当を他に保持しておけばいい、のか?
dune {build,test} --watchの体験がいい
昔マシンパワーにものを言わせてyarn jest --watchとyarn webpack --watchとyarn storybookを同時に動かしていたのを思い出した
可視性の制御がわからない
duneの libraries 項に書く/書かない以外になかったりするのか?
dune における library は cargo における crate に相当する概念に見えるが…… つまるところ，モジュール単位の可視性制御が無い気がする?
もちろん signature によるモジュールの外に見せる/見せないの制御は可能なわけだが
設計者の思想が現れるプロジェクト構造になっているはず
めっちゃ library を切り出してる！
完
すごすぎるだろ
なにもなし
みた
移動、疲労
みた
萌萌萌萌萌萌萌萌萌萌萌
声〜〜〜！ ←天才
予告のサムネイル
主人公のクラスがメイド喫茶をやる
メイド喫茶のメニューがオムライス
お化け屋敷がある
世紀末な感じの人間が出てくる
主人公が抜け出して他の店を巡る
みた
苦しい、くるs……バトル!?!?!?!
エーッ
オオッッッッ
大会とかだと意地悪な問題が与えられることを前提とするわけで，攻めた戦略を取るとそこを突かれて遅くなってしまうということなのかもしれない
sushi-sumo hell
やばくなE(?)
割とよかった
本当に単純だった，面白くなさすぎる
知った
みた
やばE
出した
各方面から作問をしろという無言有言の圧力を受けています!!!
しかしまあもしかしたら……
みた
借りた
全然別ベクトルだけど計算って好きやねんになったため
みた
ニア僧侶
実行した社交性(社交性とは？)の「反動」が出て，ここ数日静止していた
だめすぎる
4人友達がいてよかった
ビッグ・ラン
たのしい
家事
今回は普通だな……って思ったら無言パートがやばすぎた
《第一質料<プリママテリア>=エンコーディング=物質<マテリアル>コード》
《物質<マテリアル>コード=ディコーディング》
《物質<マテリアル>コード=プロセシング=四原因説<アイティア>=質量因<ヒュレー>=形相因<エイドス>=作用因<エフィシェン>=目的因<テロス>》
《エンボディメント=因果律<コーザリティ>》
第3部までやるらしいです
k3s はデフォルトでは IPv6 が無効らしいので有効にしてデュアルスタッククラスタにする ドキュメントに書け!!!
ところでどうして Canal を使わなかったんですか？ どうやら LB として選出されたノードのアドレスを持ってくるらしい
--node-ipオプションを使うと Internal なアドレスが振られるが，なぜか IPv4 を1つしか受け取ってくれなかったので，--node-external-ipオプションを使って External なアドレスを振って解決 死を賜る←そんな表現あるんだ