過去に作った Jami のアカウントをなくしてしまったので、Jami のアカウントを再度作り直しました。今回はなくないようにちゃんとバックアップも取ってます。
私に Jami 経由で話しかけたいという謎な人はどうぞ。

id: e5fdfccb74c383420e6e647897dae018a4bd61fb

emacs に (setq system-time-locale nil) と記載しておくことで Emacs の異常動作を直せることが分かっ

Show thread

あー、これは format-time-string に謎の副作用があるっぽいな。これ C のコードらしいのでつらい。

Show thread

ある Emacs Lisp のコードを利用すると突然 org-mode のタイムスタンプが漢字から英語になっちゃう問題の原因っぽいものを特定した。

ダイナミックスコープを利用して一度 system-time-locale を "C" にして format-time-string をすると、再度 format-time-string をすると system-time-locale が "C" のままになる。

これはきつい。

う、ACL2 の arithmetic ライブラリをロードしようと思って調べたら雑な自分の記事がでてきてつらい……。Japan を有効にしてなければ出てこないだけ幸いである。

これ
> 証明に成功しました。定理ライブラリの力は凄いですね。
とか書いてあるやつなので検索されて見つけられるの恥かしいんだよな。

ACL2 でもやった(ただ計算によって比較しただけなので、この定理証明に ACL2 のうまみはない)。
これを一般化したようなものを証明できたら凄そうだけど大変そうなのでやらない。

Show thread

こんな感じでちゃっちゃっと求められてしまう(動画のネタバレ回避のため閲覧注意)。

Show thread

`cons` の型を確認したところ、どうやら Lisp の `cons` ではないことが分かった。まあ、こればっかりはしょうがないな……。Lisp のただの対としての cons は静的型付きだと結構無理あるし。

Typed Racket は無理を通していて、`cons` は Racket の `cons` のままなんだけど。

おお、+ が型クラスを使った型定義になってるー!すごい……。型クラスが Lisp の手に……。

Coalton が末尾再帰の形式にしてくれない件は sbcl であれば (optimize (speed 3) (safety 0)) を指定することで回避できた。

Show thread

あ、coalton 側で tail recursion の最適化はしてくれないっぽいな。普通に SB-KERNEL::CONTROL-STACK-EXHAUSTED って言われてしまった。下の関数に (neko 100000) って入れただけなのに。これは回避法の模索が要るな。
Coalton が関数型言語である以上、処理系に依存してでも末尾再帰は最適化されて欲しいところがある。

Show thread

おおお、ちゃんと Coalton 動くー!すごい。Common Lisp で静的型付きプログラミングできるし型クラスまであるぞ!

Show thread

忙しい人はまあこれだけ見ればなんで山本一太群馬県知事が「魅力度ランキング」なるものに対してあんだけ攻撃的な態度(なお、本人としては冷静であり攻撃的な態度をしているとは認識していない様子)をとっているのか分かるだろう。
既に7月の時点で群馬県庁サイドによる「魅力度ランキング」に対する分析を終えていて、ブランド総合研究所は「魅力度ランキング」という名称に相応しい調査ができているとはいえず、杜撰なランキングであるという結論を出した上で、再度ブランド総合研究所が魅力度ランキングを発表し、メディアがそれを取り上げて社会的な影響を与えたという文脈があるわけだ。

いきなり山本一太知事が怒りくるったわけではないことがよく分かる。

Show thread

いけたわ……。Emacs がダイナミックスコープであることを利用して let で org-capture-templates を束縛してから org-capture を呼び出す関数を定義すれば文脈に応じて別の org-capture を呼びだせる。
これで org-capture の可能性が爆発的に広がった。TODO で t が既に取られているから体温は T にするかーとかもう考えなくていいんだ……。

Show thread

お、NHK のニュースサイト、Nextcloud の External sitesで表示できるじゃん。これ禁止していないんだ。Nextcloud のダッシュボード使ってないし、これをブックマークしておけばよさそう。

さっきの頼まれごとの正体は文字列のリストから n 個を取りだす全ての組合せを求めて欲しいというものだったんだけど、ACL2 で実装した。とりあえず組合せの数に関する定理を書いたら補助定理なしで自動証明できてしまって驚いた。

コード: git.tojo.tokyo/acl2-theorems.g
ACL2 の出力: ci.tojo.tokyo/jobs/acl2-verify

Show thread

LibreJS に苦情を言う機能が付いてたんだけど、Contact ページの推測に失敗したみたい。

デジタル庁のサイトを GNU IceCat のデフォルト設定で開いたときの画面

Show older
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!