TojoQK の日記

目次

TojoQK の日記はメインサイトに書くほどでもないことを投稿するためのサイトです。

デスクトップ環境を MATE にしたらやさしい感じになってよかった   Linux

<2022-09-16 Fri>

いままでは Fluxbox を使っていたのだが、デスクトップの見た目を簡単に やさしくしたい という謎のモチベーションによって、 良い感じのデスクトップを探していた。 Fluxbox でもカスタマイズすれば見た目をやさしくすることはできると思うが、 元々やさしい雰囲気のデスクトップ環境を選択することで楽によい感じにできると考えた。

そこで、 MATE Desktop Environment | MATE デスクトップを試してみた。 こんな感じになった。

デスクトップの画像を確認する

MATE について

MATE は GNOME 2 から GNOME 3 への変更を受けいれない人々によって作られたデスクトップで、この方針について私も同意している。 GNOME はなぜ見た目ばっかり激しくてよく分からんインターフェースになってしまったのか……。

見た目について

MATE デスクトップはテーマカラーが緑色でなんとなくやさしい。 私はいままではダークテーマのような格好いい雰囲気の方がよいと感じていたが、 最近はなぜかそういうのではなくてやわらかい印象を与える色を気にいるようになっていたのでなんとなく適していた。

メニューの システム > 設定 > ルックフィール > 外観 の GreenLaguna というテーマに設定し、 背景(壁紙)はデフォルトで入っている草の葉に水が垂れている感じにした。

これでなんとなく緑色が押し出されてまろやかな画面になった。

MATE デスクトップとは関係がないが、 普段から利用しているテキストエディタの Emacs と端末エミュレータの sakura では solarized-light テーマを採用した。 この色は緑色の背景にマッチしていていいし見た目もやさしい。

パネルの設定

パネルの設定は基本的にデフォルトに追加するだけで実用的なものになった。 よく使うソフトウェアを上のパネルにランチャーを追加した。

といっても私は基本的に ALT+F2 でソフトウェアを起動するクセがついているので、 常用するソフトウェアについてはあまりランチャーを使ってない。

ただ後述する MATE を使うことによって知った便利ツールのコマンド名は覚えていないので、 ランチャーから起動している。

便利ツールについて

MATE を使うことで知った便利ツールのうちで最も優れているものは、 mate-disk-usage-analyzer というコマンドで起動できる 「MATE ディスク使用量解析」 というソフトウェアである。 これを使うとホームディレクトリ以下でどのディレクトリがディスク容量を逼迫させているかを調べられる。 同じことは、 ncdu コマンドでもできると思うかもしれない。 しかし、 mate-disk-usage-analyzer の方が、円グラフで良い感じに表示してくれるからよいのだ。

次に便利だと思ったのは mate-power-statistics コマンドで起動できる 「電源使用率の統計」 というソフトウェアだ。 電源の状態を詳細に確認できて嬉しい。バッテリーに関する統計情報を見れたりする。

地味に必要な機能について

Window を画面の左端、右端にドラッグすると画面全体の左半分、右半分の位置とサイズでウィンドウを配置してくれる。 これがデフォルト設定でできるのはありがたい。

おわりに

MATE デスクトップは普通に使うのに何ら困らないし、 画面にやさしさを求める私にはフィットしていた。

あまりいないと思うけど同じモチベーションを持つ人がいたら MATE はおすすめ。

Guix に ox-rss パッケージを追加してもらった   Guix Emacs

<2022-09-07 Wed>

動機

このサイトの RSS を生成するのに Emacs の org-contrib に含まれていた ox-rss というパッケージを使用していたのですが、 9/3(土)に記事を CI サーバー経由で投稿をしようとしたところ org-contrib から ox-rss が削除されていたために失敗しました(Debugger entered--Lisp error: (void-function org-rss-publish-to-rss) というエラーメッセージから原因を特定しました)。 毎週金曜日に CI サーバーの CI 用のユーザーが利用する guix のリポジトリを自動更新していて、 この自動更新によって emacs-org-contrib パッケージが更新された影響で失敗したと分かったので、 9/3 時点では guix pull --rollback を実行して一つ前の世代に戻してから記事を投稿していました。 ただし、来週にはまたパッケージが更新されて org-contrib から ox-rss が消えてしまう問題が再発するので、 Guix の公式リポジトリに ox-rss パッケージを追加してもらうための対応をしました。

CI が失敗した原因

調べてみると orb-contrib のバージョン 0.4.0 のリリース時に ox-rss.el ファイルが削除されたことが分かりました。

~bzg/org-contrib: lisp/org-contrib.el: Bump version to 0.4 - sourcehut git

コミットメッセージによると、Nicholas Savage / ox-rss · GitLab リポジトリにあるファイルであるという理由で消されていました。 Nicholas Savage / ox-rss · GitLabox-rss.el を参照したところ、 メンテナが Bastien Guerry さんから Nick Savage さんに代わったようで今後は Nicholas Savage / ox-rss · GitLab を使うとよいと分かりました。

Guix にパッケージ追加の依頼

Guix に新しいパッケージを追加を依頼するには guix リポジトリの gnu/packages/ 以下にビルドする際の手順を表わすパッケージ定義を書いてパッチを送る必要があります。 パッチを書いて Guix の運営に送るための手順は Contributing (GNU Guix Reference Manual) に具体的に書かれています。

今回は Nicholas Savage / ox-rss · GitLabox-rss をビルドするパッケージ定義を追加してパッチを送りました。 パッチをメールで送ると自動的に Guix issue tracker というサイトに送信した内容が掲載されてスレッドが作成されます。 私が送ったパッチに関するやりとりは下記から参照できます。

[PATCH] gnu: Add emacs-ox-rss.

Nicolas Goaziou さんによってレビュー・修正された emacs-ox-rss のパッケージ定義が無事にマージされました。 素早く対応をしていただき本当にありがたいです。

おわりに

今回のような問題は自分用の Guix のチャンネルのリポジトリがあればそこにパッケージ定義を追加するだけでも解決します。 ただし、 今回の対応は比較的簡単だし同じように困る人もおそらくでてくるのに自分だけ解決するのは申し分けない感じがするので、 パッケージの追加を公式に依頼しました。

同じように Guix で Emacs のパッケージを管理しているけど、 必要なパッケージがなかったりなんらかの不具合があって困っていたりする方は是非パッチを送ってみてください。

Common Lisp の CLOG で YouTube のプレイリスト機能を実装してみた   CLOG Lisp

<2022-09-03 Sat>

はじめに

先週の土曜日に某所で CLOG - The Common Lisp Omnificent GUI というライブラリがあることを教えてもらったところ、 GUI のソフトウェア開発に革命を起しそうなポテンシャルを感じたため、 その可能性を探るために YouTube Local Playlist を開発しました。

CLOG とは

CLOG - The Common Lisp Omnificent GUI はブラウザ上で動く GUI のアプリケーションを簡単に作れるようにする Common Lisp の凄いライブラリで、 Web Scoket によるサーバー・クライアント間通信を駆使することにより サーバーサイド側からクライアント側の制御が可能となっていて、 サーバーかクライアントかをあまり意識することなく GUI アプリの開発ができます。

YouTube Local Playlist とは

私が作成した YouTube Local Playlist は、YouTube の動画を気軽に連続再生するためのソフトウェアで、 主にご飯を食べながら YouTube の動画を連続再生するために使用します。 普段は自前の Git リポジトリにソフトウェアのコードを置いているのですが、 このソフトウェアは何かあったときに対処がしやすそうという理由で GitHub に置いています。 何を懸念しているのかについてはお察しください。

GUI アプリケーションを作成した経験も CLOS を使った開発の経験も Web 開発の経験も少ないため戸惑いも多かったのですが、 私が個人的に必要とする下記機能を実装することができました。 なお、動作テスト時の環境は SBCL で CLOG のバージョンは 1.2 (古い)です。 なぜ CLOG のバージョンが 1.2 になってしまったかというと Guix に登録されている CLOG のバージョンが 1.2 だからです。 Common Lisp のパッケージを Guix に登録する方法を学習するのを先送りした結果こうなりました。

  • YouTube の動画のプレイリストを構築すること
  • 作成したプレイリストをローカルマシンに保存できること
    • 具体的には Common Lisp が動いている環境側に保存される仕様になっている
  • プレイリスト中の動画を再生できること
    • IFrame Player API で再生できるようにした
  • プレイリストの動画を連続再生できること
    • 動画の終了を検知して次の動画を自動再生した
  • ドラッグ&ドロップで動画の並び換えやプレイリスト間の移動ができること
  • ドラッグ&ドロップで動画をプレイリストに追加できること
    • UI からはまず分からないけど、url の入力フォームに YouTube の動画へのリンクをドラッグ&ドロップするだけで追加できる
      • 改善の余地はあきらかにある
  • プレイリスト中の動画をプレイリストから削除できること

CLOG を使ってみた感想

使ってみた感想としては、 かけた労力に対してはるかによいものができているという印象です。 もともと GUI の開発は自分にとってあんまり益がない割に面倒くさいので、 モチベーションがなかったのですがこれくらい楽だと少しやってみようという気持ちになってきます。

チュートリアルがとても充実していて、 それぞれのチュートリアルの趣旨を理解すればだいたい使えるようになります。

CLOS のオブジェクトと DOM が対応していて、 オブジェクトを操作すると DOM が思ったように変化するのが分かりやすい印象です。

clog-builder というツールを使うと GUI で楽に UI の作成ができるようなのですが、 このツールの使い方を覚えるコストは今回の目的に対しては割に合わない感じがしたので使いませんでした。 将来的には使えるようになりたいです。

私は日常的には Common Lisp を書いていないので、 普段から Common Lisp を使っている方が CLOG を使った場合にはもっとよいところや特徴を見つけられるのではないかと思います。 私からは「簡単で良かった、最高!」という感想しかありません。

おわりに

正直私が作った YouTube Local Playlist をみんなに使って欲しいという気持ちはほぼありません。 どちらかというと CLOG 凄いよ!みんな試してみて!という気持ちでこの文章を書きました。

是非 CLOG を使ってみてください。

記事毎に noindex するかどうかを決められるようにした   Diary

<2022-08-24 Wed>

いままでは全ての記事の個別ページに noindex を設定していたが、 しっかり書いた記事は noindex を外して投稿し DuckDuckGo や Google の検索に載せるのを許可することにした。

この記事はどうでもいいので noindex を設定している。 それに対して、 過去に投稿した ACL2 のリハビリに非末尾再帰と末尾再帰の階乗関数が等しいことを証明した は検索されてヒットしたときに「あーこれがやりたかったんだ」ってちょっと思うようなことが書かれていると思う。 この具体例から学べることは少なくないし、 「もしかして ACL2 って使えるかも?」って思える例なんじゃないかと思うしこれは noindex を外す。

全記事の情報を含む一覧ページは決して noindex を外さない。 うっかり外しちゃうとすごく邪魔になると思う。

ACL2 で検索したときに私の記事ばかりがかかるようになるのはもう正直仕方がない。 実際流行っていないなか一人だけやって情報を発信してたらそりゃそうなってしまう。 将来的にもっと SEO の強い人が ACL2 を始めれば解決する問題だし気にしないこととする。

タグをクリックするとそのタグがついている記事のリストを見れるようにした   Diary

<2022-08-24 Wed>

タグをクリックすると同じタグが付いている記事のリストを見れるようにした。

たとえばこの記事には diary というタグが付いているが、 これをクリックすると同じ diary の記事一覧にアクセスできる。

いままで無駄に表示されていたタグが機能を持って便利なサイトになってきた。

正直、既にメインのサイトの機能を越えてしまっている……。 メインサイトの方も同じくらい便利にしていきたいところ。

OpenDNS でペアレンタルコントロール的なことをした   OpenDNS

<2022-08-24 Wed>

プライベートな時間にインターネットで無駄に不毛な時間をすごさないようにするにはどうするべきか考えた結果、 原因となるウェブサイトに容易にアクセスできなくするのがよいという結論になった。

Cisco の OpenDNS というサービスで OpenDNS の DNS サーバーを利用している間は、 いたずらに時間を奪ってしまうサイトをブロックするように設定した。

Web Content Filtering の設定は High, Moderate, Low, None, Custom から選ぶことができ、 High に設定するとアダルトサイトや違法行為に関するサイト、 SNS、動画共有サイトそしてその他の時間を潰してしまう色々なサイトへのアクセスをブロックしてくれる。 ただ、High の設定では Slack も使えなくなるという問題があったので、 High の設定から ChatInstant Messaging という項目を外した Custom 設定を使うことにした。

これで、無意識に時間を潰しそうなサイトにアクセスしようとしてもすぐにブロックされて正気に戻れるようになった。 実際に Twitter や YouTube にアクセスしてみたところブロックされた。

DNS サーバーの設定を変更するだけで簡単に OpenDNS の Web Content Filtering から逃れられてしまうため強制力は低い。 どうしても拒否されたサイトにアクセスしたい場合は DNS の設定や OpenDNS の設定を変更するのではなくて、 フィルタリングの仕組みが形骸化しないように快適でない別のデバイスからアクセスをするなどの工夫をする。

org-babel で Scheme (Geiser) が機能しない問題が解決した件   Emacs Org

<2022-08-23 Tue>

注意: 現在私が使用している Emacs は GNU Emacs 28.1 です。

org-babel で Scheme のコードがうまく実行できない問題にだいぶ前(いつ?)に気づいたが、 それほどクリティカルな問題でもなかったので気にしないで過していた。

しかし、今日 org-babel でとても Scheme を使いたい状況になってしまいとても困ったので調べたところ解決した。

下記で紹介されている方法で解消する。

doom - Capturing output scheme when executing a code block in org-mode - Emacs Stack Exchange

リンク先ではソースコードを編集しているが、 私は Guix で Emacs のパッケージをインストールしている都合上コードの直接編集は無理なので、 init.el で関数を全体を上書きしてリンク先の変更点を反映した。

その結果問題なく動作するようになった。圧倒的感謝。

次 Emacs のバージョンアップをするときに修正されているかテストするのを忘れないようにしよう(私は ob-scheme をパッケージでインストールしていなくて、Emacs に同梱されているやつを使っている)。

無理して公開日記の開発に力を注ぎすぎないようにセーブすることにした   Diary

<2022-08-22 Mon>

個別ページを作成したのと同じような方法で、 記事を日付毎にまとめたページやタグごとにまとめたページを作れることが分かった。

できることは間違いないのだが実際に実現するのはちょっと面倒くさい。 現在の公開日記でも私が快適に日記を書く分には十分なので、 無理にサイト作成に力を入れすぎないようにすると決めた。

公開日記(このサイト)に記事ページを生成するようにした   Diary

<2022-08-20 Sat>

いままでの一覧ページしか存在しない仕様は記事のリンクをコピーしたい人にとっては不便なので、 単独の記事を掲載するページを生成した。 タイトルのリンクを踏むと記事のページに遷移する仕様にした。

RSS のリンク先はいままでと同様に記事の一覧ページに跳ぶようになっていて、 基本的には記事の一覧ページのみで運用する予定でいる。

個別の記事ページはこのサイト的にはおまけ機能という感じ。 記事のリンクをコピーしたいと思う人はなんとなくタイトルをクリックするんじゃないかなと想像している。

公開日記にヘッダーを追加した   Diary

<2022-08-19 Fri>

fniessen/org-html-themes: How to export Org mode files into awesome HTML in 2 minutes の readtheorg というテーマを使っていて、 既に完成されているページにヘッダーを追加するのは大変だった(1時間半もかかった)。

ヘッダーを作ることができたのでこのサイトに個別のページを作る準備が一つ整った(一生作らないかもしれないけど)。 ヘッダーがあれば個別ページから元のページにどうやって戻ればいいか分かるようにできるだろう。

ACL2の強力なルールについて   ACL2

<2022-08-18 Thu>

今日は XDOC — Practice-formulating-strong-rules の問題を解いていた。

Strong rule とは、仮定が少なくてRewriteルールでより書き換えしやすいルールのことである。 仮定がない定理をうまく記述できると、もっと式を簡単にできるのにRewriteルールが仮定にマッチしていないために発火しない……という問題に悩まされることが少なくなり自動証明がうまくいきやすくなる。 ACL2 では同じ意味の定理でも implies を使って同じことを記述するのと iffequal のみで記述するのでは、 全然動きが違うのでここら辺はよく勉強しておかないと何故かルールが使われない問題にぶち当たりまくって詰んでしまう。

Term 3 は普通に正解できたが、 iffequal の rewrite ルールの使い分けに関する知見が含まれていてよかった。 Term 5Term 6 だいぶ悩んだ結果答えを見て納得する感じだった。

Term 5 は分からなかったらあんまり深く考えずに切り上げるのがおすすめ。

Term 6 は重要で、ためらうことなく右辺に if を使うことの大切さが書かれていた。 私は nfix を使って if のないルールを書いてしまった(強いルールではある)が、 if を使った方が意味的に正しいし綺麗だしたぶんよりうまくルールが機能しそうだったので、 自分の解答よりも if を使う方がよさそうでありたいへん勉強になった。

ACL2 で非末尾再帰と末尾再帰の階乗関数が等しいことを証明した   ACL2 Lisp

<2022-08-17 Wed>

[2022-08-24 Wed] 追記: タイトルを「ACL2 のリハビリに非末尾再帰と末尾再帰の階乗関数が等しいことを証明した」から「ACL2 の非末尾再帰と末尾再帰の階乗関数が等しいことを証明した」に変更しました。

ここ最近は自分のサーバーまわりの作業ばかりをやっていて、 全然 ACL2 をやっていなくてほとんど忘れてしまった感じがするので練習のために簡単なことから始めて慣れようと思う。

末尾再帰版の階乗と非末尾再帰版の階乗を書いて、それぞれの関数の戻り値が等しくなることを証明した。

こっちが非末尾再帰の普通の階乗

(defun factorial (n)
  (if (zp n)
      1
      (* n (factorial (- n 1)))))

これが末尾再帰版の階乗

(defun factorial-tail (n a)
  (if (zp n)
      a
      (factorial-tail (- n 1)
                      (* n a))))

いきなり下記のように直接証明を試みても失敗する。

(defthm factorial-tail-factorial
  (equal (factorial-tail n 1)
         (factorial n)))
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(EQUAL (FACTORIAL-TAIL N 1)
       (FACTORIAL N))

*** Key checkpoint under a top-level induction: ***

Subgoal *1/2'
(IMPLIES (AND (NOT (ZP N))
              (EQUAL (FACTORIAL-TAIL (+ -1 N) 1)
                     (FACTORIAL (+ -1 N))))
         (EQUAL (FACTORIAL-TAIL (+ -1 N) N)
                (* N (FACTORIAL (+ -1 N)))))

ACL2 Error [Failure] in ( DEFTHM FACTORIAL-TAIL-FACTORIAL ...):  See
:DOC failure.

******** FAILED ********
 :ERROR

キーチェックポイントをみても、 正しそうな数学的帰納法を試みているだけで式変形が進んでいないのでこれだとおそらく詰み。

こういうのは、 1 を変数に置き換えて一般化すると証明できるようになる。

(defthm factorial-tail-factorial-generic
  (implies (integerp a)
           (equal (factorial-tail n a)
                  (* a (factorial n)))))
Summary
Form:  ( DEFTHM FACTORIAL-TAIL-FACTORIAL-GENERIC ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION FACTORIAL)
        (:DEFINITION FACTORIAL-TAIL)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FACTORIAL)
        (:INDUCTION FACTORIAL-TAIL)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE UNICITY-OF-1)
        (:TYPE-PRESCRIPTION FACTORIAL))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1455

---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(IMPLIES (INTEGERP A)
         (EQUAL (FACTORIAL-TAIL N A)
                (* A (FACTORIAL N))))

*** Key checkpoint under a top-level induction: ***

Subgoal *1/3'''
(IMPLIES (AND (NOT (ZP N))
              (EQUAL (FACTORIAL-TAIL (+ -1 N) (* A N))
                     (* N A (FACTORIAL (+ -1 N))))
              (INTEGERP A))
         (EQUAL (FACTORIAL-TAIL (+ -1 N) (* A N))
                (* A N (FACTORIAL (+ -1 N)))))

ACL2 Error [Failure] in ( DEFTHM FACTORIAL-TAIL-FACTORIAL-GENERIC ...):
See :DOC failure.

******** FAILED ********
 :ERROR

今度は式変形が進んでいるが、途中で止まってしまった。 Subgoal *1/3''' では、仮定の式に (* N A (FACTORIAL (+ -1 N))) 、 帰結の式に (* A N (FACTORIAL (+ -1 N))) がある。 これは、積の交換則から等しいが ACL2 はどういうわけか等しいと気づいてくれない(Rewriteルールがない)。 裸の ACL2 にも積の交換則のRewriteルールとして COMMUTATIVITY-OF-* が用意されているが、 (equal (* a b c) (* b a c)) のような状況には対応していない。 この問題は arithmetic という ACL2 のコミュニティブックによって解決されている。 下記を実行してブックを読み込む。

(local (include-book "arithmetic/top-with-meta" :dir :system))

再度、 factorial-tail-factorial-generic を試す。

(defthm factorial-tail-factorial-generic
  (implies (integerp a)
           (equal (factorial-tail n a)
                  (* a (factorial n)))))

こんどは証明に成功した。 下記の Summary に COMMUTATIVITY-2-OF-* があることに注目して欲しい。 (* a b c)(* b a c) が等しいことを表現するRewriteルールで、 これが使われたことで無事に証明に成功している。

Q.E.D.

Summary
Form:  ( DEFTHM FACTORIAL-TAIL-FACTORIAL-GENERIC ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION FACTORIAL)
        (:DEFINITION FACTORIAL-TAIL)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FACTORIAL)
        (:INDUCTION FACTORIAL-TAIL)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE UNICITY-OF-1))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  362
 FACTORIAL-TAIL-FACTORIAL-GENERIC

今回証明したいことは今証明したことの特殊な場合なので、 この定理を証明したあとであれば普通に自動証明に成功する。

(defthm factorial-tail-factorial
  (equal (factorial-tail n 1)
         (factorial n)))

FACTORIAL-TAIL-FACTORIAL-GENERIC が使われて証明に成功した。

Q.E.D.

Summary
Form:  ( DEFTHM FACTORIAL-TAIL-FACTORIAL ...)
Rules: ((:DEFINITION FIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE FACTORIAL-TAIL-FACTORIAL-GENERIC)
        (:REWRITE UNICITY-OF-1)
        (:TYPE-PRESCRIPTION FACTORIAL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  42
 FACTORIAL-TAIL-FACTORIAL

無事に目的を達成できた。 COMMUTATIVITY-2-OF-* が必要になったので驚いたが、 これは知ってたので解決できた。 一応、公式のチュートリアルのFAQの下記の質問のところに (include-book "arithmetic/top-with-meta" :dir :system) しろと書いてあるのでこれを読めば解決できる問題ではある。

Q. ACL2 doesn't know simple arithmetic that can simplify the term (+ 1 -1 x).
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS

learn-acl2 という ACL2 の勉強用のリポジトリを作ったので、 今回のを含めてこれから学習のために書いた ACL2 のコードはここ置いていくこととする。

コード: factorial.lisp CI: https://ci.tojo.tokyo/jobs/acl2-verify/523

IFTTT というサービスを利用して Twitter に自動投稿するように設定した    IFTTT

<2022-08-17 Wed>

私の Twitter アカウントは基本的に放置気味だが、たまに Twitter を開いてなんか人間行動に言及している投稿に対する批判コメントをするということを繰り返しになっている。 これが続くと Twitter の投稿履歴からは常に人間行動への言及をディスっている人にみえてしまうのでよくない。

とはいっても Twitter を開いて他者ツイートに対しての反応ではない投稿をする行動は残念ながら強化されていなくて、いまのところまったく自発しない。 この投稿履歴がひどい問題を解消するために公開日記の投稿を Twitter に流して、 私の人間行動に関する愚痴を薄める作戦を決行した。

これで私の投稿履歴になんとなくエンジニアっぽい記事へのリンクがたくさんになって、 人間行動への言及に対してディスるマンには見えなくなるだろう。

IFTTT では RSS の新しい feed をトリガーにして Twitter へ投稿するように設定した。 ちゃんと動くといいな。

なお、私の Twitter アカウントはメインサイトの お問い合わせ に記載してある。

Laminar のバージョンを 1.2 に上げた   Guix Laminar

<2022-08-17 Wed>

https://ci.tojo.tokyoLaminar のバージョンはいままで 1.1 だったが、 このバージョンの Laminar にはジョブの中でジョブを実行したときに、 出力中のサブジョブへのリンクがクォートされてしまってクリックできないというバグを含んでいた。 これは Link to queued jobs is double escaped · Issue #161 · ohwgiles/laminar で解決され、 バージョン 1.2 の Laminar CI には反映されているようだった。

丁度サブジョブを使いたくて困ったので、この機会にバージョン 1.2 に上げることにした。

現在 Laminar は Guix System の Services を使って動かしていて、 ここで利用している Laminar パッケージのバージョンが 1.1 なのが問題になっている。 GNU Guix の公式リポジトリの Laminar パッケージの最新はまだ 1.1 なので、 guix pull で更新してもバージョン 1.2 の Laminar は使えない。

なので、自分の Guix チャンネル にバージョン 1.2 の Laminar を登録して使うことにした。

パッケージ定義は元の laminar パッケージを継承して、 バージョン周りの部分を更新するだけでうまく動いた。

https://git.tojo.tokyo/tojo-tokyo-guix-channel.git/tree/tojo-tokyo/packages/ci.scm?id=845a12e73d86c204b387fdb887eba5ae3ed76891

(define-module (tojo-tokyo packages ci)
  #:use-module (gnu packages ci)
  #:use-module (guix packages)
  #:use-module (guix download)
  #:use-module (guix gexp)
  #:use-module (guix utils))

(define-public laminar-next
  (package
    (inherit laminar)
    (name "laminar-next")
    (version "1.2")
    (source
     (origin (method url-fetch)
             (uri (string-append "https://github.com/ohwgiles/laminar/archive/"
                                 version
                                 ".tar.gz"))
             (file-name (string-append name "-" version ".tar.gz"))
             (sha256
              (base32
               "0vcgpp8g67mlhqnyhkihxz9j5jz1pal79jrdhnmjl5ddbhkvji8i"))))
    (arguments
     (substitute-keyword-arguments (package-arguments laminar)
       ((#:configure-flags flags #~'())
        #~(map (lambda (x)
                 (cond ((string-prefix? "-DLAMINAR_VERSION=" x)
                        (string-append "-DLAMINAR_VERSION=" #$version))
                       (else x)))
               #$flags))))))

Guix System の config.scm で下記のように laminar-next を使うように指定したところ問題なく動作した。

(service laminar-service-type
         (laminar-configuration
          (laminar laminar-next)
          (title "CI for git.tojo.tokyo")))

結果、過去のジョブも含めてサブジョブへのリンクを踏んで遷移できるようになった。 下記のジョブの出力中の #521 をクリックするとサブジョブに遷移できる。

https://ci.tojo.tokyo/jobs/learn-acl2/5

表が崩れないように Emacs のフォントサイズを微調節した   Emacs

<2022-08-14 Sun>

Emacs のフォントサイズを調節する記事は巷に溢れていて結局どうするのがいいのかよく分からなくて困る。 私がいきついた方法が最高の方法なのかどうかもよく分からない。

Emacs のフォント設定は闇だと思うが、 日本語文字と英数字が入り乱れた表が崩れる問題が解決可能な問題であるというのは Emacs のよいところだと思う。

英数字用のフォントと日本語フォントを別々に指定している人の表が崩れないようにするには、 日本語文字のフォントのサイズを rescale する必要がある(他の方法もありそう……)。

(set-face-attribute 'default nil :family "Hermit" :height 120)
(set-fontset-font t 'japanese-jisx0208 "Noto Sans Mono CJK JP")
(add-to-list 'face-font-rescale-alist
             '(".*Noto Sans Mono CJK JP.*" . 1.3))

使用しているフォントで変わってくると思うが、私の環境では 1.3 に設定すると表が崩れなくなった。 ただ、フォントサイズを極端に拡大したり縮小したりするとこれでもズレてしまうが滅多にない状況なのでそれは受容することにした。

グッドスタインの定理をACL2で証明できるか気になってる   ACL2

<2022-08-14 Sun>

グッドスタインの定理はペアノ算術の範囲では証明できないことが示されている定理らしく順序数を使うと証明できるらしい。

下記の動画でこの定理の名前を知り Wikipedia で調べて順序数と関係のある定理であると知った。

【雑学】正しいとも間違いとも言えない数学の命題が存在する【ゆっくり解説】 - YouTube

グッドスタインの定理 - Wikipedia

ペアノ算術の範囲で証明できないことを証明するのは難しそうだが、 Wikipedia に載っている順序数を使った証明は ACL2 で可能かもしれないと思って調べてみた。

すると、グットスタインの定理を ACL2 で表現しているコードが、 ACL2 の books に misc/goodstein.lisp として掲載されていた。

acl2/goodstein.lisp at master · acl2/acl2 · GitHub

関数は :program モードで定義されているため、 このファイルを読み込んでもファイル中の goodstein 関数の停止性が自動証明されるわけではない。 コメントで何故停止するのかの説明がなされているがそれぞの関数の定義をよく読み込まないと理解できなそう。

順序数の勉強にもなりそうだし、余裕があったらとり組んでみようと思う。

メインサイトでスマホ対応した

<2022-08-13 Sat>

メインサイトのメニューバーの項目が多くなってきて、 スマホからサイトを見ると表示が崩れてしまうのが問題になっていた。

この問題を解決するためにハンバーガーメニューを導入しようと考えたが、 既存の構造を弄らないといけなくて意外と厄介だなあと思って足踏みしていた。

悩みながら試行錯誤で css を編集していたら、 ハンバーガーメニューを導入しなくても下記の追加のみで良い感じに表示されることに気づいた。

@media screen and (max-width:768px) {
    .nav-bar {
        flex-flow: column;
    }
}

ハンバーガーメニューだとわざわざクリックしないと項目が見えないというデメリットもあるしこれでいこうと思う。

機内モードを有効にする方法   Linux

<2022-08-10 Wed>

飛行機などに乗っているときは機内モードにしておきたいが、 いま使っている Window Manager にそれっぽい設定をする方法なさそうなので機内モードにする方法を調べた。

rfkill を使うと良さそう。

rfkill list all
0: hci0: Bluetooth
	Soft blocked: no
	Hard blocked: no
1: phy0: Wireless LAN
	Soft blocked: no
	Hard blocked: no

Soft blocked, Hard blocked が no なので、Bluetooth, Wireless LAN のいずれもブロックされていない。 下記コマンドで Soft blocked を on に変えることで Soft blocked を on にすることで機内モードの状態にする。

sudo rfkill block all

これを実行すると Wifi も Bluetooth も繋がらなくなる。 ソフトウェア的に機内モードにするならこれでよさそう。

実行後の rfkill list all はこんな感じ。

rfkill list all
0: hci0: Bluetooth
	Soft blocked: yes
	Hard blocked: no
1: phy0: Wireless LAN
	Soft blocked: yes
	Hard blocked: no

解除するには下記コマンドを実行する。

sudo rfkill unblock all

CI から Guix System に config.scm をデプロイして実行できるようにした   Guix

<2022-08-09 Tue>

個人で管理する Guix System のサーバーが5台もあって、 手作業で設定(config.scm)をデプロイしていると流石に大変になってきたので 非公開の CI から自動的にデプロイできるようにした。

ただ、Guix System の設定って反映した後にデーモンの再起動をした方がいい場合があって、 そういう場合に再起動を忘れてしまいそうな感じになってしまっている。

とはいえ、今の時点でも手動で作業するよりはだいぶ楽だし、 良い方法を思いつくまでデーモンの再起動の仕組みをどうするかは一旦おいておくこととした。

Guix のサーバーを全て更新した   Guix

<2022-08-07 Sun>

Guix System のサーバーをそれぞれ更新して再起動した。 そしたら Web サーバーの容量が 80% を越えてしまったことを Zabbix が通知してくれたので確認したところ /gnu/store 以下が肥大化していたことが分かった。

guix gc の対応をしたところ、20GB も一気に空いてスッキリした。

今回は生じなかったがサーバーを再起動したときに稀にプロセスが起動しない場合がある(過去に smtpd が起動しなかったのを体験している)ので、 後で Zabbix の監視にプロセス監視を追加しようと思う。

Zabbix によるサーバー監視を始めた   Zabbix

<2022-08-05 Fri>

友人にサーバーの建て方を教えるための資料を作っていて、 「セキュリティはどうすればいい?」とか「何を監視すればいいの?」などと聞かれ、 自分は5台もサーバーを運用しているのにもかかわらずたいした監視をしてない事実に気づかされた。

外形監視とお手製スクリプトによるディスク監視をしていたが、 これで色々監視しようとすると大変なので Zabbix を導入してみた。

Zabbix はいままで使ったことのないツールで、使い方を色々学習する必要があって、 一昨日あたりから趣味の時間が Zabbix 一色になってしまうというストレスフルな生活を送っていた。

まあでも最終的には以下の監視ができるようになって満足している。

  • Linux by Zabbix agent テンプレートによる監視
    • この中に Disk 監視のトリガーが入っていたのでそのまま使っている
  • メールサーバーのメール送信数の監視
    • メールサーバーが異常にメール送信したらすぐに気づくようにした
    • うっかり踏み台メールサーバーになって責任問われたら怖いので……
  • OpenVPN にログインしたときにすぐに通知するようにした
    • 私の趣味インフラの一番突破されたくない部分
      • ここを突破されると……
        • プライベートな日記とか日程をホスティングしているページにアクセスできてしまう!
        • 色んなサーバーに ssh で接続されてしまうかもしれない!
          • パスワード認証は許可してないから大丈夫なはずだが……
      • 一次対応として異常を感知したらすぐに VPN サーバーを落とすつもり
        • まさかそんなことが起こってしまうとは思いたくないが……
      • その後は VPN サーバーとそこからアクセスされうるサーバーの作り直しをすると思う
        • ssh ログインのログとかリアルタイムに記録するようにしたし、それみて他のインフラに影響がでてないかは確認できるけど気持ちわるいのでそうなったら全部作り直すと思う

外形監視は Uptimerobot の無料プランで十分なのでしないことにした。 Zabbix は一つの機能の使い方を覚えるだけでも大変なので一気に色々やるのはやめとこうと思ってる。

Zabbix の監視をどうするかは正直課題だし、Zabbix からの障害通知が監視対象であるメールサーバーを経由しているのもまた問題である。 ここらへんをどうするかは今後検討していく。

Guix System で二つのネットワークデバイスに異なるネットワークを設定できない件   Guix

<2022-08-04 Thu>

Vultr の VPS で VPC を使いたいんだけど、 Guix System で Static IP を二つのネットワークデバイスに割り振るとエラーになるみたいでつらい。

下記の Issue を見た限りではどうもまだ解決していないみたい。

service networking provided more than once

サーバー間で http 通信したいところがあって、 そこを internal なネットワークにすればとりあえず http のままでも安全になるから使いたかったんだけどどうも無理そう。

ただ、私がかかえている問題は ssh ポートフォワーディングを使うことでも解決できることなのでとりあえずそれで解決することにした。 若干手間がかかって面倒くさいこと以外には特に大きな欠点はない。 若干手間がかかって面倒くさいことが問題なのだが……。

Nextcloud を無事に終了した   Nextcloud

<2022-08-03 Wed>

課題になっていた下記二点を解消したので Nextcloud を終了した。

  • Nextcloud Password への依存
    • Pass: The Standard Unix Password Manager に移行した
      • スマホから使うための準備はしてない
        • たぶんそんなにスマホからパスワードを入力したくならないと思う
        • 必要になったらそのときに考える
        • Android から使うためのアプリが存在することは確認済み
    • ちまちま Nextcloud Password から一つずつパスワードを移行した
      • 超面倒くさかった
  • スマホで撮影した写真の Nextcloud への自動アップロード
    • 下記手順で写真をオブジェクトストレージに上げてプライベートなHTML日記から参照する
      1. VPN の LAN を経由してスマホから PC (Laptop) に画像を移動する
        • PC に phone ユーザーを作って sshd を起動し sftp で画像をアップロードする
          • このために iptables の設定などを見直した
      2. PC から自作スクリプトを使ってスマホから PC に移動した画像をオブジェクトストレージにアップする
      3. プライベートなHTML日記からオブジェクトストレージの画像を参照する
        • html のファイルは org-mode から生成している
    • 日記に残さない写真の保管は不要と判断した
      • 逆に残したい写真は必ず日記に写真を上げる運用とする

スマホで撮影した写真を日記に載せるプロセスをここで詳細に説明するのはたいへんなので大幅に省略した。 私のプライベートな日記システムや、VPN の設定などはいつか記事にしてもいいかもしれない。

プラゴミ輸出問題の解決にケミカルリサイクルがよさそう   SDGs

<2022-08-02 Tue>

今日、プラゴミを捨てるときにふと今の日本のプラスチックゴミの輸出量がどうなっているのか気になって調べてみたら、 中国が輸入規制を始める前の2017年と比べて減ってはいるものの未だに当時の半分程度は輸出されていると分かった。

Japan Export Data — Basel Action Network

いまの私にとってはもう常識になっているが最初にプラスチックゴミが輸出されていると知ったときには本当に驚いたのをよく覚えている。 てっきり全て日本でリサイクルをしているのだと思いこんでいた。 SDGs と叫ばれる昨今でもかつての私と同じようにプラスチックゴミを全て自国で処理していると思い込んでいる人は多いのではないだろうか。

私は下記の BCC News Japan の報道で知った。 この事実を日本の報道から知るのが難しいというのはたいへん残念に思う。

日本のプラスチック「リサイクル」 実際には何が起きているのか - YouTube

下記の記事によると、三菱ケミカルとエネオスの共同プロジェクトでケミカルリサイクルの技術が開発されているらしい。 これがうまくいけばプラスチックの理想的なリサイクルが実現できるようになって、 日本のゴミ輸出問題も改善されていくかもしれない。

プラスチックよどこへ行く 廃プラ問題と日本のリサイクル事情 - Chemical Technology News

個人で運用している Nextcloud を終了する   Nextcloud Org

<2022-08-01 Mon>

Nextcloud を動かすのに現在月額10USDかかっているが、 Nextcloud の役割が徐々に Org-mode に置き換わっていった結果、 現在 Nextcloud はたいした仕事をしていないのでもったいない。

Org-mode のファイルは git で管理していて、 プライベートな git リポジトリにプッシュしているので Org-mode での管理と比べて Nextcloud がクラウドであることのメリットは少ない。

以上の理由から Nextcloud の運用をやめて無駄をなくす。

Org-mode に移行したもの

  • メモ(Nextcloud Notes を使っていた)
  • カレンダー
  • タスク管理

Emacs に移行したもの

  • RSS 購読
    • elfeed を使ってる
  • メールを読む
    • Gnus を使ってる
    • Icedove(Thunderbird) も使ってる

現在 Nextcloud がやっている仕事

Nextcloud を廃止するには、 現在 Nextcloud でやっている下記の仕事の代替を用意する必要があるので、 その対応は必要になる。

写真の自動アップロード

これはオブジェクトストレージにアップロードして、 Org-mode で書いている非公開の日記から参照できるようにして解決する。

日記に載せないような写真は不要であるとすれば、 整理せずにとりあえず写真をアップロードしておくのは無駄だといえる。

Org-mode は PC から扱うので、 スマホで撮影した写真を PC に楽に移動する方法については考えないといけない。

パスワードマネージャ(Nextcloud Password)

このサイトの作り方の簡単な説明について   Diary

<2022-08-01 Mon>

使っているのは:

のみで、かなりシンプルで楽な構成になっている。 それでも私がこの日記に求める機能を十分備えているのですごい。

あとは org-capture-templates に下記を追加してキャプチャしてデプロイするだけで投稿できてる。

`(("p" "公開日記" entry (file "~/private/src/diary/index.org")
   "* %?\n:PROPERTIES:\n:CUSTOM_ID: %<%Y-%m-%d>-%^{ID}\n:RSS_PERMALINK: #%<%Y-%m-%d>-%\\1\n:PUBDATE: %T\n:END:\n%t"
   :prepend 1
   :jump-to-captured t))

他にも細かい話は多少あるので、これについてはメインサイトの方で記事にする予定。

投稿毎の個別のページは作らない予定   Diary

<2022-08-01 Mon>

いまの状態でもパーマリンクは取得できるわけだし、 個別のページは作らなくて良いと考えてる。

もしも投稿毎に個別のページを作りたくなるとしたら、 検索にかかるようになるようにしたい場合だと思うんだけど、 そもそも検索にかかりたくないという理由で始めたので個別ページを作る必要がない。

といってもまあパーマリンクを取得する機能を作っているわけだし、 投稿の引用自体は Welcome ではある。

まあ、パーマリンクっていって通じる層って限られる気がするけど、 私の日記をわざわざ見にくる人は IT リテラシー高そうだし通じるんじゃないかと思う。

画像をアップロードする手軽なスクリプト   Program

<2022-07-31 Sun>

オブジェクトストレージに画像をアップロードする便利スクリプトを書いたので公開します。 アップロードするときに画像の向きの修正とメタデータの削除をしています。

mktemp とか使って一時ファイルを作成していない雑な実装なので流用する場合には注意してください。 なお、ここでスクリプトを公開するときの著作者の名前は TojoQK とすることにしました。

#!/usr/bin/env bash
# upload-diary-image
#
# Copyright (C) 2022 TojoQK <tojoqk@tojo.tokyo>
#
# This software is released under the MIT License.
# http://opensource.org/licenses/mit-license.php
set -euo pipefail

s3prefix="<s3のURL>"

filename=
while getopts f: opt
do
  case "${opt}" in
    f) filename=${OPTARG};;
  esac
done

shift $((OPTIND - 1))
name="$1.jpg"

# ファイル名が指定されていない場合はクリップボードからアップロードする
if [ -z "$filename" ]
then
  targets="$(xclip -selection clipboard -t TARGETS -o)"
  if [ -n "$(grep 'image/jpeg' <<< "$targets")" ]
  then
    filename=/tmp/clipboard.jpg
    xclip -selection clipboard -t image/jpeg -o > "$filename"
  else
    echo クリップボードに画像が保存されていません 1>&2
    exit 1
  fi
fi

prefix="$(date '+%Y-%m-%d/%H%M-')"
s3url="s3://$s3prefix/$prefix$name"

convert -auto-orient -strip "$filename" "/tmp/uploadimage.jpg"

echo "確認してください"
display "/tmp/uploadimage.jpg"

echo -n "公開されるけどアップロードしていい?(yes/no): "
read line
echo "[$line]"

if [ "$line" != "yes" ]
then
    echo "アップロードを中断しました"
    exit 0;
fi

aws s3 cp --acl public-read --endpoint-url https://ewr1.vultrobjects.com "/tmp/uploadimage.jpg" "$s3url"

日記に書く内容の方針について   Diary

<2022-07-31 Sun>

TojoQK の日記としてサイトを開設したが、 実際のところ本当に私の日記を書くかというとそれは微妙だ。 本当に個人的な日記はまあよほどのファンでもない限りは、 需要ないだろうからな。 プライベートでも日記を書いているので、個人的な日記はそっちに書けばいい。

せっかく RSS 対応したんだから RSS 購読する価値はありそうなことを書いていきたい。 そのために何を書くかだが、 メインサイトで記事にするほどでもない程度の技術的なことを書くのがいいと思う。 メインサイトの方はどうも「はじめに」「あーだこーだ」「おわりに」という、 形式でしっかりめに記事を書く習慣ができてしまっていて大変だから、 そこまでのほどでもないことは日記の方に書いていく。

あとはまあ、記事は確実に埋もれるので備忘録的なことを書くのはあまり向いてないと思う。 一応目次から飛べば投稿へのパーマリンクを取得できるようになっているので、 投稿を参照すること自体はできるのでメモを書くことができないということはない。

タグは積極的に付けていった方がいいと思うので、 日記についての投稿には diary タグを付けることにした。

今のところあまり意味のないタグだが、もしかしたら将来活用されるかもしれない。

検索避けのためのヘッダ要素を設定した   Diary

<2022-07-31 Sun>

robots.txt で弾くだけではなくて head に <meta name="robots" content="noindex,nofollow,noarchive"/> を設定しておくと良いらしいので設定した。

このページの文章量は膨大になるので、 インデックスされると割と本当に困るので設定が効いてくれるとありがたい。

参考にさせていただいた記事

この日記、SNS 依存からの脱却に使えそう   Diary

<2022-07-31 Sun>

SNS で投稿すると、 リツイートやリプライによって反応されてしまい、 会話が始まって疲れるということがよくある。

あと投稿した後にいいねされたりすると、 SNS の投稿行動や SNS の画面を開く行動が強化されてしまって時間の無駄になりがちという問題もある。

SNS のかわりにこっちに文章を書くようにすれば、 より健康的な生活が送れると思う。

テスト投稿

<2022-07-31 Sun>

Emacs から簡単に投稿できるようになっているかのテスト。

今日から公開日記を始める   Diary

<2022-07-31 Sun>

https://www.tojo.tokyo に記事を書いてきたが、 なんというかあっちは真面目に記事を書きすぎていて気軽に記事を追加できない。

もっと雑な感じに文書を書いて公開したい。 考えてみれば最初は雑に文書を投稿する場としてサイト運営を始めたつもりだった。

じゃあ Mastodon とか Twitter あるしそこに投稿すればよくね? ってなるかもしれないけど、 あれはフォローだとかお気にいり/いいねだとかブースト/リツイートだとかリプライとかあってなんか違う。 SNS だと他者の投稿に反応する形の投稿が多めになりがちになってしまっていて目的と微妙に異なる。

あと、謎に SEO 強いのも考えもので検索したときに私の記事がでてきてしまうのも困る。 これはおそらく ACL2 とか Laminar CI のような他に日本語の情報がほとんどない記事を投稿しているせいだと思う。 こういう状況下だと気軽に公開というわけにもいかなくなるので、 検索避けのために robots.txt で検索エンジンを弾くようにした。 万が一このページが検索してでてくるようになったらそのときに対策する予定。

というわけで日記用のサイトを作ったので、 ちょっとしたことはここに書いて規模の大きいものはメインの記事にすることにした。

著者: TojoQK

Email: tojoqk@tojo.tokyo

Created: 2022-09-16 Fri 11:30

Validate