Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 175

お名前からの引っ越しを決意した。

DNS の障害、お名前.COM のメールを無意識に無視していたのが原因だった。つらい。。。

あー、7時間前のトゥートが流れてくる……。鯖缶のみなさんすみません。。。

うう、なぜあれだけ重要なメールを見逃してしまったのか……。ドメインにアクセスできないタイミングでメールを送られて企業側のバウンスリストとかに入ってたらやだな……。

いま解消したっぽいので、TTL が更新されれば復活するはず……。

住所変更した後の確認メールをクリックし忘れてたのが原因だったっぽい……。つら……。

tojo.tokyo ドメインに深く依存していることを思い知らされた。明日お名前.comに電話する……。

原因切り分けられた。 dig @8.8.8.8 tojo.tokyo で、NS レコードが返ってこないので、これはお名前.com の問題だ。Vultr の DNS までいってない。ただ、私以外に苦しんでいる人いないし、お名前.comで購入した他のドメインでは問題は発生していない。

いま私の Mastodon にトゥートを送信できているサーバーはたまたま私が引けているだけということか。タイムラインがめちゃくちゃ偏っている。

DNS の障害はちょっとダメージが大きすぎるな……。

Vultr DNS を使っていたのが原因なのか、お名前.COM 側でなにかあったのか……。

サーバーによってはまだ mastodon.tojo.tokyo が引けないところがあると思う。(uptimerobot から引けてないので)

おそらく私のトゥートは他のサーバーに飛ぶんだと思う。でも逆は厳しい可能性がある。

uptimerobot ではまだ復旧してないみたい。これ私からはアクセスできているけど、人によってはまだ障害が続いている可能性あるな。

自然復旧していて謎が深い……。

さっきまで DNS 障害が発生してた……。結局原因の切り分けでていない。なにがあったんだ……。

ACL2 では forall とか exists とか使わないで再帰関数に落し込んで証明した方がいいと。自動証明できないんじゃ ACL2 の魅力も半減だし、defun-sk はよっぽどの場合を除いて使わなくてよさそう。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____QUANTIFIERS

ACL2 に慣れてきたのでそろそろこれを読む。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____QUANTIFIER-TUTORIAL

難しい例だと難しいのでデモとして適切じゃないし簡単な例だと簡単なので自動証明されるからデモにならない。

自動証明に失敗してくれないと架空の最強ツールになってしまうので、失敗してくれないと困る。