tips
コマンドライン： lean --print-prefix lean --print-libdir lake print-paths | jq . jq . ./lake-manifest.json cat .git/HEAD cat ~/.elan/update-hashes/* | sort エディタ： #eval Lean.findOLean `Name #check と #eval で InfoViewをよく見る。 set_o…
leanprover/lean4:stable と leanprover/lean4:v4.0.0-m5 という名前のツールチェーンは同じもので、名前だけが違う。どちらも、https://github.com/leanprover/lean4/releases/expanded_assets/v4.0.0-m5 からダウンロードされる。が、elanはそれに気付かず…
lakeはnpmほどには洗練されてないみたいだ。現状では完全な自動ビルドは無理な気がする。原因不明な失敗をすることがある。ビルドの手順は、原理的には次のようなことだと思う。 ./lean-toolcahin を見て、ツールチェーンがインストールされてなければ、elan…
Lean 4ではキーワードを整理したらしく。 constantが廃止されて、axiomのみを使うようになった。 Πが廃止されて、∀のみを使うようになった。 assumeが廃止されて、funまたはλのみを使うようになった。 variables は廃止。variable が使える。 parameter, par…
Leanマニュアルでは "object" も使っているが、混乱のもとなので「要素〈element〉」を使う。「インスタンス」も混乱のもとなので使わない。「型の要素」を使う。型の要素が命題の証拠〈witness〉に対応する。次はセクションの定義： variable (F : Type → T…
「CTRL+ALT+P」で Powershell だったのだが、この設定は： [Win]+[Q] から Powershell を探す。 [ファイルの場所を開く] でディレクトリを見る。 "Windows Powershell" がリンクになっているので、プロパティを見る。 プロパティのショートカットキー項目に…
久しぶりで色々忘れている。 MSYS2のルート / は C:\msys64\ MSYS2の /c/ は C:\ したがって、/c/msys64/ は / /ucrt64/, /mingw64/, /clang64/ と、それらの32ビット版があるが、当初はダミーで空っぽ clang32.exe, clangarm64.exe, mingw64.exe, ucrt64.ex…
src/Init/Notation.lean からの情報。構文範疇precは項の優先度を表す値（の表現）のことで： 項の優先度： max = 1024, arg = 1023, lead = 1022, min = 10 パイプ記号 は優先度は min = 10 =, ∈ が50 足し算は65、 規表現風接尾辞の *,+,? は arg = 1023 S…
':=' を使わなくなったようだ。structure/where 、マクロかも知れない。 structure WordCount where wordCount : Nat lineCount : Nat charCount : Nat inWord : Bool宣言文の並びなので、構造体もコンテキストの一種、特に指標の一種と考える。インスタンス…
variable b:Bool はダメで、variable (b:Bool) 。そもそも「変数」は通常の意味の変数ではない。共通に予約された暗黙束縛変数のこと。
図のタイトルをYAMLフロントマターにするのは使えねー。 統一性がない。 構文： flowchart sequence diag. ID[ラベル] タイプ ID as ラベル ソース アロー ラベル ターゲット ソース アロー ターゲット: ラベル 次のようにすれば、統一的だった。 ノードは …
flowchart と subgraph の構文が一致しない。flowchart id[title] direction TB なら良かった。 辺へのスタイリングが番号指定でカス
---, , o--o, x--x はマニュアルにあった。 ==o, -.-o, -.-x とかも使える。 =.=> はダメ。 o-->, x--> はエラーにならないが効かない。 style nodeId styling が使える。 linkStyle linkNo styling が使えるが不便。 class id1, id2 className が使える。 c…
context と template のペアで、ドル始まり文字列を変数としてのテンプレート展開。 .context as $context | .template | walk( if (type == "string" and test("^\\$")) then $context[.[1:]] else . end ) 関数を使うとわかりやすいかも。 .context as $co…
npm list --depth=10 好きなレベルを指定できる。--all ですべてのレベル。 npm list に深い階層にあるパッケージも指定できる。依存性を上にたどるような表示 npm view パッケージ （npm show パッケージ でも同じ） npm view パッケージ dependencies npm …
短く表示する。エイリアスするといいかも。 git status -s または git status --short git log --oneline --graph git log の --decorate オプションは、現在は無意味（昔は意味があったが）。
index.js, index.ts とかでメインエントリーポイントを指定する習慣があるが、これはやめたい。 ファイル名だけでは何をするものか想像ができない。ディレクトリ名／プロジェクト名の情報が別に必要。 コピーして上書きする危険がある。 パッケージ／ディレ…
TypeScriptのテスト の続き。次をインストールする。 グローバルに esbuild ローカルに esbuild-jest ローカルに @types/jest jestの設定をする。例えば、package.json に書く。 "jest": { "verbose": true, "transform": { "\\.ts$": "esbuild-jest" } }, …
特にグローバルインストールを調べる。 古いパッケージを調べる npm outdate {-g | --global}? 脆弱性があるパッケージを確認する npm audit 、グローバルはチェックできない。 新しいバージョンに更新する npm update XXX {-g | --global}? npm install npm…
サラからの最低限環境構築を試していたが、最低限でもテストは必要。でjestは入れてみた。https://jestjs.io/ja/docs/cli により使う。jestのテストコードはそれ自身がDSLみたいなものだから、JavaScript構文で書いてもいいと思うが、テストコード自体をType…
ordering=out でほぼ思い通りの結果になる。 digraph { node [ordering=out]; /* ... */ }
シェブロテインは、ユーザーのパーザークラスのコンストラクタ内での自己分析実行関数呼び出しにより、GAST〈Grammar AST | ガスト〉を作る。ガストを作るときに、パーザー関数を呼び出す。この作業工程をレコーディングフェーズと呼ぶ。レコーディングフェ…
peformSeflAnalysys はパーザーの引数なしメソッド this.peformSeflAnalysys() 以外に、 オブジェクトを引数に取るスタティックメソッド shev.Parser.peformSeflAnalysys(obj) もあるようだ。いずれにしても、ユーザー・パーザークラスのコンストラクタで呼…
パーザークラスの宣言から RULEメソッドのプロファイルを見る。 /** * A Parser that outputs a Concrete Syntax Tree. * See: * - https://chevrotain.io/docs/tutorial/step3_adding_actions_root.html#alternatives * - https://chevrotain.io/docs/guide…
スプレッド構文 [...a, ...b] で Array.prototype.concat(a, b) スプレッド構文 {...a, ...b} で Object.assign(a, b) クラスなしのオブジェクト定義 let C = { add(x, y){return x + y}}; 分割〈destructuring〉代入 let {a, b} = {a:1, b:2, c:3}; オブジ…
https://github.com/stardog-union/millan/blob/master/src/helpers/regex.ts を少し変更する。名前を置換した： and → seq many → repeat export const regex = { or(...r: RegExp[]) { return new RegExp(r.map(({ source }) => `(${source})`).join('|'))…
let foo : Parameters<typeof someFunc>[2]; typeof someFunc で関数 someFunc の関数型〈アロー型〉を取る。 Parameters で、関数型の引数型配列を作る。 Parameters[2] で、関数型の引数型配列の三番目の型を取る。 変数 foo の型は、関数 someFunc の第三引数の型になる。</typeof>
const productions: Record<string, Rule> = parser.getGAstProductions(); console.dir(productions); GAstが意味不明だが、Generated AST かな？ ともかく、GAstProductions が内部的に構築されればバージングが出来る状態になる。</string,>
便利だった。 > git update-git-for-windows Git for Windows 2.29.2.windows.3 (64bit) Update 2.35.1.windows.2 is available Download and install Git for Windows 2.35.1(2) [N/y]? y ###############################################################…
基本的なコマンドラインツール。 パケットが届くかは ping シェルアクセスは ssh 名前が引けるかは nslookup、digはbind-utilsというパッケージに含まれる。 WebページがGETできるかは curl、情報だけは curl -I アプリケーションレベルでアクセス確認は ftp…
