Notepad++、「フリーウイグル版」と称したバージョンをリリース | スラド オープンソース
https://opensource.srad.jp/story/19/11/05/176202/
らりお・ザ・何らかの🈗然㊌ソムリエ(@lo48576@mastodon.cardina1.red)の投稿
Notepad++、「フリーウイグル版」と称したバージョンをリリース | スラド オープンソース
https://opensource.srad.jp/story/19/11/05/176202/
Coq/SSReflect/MathComp Tutorial
https://staff.aist.go.jp/reynald.affeldt/ssrcoq/
@squid999 とりあえず一つのサーバーに大人数収容するのはやめたほうがいいということだけはわかりました
なるべく小規模で分散して生息したほうがサーバー資源的にも効率が良くなる
これはLTLだけの計算量ですが、
Fediに10人いたとして一か所に10人いると
計算量が10^2 =100になるけど、
3・3・4で分散してれば
3^2+3^2+4^2=9+9+16=34になる
全員おひとり様なら1*10=10になる
そもそも分散した鯖缶にとって他人の鯖の自重なんて興味の対象外だし、自分用のサーバのローカルな負荷と通信が軽減されていれば十分
の投稿
prime@mstdn.poyo.me
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
分散のメリット、鯖の負荷だけでなく故障の局所化などもある (これは jp 見てれば誰でも気付くが)
ネットワークコストもクラウド使ってたらちゃんと数字で出てくるからわかると思うんだけど比較するとまだ安く上がるよね
の投稿
prime@mstdn.poyo.meこのアカウントは、notestockで公開設定になっていません。
LTL 廃止は数年前からずっと言ってるんだけど賛同者が極めて少ない
このアカウントは、notestockで公開設定になっていません。
https://pao.moe/@stackfield/103097603905651427
ActivityPub は HTTP の上に乗っているからこそこれだけ楽に実装できているわけで、 P2P でやろうとすると転送プロトコルから作り直すことになるけどそれでいいの？
実際それをやってもオレオレ規格になってしまうし他の似たようなプロトコルとの互換性を与えるコストが高すぎるので、単体で見れば理想的でも実際には使われないってワケ
あきょぜ（4.3.0a)の投稿
akyoz@plustodon.net
このアカウントは、notestockで公開設定になっていません。
私としてはいわゆるブロックチェーンには賛同したいんだけど、実際のところ「データベース膨れすぎたのでお掃除したい」とか言っちゃう人々が、一部でもデータを消すと妥当性が失われてしまうような「チェーン」を使いたがるんか？ほんまか？？？と思っているよ
実際、「TL に流れてきたデータを失いたくない (後から任意のタイミングで参照できるようにするため)」という思想を持っている人はごくごく一部だと踏んでいて、何故かというとそういう思想の人は「削除が飛んできたら DB から投稿を消そう」とか考えないだろうから。
「やっぱあれ消して」と言われて非公開にするでなく DB から抹消してしまうような雑な扱いをしといて、あるいは DB お掃除したら死んでるアカウントの投稿がまとめて消えるような実装を受け入れておいて、ブロックチェーンに共感しているという言葉にはあまりに説得力がないと感じてしまう
人々、 TL の再現性とか保存に極めて無関心であるらしいということがここ数年の観察で判明している
検証できないブロックチェーン、そもそもブロックチェーンである必要なさそう (単なる配列じゃん)
単に前の文脈とかを参照したいという話であれば ID でリンク付けてやればいいだけで、それこそ IRI の概念はトランスポート層非依存なんだから P2P なり何なりに適した schema を用意してやればチェーンにしなくても単なる IRI 保持によるリンクで十分そう
Matrix.org が (ブロックチェーンではないと思うけど) 「投稿より前の leaf 全部へリンクすることで DAG を作って投稿の前後関係を表現する」みたいなことをやっていた気がする (ちゃんと規格読んでないけど)
バックエンドは削除できないがフロントは隠す、みたいなのはできるかもしれない（よく知らんので適当に言ってる
私はずっとそうすべきだと思っているんですけどね (削除は非公開であって抹消にすべきでない)
https://twitter.com/aka_ringo/status/948186501476528128
これ関係の話でいろいろ思うところがある
OStatus / ActivityPub については「鯖が死んだ」という状況では他のインスタンスに一度配信された投稿は勝手に削除されたりしないわけだけど、その投稿を RT するのが無事成功するかはわからない(プロトコル調べてないけど、発信ソースへの verify が飛ぶ気がする)し、ユーザ削除があると結局投稿は根刮ぎ消されてしまう
あと、投稿の削除ができると RT を交じえての意見とかが穴開きになりうるし、そうなると一連の投稿を以てひとつの話題になっていたとき、話題の内容を維持することができなくなる
なので、個人的には投稿の削除は論理削除であってほしくて、もし本当にコンテントを抹消するのであっても、「削除された」というプレースホルダを残しておいてほしいんですよね
もちろんプライバシとか諸々の問題を考えると、削除フラグだけ立てて投稿のコンテントの抹消を禁止する実装というのはいろいろ問題が多いわけですが、今のようにサイレントに投稿が消えるというのは素敵とは言い難いし、発信者の鯖が死んだ後でも受信者側がコストを払って情報を保持していく手段が与えられていてほしい
情報の受信者の権利も重視して尊重したいところなんだけど、投稿削除機能を無力化させろとかいう主張、プライバシー情報を投稿しては削除する人々とか炎上したくない人々には絶対受け入れられないだろうし、原理主義者も程々にしておかねば……
や、べつに削除が飛んできた投稿について FTL とか LTL に表示しなくなるというのは妥当かもしれないですが、「私が見たものを私のために覚えておく権利」って確保されるべきじゃないですか。そう考えると、お一人様インスタンスで他鯖の削除が飛んできて私の HTL の投稿が消えて見られなくなるの、ちょっと強権的に過ぎるというか納得いかないところがあります
手元にある書籍が絶版になったところで、私がそれを返品する義務はないはずであって、あるいはメールも受信したものが他人の都合で削除されるべきではないわけで、 SNS で(個人的に)受信した投稿についても同じことが言えると思うんですよね。
一度誰かに受信された投稿は、もはや発信者だけのものではないし、再発信の権利(著作権とか)こそ発信者が持っているにしても、発信者が受信者のサーバのデータを削除できるべきかというのは、本来もっと議論されるべきだと思います。少なくとも、発信者が自分の投稿をあらゆるサーバのストレージから削除する権利を持っているかどうかというのは自明ではない
https://mastodon.cardina1.red/@lo48576/99286957960003993
https://mastodon.cardina1.red/@lo48576/101953778680795342
https://mastodon.cardina1.red/@lo48576/103097649307307751
の投稿
8vit@gs.yvt.jp
このアカウントは、notestockで公開設定になっていません。
無意識に排中律使おうとしてて駄目だった #直観主義論理は直観的
の投稿
prime@mstdn.poyo.meこのアカウントは、notestockで公開設定になっていません。
x^y が有理数となるような無理数 x, y の組が存在するかみたいなやつ
排中律使うと簡単に存在が示せるんだけど、構成的でないので具体的な値を提示できない
auto. で証明できたけど私はその中身が知りたいの！！
https://top-prover.top/submission/997
これ絶対何か重要な知識が欠けてる気がするんだよなぁ
なーにが tiktok じゃ、こっちは tactic やぞ
@prime 正直区別ついてないです (induction の方が用途が狭そうなので goto を避けるノリで induction にした)
Coq タクティクリファレンス: 帰納法と場合分け
https://magicant.github.io/programmingmemo/coq/t-induct.html
の投稿
prime@mstdn.poyo.meこのアカウントは、notestockで公開設定になっていません。
> 動作は induction term に似ているが、帰納法の仮定は生成されず、term の型のコンストラクタの引数だけが前提に加えられる。
の投稿
prime@mstdn.poyo.meこのアカウントは、notestockで公開設定になっていません。
ペアリングもペヤングの麺も2つの端点があるし、実質同値なのでは？ (?)
最近頭の悪い発言しかしてなくて困ってしまうな (いやべつに)
自動運転車に「『だろう運転』を一切認めない」とすると、フレーム問題にぶつかってそんなもの作れなくなる＞＜
『だろう運転 』をある程度の範囲(フレーム！＞＜)は認めるとすると、今度はその範囲の決まりを厳密に作る必要が出る＞＜
ウーバーの事故では「まさか車道に人はいない『だろう』」と言う実装が問題を起こしたけど、これをどうするか？＞＜
いっけん簡単なルールに見える「車道にいる人間を検出し避けなければならない」
段ボール箱をかぶった人間はどうしよう？＞＜
・・・・なので、自動運転車を認めるには、自動運転車を実際にテストコースで走らせて「この試験をクリア出来たら公道走行してよい」みたいな試験もセットで開発しなければアレかも＞＜
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
サンプルのスクショと現状の細部が異なって同一性が判定できない問題、興味深い (他人事だからこその感想)
CLI の再現性の高い方式はリモートでの指示や時間を越えた指示に有効であることがわかる
(ただしメッセージの中身とかは変わることがあるので基本的に自動化するときは exit status などを見ないといけないけど)
まあ CLI も CLI で stateful な面が強いので、「どこまでやったか忘れた」とか「手順を飛ばした」とこやられると難しい場合も多いんだけど
サイトに行くとポンとでる｢通知送っていい？｣のやつ、Firefoxはとりあえず全ブロックへ | ギズモード・ジャパン
https://www.gizmodo.jp/2019/11/firefox-72-notification-prompt-block.html
slnだけじゃなくだけじゃなく、明示的に「少なくとも何個以上のファイルを」って書くといいかも＞＜
「ファイルはいくつだ？」って問い詰めることができる＞＜
チェックリストが必要だし、その障碍であればチェックリストを使うことが健常な人よりも得意な人もわりといる＞＜
wasmでPDFつくるやつとか絶対誰かやってるだろと思ったら案の定出てきて草 https://github.com/jussiniinikoski/wasm-pdf
まあ Rust で書けば wasm 対応まであと一息だからね……
thunderbirdのポップアップとかもそうだけど、こんな当たり前過ぎることを調査しなければ気づけないMozillaのUXデザイナって、デザインの何を勉強してきたのか？＞＜＃
かといってデザイナがスッと決めるとそれはそれで「UI がクソ」とか言われたりするので、まあ根拠を得たことを喜びたいという感想
このアカウントは、notestockで公開設定になっていません。
問い詰められるようにってことは、チェックしてないこともチェックできる＞＜
直接的には意味がないことも有用だったりする＞＜
例えば「帽子をかぶっているか？」ってチェックする項目、「帽子をまず前後逆にかぶる」と言う項目と「帽子を180度回転させて正しい向きにあわせ、ロゴにタッチする」とかに分けると、より強力にチェックできる＞＜
いつも通り脱線すると＞＜； こういう有名な話も＞＜
ヴァン・ヘイレンがおやつにｍ＆ｍ'ｓの茶色を禁じた理由 | 0ベース思考 どんな難問もシンプルに解決できる | ダイヤモンド・オンライン https://diamond.jp/articles/-/176089?page=3
GoogleもMozillaも「だからお前らがアホなデザインする前からそれはダメだってデザインの教科書に書いてあったって言ってるじゃん＞＜＃ アホなデザインをした時から指摘されてたじゃん＞＜＃ 」ってものを『新しいデザイン』とか言って数年使い続けた末にわりと最近悔い改めコメント出してない？＞＜
あんまり悔い改めてないMS＆Appleよりは姿勢だけはちょっとマシなのかもしれないけど＞＜；
規格を書くときデータの型を明示することを全人類の義務としてほしい
このアカウントは、notestockで公開設定になっていません。
の投稿
8vit@gs.yvt.jpこのアカウントは、notestockで公開設定になっていません。
