朝起きたら

なんか、MatterMost につながらない。

　　もちかして、昨日、DBすっ飛ばした影響?!

とか思ったら「シス管ミーティングやってる!」で、入ってみたら

　　総情センタのDNSがおかしい

え。あっそ。じゃ、いいか。じゃなくて

　　「ごめん、DBのrecoveryやってもいい?」

と、今度、M1になる小川が作ってた PostresSQLの backupkから。psql -f でいいの? 本当かよ

で、ばっちりなおりました。でも、KEA-DHCP9は動いてないんだが。といいながら

　　今日はやる気はでず

そんなんでいいのか〜

しまった DB けしちゃったよ

bundle exec rails db:migrate RAILS_ENV=production DATABASE=kea

ってやると、table 消すのか。こまったな

backup は見つかったので、また、明日ね

KEA-DHCP6

AkatsukiのRailのupdateはできたので、KEA-DHCP6の方なんですが、

　Rest APIの reserve DBへのReSTアクセスが動かない

source code installまでやったんだが、ない。どうも、有料らしい。$500。あっそ

買っても良いんだが、直接、DBに書き込むので良いか。ということなら、何か確認するのが欲しいな

といったら、kea-shell があると。ところが、

　こいつも ReST APIで動く

ダメじゃん。まぁ、めくらうちでもいいか。動けばな。PowerDNSは、それでなんとかしたので

ただ KEA-DHCP6 って DB のupdateが結構、頻繁にあるらしい。drop db して create db してとか、やるはめに。どうして?

なので、よくわからないまま、とりあえず Railsのschema 作るか

Graph から CCC

ってのを agda で書くってのをやってるんですが、ぜんぜんできないです
もちろん、Graph から圏は、辺のリストを使えば簡単

ずいぶん昔に、Positive Logicってのを圏だと示すってのはやってて。
その延長でできるだろうってことなんですが

　　id と ○ a が唯一である必要がある

ってところからわかんない

教科書(LambekのIntroruction to Higer order categorical logic)には、
Graph から Deduction System を作って、それから smallest equivalence relation を使ってCCC を作るとか書いてある

Sets がCCCは割と簡単に示せる。(*-cong には関数外延性が必要) 。Deduction System って Sets のことか?

Setsだと、射は関数なので、○ a : a → ⊤ は、tt : ⊤ を返す関数でよい。aが ⊤ なら、id と一緒だ

comonad で A[x] を書くってのはできたが、Functional compleness がなんかおかしい。なので、Graph からCCCを書くという
気になったのだが...

Magsafe でない

iPhone 16e がそうなんだけど、それとは関係なく

　　Magsafeではない非接触充電器

ってのをうっかり買ってしまって。そーっと置くと充電するのだが、すぐにずれる

調子の悪い Thunderbolt ケーブルと差がないんですが

どうりで安いと思ったよ

blogの回数

2005年に原田先生に「mixi書かないんですか」っていわれて、その頃は fj 中心に書いてたんですけど、
移行してみました。2008年には、facebook と平行して書くようになって、2010年に mixi が100MBの制限に
引っかかって停止。それ以降は facebook ですね

blogger の方は2010年からで、それ以前のは mixi のを移行したもの。facebook にbloggerからnoteを使った
自動投稿があって、それが便利だったが、それが禁止になって API 経由にしたんだが、それも2015に廃止。
今は手書きでコピーしてます。ダサい

2017の160ってのはなんなんだ? Ingressにはまってたから? それで反省して、毎日書くようにしてるんだが、
最近はネタがなくてな。でも、なんか書けよ

blogを見直すのは面白いんだからさ

2024 286 ****************************
2023 320 ********************************
2022 328 ********************************
2021 349 **********************************
2020 353 ***********************************
2019 332 *********************************
2018 307 ******************************
2017 160 ****************
2016 191 *******************
2015 249 ************************
2014 285 ****************************
2013 324 ********************************
2012 329 ********************************
2011 355 ***********************************
2009 347 **********************************
2008 444 ********************************************
2007 466 **********************************************
2006 551 *******************************************************
2005 358 ***********************************

休み中は買えない自販機

最近、コカコーラゼロに少しはまってて

でも休日は締め出されて買えません

キースラー 無限小解析の基礎

学生時代にうっかり買ってしまった本ですね。超準解析とかいうかっこいい名前がある

超実数は、実数の可算無限個の集まり
全部同じ実数にすると、実数に一致する
演算は、その要素ごとに行うわけね

0.3… は、0.3,0.33,0.333,… の集まりわけ
1/3は、1/3,1/3,…ね

この差の逆数を取ると、無限に大きな数が集まりに入ってくる。つまり無限大。この差は、その逆数の無限小なわけ

ところが、斎藤先生なにを考えたんだか、この「実数の可算無限個の集まり」の説明を抜いてある

英語の方にはあるのに

まぁ、超実数の存在には選択公理が必要なので、それを除いたのはわかるんだが、理不尽だと思いました

https://people.math.wisc.edu/~hkeisler/foundations.html

Ingress Recursion 5回目

Lv 16になったので。火曜日に合わせたつもりだが、時間短いのか...

まぁ、でも浦添総合公園で Lv6の半分、琉大で Lv7の半分まで

そんなものかな。前回も、なんか中途半端に残したっけ

FD case

なんで、こんなものを持っていたのかは謎。00年代の最初くらいまでは使っていたはず

iBook に切り替えたら、FDは付いてなくて、CDドライブだけだった

OSの課題

全部提出したのが二人。去年も二人だったな

シラバスには「全部出せ」って書いてあるんですけどね

まぁ、でも全部出すのはえらいのか

LLMな時代なので、テストしないとダメ説はあるけど、自分があんまり好きでないので

教科書の課題とかでも、LLMにだめといわれているのに提出してしまうのがいてなぁ

まぁ、来年は、ずっとやさしいはずなので、来年とれば?

まだ、早いひな祭り

浦添総合病院で。24時間心電図も特に問題ないらしく。次の検診は12月っていうことに

たまに動悸はするんだが、CPAPで良くなるとかいう話もあるが、あんまりない気もする

ま、この歳だから、そんなものか

薬が切れたら、いつもの内科ってことらしいです

朝起きて

10時半過ぎだったので、びっくり。で、学校まであるくと ingress 結構取れそう

で、歩いていったんですが、これかよ

いや、まぁ、よくあるミスですけどね

Akatsuki Rails 8.0.1

結局、 ruby 3.2.7 , Rails 8.0.1 まで、あげる羽目に

どうでもいいけど、LDAP ではなくて、Ldap になったのか

まったく、動く気がしないな

Gemfile なおしては、podman build という気の長い話ね

卒研発表

いくつかはみました。去年は、自分の体調も良くなくて結構大変だったが、今年は学生はいないので楽

AI時代の卒研はいろいろ難しいよね

321/322が工事中らしく、221/222でやってたが、階段教室はZoomな時代には使いづらい感じね

Wifiも問題。根性があれば、Aero Hive を移動したんだが。まぁ、来年になれば

桜

まぁ、満開かな〜

紅茶とケーキ

おみやげの定番ですね

ビール1ケースもあったが、ここ半年禁酒中だからな

そして、さんざん、おしゃべり。まぁ、そういう時代の研究室もあったなっていう感じ

ハリーズでのOB会

OBたちが集まって、ハリーズ

結構、リモートで仕事してる人たちが多い

「楽しそうですね〜」とは、ハリーズのネーネーの話

OCさんと金川がいたので、特にそうだったかも

なんか甘いもん

いや、食べないと体重が減っちゃうので...

でも食後にこれは多いな

ラグナガーデンのロビーは、飲み物はおかわりし放題らしい

ラグナガーデンホテル

歯医者のついでに寄ってきました

「なんか会員ってありましたよね」「今年でなくなります。新規は受け付けてません。継続なら可能です」

5万円で5万円の金券がついてきて、プールが半額。3,800円が1,650円に

Ingress始めてから、あまり泳ぎにいかなくなったので、2015年でやめたんだよな

地元住人向けのサービスだったんだけど、あんまり扱いがよろしくなくてな〜

お昼の坦々麺のセットは2,500円に。昔は1500円だった

コンクリートの土台

いや、こんなものだけ作って、上どうするんだろ?

教会の隣だから、駐車場でも作るのかと思ってたんだが

ママの携帯

なんか、どうも

　LINEスタンプ

らしいんだよな。どうして物理スタンプになったのかは聞きそびれました

割と、ロックなママなのでよろしい。たまにいってます