TojoQK の日記

<2022-11-21 Mon>

いままでは日記として技術的な記事を書くようにしていましたが、 今後は本当にどうでもいい長文を日記の方にアップしていくことにします。

技術的な要素のある記事は TojoQK の投稿 の方にアップしていきますので、 そちらの方のみRSSの購読をしていただければと思います。 「TojoQK の投稿」の方でも Google からの INDEX を許可するかどうかを、 記事ごとに制御できるようになったので今後は気楽に記事をアップできると思います。

具体的にどのようなことを書いていくつもりかというと、 新作のポケモンのゲーム(スカーレット)のことや、 仕事がこんな感じだったみたいなことを日記に書いていきます。

自由ソフトウェアがどうとかいっているのにポケモンはするのかと思われるかもしれませんが、 まあ自由ソフトウェアについて語るならポケモンはやるなといったら、 いまどき自由ソフトウェアが流行るわけないので、気にせずにポケモンはやろうと思ってます。 だからといってゲームも自由ソフトウェアでなくてよいと思っているわけではなくて、 理想的に自由ソフトウェアにできればよいとは考えています。

ゲームと DRM については結構考えているので、 将来的にはこの件について何か記事を書くかもしれません。

<2022-11-19 Sat>

Web 開発のチームに所属して1ヶ月以上経過した。 まだ新人としての扱いのため期限が迫っているような仕事は振られないため、 いまのところ業務負荷について心配する必要はなさそうだ。

<2022-10-02 Sun>

今日小さめではあるが古典AIの文脈で多少の規模のあるシステムを拡張する形のプログラムを書く必要のある問題を解いたのだが、 そのときに利用しているプログラミング言語が Common Lisp でよかったと感じたことについて書く。

なお、これについてうだうだ考えて眠れないので出力してしまってすっきりするための文書なのであまり鵜呑みにしないように。

与えられた問題に対してどう書けば正しいものを書けるのかを探るのに、 まず間違ったプログラムをまず書くという方法があると思う。

最初は問題を解くための方針をとりあえず考える。 ただそれでも今日の問題は少し難しくアイデアが漠然としていて、プログラムの設計みたいなのを明確にするのは難しかった。 それに実質的な提出期限みたいなのもなんとなくあって時間もなかった。 だからまず雑にアイデアに沿う関数をなんとなくテキトーに書いた。この関数は間違っている。

これを REPL で実行して、間違った関数がどう振る舞うのかを観察する。 その結果を見ながら、どう修正すれば正しく動くのかを考えて手を動かした結果、 わりと短時間で正しい挙動をするプログラムを書くとができた。

で、こんな経験についてわざわざ書いたのは次の3つの理由がある。

• これができるのは REPL が強力かつ動的型付きなおかげなので、Lisp じゃないと苦痛ではないのか？
• みなさん、間違ったプログラムを動かす前に正しいプログラムを導けるんですか？
• 結局のところ、正しいプログラムを書くのに必要なことは間違ったプログラムを書くことなのでは？

ということをなげかけたかっただけである。

もちろん、他の人達と協調してプログラムを書くことが大切みたいな文脈もそれはあると思っていて、 そういうときには最初に設計を共有してそれから外れないようにプログラムを書けることが大切な場合もあるんだろうなとは思う。

でも、本当にそれがプログラミングの仕事をするのに大切なことなのかも疑問に思っている。 いま世の中で必要とされているプログラミングのほとんどは Web 開発だろう。 で、私はこれから Web 開発が始まるという文脈にいるのだが、 Web 開発において究極的に大切なことは DB の設計であってプログラムそのものではないことがもう見えている。 正直なところテーブル設計以外の部分はみなただの雑用のようにしか見えていない。 おそらくテーブル設計の要素を除いてしまえば、今日書いたプログラムよりも高度なことは何もないんじゃないかとすら思えてくる。

そこで、「正しいプログラム」を設計して正しくプログラミングができることにどれだけの価値があるのかまったく分からない。 まあ、私はまだ Web 開発に投入されていないのでそう思っているだけなのかもしれないが。

もしかしたらこの認識は一ヶ月くらいしたら変わるかもしれないが、どうせ変わらないんじゃないかなあと思っている。

というわけで、寝ます。おやすみなさい。

<2022-09-16 Fri>

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

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

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

<2022-09-07 Wed>

<2022-09-03 Sat>

<2022-08-24 Wed>

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

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

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

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

<2022-08-24 Wed>

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

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

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

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

<2022-08-24 Wed>

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

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

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

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

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

<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 に同梱されているやつを使っている)。

<2022-08-22 Mon>

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

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

<2022-08-20 Sat>

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

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

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

<2022-08-19 Fri>

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

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

<2022-08-18 Thu>

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

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

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

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

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

<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

<2022-08-17 Wed>

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

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

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

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

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

<2022-08-17 Wed>

https://ci.tojo.tokyo の Laminar のバージョンはいままで 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

<2022-08-14 Sun>

org-capture の設定を下記のように変更することで記事へのパーマリンクを張れるようにした。

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

これでパーマリンクをどうやったらコピーできるのかが分かりやすくなったと思う。 いままでは目次からクリックしないとパーマリンクを取得できないという残念な仕様だった。

RSS_TITLE は設定しないと RSS 側のタイトルが #add-permalink のような感じになってしまうので設定している(RSS の xml ファイルの生成には ox-rss を使っている)。 二重に書いているのが嫌だがまあ org-capture で二重に書くことを自動化できたのでよしとしよう……(RSS_TITLE の方を修正し忘れる未来がみえる)。

org-mode で [[#custom_id][カスタムID]] のようにリンクを張ると、 Emacs 内でもジャンプできることが分かった。 [[filename.org::#custom_id][別ファイルのヘッダー]] のようにすれば別ファイルでもオーケーだ。 CUSTOM_ID プロパティを設定していれば org-store-link を使ったときに、この #custom_id の形式のリンクが取得できるようだ。 いままで CUSTOM_ID を使用していなかったせいで、 リンクが壊れることがよくあったのでこれからは使っていきたい。 org-capture-template で CUSTOM_ID に日付を自動的にプレフィックスとして付けるようにしておけば CUSTOM_ID の衝突について考える必要はない。

過去の投稿のタイトルにもパーマリンクを張ることを考えたが面倒なのでやめた。

<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 に設定すると表が崩れなくなった。 ただ、フォントサイズを極端に拡大したり縮小したりするとこれでもズレてしまうが滅多にない状況なのでそれは受容することにした。

<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;
    }
}

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

<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

<2022-08-09 Tue>

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

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

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

<2022-08-07 Sun>

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

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

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

<2022-08-05 Fri>

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

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

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

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

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

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

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

<2022-08-04 Thu>

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

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

service networking provided more than once

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

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

<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 の設定などはいつか記事にしてもいいかもしれない。

<2022-08-02 Tue>

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

Japan Export Data — Basel Action Network

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

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

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

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

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

<2022-08-01 Mon>

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

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

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

<2022-08-01 Mon>

使っているのは:

• org-html-themes: GitHub - fniessen/org-html-themes: How to export Org mode files into awesome HTML in 2 minutes
• ox-rss: Org-mode Contributed Packages
• org-mode: Org mode for Emacs

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

あとは 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))

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

<2022-08-01 Mon>

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

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

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

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

<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"

<2022-07-31 Sun>

ブラウザの検索機能で日付を検索してください。

<2022-07-31 Sun>

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

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

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

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

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

<2022-07-31 Sun>

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

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

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

• 検索エンジンに登録されないようにする方法 - レンタルサーバー JSN

<2022-07-31 Sun>

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

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

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

<2022-07-31 Sun>

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

<2022-07-31 Sun>

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

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

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

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

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