Home | Notifications | New Note | Local | Federated | Search | Logout
きゅーけー@tojoqk@mastodon.tojo.tokyo
Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバーを運用しています。
Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Agda 学習がメインです。
生活リズムの安定のため、深夜 02:00 から 10:00 までの間はアカウントロックをかけています。その間は何も反応しません。
個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk
Joined: 2025-12-01 20:07:27
190 notes, 1 following, 1 followers
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@kyu3a@social.vivaldi.net (2026-05-27 19:02:52)
DuckDuckGoのユーザー数が急増、Google I/OでのAI関連の発表を受けて - GIGAZINE
https://gigazine.net/news/20260527-not-google-but-duckduckgo/
『特にアメリカのiOSユーザーで伸びが目立ち、従来型の検索体験を求める動きが広がっています』
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 22:29:43)
Xはログインしないとタイムラインがまともに読めなくなったあたりから見なくなった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 22:23:06)
世間の型の価値がどうなってもAgdaが最高に素晴らしいことになんも変化はない
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 22:20:37)
まあ、私はXエンジニア界隈からは離れてひっそりAgdaを書く生活を送ろう…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 21:36:47)
新しい型チェッカーとして話題になっているRubyのRigorというソフトウェア。少なくとも現状の私の理解の範囲ではあんまり聞いていていい気持ちにならない…。
テストにかかれている情報を型推論に使うということだけど、それは存在命題の証明を得ているということであり、矛盾の存在を証拠にコード上のバグを検出できるということに価値はあると思う。
でも型システムとして一般に期待することは全称命題を型システムが証明してくれていることだと思うので、「型チェッカー」と聞いて期待するものと違いすぎるように思う。仮にこのような仕組みが「Rubyの型チェッカー」として広まるようなことがあれば、型チェッカーという言葉の価値が毀損されてしまうのではないか…。
これが「セマンティックなLinter」みたいなキャッチフレーズであったら何も思わなかったかもしれない。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:50:58)
この仕組みに今回 agda コードを載せる場合のロジックが追加されたと…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:49:53)
過去記事を振り返ってみたら、私の闇のお手製な静的サイトジェネレーティングについてしっかり記事を書いて公開してるじゃん……
https://www.tojo.tokyo/posts/create-website-with-emacs.html
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:41:22)
(間違って一回外からアクセスできないテスト環境用のURL貼ってしまったので一回投稿消した…)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:40:47)
Agdaのコード含めた記事を書いて自分のサイトに公開するためのインフラが整いました!
今後はこの仕組みで色々Agdaの記事を書いていきたいところ…
https://www.tojo.tokyo/posts/agda-on-www-tojo-tokyo.html
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 00:38:45)
Adga のコードを含む記事を書いて公開できるようになりました!
Agdaの記事を書くインフラがついに整ったのでこれから色々書いていきたい…
https://www.internal.tojo.tokyo/posts/agda-on-www-tojo-tokyo.html
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 23:07:24)
「みんなが使っているから安全」ということはなくて、むしろ「みんなをサポートしている方が対応が遅くなって危険」なんだなと感じている…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 22:43:14)
Ubuntuから完全脱却して CVE-2026-46333 が他人事になったのが一番でかい。Guix Systemへの移行と念のためssh鍵のローテーションも完了してる。
Guix Systemは修正版のLinuxカーネルがリリースされてかなり短い時間で、修正版が上がってきていたのに対して Ubuntu ではいまだに脆弱なままで修正されてない…
https://ubuntu.com/security/CVE-2026-46333
https://nvd.nist.gov/vuln/detail/CVE-2026-46333
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 12:17:24)
cryfs よさそうだと思ったけど、自分が暗号化したい粒度的には rclone についている encrypt 機能を使うのが丁度よさそうな感じだった。
(自分は完全なメタデータの隠蔽をそれほど求めてなかった)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 10:46:38)
調べたところ Guix のパッケージにもあったので使ってみようかな
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@LwVe9@mstdn.poyo.me (2026-05-24 10:29:35)
CryFS: Encrypt your cloud storage
https://www.cryfs.org/
昨今のクラウドストレージ検閲対策でそういうヤツない？とchatgptに調べさせたら、やっぱあるな
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-24 01:45:07)
全ての趣味インフラがGuix Systemのみになったので、日常でsystemdの知見を得るのは不可能になったな。まあ仕事でも systemd は別に必要にならなそうだしいいか……
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 23:12:46)
マストドンのバージョンが手元の Guix System の config ファイルの更新と同期して git commit されるようになったの最高だな…。本当にサーバーで持つ状態が減った。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 22:52:52)
Mastodonのバージョンアップすごい楽になったな。assets:precompile しないだけでこんだけ負担が減るとは…。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 20:12:01)
正直、よくわからんことになりつつあった Ubuntu サーバーはちょっと私のなかでもうちょっと負債になりつつあって若干嫌になってたので、ここで Guix System に移行できたことでこのお一人様サーバーの寿命がだいぶ延びた説ある。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 20:07:04)
バックアップスクリプトも Guile で書いた。Gexpsが最高。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 20:06:13)
私の Mastodon サーバーを Guix System にお引っ越しして、以下のたくさんの仕事を全て Guile Scheme の DSL である、Guix System で書ききっていま実際に動作する状態になったので大満足。
- OS の基本設定
- podman container のサービス登録 (oci-service-type)
- mastodon-web, mastodon-sidekiq, mastodon-streaming
- letsencrypt で証明書の作成・自動更新
- velkey のサービスの起動オプション設定とサービス登録
- postgresql のサービスの登録
- nginx のサービス登録と Nginx の設定
- openssh の設定 (私の ssh 公開鍵登録)
- mastodon の必要ファイルのバックアップ (mcronで定期実行)
上記の設定やスクリプトが一枚の config.scm の中に全て記述されている。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 18:22:45)
Mastodon の定期バックアップまわりの処理も書かなきゃ。
Guix の Gexps と相性がいいから、こういった処理も全部 Guile Scheme で書くことにしている。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 16:40:25)
ついに、Ubuntuから解放された……。これはでかい。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-23 16:39:47)
Mastodon を Guix System で動かすのに成功したっぽい!
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-22 10:53:48)
はやくこれを完了しないと…
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@tojoqk@mastodon.tojo.tokyo (2026-05-12 11:02:23)
立て続けに Guix System の方がカーネルの脆弱性修正の更新対応が早いということが実際に起きているので、Mastodon サーバーを Podman on Guix System へ移行しようという気持ちがかなり強まっている。
すでに Guix でいくつかサーバーを運用してて、実際に対応速度の差を深く実感してしていて、Guix System の価値いまがとても輝いている。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-22 10:52:54)
これでようやく再現性のないよくわからんシステムから脱却できる…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-22 10:51:59)
Guix が優れてるので podman compose も別にいらなかった
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-22 10:50:29)
大きなインフラ対応するっていってまだ終わってないけど着実に進んでる。
Guix System で Ngnix と Postgesql と Valkey をサービスとして動かすところまで終わってて、必要なファイルもすでに取り込み済み。
あと、残りは nginx の設定ファイルを Guix の形式にして書ききって podman で Mastodon を動かすサービスを3た作るだけ。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-20 01:00:23)
これ始めたけど今日中には終わなそうなので明日続きをすることにした。
睡眠時間は大切なので無理に今日やらない方がいい。
(ここでいう今日とは5月19日のこと)
Older Notes