プラウダ

モスクワの報道は三つのカテゴリーにわかれている。すなわち「真実」「たぶん真実」及び「真実性のないもの」の三つである。 第一のカテゴリーには時報、第二のカテゴリーには天気予報、そして第三のカテゴリーには他の全てが含まれている。 ――アネクドート

最近の記事

• idris を始めた話

  2025-04-12

  最近は LLM とアイディアを色々壁打ちするのが日課になっている。そのことはまた話すとしてその中で出てきたのが **Idris2 の DSL で記述された型安全な CAD** といういかついアイディアである。 千里の道も一歩から、偉大なプロジェクトも環境構築からである。そんなわけで Idris2 の環境構築の仕方を記しておく。 ## 前提条件 - Linux(Ubuntu 22.04) - Emacs 29 ## pack を導入する [pack](https://github.com/stefan-hoeck/idris2-pack) は Idris2 のパッケージ管理ツールだ。 [インストールガイド](https://github.com/stefan-hoeck/idris2-pack/blob/main/INSTALL.md)を見ればインストールできる。 Chezscheme が必要なので `apt` で入手しておこう。 ```console sudo apt install chezscheme ``` 入手したあとはインストールガイドのスクリプトを実行すれば良い。結構長いので待つべし。 pack は Haskell で言うところの ghcup + cabal, Rust で言うところの rustup + cargo のようなものでこれを入れれば Idris2 本体も入ってしまう。 `~/.pack/bin` と `~/.idris2/bin` 以下に入るのでそれぞれパスを通しておこう。 ```bash export PATH="$HOME/.pack/bin:$HOME/.idris2/bin:$PATH" ``` `idris2`, `pack` で実行できたら成功だ。 ```console planaktia on  main took 2s ❯ idris2 ____ __ _ ___ / _/___/ /____(_)____ |__ \ / // __ / ___/ / ___/ __/ / Version 0.7.0-6c6ee58eb _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org /___/\__,_/_/ /_/____/ /____/ Type :? for help Welcome to Idris 2. Enjoy yourself! Main> Bye for now! planaktia on  main took 2s ❯ pack Usage: pack [options] <cmd> [<args>] Options: ... ``` ## プロジェクトを開始する プロジェクトを作るには `pack new` を実行すればいい。プロジェクトに必要なソースコード生成と git の初期化をしてくれる。 ```console pack new bin hello ``` `bin` を選ぶと `.ipkg` というパッケージの設定ファイルに `executable` が設定され `pack run` で実行できる。 ```console test on  master [?] ❯ pack run Hello from Idris2! ``` これでプロジェクトの設定は終わりである。ちなみに `bin` の代わりに `lib` を選ぶとライブラリ用の設定になる。が、大して変わらないのであとから手作業で直しても大丈夫だ。 ## Emacs の設定 エディタには Emacs を利用した。VS Code は拡張の対応が微妙らしい。とりあえず Emacs はインストールしてあるとする。 LSP 自体は pack でインストールすることができる。 ```console pack install-app idris2-lsp ``` バージョンが出れば精巧である。 ```console test on  master [?] ❯ idris2-lsp --version Idris2 LSP: 0.1.0-2736cd1a8 Idris2 API: 0.7.0-6c6ee58eb ``` 続いて Emacs 自体の設定に映る。正直めんどくさかったので `init.el` は LLM に生成させた。`lsp-mode` が必要だがすでに入っているかもしれない。ない場合は以下のようにしておく。 ```elisp (use-package lsp-mode :ensure t :commands lsp :hook ((prog-mode . lsp)) :custom (lsp-completion-provider :capf) (read-process-output-max (* 1024 1024)) (lsp-idle-delay 0.1) (lsp-headerline-breadcrumb-enable t) (lsp-modeline-diagnostics-enable t) (lsp-modeline-code-actions-enable t) :init (setq lsp-keymap-prefix "C-c l")) (use-package lsp-ui :ensure t :commands lsp-ui-mode :hook (lsp-mode . lsp-ui-mode) :init (setq lsp-ui-doc-enable t)) ;; ← sideline 系の設定は不要 or 別方式に変更 ``` `use-package` を使っているがこれは個々人好みとかあると思うのでよしなにしてほしい。初めてでめんどくさければ LLM に全投げじゃ。 あと GUI から起動すると LSP のパスをうまく見つけられなかったりするので以下を入れておく。 ```elisp (use-package exec-path-from-shell :ensure t :config (exec-path-from-shell-initialize)) ``` これで先程作ったプロジェクトの `src/Main.idr` を開けばソースコードがハイライトされているはずだ。C-c C-z を押すと REPL が起動し下のような画面になる。 <img src="https://res.cloudinary.com/pravda/image/upload/v1744454879/20250412-idris.png" alt="Idris REPL を起動した Emacs" width=500 /> 使い方はまだ自分が慣れていないので慣れた頃にまとめるかもしれない。

• 麻婆豆腐の心得

  2025-04-01

  麻婆豆腐を作った。 <img src="https://res.cloudinary.com/pravda/image/upload/v1743511010/20250401-mabo.jpg" alt="作った麻婆豆腐" width="400" /> （画像は七面倒くさかったので素の `img` タグである） [このレシピ](https://mi-journey.jp/foodie/24954/)を参考にアレンジして、いやところどころ手を抜いて作った。 美味しいことは美味しかった。お肉たっぷりで――これがダメだったのだ。麻婆豆腐は豆腐が主役である。肉はあくまで引き立て役。 豆腐のためにあらねばならないのだ。肉が多ければ満足感は増す。しかし、肉に負けて豆腐は添え物になる。それではいけない。 今回は小さめの豆腐半丁に対し豚ひき肉を 150 g も入れてしまった。せめて豆腐を 1 丁丸々入れるべきであった。 また、基本的にひき肉は脂が多い。肉が多ければ脂も多くなりたいへんくどくなってしまう。今回の麻婆豆腐は豆腐が脂に浮かんでしまっていた。 色々と反省点はあるがお酒のアテとしては最高この上ないものであった。自炊による豊かな食事は心に効く。 せっかくなので他にも注意点をまとめておこう。 - ひき肉は入れすぎてはいけない - ネギはみじん切りと小口切りを用意しみじん切りは最初に炒め小口切りは最後に入れる - 必要以上に香味野菜と肉を炒めない - 鶏ガラスープは多めに入れても構わない、というか豆腐を煮れるように入れるべきだ - 水のいらない片栗粉では力不足なのでしっかり水溶き片栗粉を作る 私とみなさんに良い麻婆豆腐ライフがあらんことを。

• 2025 年 03 月 30 日: 競馬の反省

  2025-03-30

  今まで漫然と馬券を買い外れてはアーという顔をしていたのがこのままではお金がなくなり感情までアーとなりそうなのでそうならないためにも予想の精度を上げていきたい。 手始めに予想の言語化とその反省をすることから始めたいと思う。[Consense に放置してあるプロジェクト](https://scrapbox.io/kirisaki-uma/)を使っても良かったが、 記事としてまとめたほうが良いのかもしれないと思いブログに書いてみることにした。 なお全レースこれをやるのは無理なので狙いを定めたレースとか覚えてるレースだけで行こうと思う。 ## 阪神 4 R 障害未勝利 ### 予想 - ◎ 12 アメリカンピース - ◯ 6 テイエムマジック - ▲ 1 ザスリーサーティ - △ 2 コンクエスト - △ 3 テーオーリカード ### 馬券 <dl> <dt>3 連単フォーメーション</dt> <dd>6, 12 - 1, 2, 3, 6, 12 - 1, 2, 3, 6, 12</dd> </dl> ### 結果 1. 1 ザスリーサーティ 2. 6 テイエムマジック 3. 3 テーオーリカード ### 反省 テーオーリカード入れたのはめちゃくちゃ好プレイ。ザスリーサーティも。しかし 1 着に来るとは思ってなかったよ。 たしかに遡って見てみると阪神の障害で好走してるし近走もそんな悪くないから全然 1 着目に入れてよかったんだな。 障害初のテーオーリカード入れてたのは平地で良さげなときに netkeiba の印つけてたからですね。 このレースで 8 万円を逃したのが痛すぎる。でも買い目増やしたとしても 1 着目はテーオーリカード増やしてたんとちゃうかな……。 ## 中山 10 R 船橋ステークス ### 予想 - ◎ 8 オメガキャプテン - ◯ 5 レオテミス - ▲ 13 ランドオブラヴ - △ 6 エコロレジーナ - △ 9 トーアアイギス ### 馬券 <dl> <dt>ワイドながし</dt> <dd>8 - 5, 6, 9, 13</dd> <dl>3 連単 2 頭軸ながしマルチ</dl> <dd>8 - 5 - 6, 9, 13</dd> </dl> ### 結果 1. ジョーメッドウィン 2. イサチルシーサイド 3. オメガキャプテン ### 反省 相手選びの失敗。ジョーメッドウィンの前走をもっと評価すべきだった。 あと他の相手はオッズ的に夢見すぎたかな……とはいえイサチルシーサイドは選べてよかったやろって思う。 見返したらステークホルダーといい勝負しててこのオッズとか買いだった。 ## 中京 11 R 高松宮記念 ### 予想 - ◎ 10 サトノレーヴ - ◯ 14 ナムラクレア - ▲ 15 ママコチャ - △ 13 エイシンフェンサー - △ 3 ビッグシーザー - △ 18 ペアポルックス - ☆ 2 ウイングレイテスト ### 馬券 <dl> <dt>3 連複フォーメーション</dt> <dd>10, 14, 15 - 2, 3, 10, 13, 14, 15, 18 - 2, 3, 10, 13, 14, 15, 18</dd> </dl> ### 結果 1. 10 サトノレーヴ 2. 14 ナムラクレア 3. 15 ママコチャ ### 反省 予想は完璧だったが馬券がガミ。余計な穴を入れすぎたのが敗因。 ナムラクレアとサトノレーヴで勝ち負けするだろうとかマッドクールは内枠すぎ、ルガルの 2 連覇は難しい、穴を開けるならママコチャというところまであっていたというのに。 余計な欲を出して点数増えてこのざまである。いやでも私はウイングレイテストに夢を見たかった。 馬券はガミだが予想としては完璧だったのでその点は満足である。 ## 中京 12 R 鈴鹿特別 ### 予想 - ◎ 9 ミッドナイトラスタ - ◯ 8 キングクー - ▲ 2 クレイヴィンオナー - △ 12 ニシノスピカ - △ 13 レッドフランカー ### 馬券 <dl> <dt>ワイド</dt> <dd>8 - 12</dd> <dd>9 - 12</dd> <dd>8 - 9</dd> <dl>3 連単 2 頭軸ながしマルチ</dt> <dd>9 - 8 - 2, 13</dd> <dd>9 - 12 - 2, 13</dd> <dd>9 - 8 - 12</dd> </dl> ### 結果 1. 6 セミマル 2. 11 ルージュスタニング 3. ニシノスピカ ### 反省 「セミマルは中京苦手な気がするから切り(ｷﾘｯ」とか言ったら普通に来ちゃった。鞍上モレイラだったし入れておくべきだったよなあと。 2 着も人気順だったのでこの買い方は多分できないな……。ニシノスピカ 3 着は頑張ったと思います。ちゃんと適正見抜けた気がする。 キングクーも実は 4 着で着差も悪くなかったけど上 2 頭が強すぎたなって印象。そのあたりは救いですね。 ## 戦績 - 予算 40,000 円 - 購入 47,100 円 - 払戻 22,780 円 - 差引 -22,780 円 - 回収率 43.2 %

• ブログを始めてみた

  2025-03-28

  ブログを始めてみた。[以前はてなブログにも作っていた](https://kirisaki.hateblo.jp/)がまた使い始めるには使い勝手がよろしくないので自前で用意した。 と言っても Astro で作って Netlify にぺろっとデプロイしただけ。カスタマイズ性はもちろん抜群だし記事更新も GitHub に push すればいい。便利な世の中になった。 HTML を FTP で送ったり Perl 製の日記 CGI を設置したりといった苦労は――やめよっか、この話。 このブログは技術的なことを書いていくつもりではあるが、それにとどまらない散文的なものも書いていこうかなと思う。 ちょっとカッコつけすぎて恥ずかしくなっちゃうかもしれない。自分が後々恥ずかしがる分にはいいのだ。それは自分の書いた文が稚拙だと思えるようになった、すなわち成長の証なのだから。 技術記事でも同じことが言えるように切磋琢磨していきたいと思う所存である。 他人が恥ずかしがる分はどうするか？知るか。 始めるにあたってできるだけプリミティブに……と思ったのだが結構体裁整えてしまった。悪い癖である。 そうは言ってもタグ画面とかリスト置きっぱなしだし脚注のスタイリングとか共有ボタンみたいなのも全然できてないんだけどね。 やることが意外とあるのだった。 週 1 は更新していきたい、などとのたまうとすぐに更新しなくなってしまうのでだらだら行きたいと思う。だらだら行ってももちろん、更新しなくなる。定めである。