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

問題は、「よしブラウザ作るか！」って思ったときにもう簡単に作れない時代になってしまったところにあると思ってるんだよな。なんでWebブラウジングするのに JavaScript とかいう言語処理系の実装が必要になるんや……。

いまは GNU IceCat を使ってて GNU IceCat で正常に見れないサイトを使うのは基本的には諦めるという方針に舵を切ってるからな……。

とはいえ、LibreJS はやっぱきつすぎて無効にしちゃったけど……。

そもそも Web で色々やりすぎだと思うんだよな(と Mastodon を使いながらいう)。

PayPay銀行による Firefox のサポート終了の知らせが起点だったのではないかと教えていただきました。

https://mstdn.maud.io/@giraffe_beer/108028303950162914

@giraffe_beer

PayPay がこの話題の起点っぽいんですね。ありがとうございます。

「Firefox」サポートしないサービス続々　国内シェア今や6%足らずに（2022年3月26日）｜BIGLOBEニュースhttps://news.biglobe.ne.jp/trend/0326/jc_220326_9692926362.html

このニュースが起点か？

なんか最近 Firefox がピンチみたいな話題をよくみかけるんだけど追えてない。

私のサイト RSS の URL 変わって追跡できなくなった人いる気がするんだけど、リダイレクトすれば対応できる気がする。

でも、Atom から RSS 2.0 にいきなり変わったときに RSS Reader がどう反応するか分からないし、いきなり謎に過去記事の通知がいっちゃうかもしれないしそれはやりにくいな……。

一応 RSS で変わること通知したし、それを見て購読しなおさないという判断を尊重してそのままにするか……。

GNU Guix の Xfce4 の天気のパネルが何故かうまく動かない問題が解決すればいいんだけど……。何が起きてるのか分からなすぎてつらい。

さっき map-list-count の説明追記した。たぶん、あの記事のなかで最重要関数なのになんで説明するの忘れちゃったんだろう。

え、今登録しようと思ったのにこれもうすぐ終わるのか……。

> Yahoo!天気 RSS提供終了のお知らせ>> 2022年3月末をもちまして提供を終了させていただきます。長らくご愛顧いただき、ありがとうございました。> ご愛用いただいた皆様におかれましてはご不便をおかけしますが、何卒ご理解のほどよろしくお願いいたします。

か、かなしい……。提供RSS - Yahoo!天気・災害https://weather.yahoo.co.jp/weather/rss/

この記事、 map-list-count 関数の説明が何故か無だったので明日追記しよ。

関数の中身みれば何をやりたいのかまあ分かるし文脈でどんな役割の関数なのかは分かるだろうけど結構重要なのに説明がないのはおかしい。

過去に ACL2 の結果と CI の結果だけ公開して定理証明できたーとか言ってた時期あったけどあれが如何に無意味なことなのかよくわかったわ。

鳩の巣の原理も半年くらい前に自分で書いたはずなんだけど、なんでそれで証明できたのか意味分からんかった。

やはり記事にしないと駄目だ。

次はハフマン木やな。encode して decode したら元に戻るのが証明できるのはなんか凄いから強いだろう。鳩の巣の原理はたぶんインパクトが弱い。

超広告したい気持ちがあるので休日日中ブーストした。

たしかに *shell* バッファで作業しても実際のところなんら問題ないんだけどいつか事故りそう。

私のPCに defun とか dethm みたいな名前の危険なコマンドを仕込まれるとやばいし、他の人い同じような危い目にあわせるわけにもいかない。(まあ侵入された時点で終わり感あるけど)

ACL2 で org-babel するの ACL2 公式と同様に acl2 のコードを *shell* に投げ込む仕様という激ヤバなんでちょっと公開しにくいんだよなあ……。

ACL2 の鳩の巣の原理の記事完成したー！これは ACL2 で実際の使い方がなんとなく分かる良い感じの例題になってると思う。ACL2、ちょっと興味あるけど実際どんな感じなのかよく分からんって人に見て欲しい感じの記事。

ACL2 で鳩の巣の原理を使ってみたhttps://www.tojo.tokyo/acl2-pigeonhole.html

記事を書く過程で知ったんだが、ACL2 の定理の仮説を並べる順番って意味あるのか。「自由変数」(帰結部分の lhs に出てこない変数)にでのマッチの処理に影響するらしい。マジかよ。

:doc free-variables に書いてある。

ACL2 の記事を投稿した。一番証明したい性質はどうしても証明できなかったんで、そこはもう正直に無理でしたって書くことにして一旦この問題は忘れることにした。

ACL2 でリストの回転に関する性質を証明してみたhttps://www.tojo.tokyo/acl2-rotate-list.html