diff --git a/LeanByExample/Diagnostic/Lint.lean b/LeanByExample/Diagnostic/Lint.lean index 03d8f1e7..e09e9f88 100644 --- a/LeanByExample/Diagnostic/Lint.lean +++ b/LeanByExample/Diagnostic/Lint.lean @@ -21,8 +21,14 @@ info: -- Found 0 errors in 1 declarations -- 定理は対象外なのでスルーされる #lint only docBlame --- 技術的な理由で `#lint` の出力は省略しているが、 -- エラーになっている -#guard_msgs (drop error) in +/-- +error: -- Found 1 error in 1 declarations (plus 0 automatically generated ones) in the current file with 1 linters + +/- The `docBlameThm` linter reports: +THEOREMS ARE MISSING DOCUMENTATION STRINGS: -/ +#check hoge /- theorem missing documentation string -/ +-/ +#guard_msgs (error) in -- ドキュメントコメントのない定理に対して警告するリンタを実行している #lint only docBlameThm diff --git a/lake-manifest.json b/lake-manifest.json index 0242d380..ef775935 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -8,14 +8,14 @@ "rev": "ec10d9ba44225d66e790787d0f5b19a14830337e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "ec10d9ba44225d66e790787d0f5b19a14830337e", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/Seasawher/mdgen", "type": "git", "subDir": null, "scope": "", - "rev": "0d7e8b67b1088cb2d51bb2d3f175f9517e5e0fa3", + "rev": "ddec7bc2d811777502789c678445b7a47a265baa", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 5123a66d..15ebc707 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,7 @@ abbrev linterOptions : Array LeanOption := #[ ] package «Lean by Example» where - keywords := #["manual", "reference", "tutorial", "japanese", "cheatsheet"] + keywords := #["manual", "reference", "japanese"] description := "プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。" leanOptions := #[ ⟨`autoImplicit, false⟩, @@ -24,7 +24,7 @@ require mdgen from git "https://github.com/Seasawher/mdgen" @ "main" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "master" + "https://github.com/leanprover-community/mathlib4.git" @ "ec10d9ba44225d66e790787d0f5b19a14830337e" @[default_target] lean_lib LeanByExample where