未来からのホットライン

JPホーガンの昔の作品。なんか、なくしてしまってさ。Kindle で買いなおしてもらいました

スコットランドで核融合炉作ってたり、大西洋トンネル掘るとかいってたり

　　バラ色の科学技術的未来な話

なんだが、それが200万個のマイクロブラックホールばらまいたり、宇宙から人工ウイルスばらまいたり。それがスコットランドのご近所で起きる

色恋ばなしとからんでたりで、結構楽しい。もちろん、タイムマシンの話は眉唾なわけだけど

　　眉唾と分かってても楽しい

そういう話ね。あの頃のミニコン話でもある

https://amzn.asia/d/aTK6Qo8

喜屋武盛基先生告別式

近所なので、いってきたんですが、意外に人が少ない?

とかいってさっさと、てだこ浦西駅にいったら、そこで、こまきさんとばったり

みんな心配してるんだから、facebook になんかかいてよとは思うが、

＊　杖はついてますが元気そうでした

おもろまちまでゆっくり話せて良かった

ともだちが見にきて「ぜったいおかしい」で病院にいったらしいが、そこから2ヶ月は覚えてないらしい

で、聞いたのが

＊　2:15くらいから人がたくさん来たみたい

え、それなら、もう少しうだうだしているべきだったか。まあ、別にいいか。あんまり、そういうの好きじゃないし

その後、おもろまちのスタバで、タンブラーのふたをふっとばして、そこのお姉さんたちに探してもらった事件があったが、まぁ、それもいいかな

Google Photos

大学の使えば無制限なんだが、なぜか自分のにあげてて、最近、「いっぱいだ」とうるさい

2016あたりに重複( JPG と HEIC )が常にあるので、それを消してごまかしてたんだが

　そういうのと関係なくいっぱいだといってる

らしい。まぁ、無料でずーっと使いつづけるのもあれかなとおもったので100GB課金しました

いや、写真だけでも202GBあるので、計算おかしいんだよな

まぁ、いいか。気にしなくて

ただ、これらは、結局は消えてしまうんだろう。デジタル時代になって、むしろ残らなくなる

まあ、それも面白いかな

今日は劇寒

なんだが、16度。風速8mで、体感は10度。超ミニスカのお姉さんが寒そうだ

おもろまちで16:30にバスに乗って、真栄原に19:10ってなんだよ。いったいなんなの?

バスに乗る人も「なんかあったんですか?」とか聞くんですが「混んでただけです」

まぁ、年末だからな

CC さくら

なんとなく見ようと思ってたものの一つ

iPhone 13に Lightnening HDMI をつけてなんですが

　微妙に面白くない

まぁ、当時なら面白かった? でもないか。クロウカード編だけでいいかな

観てないガンダムも結構ある。00、レコンギスタ、鉄華団

プチエトワール

今年もいってきました。嘉数のフレンチ

今年は特にステーキがうまかった。ローストだが「オーブンから出したり入れたり繰り返す」みたいな話

まぁ、毎年いってるわけだけど、そういうのがよい

今年はお昼を値上げした。土曜日は5千円、平日は3,800円。なのでお客さんが減って大変だったとか

まぁ、月一はいくべきかなぁ

トラップ

美浜のスタバで見かけました。いまどき、そんなもの使うのか?

いったい、何に対して?

まぁ、ねずみなんだろうけど...

ローズガーデン

もともと、沖縄市にいく330の途中にあったんですが、経塚のサンエーの裏に移転

なんか、見つけたんですが、そんなに便利なわけでもない

なんだが、ハーリズがお休みだったので「いくか!」

前田から歩いて20分。まぁ、車ならすぐなんだけどね。


まぁ、サムズのお仲間みたいなものなんだよな。なんだけど、

　　昔のBSE騒ぎでだいぶ質が落ちて、そのまま

な感じ。でも、

　　煮詰まった玉ねぎのスープ

は、「高級ホテルのスープです」といわれれば、そんな気もするようなものでした。ジャッキーとかの死んだコーンスープよりはよい

ステーキは、サーロインステーキNYカットで3千円。まぁ、値段相当か

最近、ライカムのなべしま、浦添パルコの叙々苑、そして、城間の四季の評価が高い。それに比べると、ちょっといまいちかな

ただ、量は結構あった

Ingress +Beta Shard Storm

なんか、そういうイベントで、きらきらビーチにいってきました

少し前に「Shard くるからいかない?」なんだが

　Telegram で、なんか位置のアプリがあって.. ?!

という感じで「まったくルールがわからないまま」現地に(いつものことだが)

　なんか、指令がくるから言う通りにやってればいい

前日に「キー受け取りに失敗」なんても。Telegram に通話機能があるとかしらんし

でも、さきのりや、園長、ぷにちゃんとか頑張ってて、現地は免疫、真っ青+ガードリンク

ちゃんと緑の人も来てくれて、30分守りきって終わり〜 シャードは勝連の園長のところへ

ポイントは最初のジャンプだけらしく。それで終わり。お疲れ様でした

MR ゆいれーる

なんか、そんなのを見つけてきた人が

　てだこ浦西から、空港まで

巨大ディスプレイ付き車両でいくらしい

いや、まぁ、まるで昔の LaserDisk Shooting みたいな。いや、なんか期待したわけではないんだが

ソニーの提供とかいってたが、ディスプレイって、もう作ってないんじゃないかな

そこそこ大きい。80inch くらい? 後ろが透けて見えるんだが、かなり綺麗だ

窓枠がないのはきれい

まぁ、そこになにを映すかは、沖縄のだめさがでるわけだけど

違うところの映像を出されると酔う

別に普通の短篇映画でいいんじゃないのと思わなくもなかったかな

Okica の半額モニタ

きました。まぁ、いいんだけど

　今使ってる Okica の番号

で、十分なはずだろ? 終わったら送り返せだのうるさい

果てしなきスカーレット

これは、名作じゃないですか? まぁ、嫌いな人もいると思うけど、それは

　心が汚れてるから

だろ? アベンジャーとかハリウッド系の残念な話に比べて、ぜんぜんいいじゃんん

デンマークとか王国とかの話も、まったく関係ない。最初のシーンで、あ、これは

　死んでからの話だと、はっきりわかる

昔のNHKの木星行きのロケットの中で目覚める話とか、コニーウィリスの航路とか、そういうジャンルの話なわけね

　スカーレットが強くて綺麗で可愛くて、いじめられる
　そして、目覚める

まぁ、あのお兄ちゃんどうなのとは思わなくもないけど。なんで日本人なんだよ

まあ、あんな能天気なのは、もはや日本人にしかいないような気もする

さいきん、ほうせんか観たので、「あれよりはぜんぜんいい」いや、あれだって、そこそこ面白かった

そういえば、あれも、なんか良いように見えなくもない男の話だった

https://scarlet-movie.jp/

lightening

ライカムのNewcommにいったら、Lightening / HDMI のケーブルが1980円なので、レジに持っていったら

　7980円です

はぁ? それならいらないです。Amazon で1980円で売ってるのに、なんで、そんな値段で買うのか

で、そのままコジマにいって、おっちゃんに聞いたら「Lightening cable はうちではもう扱ってない。Amazon で買え」

というわけで、プライムな奥様にお願いすることに

Apple TVがめねおけば良かったんだよな

VLC使ってみてもよいんだが

なんか、不便な世界だよな

NASと録画

まぁ、別にいいんだが、昔のまだ見てない録画が NAS に

　CCさくら、Gundam 00、レコンギスタ

くらいなんだが。ところが

　PS3/PS4 では観れなくなった
　NAS上のDLNAサーバはいまいち

まぁ、商売上の理由なんだろうけどね。アマプラでは有料

録画したBD出せば観れるんだが、せっかくNASに入っているのにね

でも、CIFS経由なら見る方法はいくらでもある。でもPCつなくの?

　MP4にencodeしなおせばPS3/PS4で観れる

いや、やらんだろ? 昔ならやったかも

Lightening cable / HDMI 変換で見る、Apple TV経由で見るとか

なんだかね〜 まぁ、Lightneng cable / HDMI は2千円しないから…

Lean 4

Agda と同じ定理証明系なんですが、少し触ってみようかと

VSCode で入れるらしいが、入るけど

　　なに入力すればいいの?

まぁ、ChatGTPに聞けばいいか。#eval 1 + 2 とかするらしい

import First.Basic

#eval 1 + 2

def square (x : Nat) : Nat :=
x * x

#eval square 4

theorem hello1 : 1 + 1 = 2 := by
decide


コマンドラインからできるんだろと思ったが、なんか、動かない

+leo+kono ~/.elan/bin/lean First.lean
First.lean:3:0: error: unknown module prefix 'First'
No directory 'First' or file 'First.olean' in the search path entries:


build は動く

+leo+kono ~/.elan/bin/lake build -v First.lean
ℹ [2/3] Replayed First.Basic
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First/Basic.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.setup.json --json
ℹ [3/3] Replayed First
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First.setup.json --json
info: First.lean:5:0: 3
info: First.lean:10:0: 16
Build completed successfully (3 jobs).

なんか、結構、えげつない呼び出しだな

まぁ、動いたみたい。

一旦、C に変換するの? 微妙だな

agda みたいに「全部、Haskell でがんばる」ってのがいいかどうかは、また別だけどね

Restrant Lily

沢岻の少し奥にあるレストラン

経塚のサンエーから、あるいて330までいく途中で見かけました

行ってみたい気もする

崖崩れする前にいった方がよいか?

歯医者

なんか、詰め物がとれてしまって。といっても、11/20くらいでさ

「年末で混んでて」で、今頃に。来週には予約してたのに

まぁ、そこまで延ばすのも良くない。でも、いったら

　「2年前にも取れてる。少し強力な接着剤使うか」

う、うーん、ま、まぁ、そんなものかな?

まぁ、すぐに終わりました