Coq なぁ

自動証明/証明支援、ずっと興味はあったんだけど進捗にかまけて手を出してこなかった

今がチャンスか？

今も実装したいプロジェクトが数個溜まっていてどうしようもない

弊サークルには「線形代数は人生を豊かにする」という格言が伝わっている

This account is not set to public on notestock.

非線形なものについては「非線形の裁き」などというジャーゴンが伝わっています

https://mastodon.cardina1.red/@lo48576/102819858973632048

制御屋さんは大変だなぁ (他人事)

私の専攻では非線形の裁きは滅多にないので (代わりに迂闊なシステムは NP 困難になる)

人生は苦難に満ち溢れている

This account is not set to public on notestock.

This account is not set to public on notestock.

https://mstdn.f72u.net/@a/102819895723149730

それは「分散 SNS の鯖缶」というより「寄合所帯インスタンスの鯖缶」では

その苦労は中央集権サービスの苦労だから分散 SNS の〜という主語で言われても正直説得力が全然ない……

boxed slice と vec が本質的に近いものに見えてきたのでなんとかして統合したいみたいな気持ちがある (`[T]` からの変換さえうまくまとめられればいいんだけど)

[T] から Box<[T]> への unsafe な変換をもう既に人生で n 回くらい書いている (ライブラリ化しているのにそのライブラリを n 回書き直しているの意)

案外簡単に統合できてしまったので終了

先輩 (センパイ)
中輩 (チューハイ)
後輩 (コーハイ)

　　　　　　北京大学
西京大学校　京都大学　東京大学
　　　　　　南京大学

This account is not set to public on notestock.

https://mstdn.jp/@TaiseiMiyahara/102820059523353172

いよいよ麻雀みたいになってきたぞ (適当)

This account is not set to public on notestock.

いつもより3時間以上早く寝られそうだ……

風呂に入って出力手段が断たれてから続々とアイデアが押し寄せてきてオーバーフローして消えていくのやめてほしい、帯域制御してくれ

This account is not set to public on notestock.

This account is not set to public on notestock.

This account is not set to public on notestock.

っ【literate programming】

This account is not set to public on notestock.

少なくともインターフェースについては多分に芸術的要素を含んでいると思う (これは工学的要素の存在を否定するものではない)

退学とD進はペラ紙一枚でできる……？

D進の意思表明 ≠ D進

邪悪なD進煽りよくない

https://twitter.com/monpoke1/status/1174731732832010241

internally defined expression #適当

This account is not set to public on notestock.

This account is not set to public on notestock.

internal definition 、隠語としては悪くなさそう (ほんまか)

「適合係数」よりはわかりやすい (適当)

数学で言うところの「美しさ」と近い概念だと思う

私の尿意棒はヌッと伸ばせるし筋途ウンは重いウンコを空中に持ち上げて運ぶことができる、つまり私の股間は西遊記を体現していると言っても過言ではないということです

崇めなさい

This account is not set to public on notestock.

【速報】児童ポルノ禁止条約運用ガイドラインに案の定創作物規制が盛り込まれる - Togetter
https://togetter.com/li/1405695

"Put me down" #portal

This account is not set to public on notestock.

This account is not set to public on notestock.

研究活動をしている #portal

透明床だし柵がないし落ちたら戻れないので緊張感がある #portal

高いところに行きたいとき、定番の pause glitch をな #portal

どうも不可視の天井があるっぽいな……？これより上に行くのは難しいかもしれない #portal

不可視の天井と上の通路の間に隙間があるっぽいのが気になるな…… #portal

通路というか棒というか…… #portal

portal から床の当たり判定がはみ出しとるやんけw #portal

頭が上に抜けるってことは、どうにかしてこの天井に乗れそうなんだよなぁ…… #portal

いや乗れそうなのは天井じゃなくて棒

諦めて noclip して確かめてみた。棒は一応通路として機能しているっぽいんだけど常時 crouch 状態になってジャンプさえできない状態だったので、 noclip なしでは乗れそうにない。
で、その上の空間は透明なペラい天井ではなく透明な物体でまるまる満たされていそう。 portal が進まない。 #portal

やたら分厚い天井を越えると、次に活動可能な空間は本当に部屋そのものの天井の直下くらいなので、これも侵入は難しそう。
この GLaDOS 部屋の天井が escape 02 で一番高いので。 #portal

しかもこの床も途中で途切れてるな？なんなんだ #portal

別の方角を探っていたら今度は壁まで続いてた…… #portal

一部の壁だけ可視になってるのか、ウケる #portal

This account is not set to public on notestock.

結局あれ webextensions に移植できなかったのかな

今日の研究活動はここまでにしておこう

This account is not set to public on notestock.

Haskell の >>= みたいなのを見ると「カッケー！！！」となるけど、べつに普通の言語を書いててもわかりやすい変化は -> が → になるとか != が ≠ になる程度の恩恵しかないし正直微妙

tonsky/FiraCode: Monospaced font with programming ligatures
https://github.com/tonsky/FiraCode

https://github.com/tonsky/FiraCode/blob/master/showcases/all_ligatures.png

まあ慣れてくれば脳が適応して効率上がるのかもしれないけど……

Support for ligatures · Issue #50 · jwilm/alacritty
https://github.com/jwilm/alacritty/issues/50

alacritty が ligature サポートするまでまだまだかかりそうなので……

This account is not set to public on notestock.

display: none;

セブンのグループが運営してる図書館なのでは (適当)

This account is not set to public on notestock.

大河内 一楼 on Twitter: "2019年（今年だ！）には、劇場も予定してます。みなさま、これからも『プリンセス・プリンシパル』をよろしくお願いします！　https://t.co/rbXRTai3TU" / Twitter
https://twitter.com/ichirou_o/status/1174990570055319552

劇場版の予定あるのか！！！ (声優はどうなるんだろう)

ふと "series of tubes" を思い出した

Series of tubes - Wikipedia
https://en.wikipedia.org/wiki/Series_of_tubes

米国議会にはコメディアンがいっぱいいるらしい。 «albinoalbinism albinoalbinism
https://albinoalbinism.wordpress.com/2006/07/15/%E7%B1%B3%E5%9B%BD%E8%AD%B0%E4%BC%9A%E3%81%AB%E3%81%AF%E3%82%B3%E3%83%A1%E3%83%87%E3%82%A3%E3%82%A2%E3%83%B3%E3%81%8C%E3%81%84%E3%81%A3%E3%81%B1%E3%81%84%E3%81%84%E3%82%8B%E3%82%89%E3%81%97%E3%81%84e/

> Ted Stevensd上院議員 : ｢インターネットにあまり大きなものを放り込んではいけない。ダンプカーじゃないんだ。細い管(Tube)の集まりなんだ。｣

> ｢ポーカーのチップをネットに通すと詰まってポルノやイーベイで買ったものが通らなくなってしまう。これこそオンラインの賭け事が必要となる最大の理由だ。lottery ballを管の中で転がしてネットの詰まりを取り除くのさ。｣

"Well, as we all know, internet is a series of tubes."

声に出して読みたい英語

まあ実際インターネッツは series of (You)Tube みたいなところあるよ (適当)

This account is not set to public on notestock.

下ネタ禁止月間とか作ってみて実験してみたらどうだろう (適当)

弊サークルには新入部員が入ってくる4〜5月あたりに「シリアス系汚い言葉禁止月間」が設定されています

冷静に考えると意味がわからん……

部内 wiki にちゃんと解説があって :naruhodo_naru: :naruhodo_hodo: になった

This account is not set to public on notestock.

存在禁止月間 (SNS 断食)

インターネットに遍在しような (適当)

適当発言禁止月間したら存在消えそうなので絶対適当発言しような (?)

This account is not set to public on notestock.

キャラクターやアバター関係、そもそも 3D 界隈の著作権やライセンスﾔﾊﾞﾔﾊﾞなのに加えて著作者人格権に絡む諸々の問題なども悪魔合体してトラブルの宝庫になりそうという感想しかないので、こわすぎて自分で生命を冒涜した方がまだマシそうという気持ちがある

あとアバター生成器の出力にまで特殊なライセンスが及ぶというのもなかなか険しい気持ちになってしまう (これをどう正当化できるのかまだ自分の中で納得できていない)

まあ正当化もなにも EULA が強烈というだけの話なんだけどさ……

This account is not set to public on notestock.

実態として既存リソースのパックに過ぎないためその組み合わせにも元素材同様のライセンスが及ぶ……みたいな解釈はまあできる

美少女生成アルゴリズムを自由ソフトウェアとして公開して市場に火を放ちてえな…… (言うだけ)

リアル系の人体モデル生成であれば MakeHuman という自由ソフトウェアが存在する

http://www.makehumancommunity.org/

ニコラス形而

ライセンスで許されてるんだから何しようがフリーライドしようが勝手みたいな意見、まったくもって正論だけど、中学高校の社会科の授業を理解できなかったせいで CSR とかメセナみたいな現代的な概念を知らずに育ったんだろうなと思うと悲しくてな

現代 (ここ数十年)

This account is not set to public on notestock.

medium はゴミすぎて是非とも廃れてほしいし、 note.mu は同じ轍を踏まないよう頑張ってほしい

This account is not set to public on notestock.

ライセンスが不透明っぽくてこわい (わがまま)

ともあれ初めて知ったので㍂という感じだ

まあそもそも FBX SDK 自体が不自由なライセンスなので、もしそれをバンドルしていたら当然ソフトウェア自体も不自由な可能性は十分高い

FBX やめて glTF を使おうな……

Hitogata
https://sites.google.com/site/vhitogata/

ダウンロードしてライセンス確認したけど普通に不自由なライセンスだったので終了

あと以下の『禁止事項』が気になる:

> ・当ソフトウェアにより生成されたモデルをそのまま、もしくは一部改造した状態で販売すること

> 当ソフトウェアを利用して作成されたモデル・モーション・動画については、商用・非商用問わず制限なく利用することが可能です。

直前に書いてあるこれと矛盾してない？

書いてる人は「利用」を「VTuber として動画などを作成して公開する」くらいのつもりなのかもしれないけど、普通に考えておかしいでしょ

これだからオレオレライセンスは怖いんですよ

同梱されていた FbxLib が開発者によるものらしいので FBX SDK のライセンス制約を受ける心配はなさそう？ (中身が不明なのでわからんけど)

strings で中身覗いてみたら普通に fbxsdk::FbxString とか多数あるし不穏すぎるな

やめやめ、どうせ私は絶対使わない

This account is not set to public on notestock.

ですよねぇ…… (そうして FBX を自力で読んで大変苦労した)

ぐぬぬ

std::borrow::Borrow<U> の自動実装を試みたところ impl<T> std::borrow::Borrow<T> for T と競合した……

もしかしてこのアプローチってあまり筋が良くない……

From / Into あたりでも同様の問題が発生する予感があるぞ

こまった

This account is not set to public on notestock.

This account is not set to public on notestock.

バイナリのみ制約をゆるめる……まあ公式の開発者が自分用に派生物や複製に対して例外的なライセンスを付与することは可能……なるほどなぁ

アルゴリズム実装者とは別人によって著作者人格権が及びうる 3D モデル生成器の成果物については copyleft がデフォルトであるべきではないというのが個人的な感想

というのも、 copyleft にすると生成されたモデルに人格を紐付ける利用を阻害する要因になるので、あまりよろしいものに思えないため

生成アルゴリズムの方が自由ならばそれで十分でしょうという感想

https://github.com/animate1978/MB-Lab/blob/2c25a2803985467f420472c0f300c4449bf9a8cc/license.txt#L41-L66

AGPL-3 が原則で、 "official software" (公式に配布されているもの？) による生成物は CC-BY 4.0 が選べるらしい

> The AGPL can be an obstacle in case someone wants to create a closed source game or closed source 3D models using 3D characters made with the lab because the AGPL will propagate from the base models and from the database to the output models.

あたりまえすぎる

This account is not set to public on notestock.

This account is not set to public on notestock.

オープンソース開発者にもっとお金が廻るようになれば社会はもっと良くなるという話 - orangeitems’s diary
https://www.orangeitems.com/entry/2019/09/19/104723

This account is not set to public on notestock.