Seasawher

import Mathlib.Tactic

universe u v

inductive Many (α : Type u) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

variable {α : Type u} {β : Type v}

Seasawher

import Mathlib.Tactic

-- `Nat.succ` を `x + 1` に変換するのが面倒なので導入
@[simp]
theorem nat_succ_eq_add_one {x : Nat} : Nat.succ x = x + 1 := by rfl

-- `Nat.zero` を `0` に変換するのが面倒なので導入
@[simp]
theorem nat_zero_eq_zero : Nat.zero = 0 := by rfl

Seasawher

import Lean

open Lean Meta Tactic

def myAssumption (mvarId : MVarId) : Elab.Tactic.TacticM PUnit := do
  -- Check that `mvarId` is not already assigned.
  mvarId.checkNotAssigned `myAssumption
  -- Use the local context of `mvarId`.
  mvarId.withContext do
    -- The target is the type of `mvarId`.

Seasawher

lake update 時に表題のエラーが出て，mathlib のアップデートができないときの対処法．

以下はあくまで私の環境での一例です．

1. 次のコマンドでツールチェインをアンインストール.

elan toolchain uninstall leanprover/lean4:v4.7.0-rc2

Seasawher

学習記録

• ✅ - 修了済み
• 🚧 - 途中

HarvardX

Harvard 大学が公開しているオープン講座．課題の提出物を GitHub 上で公開できないという縛りがあるものの，わかりやすくて勉強になるのでとても気に入っています．

無料で受講でき，修了証まで出してもらえます．

Seasawher

kaggle のAPIをインストールしようとしてエラー．

エラー内容

https://www.kaggle.com/docs/api に従って，pip install kaggle を実行．インストールはできているようで，pip show kaggle は成功する．

しかし，kaggle -h と打つと下記のエラー：

kaggle: The term 'kaggle' is not recognized as a name of a cmdlet, function, script file, or executable program.

Seasawher

Devcontainer でコンテナを立ち上げたときに，コミットしようとしたら git のユーザ名とEメールアドレスが設定されていないというエラー

原因がよくわからないので解決方法だけ述べます．

postCreateCommand コマンドで git config --global --add safe.directory ${containerWorkspaceFolder} を設定していたのですが， これがよくなかったようです．

postStartCommand に移動させたところ，解決しました．

Seasawher

VSCode DevContainer でコンテナを立ち上げたときに，unsafe repository と言われて Git が無効にされる問題

問題の概要

VSCode DevContainer でコンテナを立ち上げたときに，unsafe repository と言われて Git が無効にされます. Git Graph 拡張機能も無効にされます．

毎回コンテナを立ち上げてから手動で「安全です」とVSCodeに教える必要があり，手間がかかっていた．

解決策

Seasawher

Docker Multistage Build でなぜかイメージが大きくなる理由

マルチステージビルドの間，ENV で定義した値は保持されるのかと思っていましたが，実は FROM 文をまたいだときにすべて一新されてしまうようです．

古い環境変数を用いてもエラーにはならないので気づきませんでした．

COPY 文の中に環境変数を使っていたりすると，「全部をまるごとコピー」というめちゃくちゃな挙動をするようです．

参考：https://stackoverflow.com/questions/72596395/why-is-my-docker-image-larger-with-a-multi-stage-build-compared-to-a-one-stage-b

Seasawher

VSCodeで正規表現置換する際に，マッチした文字列そのものを参照する方法

VSCode で検索するときに正規表現を使って検索して，マッチした文字列を置換するということができます．

「検索する方は正規表現が使えるけど，置換する方は単に一様な文字列に置き換えるだけだなー」と思っておりました．

しかし，実は「検索でマッチした文字列」を置換のときに参照することができます．

正規表現検索のときに () を使ったら，マッチした内容を $1 等と参照できるのです．