WordPress から Hugo への移行のまとめ

WordPressのDBから *.md を拾ってくるのが正解な気もするけど、*.html から、直接 *.md 生成する方針で

で、theme も元の WordPress のを、そのままコピる。

*.md はPerl で find file しながら適当に。変換するファイルを list.txt に入れておく方式です。

ファイルの日付は、*.html に合わせて、それを保存します。

https://github.com/ie-developers/wp-to-md

これで、*/_index.md などができるので、これを content に入れて、hugo を設定すれば良い。

この時に、

　　content/ja content/en

とすると多言語対応が可能。

なのだが、元の WordPress の html file から、css / js を抜き出して、そのまま hugo theme にしまし√た。

抜き出した css / js は static の下。前後を header.html / footer.html で抜き出して layouts/partials に置く。

    ie-hugo-theme
    ├── LICENSE
    ├── README.md
    ├── archetypes
    │   └── default.md
    ├── layouts
    │   ├── 404.html
    │   ├── _default
    │   │   ├── baseof.html
    │   │   ├── list.html
    │   │   ├── section.html
    │   │   ├── single.html
    │   │   ├── staff.html
    │   │   └── top.html
    │   └── partials
    │       ├── footer.html
    │       ├── header.html
    │       ├── ie-jquery.html
    │       └── top-jquery.html
    ├── static
    │   ├── before.css
    │   ├── profile.css
    │   └── top.css
    └── theme.toml

https://github.com/ie-developers/ie-hugo-theme.git

config.toml は以下のような感じです (hugo v0.112.0)

    hasCJKLanguage = true
    baseurl = "https://ie.u-ryukyu.ac.jp/"  # Include trailing slash
    title = "home"
    copyright = "Copyright © 2021-2023"
    # canonifyurls = true
    paginate = 10
    theme = "ie-hugo-theme"
    drafts = false
    enableRobotsTXT = true
    [languages]
      [languages.en]
        title = "Your Website Title in English"
        languageName = "English"
        contentDir = "content/en"
        weight = 1
      [languages.ja]
        title = "Your Website Title in Japanese"
        languageName = "日本語"
        contentDir = "content/ja"
    [params]
      description = "This is a multilingual Hugo site"
      author = "Author Name"
    [[menu.main]]
        identifier = "home"
        name = "Home"
        url = "/"
        weight = 10
    [[menu.main]]
        identifier = "hugo"
        name = "Hugo"
        url = "/"
        weight = 20
    [permalinks]
        section = "/:sections/:title/"
    [frontmatter]
       date                       = [ "date", ":filename", ":default"]
       publishDate                = [ "publishDate", "date"]
       lastmod                    = [ "lastmod", ":fileModTime", "publishDate"]
       expiryDate                 = [ "expiryDate"]

LLVM clang merge

去年、LLVM16 やってた時に

　　merge を間違えた

らしく、ぜんぜん、merge されてない。おかげで、

　　全部手動で merge するはめに

まぁ、おかげで要らないコードをだいぶ減らせた。

Code Segment か普通のCの関数かを区別するために __code という型を入れて、void と同じ扱いにしてるんだけど、

その辺のコードが多い。本当は関数の属性で良いんだが... そうすれば変更は少し減る。

tail call forcing は LLVM でもだいぶ追加されてるんですが、まだ、足りない感じ。

正規言語とPumping Lemma

Pumping Lemma 自体は、Agda でだいぶ昔に証明したんですけどね、

　　0{n}1{n}

つまり、n 個の0とn個の1ってのは、正規言語じゃない、正規表現で書けないってのがなんか難しくって。

カッコの対応なので stack 使えば良いだけだが。授業中に書き始めて、これは難しいとなった記憶がある。

その残骸が残ってたわけですが、それは書き方が悪いな。生成器と検査器を書くんだが、

　　それが並行するように書くんだよ

片方再帰で片方ループとかだめだろ。ってわけでうっかり書き始めて一応書けたんだが複雑すぎる。

0と1の個数が同じってのが x ++ y ++ z と x ++ y ++ y ++ z とで両方成立するからとかやってる。

でも、書き終わったあとに簡単なのを思いつくのはよくある。

　　だから、検査を通るなら、unique に生成器と同じ

ってのを示せば、いろいろ証明しないで、x ++ y ++ z と x ++ y ++ y ++ z とを生成器と一緒に走らせればいいじゃん。

でも、そこそこ面倒で本質的には変わらないらしい。uniquenessを使うのは圏論っぽくっていいかな。

pumpling lemma は Berstein と似てるところもある。この辺の復習は面白い。

君は...

2回目みてきました。

そんなにねたばれがだめな映画ってわけでもないけど、さっさと見た方が。

やっぱり、子供が見にきてしまうんだけど、場違い感はあるかもしれないか。

でも、背伸びして、こういうのを見る子供ってのもいいよね。

最初は構えて見てしまうけど、二回目は落ち着いていろいろ見れるのが良い。

インディージョーンズ

引退する教授という設定ですが、80まで授業するの? 元気だな。

話はマンネリだが、マトリックス4みたいに変なメタなもの入れるよりはいいかも。

Hugo で表

学科の staff の page が表構造になってて。まあ、あとでもいいかと思ったんですが、

　　練習にちょうど良いかな

と思って。ChatGPT に

　　こういうHTML を hugo 出したいんだけど

というと、staff.yml を作って、template で生成できるらしい。なるほど。

<h2>教員</h2>
　　<div class="profile-list">
　{{ range .Site.Data.staff.staff }} <!-- staff.ymlのstaff要素を参照 -->
　　　<div class="profile">
　　　　<div class="profile-img">
　　　　　<img class="aligncenter size-full" src="{{ .image }}" alt="" width="250">
　　　　　<h3>{{ .name }}</h3>
　　　　　<p>{{ .nameKana }}</p>
　　　　</div>

まではいいんだが、その他はいろいろいろでたらめでな。

また、Hugo の Manual page が

　　　絶対に例題は書きません主義

らしくて。まったく、エラーメッセージは出さないは、くそな仕様にはするわで割とひどい。

issei にそういったら astra はどうですかとかいうのが、

　　　今更、また新しいのと格闘するのか?!

いや、この程度は学生はやってくれるはずなんですが、コロナ世代は自分からはまったく動かない感じだなぁ。

でも、ちょっと時間はかかったが、問題なくできました。

来週は学生に、英語のページを全部作ってもらおう。

Hugo を使った Web の多言語対応

といっても、英語と日本語だけですけどね。

　　content/ja/hoge/_index.md
　　content/en/hoge/_index.md

にするだけ。切り替えボタンも付けました。これから増やしていこう。

この辺、昔、WordPress にした時に、一生懸命英語のページを入れた気が。でも。

　　うっかりすると、学生に落とされてしまう

復活できて少しうれしいが、自分のブラウザ側で翻訳することも可能。でも、そこまで手間かけて見るかというとね。

日本の安さみたいなので留学生が来るようになるかも。ならんか。

hugo にした時に即座に対応するべきだったが、なかなかな。

pytorch の続き

pytorch は諦めて、cmakeの debug build したんですが、

　　python3 が debug build な *.so を呼んでくれない

LD_LIBRARY_PATH を無視するって極悪でしょ。どうも、

　　内部で指定しているらしい

sys.path を指定するくらいではだめ。どういうことなの? さすが、

　　くそ Python

ってところですけどね。変なことするなよ。

　　# go into the build folder
　　cd build
　　# compile main.cpp file
　　cmake ..
　　# build it
　　make
　　# run the built file
　　./debugfunc

えぇ、なにそれ。

OBとカレー

この前もOBのハリーズにいったんですが、今日もOBが大学に。

　　知ってる顔がいるうちに来る
　　できれば毎年来る

みたいなのが良い気もします。自分もしばらく寄ってた。大学はそういうコネを作るところだから。

ゼミだと、カレーを取りにいって研究室で食べる感じ。これだと

　　お店を一杯にしたりしない

のが良い。そうそう、

　　学生に見せる自分の紹介用の Web page があると良い

例えば、github とか。notion とか。blog でも。名刺に、そこへの QR code を貼ると良いかな。会社とは別でさ。

昔の研究室でネット使うだけでも良いかな。あぁでも

　　連絡しないで先生と会うのは難しいと思よ

オープンキャンパス

沖国と重なってたのね。バスで通勤ですが、激混み。それにチャーターバスも三台。

ロートルなのに、シス管のプレゼン、シス管のサーバー室、プログラミングIIIと三つ見るのか。

プログラミングIIIは期待してなかったんですが、ポスターとOculus Questのゲームでプレゼンしてくれました。

シス管も、ポスター作ったり、シス管の紹介動画があったり。人が育っていれば楽できます。

去年は山田研の学生にやるよねで詰め寄ってやってもらったような気がするが、今年はお休みか。

ホイメイもご苦労様でした。

時間が5分しかなくて、QRコードはって「ここに動画あるから見てね!」みたいな感じ。

でも、自由時間なものもあって、興味のある人たちとはゆっくり話せました。

オープンキャンパスいましたな学生が説明に廻ったりするのが大学の面白いところですね。

Apple watch の位置

これくらいならキーボード打つのに邪魔にならないかな

ってわけで、外で使うとか論外な感じ

血圧計的な一日一回測定的なものが欲しいかも

BD-RE and macOS ventura

久しぶりに BD-RE の index とろうかと。index だけなら、暗号化されてるわけでもないので。

のだが、なんか認識しない。なので、ドライブがへたったかと思って、Buffalo のを買ってきた。6千円。

で、GPD3 では動いたんですが、前の Logitech のでも読める。お?

macOS ventura に再接続したら、

　　読める

のだが、

　　Spotlight のバカが BD-REに なんか書き込みに

いや、launchctl で止めてるはずなんだが。reboot してSIP入れなおして。

で、25GBの方は Logitech / Buffalo でも認識したりするんですが、BD RE DL は、どっちもうんすん。

Buffalo にいたっては、eject に macOS ventura が panic 。

こまったな。方法は二つか。

　　Windows 10 をVMで動かして、そっちに直接接続する
　　GPD3 に Windows 経由で接続して、Ubuntu 22.04 からアクセスする

んたく、余計な手間を...

一瞬見えたりしたので、driveの問題ではないらしい。OSの問題だな。

VMware Fusionはだめだったが

GPD3では普通に読めた

ただ、Logitechのドライブではだめだった

ってわけでなんとか乗り切れそう

WordPress Hugo 変換はだいたいできた

アイデア的には、WordPress で生成したものを

　　<main id="main" class="post-main-content role="main">

から

　　<div id="wp-browsing-history-title" style="display:none;">

までを切り出して、Markdown に変換。

Hugo で、

　　themes/ie-hugo-theme/layouts/_default/baseof.html
　　<!DOCTYPE html>
　　　　<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
　　<html>
　　　　{{ partial "header.html" . }}
　　<body>
　　　　<div id="content">
　　　　　　{{- block "main" . }}{{- end }}
　　　　</div>
　　　　{{ partial "footer.html" . }}
　　</body>
　　</html>

　　themes/ie-hugo-theme/layouts/_default/section.html
　　{{ define "main" }}
　　　{{ partial "ie-jquery.html" . }}
　　　<div id="content">
　　　　{{ .Content }}
　　　</div>
　　{{ end }}

切り落とした部分を再度前後に付けるだけ。

なんですが、結構難しかった。Browser で分解前と hugo 後のを developper mode の Entities で見比べながらなおしました。

ほぼできたので、一気に移行してしまおうかという気になってます。

いや、この程度、Anatouf と MK なら一瞬だったと思うけどね。今の学生だとちょっと難しいらしい。

https://gitlab.ie.u-ryukyu.ac.jp/ie-syskan/ie-web-md-converter

Hugo 解決篇

Web は時代遅れなんだから、そろそろ新しいの作れよってところですが...

既存の HTML / WordPress を *.md に変換して、Hugo で生成するんですが

　　どうしても変換されないものがある

Hugo 作った人はかなり頭がおかしくて

　　エラーメッセージ一切出さない方針らしい

何が起きてるのかさっぱりわからない。ファイル一つを単体で変換する方法さえもない。変換対象のファイルを表示するのもない。

　　hugo list all

がなにを表示しているのかも意味不明。hugo-extended とかが別 repository であるのも勘弁して欲しいんだよな。

でも、誰がやってくれるわけでもないので午後格闘していたんですが、

　　＊ ＊ ＊ index.md がある directory は、その下の directory は全部無視する

という仕様なのを発見。そして、その work around は、

　　＊ ＊ ＊ index.md ではなく、_index.md にする

ってことらしい。このくそ仕様の肝は、

　　生成ファイルと、そのdirectory ではなく、その上に影響される

ってことね。そんなのわからんし。いや、わかったけど。

結構困るのは、サイト内の link の絶対パスだな。*.md と *.html の位置が異なるので、何を入れれば良いのか不明。

この辺は CMS の方がまともだな。

自分は、おれおれmarkdown を html と同じ場所に置いてるので、あんまり困ってないんですけどね。

ひさしぶりに ingress

学生と一緒に。といっても、Lv8 でなければ、あんまり役に立たないわけですが

ですが、車乗せてもらうのはありがたい

今の時期は、水分とらないとな...

次の日曜日はオープンキャンパスだ。さぼってるとつけが回るパターン。

ちょっと blog さぼり気味

一時期、書かなかったことがあって、少し反省して twtter 的でもいいかと思ってたんですが...

　　まぁ、無理に書いてもな

anthy は、かな漢字変換は「ひらがなから」だけだったりするらしく、agdaの記号を入れるのは断念。

その代わり、nvim に常時入れることに。なんだが、vim には入らない

　　runtime agda-input.vim

ではだめなのか。

　　noremap! <buffer> <LocalLeader>bot ⊥

を手動で入れると動くので、runtime がだめらしい。

Cantor

Bernstein までできたので、Cantor までやるのが礼儀かなと。

S と Power S の Bijection はないってやつですが、

集合論でないのは

　　diagonal : { S : Set } → ¬ Bijection　( S → Bool ) S

と割と普通に対角線論法で証明できてる。

　　_c<_ : ( A B : HOD ) → Set n
　　A c< B = ¬ ( Injection (& B)　(& A) )

で順序を定義してやって、Powers S から S への injection がないこと示せば良い。

　　Cantor1 : ( S : HOD ) → S c< Power S

つまり

　　 f2 : Injection (& (Power S)) (& S)

から矛盾を示せば良いわけですが、

　　 f1 : Injection (& S) (& (Power S))

は簡単に作れる。Sの要素 x を {x} にすれば良い。なので、Bernstein から Bijection を作れる。

　　 b : HODBijection (Power S) S
　　 b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)　

あとは、対角線論法を実行すれば良いわけですが、割と迷走。結論的には

　　 diag : {x : Ordinal} → (sx : odef S x) → Bool

で対角線の要素が部分集合に入っているかを調べて、

　　 Diag : HOD
　　 Diag = record { od = record { def = λ x → odef S x ∧ ((sx : odef S x) → diag sx ≡ false) }
　　　　 ; odmax = & S ; <odmax = odef∧< }

みたいな形で HOD を作れば良いらしい。Diag は Power S の要素なので、S の要素に戻せるわけですが、

　　 odef S n → ¬ (fun→ b (& Diag) diag3 ≡ n)

を示せるので、Sの要素どれとも等しくない。なので矛盾。

なのだが、

　　Berstein の証明の check に 30秒
　　対角線論法 の証明の check に1分

かかる。さらに、Bijection から Injection は容易に導出できるので、Bijection がないとも示せるんですが、

　　Cantor2 : (u : HOD) → ¬ ( HODBijection u (Power u) )

には、50分。どういうことなのかなぁ。Bernstein を切り離すと数秒でいけるんですが。

ただ、切り離すと、少し条件を甘くしても check が通ってしまう。つまり、切り離して証明してもつなげると通らない。

まぁ、一応、通ったから良いんだが、あまりよろしくないな。証明の信頼性に問題があるってことでしょ。

集合論の難しさでもあるな。

macOS text replacement

UIだとひどくて、フリーズとかするわけですが、実は

~/Library/KeyboardServices/TextReplacements.db

に sqlite3 がある。こっちを直接いじれば良いわけね。

my $DBname = "$ENV{'HOME'}/Library/KeyboardServices/TextReplacements.db";
my $mdb = DBI->connect("dbi:SQLite:dbname=$DBname","","") or die("db errr $!\n");

my $sql = $mdb->prepare("
INSERT INTO ZTEXTREPLACEMENTENTRY (Z_PK, Z_ENT, Z_OPT, ZNEEDSSAVETOCLOUD, ZWASDELETED, ZTIMESTAMP,
ZPHRASE, ZSHORTCUT, ZUNIQUENAME, ZREMOTERECORDINFO)
VALUES (NULL, 0, 1, 1, 0, CURRENT_TIMESTAMP, '$abrev', '\\$word', '$unique_name', NULL);
");

で、良いらしい。

Cloud 同期を入れれば、iPhone 側にいくはずですが...

reboot しないと反映されないのは残念だな。

Programming 3 がなんか学生が何も言わないので、最近は、勝手にそんなことしてます。

misskey

学生達が、misskey server をあげてて 学科のアカウントで入れるんですが

　　卒業生どうする

って話が。実は LDAP は総情と同期してるんだが

　　古い学生のも graduate で残してある

この辺の attribute と pam.d の記述でいろいろできるらしい。

アカウントは、なんと 2003 まで遡れるらしい。GMailへの移行が2011なんだが、

　　GMail 側で変更されると、こちらへは伝搬しない

それに、

　　10年前のアカウントのパスワードとか覚えてないだろ

なんですが、既に何人か login に成功してるみたい。ダメな人は、なんらかの方法で連絡してくれればパスワード再発行します。

Tweet Deck っぽいUIだが、微妙にできがよろしくないな。

twitter から拾って misskey に投げるのを書くか? 既にある? twilog とかにそういう機能があると良いが...

あるいは、ブラウザマクロみたいなの。

Bernstein 解決篇

可算版もかなり面白かったんですが、集合の方も割と迷走

二つの injection map

　　f : A → B
　　g : B → A

があるなら bijection があるというやつですが、まず、

　　A \ Img g から始めて、g・ f の閉包を取る

なんだが、ZFっぽくない。普通にやると、recursive record とか文句を言ってくる。

こういう時は、順序数方程式にしてやると良い。HODでやるときの定番だな。

　　　data gfImage :　(x : Ordinal) → Set n where
　　　　　a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage　x
　　　　　next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage.y ix) ) → gfImage　x

リスト構造みたいなものね。

これで、UC が定義てきたので、割と簡単に UC と UCのfの像f(UC)との Bijection 、そして、A \ UC と g⁻¹ の像との Bijection
が得られるわけですが、この場合分けの写像を作ろうとすると全然できない。

　　cca : (A ∋x) → C x ∨ ¬ C x
　　h : (A ∋ x) → cca ax → B
　　h ac (case1 cc) = h1 ac
　　h ac (case2 cc) = h2 ac

とかするんだが、h⁻¹ と組み合わせると、gfImage is not strongly positive とか言ってくる。

要するに、hの後に、さらに C x で場合分けするのが許されないらしい。

で、Aを分割してマーク付けるかとか起き抜けに考えてたんですが...

　　bi-∪　: {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D )　
　　　　　 → HODBijection (A ∪ C) (B ∪ D)

があるのに気がついた。

　 A ≡ UC ∪ A \ UC
　 B ≡ f(UC) ∪ B \ f(UC)

で書いたら、超簡単に。まぁ、そうだよな。h の場合分けは hの構成的な定義によってきまるわけじゃない。

非構成的(排中律)な場合分けだから、h から切り分けられない。そういう直観主義論理から見たら無理がある関数になってる。

可算の場合も、

　ℕ ⇆ A → B → C ⇆ ℕ

Bは

　 Aから指されててCにいる奴
　 指されてない奴

の二つにわかれてるので対応があって面白い。堪能しました。

https://shinji-kono.github.io/zf-in-agda/html/cardinal.html

バスロケ

text 版が使いやすくて良いんだが、次にくる最初を見るには、

　　これを順々にクリックするしかない

三つ前のバス停まで来れば上にでるんですが、それでは歩いて間に合わない...

それ以外は、まぁ、実用です