2022-05
https://open.spotify.com/album/4ZHduve9XLSCzgzuAEpo91?si=cOwNjlhcQwiwyORhEzk3uw
いいね
みた
2022/05/25 17:20:28 failed to run NDP proxy: failed to speak MLD: failed to join MLD multicast group: setsockopt: cannot allocate memory
なるほど確かに落ちた
忙しすぎてCSになってしまった，次回
2週間くらい動作できるらしい
みょん
Go処理系は基本的に互換性を壊さないので
厳密に不要というわけではないが
これをやったからといってそこまで複雑さが軽減されるわけでもないのが辛いところではある
protocもgo runのフレームワークに載せられたりしないのかな
$ cat /proc/cpuinfoしてみよう！
code:U6-Lite
U6-Lite-BZ.6.0.19# cat /proc/cpuinfo
system type : MediaTek MT7621 ver:1 eco:3
machine : Ubiquiti Networks, Inc. U6-Lite
processor : 0
cpu model : MIPS 1004Kc V2.15
BogoMIPS : 586.13
wait instruction : yes
microsecond timers : yes
tlb_entries : 32
extra interrupt vector : yes
isa : mips1 mips2 mips32r1 mips32r2
ASEs implemented : mips16 dsp mt
shadow register sets : 1
kscratch registers : 0
package : 0
core : 0
VCED exceptions : not available
VCEI exceptions : not available
VPE : 0
2C4T
2022年だぞここは
code:ER-Lite3
admin@ubnt:~$ cat /proc/cpuinfo
system type : UBNT_E100
machine : Unknown
processor : 0
cpu model : Cavium Octeon+ V0.1
BogoMIPS : 1000.00
wait instruction : yes
microsecond timers : yes
tlb_entries : 64
extra interrupt vector : yes
isa : mips1 mips2 mips3 mips4 mips5 mips64r2
ASEs implemented :
shadow register sets : 1
kscratch registers : 0
package : 0
core : 0
VCED exceptions : not available
VCEI exceptions : not available
みた
みた
みた
一応週〜月単位で進行するリソースリークが存在するのでそこが直しどきではある
みた
みた
よすぎ
https://scrapbox.io/files/627ccc370b810d001db445e3.gif https://www.kame.net/
ついに我が家に，IPv6インターネットが……２(ツー) https://scrapbox.io/files/6276f613a9318d001d8ba0bf.png
ついに我が家に，IPv6インターネットが……
v1とv2がある
v2はMulticast Listener Discovery Reportを再定義しているだけのはずだが
tcpdumpしてみるとICMP6 multicast listener query v2の表示が メッセージフォーマットにはないはずのrobustnessとqqiが含まれている
受け取ったデータをよく見るとmulticast addressの後に4オクテット増えてる
発見的にはrobustness variableとquery interval variableの位置は理解できたけど，どこに書いてあるのかは全くわからんな
諦めが悪いので自然演繹の自動生成について考えていた
書き写すのすら面倒
$ \landとか$ \lor，$ \to(\supset)，$ \negの導入規則は単純に処理できる
自明
これらの除去規則をどうするか
仮定を仮定環境に導入する際に，その仮定に除去規則を適用することで導くことができる命題を列挙しておく
その仮定が関わって導くことができる可能性のある命題
自明な規則の適用で進めなくなったら列挙した命題から今の命題を探してきて，あったらその仮定を使って前に進もうとしてみる
矛盾律も同じように求められるはず(全ての関連命題に$ \bot)を含めておく
よくわからん
$ \lor除去規則
見つからなかったら適当な$ \lorを見つけてきて使ってみる?
どこで適用するのかわからなさすぎ
最終手段として持っておく?
どの式に対して排中律を適用すればいいんだ?
よく考えると次の講義も命題論理というのは考えにくいな
こんな変なことをしたとしても判定能力としてはSATよりも弱い あっちは充足可能性を判定した上に充足する割当まで出力できるが，こっちはトートロジー判定しかできない screenでシリアルコンソール繋ぐと微妙に扱いにくくて困る スクロールが上下キーにマップされて履歴表示と衝突してたりする
これをやらないと(物理ポート数が足りなくて)先に進めないといった状態
証明図実装を若干改良した
古典論理だと$ (\neg a\to a) \iff aなんだ 命題論理の自然演繹やるのそろそろ飽きてきたから計算機ににやらせたいと思ったけど，型に沿ったプログラムを書くのと同義だし普通に厄介だな みた
午前中はひたすら確率論をやっていた
積分積分アンド積分
このAPIまだ生きてたのかよ
少なくとも5年前に既にdeprecatedって書かれてたぞ
そろそろ真面目に証明図を書くライブラリが欲しくなってきた (声にならない叫び)
ここからはシンタックスハイライトありでお送りします(OCamlのため) MathFractionという値になる
文脈とかと合わせてサイズ評価されてLowMathFractionになる
proof.satyに証明図向きな\fracのユーザースペース再実装があり，それを再利用して勢いで書いた https://pbs.twimg.com/media/FR8EfYBaMAAsUCu.png
値の引き回しとかの設計はSATySFiのmath実装をそれなりに参考にしているので↑のコードリーディングは無駄ではない…… みた
赤兎馬カンフーのジャケットの裏に関聖帝君と書かれてた
そんなことあるんだ
ci7lus.iconとrokoucha.iconと横浜に行った
中華街に行ったら死ぬほど混んでいた，ゴールデンウィークに行く場所ではない
「関聖帝君」って言い方本当にするんだ
帝君 > 真君らしい
めんどいな
みた
厄介な要求のために厄介なネットワーク構成をし，ハブの4/5を埋めた
https://scrapbox.io/files/626f8ff58e998f001daa6ac6.png