おそらく金曜（2023-11-10）あたりから、HackMDの数式表示が壊れている。改行処理が走らないのと、拡張モジュールが読み込めないのが症状。拡張モジュールは \require{XXXX} としてロードする。次のソースコードをサンプルにする。 色付け $\require{color}\…

今日から起算して、20日後くらいにはできると思う。こちらから問い合わせしないと知らせてくれない。

Texcy Luxe〈テクシーリュクス〉という靴が履きやすい。25cm EEE。 公式サイト

/-! ファミリーと多項式 -/ /- →《《《《《《《《《《《《《《《《《《《《 → -/ namespace My /- 型コンストラクタ Fam -/ def Fam (X : Type) := X → Type abbrev FamOver := Fam variable (I : Type) (i j : I) variable (F G : FamOver I) def Sigm {X: …

一応できた。sectionは要らないみたい。 /-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a …

/- 用語： スタブ： from https://e-words.jp/w/%E3%82%B9%E3%82%BF%E3%83%96.html スタブとは、切り株、半券、（何かが減ったり短くなった）残り、などの意味を持つ英単語。ITの分野では、本物が用意できないときに動作に支障が無いようにとりあえず置いて…

/-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a def Cut {A B C : Prop} (p: A → B) (q: …

最後の行がエラー。 /-- 記法クラス -/ class LE (X : Type) where le : X → X → Prop scoped infix:50 "≦" => LE.le #check LE section LE_Test variable -- セミローカルコンテキストの導入 (A: Type) [LE A] (a b:A) #check a≦b end LE_Test /-- 全順序集…

WindowsのVoltaはかなり変な作りをしているらしい。C:/Program Files/Volta/ にある実行可能ファイルを実行すると、同名のcmdスクリプト/exeファイルを順番に再帰的にプロセス起動して、無限にプロセスを生成してしまう。C:/Program Files/Volta/ 内でプログ…

Voltaをバイナリでインストールした。 which node で C:\Program Files\Volta\node.exe それなら、C:\Program Files\nodejs\node.exe はいらないだろうとアンイストール。 node.exe を起動できなくなった。 どうやら、もともとあった node.js v16.14.0 をVol…

まず、 $ git clone https://github.com/xubaiw/Socket.lean $ cd Socket.lean $ cat lean-toolchain leanprover/lean4:nightly-2022-06-16 去年だと、「ふるっ！」と思う。 $ git branch * main $ git rev-parse main 9fc98bc24ccdb4471b2e38e94dccd18f75d2…

バージョン 3 の lean 3.23.0 lean.exe leanchecker.exe leanpkg leanpkg.bat libgcc_s_seh-1.dll libgmp-10.dll libstdc++-6.dll libwinpthread-1.dll バージョン4のクリスマスイブ版 nightly-2022-12-24 clang.exe lake.exe ld.lld.exe lean.exe leanc.exe…

cat lean-toolchain elan toolchain list elan show だとダウンロードが始まる cat lakefile.lean cat .git/HEAD デタッチされているか？ git branch git rev-parse カレントブランチ git tag git rev-parse $(git tag | tail -1) git log --oneline git rev…

Powershell では、foo |& bar も foo 2>&1 | bar も効かない。標準エラー出力を tee でファイルに落とすのは現状分からない。bashなら次が出来るが、Powershellの代替は見つからないでいる。 lake build -v |& tee $(date +%Y-%m-%d_%H-%M-%S).lake-build.log

次のパッケージをトップレベルパッケージ（依存パッケージではなく）git clone でインストールする。 "leancolls" : https://github.com/jamesgallicchio/leancolls インストールしてすぐ気がつくのは： ./lean_packages/ というディレクトリがある。./lake-…

wt.exe が2箇所にあった。 C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt.exe C:\Program Files\WindowsApps\Microsoft.WindowsTerminal_1.15.3466.0_x64__8wekyb3d8bbwe\wt.exe が、C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt…

「CTRL+ALT+P」で Powershell だったのだが、この設定は： [Win]+[Q] から Powershell を探す。 [ファイルの場所を開く] でディレクトリを見る。 "Windows Powershell" がリンクになっているので、プロパティを見る。 プロパティのショートカットキー項目に…

JQPlayGround が自分用の jq を自分でインストールした。場所は： c:\Users\m-hiyama\AppData\Roaming\Code\User\globalStorage\davidnussio.vscode-jq-playground これで jq.exe の実体は2つになる。最初のインストールは C:\Users\m-hiyama\Work\bin\jq.exe…

> alias curl CommandType Name ----------- ---- Alias curl -> Invoke-WebRequestこれが邪魔。 > rm alias:curl

gitの誤認例：.gitignore, --squash - (新) 檜山正幸のキマイラ飼育記 メモ編 にて： 今まで、変な説明を見ても記録しなかったが、これからは記録に残そう。 https://qiita.com/ryosuketter/items/a6047b0270ea999fd51b 今回は、ステージングエリアから、ワ…

gitのキャッシュ？ ステージ？ インデックス？ - (新) 檜山正幸のキマイラ飼育記 メモ編 を書いたキッカケは： https://zenn.dev/unemployed/articles/git-github-team 「間違えてアップしたファイルを.gitignoreで削除する方法」という記述がある。どうも、…

SSH関係の過去記事： SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編 2022-08-22 SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 2022-08-24 SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編 2022-08-24 前後の事情、具体的な設定…

靴やジーパンをネット通販で買うことを目指して： リーバイスのジーンズ - (新) 檜山正幸のキマイラ飼育記 メモ編 そうか、メモしておけばよい - (新) 檜山正幸のキマイラ飼育記 メモ編 無印良品〈MUJI〉ジーンズ： w31 (78.5cm) 股下 82cm 股下を 71.5cm に…

ペンの太さを記録してくれない。 普通は：2.5px, 7px 太めは： 5px, 8px かな。

NPMでインストールできて簡単、と思ったら PowerShell から実行できない。.bin という拡張子のファイルを実行しようとして、データ扱いされる。cmd.exe では実行できる。Webで調べた解決策は： 環境変数 PATHEXT に .BIN を追加する。 自作のコマンドレット …

choco upgrade chocolatey コマンでアップグレードしたが失敗。なんかグチャグチャになってしまった。OneDriveの“ドキュメント\”パスが関係しているようだが、よくワカラン。最初からインストールし直しするしかなさそうだが、choco使うのやめようかな。WinG…

会社： levi strauss & co オンライン： https://www.levi.jp/ タイプ： 511 サイズ： W31 L32 または W32 L32 ジーパン

npm version 8.12.2 の挙動が変なんでダウングレードした。これは、バージョン指定してインストール。 > npm -v npm WARN logfile could not be created: TypeError: fs.withOwnerSync is not a function 8.12.2 > npm install npm@8.12.0 --global npm WARN…

素のディレクトリでまだハマっている所がある。サンプルコードは var map:Map<number, string>; map = new Map<number, string>(); map.set(3, "hello"); console.log(map.get(3)); map.set(5, "world"); console.log(map.get(5)); for (let [key, val] of map) { console.log(`${key} = ${va</number,></number,>…

TypeScriptプロジェクトを始めたら ： もう一度サラからやってみるか。 サラからやった記録。 TmpTsDev > which tsc C:\Users\m-hiyama\AppData\Roaming\npm\tsc.ps1 TmpTsDev > tsc --version Version 4.6.2 ディレクトリを作る。 map.ts を作る。 グローバ…