From eb7e44375d92cab32f751f517e7068b27dffdeb8 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 01:39:45 -0400 Subject: [PATCH] feat: initial commit, adapted from mathlib4 mathlib4 commit: 2e3cdfaaa8ba1639dc092757cee447e77591ad00 --- .github/workflows/build.yml | 40 +++++ .gitignore | 2 + .vscode/copyright.code-snippets | 13 ++ .vscode/settings.json | 11 ++ GNUmakefile | 16 ++ README.md | 20 +++ Std.lean | 10 ++ Std/Data/Array/Defs.lean | 42 +++++ Std/Lean/NameMapAttribute.lean | 72 +++++++++ Std/Tactic/Lint.lean | 3 + Std/Tactic/Lint/Basic.lean | 104 +++++++++++++ Std/Tactic/Lint/Frontend.lean | 231 ++++++++++++++++++++++++++++ Std/Tactic/Lint/Misc.lean | 263 ++++++++++++++++++++++++++++++++ Std/Tactic/Lint/Simp.lean | 248 ++++++++++++++++++++++++++++++ Std/Tactic/OpenPrivate.lean | 125 +++++++++++++++ Std/Util/LibraryNote.lean | 46 ++++++ Std/Util/TermUnsafe.lean | 47 ++++++ bors.toml | 6 + lakefile.lean | 13 ++ lean-toolchain | 1 + scripts/runLinter.lean | 60 ++++++++ test/hello.lean | 0 22 files changed, 1373 insertions(+) create mode 100644 .github/workflows/build.yml create mode 100644 .gitignore create mode 100644 .vscode/copyright.code-snippets create mode 100644 .vscode/settings.json create mode 100644 GNUmakefile create mode 100644 README.md create mode 100644 Std.lean create mode 100644 Std/Data/Array/Defs.lean create mode 100644 Std/Lean/NameMapAttribute.lean create mode 100644 Std/Tactic/Lint.lean create mode 100644 Std/Tactic/Lint/Basic.lean create mode 100644 Std/Tactic/Lint/Frontend.lean create mode 100644 Std/Tactic/Lint/Misc.lean create mode 100644 Std/Tactic/Lint/Simp.lean create mode 100644 Std/Tactic/OpenPrivate.lean create mode 100644 Std/Util/LibraryNote.lean create mode 100644 Std/Util/TermUnsafe.lean create mode 100644 bors.toml create mode 100644 lakefile.lean create mode 100644 lean-toolchain create mode 100644 scripts/runLinter.lean create mode 100644 test/hello.lean diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000000..e9badaab0a --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,40 @@ +on: + push: + branches-ignore: + # ignore tmp branches used by bors + - 'staging.tmp*' + - 'trying.tmp*' + - 'staging*.tmp' + pull_request: + +name: ci + +jobs: + build: + name: Build + runs-on: ubuntu-latest + steps: + - name: install elan + run: | + set -o pipefail + curl -sSfL https://github.com/leanprover/elan/releases/download/v1.3.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y --default-toolchain none + echo "$HOME/.elan/bin" >> $GITHUB_PATH + + - uses: actions/checkout@v2 + + - name: update Std.lean + run: | + find Std -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Std.lean + + - name: build std + run: lake build + + - name: test std + run: make test + + - name: lint std + run: make lint + + - name: check that all files are imported + run: git diff --exit-code diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000000..0cfd28eb63 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +/build +/prelude/build diff --git a/.vscode/copyright.code-snippets b/.vscode/copyright.code-snippets new file mode 100644 index 0000000000..582fbdba06 --- /dev/null +++ b/.vscode/copyright.code-snippets @@ -0,0 +1,13 @@ +{ + "Copyright header for std": { + "scope": "lean4", + "prefix": "copyright", + "body": [ + "/-", + "Copyright (c) ${CURRENT_YEAR} $1. All rights reserved.", + "Released under Apache 2.0 license as described in the file LICENSE.", + "Authors: $1", + "-/" + ] + } +} diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000000..b0f95471e6 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,11 @@ +{ + "editor.insertSpaces": true, + "editor.tabSize": 2, + "editor.rulers" : [100], + "files.encoding": "utf8", + "files.eol": "\n", + "files.insertFinalNewline": true, + "files.trimFinalNewlines": true, + "files.trimTrailingWhitespace": true, + "search.usePCRE2": true +} diff --git a/GNUmakefile b/GNUmakefile new file mode 100644 index 0000000000..689b42709f --- /dev/null +++ b/GNUmakefile @@ -0,0 +1,16 @@ +TESTS = $(wildcard test/*.lean) + +.PHONY: all build test lint + +all: build test + +build: + lake build + +test: $(addsuffix .run, $(TESTS)) + +test/%.run: build + lake env lean test/$* + +lint: build + ./build/bin/runLinter diff --git a/README.md b/README.md new file mode 100644 index 0000000000..44c6c89fc5 --- /dev/null +++ b/README.md @@ -0,0 +1,20 @@ +# std4 + +Work in progress standard library for Lean 4. This is a collection of data structures and tactics intended for use by both computer-science applications and mathematics applications of Lean 4. + +# Build instructions + +* Get the newest version of `elan`. If you already have installed a version of Lean, you can run + ``` + elan self update + ``` + If the above command fails, or if you need to install `elan`, run + ``` + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh + ``` + If this also fails, follow the instructions under `Regular install` [here](https://leanprover-community.github.io/get_started.html). +* To build `std4` run `lake build`. To build and run all tests, run `make`. +* If you added a new file, run the following command to update `Std.lean` + ``` + find Std -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Std.lean + ``` diff --git a/Std.lean b/Std.lean new file mode 100644 index 0000000000..b8b9ebdca7 --- /dev/null +++ b/Std.lean @@ -0,0 +1,10 @@ +import Std.Data.Array.Defs +import Std.Lean.NameMapAttribute +import Std.Tactic.Lint +import Std.Tactic.Lint.Basic +import Std.Tactic.Lint.Frontend +import Std.Tactic.Lint.Misc +import Std.Tactic.Lint.Simp +import Std.Tactic.OpenPrivate +import Std.Util.LibraryNote +import Std.Util.TermUnsafe diff --git a/Std/Data/Array/Defs.lean b/Std/Data/Array/Defs.lean new file mode 100644 index 0000000000..b0ce341204 --- /dev/null +++ b/Std/Data/Array/Defs.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2021 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Paulino, Floris van Doorn +-/ + +/-! +## Definitions on Arrays + +This file contains various definitions on `Array`. It does not contain +proofs about these definitions, those are contained in other files in `Std.Data.Array`. +-/ + +namespace Array + +/-- The array `#[f 0, ..., f n]` -/ +def ofFn (n : Nat) (f : Fin n → α) : Array α := + loop 0 (mkEmpty n) +where + /-- Implementation detail of `Array.ofFn`. -/ + loop (i : Nat) (acc : Array α) : Array α := + if h : i < n then + let acc := acc.push (f ⟨i, h⟩) + loop (i + 1) acc + else + acc +termination_by + loop i acc => n - i + +/-- The array `#[0, 1, ..., n - 1]`. -/ +def range (n : Nat) : Array Nat := + n.fold (flip Array.push) #[] + +/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/ +def reduceOption (l : Array (Option α)) : Array α := + l.filterMap id + +/-- Turns `#[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` into `#[a₁, a₂, ⋯, b₁, b₂, ⋯]` -/ +def flatten (arr : Array (Array α)) : Array α := + arr.foldl (init := #[]) fun acc a => acc.append a + +end Array diff --git a/Std/Lean/NameMapAttribute.lean b/Std/Lean/NameMapAttribute.lean new file mode 100644 index 0000000000..8db915c733 --- /dev/null +++ b/Std/Lean/NameMapAttribute.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2022 E.W.Ayers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: E.W.Ayers +-/ +import Lean + +namespace Lean + +/-- Maps declaration names to α. -/ +def NameMapExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α) + +instance : Inhabited (NameMapExtension α) := + inferInstanceAs <| Inhabited (SimplePersistentEnvExtension ..) + +def NameMapExtension.find? (ext : NameMapExtension α) (env : Environment) : Name → Option α := + (SimplePersistentEnvExtension.getState ext env).find? + +/-- Add the given k,v pair to the NameMapExtension. -/ +def NameMapExtension.add [Monad M] [MonadEnv M] [MonadError M] + (ext : NameMapExtension α) (k : Name) (v : α) : M Unit := do + if let some _ := ext.find? (←getEnv) k then + throwError "Already exists entry for {ext.name} {k}" + else + ext.addEntry (←getEnv) (k, v) |> setEnv + +def mkNameMapExtension (α) (name : Name): IO (NameMapExtension α) := do + registerSimplePersistentEnvExtension { + name := name, + addImportedFn := fun ass => ass.foldl (init := ∅) fun + | names, as => as.foldl (init := names) fun + | names, (a,b) => names.insert a b, + addEntryFn := fun s n => s.insert n.1 n.2 , + toArrayFn := fun es => es.toArray + } + +structure NameMapAttributeImpl (α : Type) where + name : Name + descr : String + add : (src : Name) → (stx : Syntax) → AttrM α + deriving Inhabited + +/-- Similar to ParametricAttribute except that attributes do not +have to be assigned in the same file as the declaration. -/ +structure NameMapAttribute (α) where + impl : NameMapAttributeImpl α + ext : NameMapExtension α + deriving Inhabited + +def NameMapAttribute.find? (attr : NameMapAttribute α) + : (env : Environment) → Name → Option α := attr.ext.find? + +def NameMapAttribute.add [Monad M] [MonadEnv M] [MonadError M] + (attr : NameMapAttribute α) (k : Name) (v : α) : M Unit := + attr.ext.add k v + +def registerNameMapAttribute (impl : NameMapAttributeImpl α) : IO (NameMapAttribute α) := do + let ext ← mkNameMapExtension α impl.name + registerBuiltinAttribute { + name := impl.name + descr := impl.descr + add := fun src stx _kind => do + let a : α ← impl.add src stx + ext.add src a + } + return { + impl := impl + ext := ext + } + + +end Lean diff --git a/Std/Tactic/Lint.lean b/Std/Tactic/Lint.lean new file mode 100644 index 0000000000..df61206747 --- /dev/null +++ b/Std/Tactic/Lint.lean @@ -0,0 +1,3 @@ +import Std.Tactic.Lint.Misc +import Std.Tactic.Lint.Simp +import Std.Tactic.Lint.Frontend diff --git a/Std/Tactic/Lint/Basic.lean b/Std/Tactic/Lint/Basic.lean new file mode 100644 index 0000000000..de8c870735 --- /dev/null +++ b/Std/Tactic/Lint/Basic.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner +-/ + +import Lean +import Std.Util.TermUnsafe +import Std.Lean.NameMapAttribute +open Lean Meta + +namespace Std.Tactic.Lint + +/-! +# Basic linter types and attributes + +This file defines the basic types and attributes used by the linting +framework. A linter essentially consists of a function +`(declaration : Name) → MetaM (Option MessageData)`, this function together with some +metadata is stored in the `Linter` structure. We define two attributes: + + * `@[stdLinter]` applies to a declaration of type `Linter` and adds it to the default linter set. + + * `@[nolint linterName]` omits the tagged declaration from being checked by + the linter with name `linterName`. +-/ + +syntax (name := nolint) "nolint" (ppSpace ident)+ : attr + +-- Defines the user attribute `nolint` for skipping `#lint` +initialize nolintAttr : NameMapAttribute (Array Name) ← + registerNameMapAttribute { + name := `nolint + descr := "Do not report this declaration in any of the tests of `#lint`" + add := fun _decl stx => + match stx with + -- TODO: validate linter names + | `(attr|nolint $[$ids]*) => pure $ ids.map (·.getId.eraseMacroScopes) + | _ => throwError "unexpected nolint syntax {stx}" + } + +/-- Returns true if `decl` should be checked +using `linter`, i.e., if there is no `nolint` attribute. -/ +def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool := + return !((nolintAttr.find? (← getEnv) decl).getD {}).contains linter + +/-- +Returns true if `decl` is an automatically generated declaration. + +Also returns true if `decl` is an internal name or created during macro +expansion. +-/ +def isAutoDecl (decl : Name) : CoreM Bool := do + if decl.hasMacroScopes then return true + if decl.isInternal then return true + if let Name.str n s := decl then + if s.startsWith "proof_" || s.startsWith "match_" then return true + if (← getEnv).isConstructor n && ["injEq", "inj", "sizeOf_spec"].any (· == s) then + return true + if let ConstantInfo.inductInfo _ := (← getEnv).find? n then + if [casesOnSuffix, recOnSuffix, brecOnSuffix, binductionOnSuffix, belowSuffix, + "ndrec", "ndrecOn", "noConfusionType", "noConfusion"].any (· == s) then + return true + pure false + +/-- +A linting test for the `#lint` command. + +`test` defines a test to perform on every declaration. It should never fail. Returning `none` +signifies a passing test. Returning `some msg` reports a failing test with error `msg`. + +`noErrorsFound` is the message printed when all tests are negative, and `errorsFound` is printed +when at least one test is positive. + +If `isFast` is false, this test will be omitted from `#lint-`. +-/ +structure Linter where + test : Name → MetaM (Option MessageData) + noErrorsFound : MessageData + errorsFound : MessageData + isFast := true + +structure NamedLinter extends Linter where + declName : Name + +def NamedLinter.name (l : NamedLinter) : Name := l.declName.updatePrefix Name.anonymous + +def getLinter (declName : Name) : CoreM NamedLinter := unsafe + return { ← evalConstCheck Linter ``Linter declName with declName } + +/-- Takes a list of names that resolve to declarations of type `linter`, +and produces a list of linters. -/ +def getLinters (l : List Name) : CoreM (List NamedLinter) := + l.mapM getLinter + +-- Defines the user attribute `stdLinter` for adding a linter to the default set. +initialize stdLinterAttr : TagAttribute ← + registerTagAttribute + (name := `stdLinter) + (descr := "Use this declaration as a linting test in #lint") + (validate := fun name => do + let constInfo ← getConstInfo name + unless ← (isDefEq constInfo.type (mkConst ``Linter)).run' do + throwError "must have type Linter, got {constInfo.type}") diff --git a/Std/Tactic/Lint/Frontend.lean b/Std/Tactic/Lint/Frontend.lean new file mode 100644 index 0000000000..881e1fe5fd --- /dev/null +++ b/Std/Tactic/Lint/Frontend.lean @@ -0,0 +1,231 @@ +/- +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner +-/ +import Std.Tactic.Lint.Basic + +/-! +# Linter frontend and commands + +This file defines the linter commands which spot common mistakes in the code. +* `#lint`: check all declarations in the current file +* `#lint Pkg`: check all declarations in the package `Pkg` (so excluding core or other projects, + and also excluding the current file) +* `#lint all`: check all declarations in the environment (the current file and all + imported files) + +For a list of default / non-default linters, see the "Linting Commands" user command doc entry. + +The command `#list_linters` prints a list of the names of all available linters. + +You can append a `*` to any command (e.g. `#lint Std*`) to omit the slow tests (4). + +You can append a `-` to any command (e.g. `#lint Std-`) to run a silent lint +that suppresses the output if all checks pass. +A silent lint will fail if any test fails. + +You can append a `+` to any command (e.g. `#lint Std+`) to run a verbose lint +that reports the result of each linter, including the successes. + +You can append a sequence of linter names to any command to run extra tests, in addition to the +default ones. e.g. `#lint doc_blame_thm` will run all default tests and `doc_blame_thm`. + +You can append `only name1 name2 ...` to any command to run a subset of linters, e.g. +`#lint only unused_arguments` + +You can add custom linters by defining a term of type `Linter` in the `Std.Tactic.Lint` namespace. +A linter defined with the name `Std.Tactic.Lint.myNewCheck` can be run with `#lint myNewCheck` +or `lint only myNewCheck`. +If you add the attribute `@[stdLinter]` to `linter.myNewCheck` it will run by default. + +Adding the attribute `@[nolint doc_blame unused_arguments]` to a declaration +omits it from only the specified linter checks. + +## Tags + +sanity check, lint, cleanup, command, tactic +-/ + +def Lean.TagAttribute.getDecls (attr : TagAttribute) (env : Environment) : Array Name := Id.run do + let st := attr.ext.toEnvExtension.getState env + let mut decls := st.state.toArray + for ds in st.importedEntries do + decls := decls ++ ds + decls + +namespace Std.Tactic.Lint +open Lean Std + +/-- +Verbosity for the linter output. +* `low`: only print failing checks, print nothing on success. +* `medium`: only print failing checks, print confirmation on success. +* `high`: print output of every check. +-/ +inductive LintVerbosity | low | medium | high + deriving Inhabited, DecidableEq, Repr + +/-- `getChecks slow extra use_only` produces a list of linters. +`extras` is a list of names that should resolve to declarations with type `linter`. +If `useOnly` is true, it only uses the linters in `extra`. +Otherwise, it uses all linters in the environment tagged with `@[linter]`. +If `slow` is false, it only uses the fast default tests. -/ +def getChecks (slow : Bool) (extra : List Name) (useOnly : Bool) : CoreM (List NamedLinter) := do + let default ← if useOnly then pure [] else + getLinters (stdLinterAttr.getDecls (← getEnv)).toList + let default := if slow then default else default.filter (·.isFast) + pure $ default ++ (← getLinters extra) + +def lintCore (decls : Array Name) (linters : Array NamedLinter) : + CoreM (Array (NamedLinter × HashMap Name MessageData)) := do + let env ← getEnv + let options ← getOptions -- TODO: sanitize options? + + let tasks : Array (NamedLinter × Array (Name × Task (Option MessageData))) ← + linters.mapM fun linter => do + let decls ← decls.filterM (shouldBeLinted linter.name) + (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do + BaseIO.asTask do + match ← withCurrHeartbeats (linter.test decl) + |>.run'.run' {options, fileName := "", fileMap := default} {env} + |>.toBaseIO with + | Except.ok msg? => pure msg? + | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}" + + tasks.mapM fun (linter, decls) => do + let mut msgs : HashMap Name MessageData := {} + for (declName, msg?) in decls do + if let some msg := msg?.get then + msgs := msgs.insert declName msg + pure (linter, msgs) + +/-- Sorts a map with declaration keys as names by line number. -/ +def sortResults {α} [Inhabited α] (results : HashMap Name α) : CoreM <| Array (Name × α) := do + let mut key : HashMap Name Nat := {} + for (n, _) in results.toArray do + if let some range ← findDeclarationRanges? n then + key := key.insert n <| range.range.pos.line + pure $ results.toArray.qsort fun (a, _) (b, _) => key.findD a 0 < key.findD b 0 + +/-- Formats a linter warning as `#check` command with comment. -/ +def printWarning (declName : Name) (warning : MessageData) : CoreM MessageData := do + pure m!"#check {← mkConstWithLevelParams declName} /- {warning} -/" + +/-- Formats a map of linter warnings using `print_warning`, sorted by line number. -/ +def printWarnings (results : HashMap Name MessageData) : CoreM MessageData := do + (MessageData.joinSep ·.toList Format.line) <$> + (← sortResults results).mapM fun (declName, warning) => printWarning declName warning + +/-- +Formats a map of linter warnings grouped by filename with `-- filename` comments. +The first `drop_fn_chars` characters are stripped from the filename. +-/ +def groupedByFilename (results : HashMap Name MessageData) : CoreM MessageData := do + let mut grouped : HashMap Name (HashMap Name MessageData) := {} + for (declName, msg) in results.toArray do + let mod ← findModuleOf? declName + let mod := mod.getD (← getEnv).mainModule + grouped := grouped.insert mod <| grouped.findD mod {} |>.insert declName msg + let grouped' := grouped.toArray.qsort fun (a, _) (b, _) => toString a < toString b + (MessageData.joinSep · (Format.line ++ Format.line)) <$> + grouped'.toList.mapM fun (mod, msgs) => do + pure m!"-- {mod}\n{← printWarnings msgs}" + +/-- +Formats the linter results as Lean code with comments and `#print` commands. +-/ +def formatLinterResults + (results : Array (NamedLinter × HashMap Name MessageData)) + (decls : Array Name) + (groupByFilename : Bool) + (whereDesc : String) (runSlowLinters : Bool) + (verbose : LintVerbosity) (numLinters : Nat) : + CoreM MessageData := do + let formattedResults ← results.filterMapM fun (linter, results) => do + if !results.isEmpty then + let warnings ← + if groupByFilename then + groupedByFilename results + else + printWarnings results + pure $ some m!"/- The `{linter.name}` linter reports:\n{linter.errorsFound} -/\n{warnings}\n" + else if verbose = LintVerbosity.high then + pure $ some m!"/- OK: {linter.noErrorsFound} -/" + else + pure none + let mut s := MessageData.joinSep formattedResults.toList Format.line + let numAutoDecls := (← decls.filterM isAutoDecl).size + let failed := results.map (·.2.size) |>.foldl (·+·) 0 + unless verbose matches LintVerbosity.low do + s := m!"-- Found {failed} error{if failed == 1 then "" else "s" + } in {decls.size - numAutoDecls} declarations (plus { + numAutoDecls} automatically generated ones) {whereDesc + } with {numLinters} linters\n\n{s}" + unless runSlowLinters do s := m!"{s}-- (slow linters skipped)\n" + pure s + +def getDeclsInCurrModule : CoreM (Array Name) := do + pure $ (← getEnv).constants.map₂.toList.toArray.map (·.1) + +def getAllDecls : CoreM (Array Name) := do + pure $ (← getDeclsInCurrModule) ++ + (← getEnv).constants.map₁.toArray.map (·.1) + +def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do + let mut decls ← getDeclsInCurrModule + let modules := (← getEnv).header.moduleNames.map (pkg.isPrefixOf ·) + for (declName, moduleIdx) in (← getEnv).const2ModIdx.toArray do + if modules[(id moduleIdx : Nat)]? == true then + decls := decls.push declName + pure decls + +open Elab Command in +/-- The command `#lint` runs the linters on the current file (by default). -/ +elab "#lint" + project:(ident)? + verbosity:("+" <|> "-")? + fast:"*"? + only:(&"only")? linters:(ident)* + : command => do + let (decls, whereDesc, groupByFilename) ← match project with + | none => do pure (← liftCoreM getDeclsInCurrModule, "in the current file", false) + | some id => do + let id := id.getId.eraseMacroScopes + if id == `all then + pure (← liftCoreM getAllDecls, "in all files", true) + else + pure (← liftCoreM (getDeclsInPackage id), s!"in {id}", true) + let verbosity : LintVerbosity ← match verbosity with + | none => pure .medium + | some ⟨.atom _ "+"⟩ => pure .high + | some ⟨.atom _ "-"⟩ => pure .low + | _ => throwUnsupportedSyntax + let fast := fast.isSome + let only := only.isSome + let extraLinters ← linters.mapM fun id => + withScope ({ · with currNamespace := `Std.Tactic.Lint }) <| + resolveGlobalConstNoOverload id + let linters ← liftCoreM <| getChecks (slow := !fast) extraLinters.toList only + let results ← liftCoreM <| lintCore decls linters.toArray + let failed := results.any (!·.2.isEmpty) + let mut fmtResults ← liftCoreM <| + formatLinterResults results decls (groupByFilename := groupByFilename) + whereDesc (runSlowLinters := !fast) verbosity linters.length + if failed then + logError fmtResults + else if verbosity != LintVerbosity.low then + logInfo m!"{fmtResults}\n-- All linting checks passed!" + +open Elab Command in +/-- The command `#list_linters` prints a list of all available linters. -/ +elab "#list_linters" : command => do + let env ← getEnv + let ns : Array Name := env.constants.fold (init := #[]) fun ns n ci => + if n.getPrefix == `Std.Tactic.Lint && ci.type == mkConst ``Std.Tactic.Lint.Linter + then ns.push n else ns + let linters ← ns.mapM fun n => do + let b := stdLinterAttr.hasTag (← getEnv) n + pure $ toString (n.updatePrefix Name.anonymous) ++ if b then " (*)" else "" + logInfo m!"Available linters (linters marked with (*) are in the default lint set):\n{ + Format.joinSep linters.toList Format.line}" diff --git a/Std/Tactic/Lint/Misc.lean b/Std/Tactic/Lint/Misc.lean new file mode 100644 index 0000000000..34fb089fa0 --- /dev/null +++ b/Std/Tactic/Lint/Misc.lean @@ -0,0 +1,263 @@ +/- +Copyright (c) 2020 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Robert Y. Lewis, Arthur Paulino, Gabriel Ebner +-/ +import Std.Tactic.Lint.Basic +import Std.Data.Array.Defs + +open Lean Meta + +namespace Std.Tactic.Lint + +/-! +# Various linters + +This file defines several small linters. +-/ + +/-- A linter for checking whether a declaration has a namespace twice consecutively in its name. -/ +@[stdLinter] def dupNamespace : Linter where + noErrorsFound := "No declarations have a duplicate namespace." + errorsFound := "DUPLICATED NAMESPACES IN NAME:" + test declName := do + if isGlobalInstance (← getEnv) declName then + return none + let nm := declName.components + let some (dup, _) := nm.zip nm.tail! |>.find? fun (x, y) => x == y + | return none + return m!"The namespace {dup} is duplicated in the name" + +/-- A linter object for checking for unused arguments. +We skip all declarations that contain `sorry` in their value. -/ +@[stdLinter] def unusedArguments : Linter where + noErrorsFound := "No unused arguments." + errorsFound := "UNUSED ARGUMENTS." + test declName := do + if ← isAutoDecl declName then return none + if ← isProjectionFn declName then return none + let info ← getConstInfo declName + let ty := info.type + let some val := info.value? | return none + forallTelescope ty fun args ty => do + let mut e := (mkAppN val args).headBeta + e := mkApp e ty + for arg in args do + let ldecl ← getFVarLocalDecl arg + e := mkApp e ldecl.type + if let some val := ldecl.value? then + e := mkApp e val + let unused := args.zip (.range args.size) |>.filter fun (arg, _) => + !e.containsFVar arg.fvarId! + if unused.isEmpty then return none + addMessageContextFull <| .joinSep (← unused.toList.mapM fun (arg, i) => + return m!"argument {i+1} {arg} : {← inferType arg}") m!", " + +/-- A linter for checking definition doc strings -/ +@[stdLinter] def docBlame : Linter where + noErrorsFound := "No definitions are missing documentation." + errorsFound := "DEFINITIONS ARE MISSING DOCUMENTATION STRINGS:" + test declName := do + if (← isAutoDecl declName) || isGlobalInstance (← getEnv) declName then + return none + if declName matches .str _ "parenthesizer" | .str _ "formatter" then + return none + let kind ← match ← getConstInfo declName with + | .axiomInfo .. => pure "axiom" + | .opaqueInfo .. => pure "constant" + | .defnInfo .. => pure "definition" + | .inductInfo .. => pure "inductive" + | _ => return none + let (none) ← findDocString? (← getEnv) declName | return none + return m!"{kind} missing documentation string" + +/-- A linter for checking theorem doc strings -/ +def docBlameThm : Linter where + noErrorsFound := "No theorems are missing documentation." + errorsFound := "THEOREMS ARE MISSING DOCUMENTATION STRINGS:" + test declName := do + if ← isAutoDecl declName then + return none + let kind ← match ← getConstInfo declName with + | .thmInfo .. => pure "theorem" + | _ => return none + let (none) ← findDocString? (← getEnv) declName | return none + return m!"{kind} missing documentation string" + +/-- A linter for checking whether the correct declaration constructor (definition or theorem) +has been used. -/ +@[stdLinter] def defLemma : Linter where + noErrorsFound := "All declarations correctly marked as def/lemma." + errorsFound := "INCORRECT DEF/LEMMA:" + test declName := do + if (← isAutoDecl declName) || isGlobalInstance (← getEnv) declName then + return none + if ← isProjectionFn declName then return none + let info ← getConstInfo declName + let isThm ← match info with + | .defnInfo .. => pure false + | .thmInfo .. => pure true + | _ => return none + match isThm, ← isProp info.type with + | true, false => pure "is a lemma/theorem, should be a def" + | false, true => pure "is a def, should be lemma/theorem" + | _, _ => return none + +/-- A linter for missing checking whether statements of declarations are well-typed. -/ +@[stdLinter] def checkType : Linter where + noErrorsFound := + "The statements of all declarations type-check with default reducibility settings." + errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK." + isFast := true + test declName := do + if ← isAutoDecl declName then return none + if ← isTypeCorrect (← getConstInfo declName).type then return none + return m!"the statement doesn't type check." + +/-- +`univParamsGrouped e` computes for each `level` `u` of `e` the parameters that occur in `u`, +and returns the corresponding set of lists of parameters. +In pseudo-mathematical form, this returns `{ { p : parameter | p ∈ u } | (u : level) ∈ e }` +FIXME: We use `Array Name` instead of `HashSet Name`, since `HashSet` does not have an equality instance. +It will ignore `nm₀.proof_i` declarations. +-/ +private def univParamsGrouped (e : Expr) (nm₀ : Name) : BaseIO (Std.HashSet (Array Name)) := do + let res ← IO.mkRef {} + e.forEach fun + | e@(Expr.sort ..) => + res.modify (·.insert (collectLevelParams {} e).params) + | e@(Expr.const n ..) => do + if let .str n s .. := n then + if n == nm₀ && s.startsWith "proof_" then + return + res.modify (·.insert (collectLevelParams {} e).params) + | _ => pure () + res.get + +/-- +The good parameters are the parameters that occur somewhere in the set as a singleton or +(recursively) with only other good parameters. +All other parameters in the set are bad. +-/ +private partial def badParams (l : Array (Array Name)) : Array Name := + let goodLevels := l.filterMap fun + | #[u] => some u + | _ => none + if goodLevels.isEmpty then + l.flatten.toList.eraseDups.toArray + else + badParams <| l.map (·.filter (!goodLevels.contains ·)) + +/-- A linter for checking that there are no bad `max u v` universe levels. +Checks whether all universe levels `u` in the type of `d` are "good". +This means that `u` either occurs in a `level` of `d` by itself, or (recursively) +with only other good levels. +When this fails, usually this means that there is a level `max u v`, where neither `u` nor `v` +occur by themselves in a level. It is ok if *one* of `u` or `v` never occurs alone. For example, +`(α : Type u) (β : Type (max u v))` is a occasionally useful method of saying that `β` lives in +a higher universe level than `α`. +-/ +@[stdLinter] def checkUnivs : Linter where + noErrorsFound := + "All declarations have good universe levels." + errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. " ++ +"This usually means that there is a `max u v` in the type where neither `u` nor `v` " ++ +"occur by themselves. Solution: Find the type (or type bundled with data) that has this " ++ +"universe argument and provide the universe level explicitly. If this happens in an implicit " ++ +"argument of the declaration, a better solution is to move this argument to a `variables` " ++ +"command (then it's not necessary to provide the universe level). +It is possible that this linter gives a false positive on definitions where the value of the " ++ +"definition has the universes occur separately, and the definition will usually be used with " ++ +"explicit universe arguments. In this case, feel free to add `@[nolint check_univs]`." + isFast := true + test declName := do + if ← isAutoDecl declName then return none + let bad := badParams (← univParamsGrouped (← getConstInfo declName).type declName).toArray + if bad.isEmpty then return none + return m!"universes {bad} only occur together." + +/-- A linter for checking that declarations aren't syntactic tautologies. +Checks whether a lemma is a declaration of the form `∀ a b ... z, e₁ = e₂` +where `e₁` and `e₂` are identical exprs. +We call declarations of this form syntactic tautologies. +Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts +with rfl when elaboration results in a different term than the user intended. -/ +@[stdLinter] def synTaut : Linter where + noErrorsFound := + "No declarations are syntactic tautologies." + errorsFound := "THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. " ++ +"This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are " ++ +"identical expressions. We call declarations of this form syntactic tautologies. " ++ +"Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving " ++ +"basic facts using `rfl`, when elaboration results in a different term than the user intended. " ++ +"You should check that the declaration really says what you think it does." + isFast := true + test declName := do + if ← isAutoDecl declName then return none + forallTelescope (← getConstInfo declName).type fun _ ty => do + let some (lhs, rhs) := ty.eq?.map (fun (_, l, r) => (l, r)) <|> ty.iff? + | return none + if lhs == rhs then + return m!"LHS equals RHS syntactically" + return none + +attribute [nolint synTaut] rfl + + +/-- +Return a list of unused have/suffices/let_fun terms in an expression. +This actually finds all beta-redexes. +-/ +def findUnusedHaves (e : Expr) : MetaM (Array MessageData) := do + let res ← IO.mkRef #[] + forEachExpr e fun e => do + let some e := letFunAnnotation? e | return + let Expr.app (Expr.lam n t b ..) _ .. := e | return + if n.getRoot == `_fun_discr then return + if b.hasLooseBVars then return + let msg ← addMessageContextFull m!"unnecessary have {n.eraseMacroScopes} : {t}" + res.modify (·.push msg) + res.get + +/-- A linter for checking that declarations don't have unused term mode have statements. We do not +tag this as `@[stdLlinter]` so that it is not in the default linter set as it is slow and an +uncommon problem. -/ +@[stdLinter] def unusedHavesSuffices : Linter where + noErrorsFound := "No declarations have unused term mode have statements." + errorsFound := "THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. " ++ + "In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not " ++ + "refer to `foo`. Such statements have no effect on the generated proof, and can just be " ++ + "replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions " ++ + "in proofs appear as if they are used. " ++ + "For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo` where" ++ + " `proof_of_goal` does not refer to `foo`. " ++ + "Such statements have no effect on the generated proof, and can just be replaced by " ++ + "`proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions in " ++ + "proofs appear as if they are used. " + test declName := do + if ← isAutoDecl declName then return none + let info ← getConstInfo declName + let mut unused ← findUnusedHaves info.type + if let some value := info.value? then + unused := unused ++ (← findUnusedHaves value) + unless unused.isEmpty do + return some <| .joinSep unused.toList ", " + return none + +/-- +A linter for checking if variables appearing on both sides of an iff are explicit. Ideally, such +variables should be implicit instead. +-/ +def explicitVarsOfIff : Linter where + noErrorsFound := "No explicit variables on both sides of iff" + errorsFound := "EXPLICIT VARIABLES ON BOTH SIDES OF IFF" + test declName := do + if ← isAutoDecl declName then return none + forallTelescope (← getConstInfo declName).type fun args ty => do + let some (lhs, rhs) := ty.iff? | return none + let explicit ← args.filterM fun arg => + return (← getFVarLocalDecl arg).binderInfo.isExplicit && + lhs.containsFVar arg.fvarId! && rhs.containsFVar arg.fvarId! + if explicit.isEmpty then return none + addMessageContextFull m!"should be made implicit: { + MessageData.joinSep (explicit.toList.map (m!"{·}")) ", "}" diff --git a/Std/Tactic/Lint/Simp.lean b/Std/Tactic/Lint/Simp.lean new file mode 100644 index 0000000000..1ee504dd90 --- /dev/null +++ b/Std/Tactic/Lint/Simp.lean @@ -0,0 +1,248 @@ +/- +Copyright (c) 2020 Gabriel Ebner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner +-/ +import Std.Tactic.Lint.Basic +import Std.Tactic.OpenPrivate +import Std.Util.LibraryNote +open Lean Meta + +namespace Std.Tactic.Lint + +/-! +# Linter for simplification lemmas + +This files defines several linters that prevent common mistakes when declaring simp lemmas: + + * `simpNF` checks that the left-hand side of a simp lemma is not simplified by a different lemma. + * `simpVarHead` checks that the head symbol of the left-hand side is not a variable. + * `simpComm` checks that commutativity lemmas are not marked as simplification lemmas. +-/ + +structure SimpTheoremInfo where + hyps : Array Expr + isConditional : Bool + lhs : Expr + rhs : Expr + +def isConditionalHyps (eq : Expr) : List Expr → MetaM Bool + | [] => pure false + | h :: hs => do + let ldecl ← getFVarLocalDecl h + if !ldecl.binderInfo.isInstImplicit + && !(← hs.anyM fun h' => do pure $ (← inferType h').containsFVar h.fvarId!) + && !eq.containsFVar h.fvarId! then + return true + isConditionalHyps eq hs + +open private preprocess from Lean.Meta.Tactic.Simp.SimpTheorems in +def withSimpTheoremInfos (ty : Expr) (k : SimpTheoremInfo → MetaM α) : MetaM (Array α) := withReducible do + (← preprocess (← mkSorry ty true) ty (inv := false) (isGlobal := true)) + |>.toArray.mapM fun (_, ty') => do + forallTelescopeReducing ty' fun hyps eq => do + let some (_, lhs, rhs) := eq.eq? | throwError "not an equality {eq}" + k { + hyps, lhs, rhs + isConditional := ← isConditionalHyps eq hyps.toList + } + +/-- Checks whether two expressions are equal for the simplifier. That is, +they are reducibly-definitional equal, and they have the same head symbol. -/ +def isSimpEq (a b : Expr) (whnfFirst := true) : MetaM Bool := withReducible do + let a ← if whnfFirst then whnf a else pure a + let b ← if whnfFirst then whnf b else pure b + if a.getAppFn.constName? != b.getAppFn.constName? then return false + isDefEq a b + +def checkAllSimpTheoremInfos (ty : Expr) (k : SimpTheoremInfo → MetaM (Option MessageData)) : MetaM (Option MessageData) := do + let errors := (← withSimpTheoremInfos ty fun i => do (← k i).mapM addMessageContextFull).filterMap id + if errors.isEmpty then + return none + else + return MessageData.joinSep errors.toList Format.line + +def isSimpTheorem (declName : Name) : MetaM Bool := do + pure $ (← getSimpTheorems).lemmaNames.contains declName + +open Lean.Meta.DiscrTree +partial def trieElements : Trie α → StateT (Array α) Id Unit + | Trie.node vs children => do + modify (· ++ vs) + for (_, child) in children do + trieElements child + +def elements (d : DiscrTree α) : StateT (Array α) Id Unit := do + for (_, child) in d.root.toList do + trieElements child + +open Std + +-- In Lean 4, the simplifier adds auxiliary lemmas if the declaration is not an equation. +-- For example, for `decl : a ↔ b` it generates `decl._auxLemma.1 : a = b`. +-- This function computes the map ``{`decl._auxLemma.1 ↦ `decl}`` +def constToSimpDeclMap (ctx : Simp.Context) : HashMap Name Name := Id.run do + let mut map : HashMap Name Name := {} + for sls' in ctx.simpTheorems do + for sls in [sls'.pre, sls'.post] do + for sl in ((elements sls).run #[]).2 do + if let some declName := sl.name? then + if let some auxDeclName := sl.proof.getAppFn.constName? then + map := map.insert auxDeclName declName + return map + +def isEqnLemma? (n : Name) : Option Name := + if n.isStr && n.getString!.startsWith "_eq_" then + n.getPrefix + else + none + +def heuristicallyExtractSimpTheoremsCore (ctx : Simp.Context) (constToSimpDecl : HashMap Name Name) (prf : Expr) : Array Name := Id.run do + let mut cnsts : HashSet Name := {} + for c in prf.getUsedConstants do + if ctx.simpTheorems.isDeclToUnfold c then + cnsts := cnsts.insert c + else if ctx.congrTheorems.lemmas.contains c then + cnsts := cnsts.insert c + else if let some c' := constToSimpDecl.find? c then + cnsts := cnsts.insert c' + else if let some c' := isEqnLemma? c then + cnsts := cnsts.insert c' + return cnsts.toArray + +@[inline] def heuristicallyExtractSimpTheorems (ctx : Simp.Context) (prf : Expr) : Array Name := + heuristicallyExtractSimpTheoremsCore ctx (constToSimpDeclMap ctx) prf + +def decorateError (msg : MessageData) (k : MetaM α) : MetaM α := do + try k catch e => throw (.error e.getRef m!"{msg}\n{e.toMessageData}") + +def formatLemmas (lems : Array Name) : CoreM MessageData := do + toMessageData <$> lems.mapM mkConstWithLevelParams + +/-- A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire. -/ +@[stdLinter] def simpNF : Linter where + noErrorsFound := "All left-hand sides of simp lemmas are in simp-normal form." + errorsFound := "SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM. +see note [simp-normal form] for tips how to debug this. +https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form" + + test := fun declName => do + unless ← isSimpTheorem declName do return none + -- TODO: equation lemmas + let ctx ← Simp.Context.mkDefault + let ctx := { ctx with config.decide := false } + checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do + let ⟨lhs', prf1, _⟩ ← decorateError "simplify fails on left-hand side:" <| simp lhs ctx + let prf1_lems := heuristicallyExtractSimpTheorems ctx (prf1.getD (mkBVar 0)) + if prf1_lems.contains declName then return none + let ⟨rhs', prf2, _⟩ ← decorateError "simplify fails on right-hand side:" <| simp rhs ctx + let lhs'_eq_rhs' ← isSimpEq lhs' rhs' (whnfFirst := false) + let lhs_in_nf ← isSimpEq lhs' lhs + if lhs'_eq_rhs' then do + if prf1.isNone then return none -- TODO: cannot detect used rfl-lemmas + if let .str _n "sizeOf_spec" := declName then + return none -- HACK: these often use rfl-lemmas but are not rfl + let used_lemmas := heuristicallyExtractSimpTheorems ctx <| + mkApp (prf1.getD (mkBVar 0)) (prf2.getD (mkBVar 0)) + return m!"simp can prove this: + by simp only {← formatLemmas used_lemmas} +One of the lemmas above could be a duplicate. +If that's not the case try reordering lemmas or adding @[priority]. +" + else if ¬ lhs_in_nf then do + return m!"Left-hand side simplifies from + {lhs} +to + {lhs'} +using + {← formatLemmas prf1_lems} +Try to change the left-hand side to the simplified term! +" + else if !isConditional && lhs == lhs' then + return m!"Left-hand side does not simplify. +You need to debug this yourself using `set_option trace.Meta.Tactic.simp.rewrite true`" + else + return none + +library_note "simp-normal form" /-- +This note gives you some tips to debug any errors that the simp-normal form linter raises. + +The reason that a lemma was considered faulty is because its left-hand side is not in simp-normal +form. +These lemmas are hence never used by the simplifier. + +This linter gives you a list of other simp lemmas: look at them! + +Here are some tips depending on the error raised by the linter: + + 1. 'the left-hand side reduces to XYZ': + you should probably use XYZ as the left-hand side. + + 2. 'simp can prove this': + This typically means that lemma is a duplicate, or is shadowed by another lemma: + + 2a. Always put more general lemmas after specific ones: + ``` + @[simp] lemma zero_add_zero : 0 + 0 = 0 := rfl + @[simp] lemma add_zero : x + 0 = x := rfl + ``` + + And not the other way around! The simplifier always picks the last matching lemma. + + 2b. You can also use `@[priority]` instead of moving simp-lemmas around in the file. + + Tip: the default priority is 1000. + Use `@[priority 1100]` instead of moving a lemma down, + and `@[priority 900]` instead of moving a lemma up. + + 2c. Conditional simp lemmas are tried last. If they are shadowed + just remove the `simp` attribute. + + 2d. If two lemmas are duplicates, the linter will complain about the first one. + Try to fix the second one instead! + (You can find it among the other simp lemmas the linter prints out!) + + 3. 'try_for tactic failed, timeout': + This typically means that there is a loop of simp lemmas. + Try to apply squeeze_simp to the right-hand side (removing this lemma from the simp set) to see + what lemmas might be causing the loop. + + Another trick is to `set_option trace.simplify.rewrite true` and + then apply `try_for 10000 { simp }` to the right-hand side. You will + see a periodic sequence of lemma applications in the trace message. +-/ + +/-- +A linter for simp lemmas whose lhs has a variable as head symbol, +and which hence never fire. +-/ +@[stdLinter] def simpVarHead : Linter where + noErrorsFound := + "No left-hand sides of a simp lemma has a variable as head symbol." + errorsFound := "LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL. +Some simp lemmas have a variable as head symbol of the left-hand side:" + test := fun declName => do + unless ← isSimpTheorem declName do return none + checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, ..} => do + let headSym := lhs.getAppFn + unless headSym.isFVar do return none + return m!"Left-hand side has variable as head symbol: {headSym}" + +/-- A linter for commutativity lemmas that are marked simp. -/ +@[stdLinter] def simpComm : Linter where + noErrorsFound := "No commutativity lemma is marked simp." + errorsFound := "COMMUTATIVITY LEMMA IS SIMP. +Some commutativity lemmas are simp lemmas:" + test := fun declName => withReducible do + unless ← isSimpTheorem declName do return none + let ty := (← getConstInfo declName).type + forallTelescopeReducing ty fun _ ty => do + let some (_, lhs, rhs) := ty.eq? | return none + unless lhs.getAppFn.constName? == rhs.getAppFn.constName? do return none + let (_, _, ty') ← forallMetaTelescopeReducing ty + let some (_, lhs', rhs') := ty'.eq? | return none + unless ← isDefEq rhs lhs' do return none + unless ← withNewMCtxDepth (isDefEq rhs lhs') do return none + -- ensure that the second application makes progress: + if ← isDefEq lhs' rhs' then return none + pure m!"should not be marked simp" diff --git a/Std/Tactic/OpenPrivate.lean b/Std/Tactic/OpenPrivate.lean new file mode 100644 index 0000000000..afdfd78b17 --- /dev/null +++ b/Std/Tactic/OpenPrivate.lean @@ -0,0 +1,125 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +import Lean.Elab.Command +import Lean.Util.FoldConsts + +open Lean Parser.Tactic Elab Command + +namespace Lean + +def Meta.collectPrivateIn [Monad m] [MonadEnv m] [MonadError m] + (n : Name) (set := NameSet.empty) : m NameSet := do + let c ← getConstInfo n + let traverse value := Expr.foldConsts value set fun c a => + if isPrivateName c then a.insert c else a + if let some value := c.value? then return traverse value + if let some c := (← getEnv).find? (n ++ `_cstage1) then + if let some value := c.value? then return traverse value + return traverse c.type + +def Environment.moduleIdxForModule? (env : Environment) (mod : Name) : Option ModuleIdx := + (env.allImportedModuleNames.indexOf? mod).map fun idx => idx.val + +instance : DecidableEq ModuleIdx := instDecidableEqNat + +def Environment.declsInModuleIdx (env : Environment) (idx : ModuleIdx) : List Name := + env.const2ModIdx.fold (fun acc n i => if i = idx then n :: acc else acc) [] + +namespace Elab.Command + +def elabOpenPrivateLike (ids : Array Syntax) (tgts mods : Option (Array Syntax)) + (f : (priv full user : Name) → CommandElabM Name) : CommandElabM Unit := do + let mut names := NameSet.empty + for tgt in tgts.getD #[] do + let n ← resolveGlobalConstNoOverload tgt + names ← Meta.collectPrivateIn n names + for mod in mods.getD #[] do + let some modIdx := (← getEnv).moduleIdxForModule? mod.getId + | throwError "unknown module {mod}" + for declName in (← getEnv).declsInModuleIdx modIdx do + if isPrivateName declName then + names := names.insert declName + let appendNames (msg : String) : String := Id.run do + let mut msg := msg + for c in names do + if let some name := privateToUserName? c then + msg := msg ++ s!"{name}\n" + msg + if ids.isEmpty && !names.isEmpty then + logInfo (appendNames "found private declarations:\n") + let mut decls := #[] + for n in ids do + let n := n.getId + let mut found := [] + for c in names do + if n.isSuffixOf c then + found := c::found + match found with + | [] => throwError (appendNames s!"'{n}' not found in the provided declarations:\n") + | [c] => + if let some name := privateToUserName? c then + let new ← f c name n + decls := decls.push (OpenDecl.explicit n new) + else unreachable! + | _ => throwError s!"provided name is ambiguous: found {found.map privateToUserName?}" + modifyScope fun scope => Id.run do + let mut openDecls := scope.openDecls + for decl in decls do + openDecls := decl::openDecls + { scope with openDecls := openDecls } + +syntax (name := openPrivate) "open private" ident* ("in" ident*)? ("from" ident*)? : command + +/-- +The command `open private a b c in foo bar` will look for private definitions named `a`, `b`, `c` +in declarations `foo` and `bar` and open them in the current scope. This does not make the +definitions public, but rather makes them accessible in the current section by the short name `a` +instead of the (unnameable) internal name for the private declaration, something like +`_private.Other.Module.0.Other.Namespace.foo.a`, which cannot be typed directly because of the `0` +name component. + +It is also possible to specify the module instead with +`open private a b c from Other.Module`. +-/ +@[commandElab openPrivate] def elabOpenPrivate : CommandElab +| `(open private $ids* $[in $tgts*]? $[from $mods*]?) => + elabOpenPrivateLike ids tgts mods fun c _ _ => pure c +| _ => throwUnsupportedSyntax + +syntax (name := exportPrivate) "export private" ident* ("in" ident*)? ("from" ident*)? : command + +/-- +The command `export private a b c in foo bar` is similar to `open private`, but instead of opening +them in the current scope it will create public aliases to the private definition. The definition +will exist at exactly the original location and name, as if the `private` keyword was not used +originally. + +It will also open the newly created alias definition under the provided short name, like +`open private`. +It is also possible to specify the module instead with +`export private a b c from Other.Module`. +-/ +@[commandElab exportPrivate] def elabExportPrivate : CommandElab +| `(export private $ids* $[in $tgts*]? $[from $mods*]?) => + elabOpenPrivateLike ids tgts mods fun c name _ => do + let cinfo ← getConstInfo c + if (← getEnv).contains name then + throwError s!"'{name}' has already been declared" + let decl := Declaration.defnDecl { + name := name, + levelParams := cinfo.levelParams, + type := cinfo.type, + value := mkConst c (cinfo.levelParams.map mkLevelParam), + hints := ReducibilityHints.abbrev, + safety := if cinfo.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe + } + addDecl decl + compileDecl decl + pure name +| _ => throwUnsupportedSyntax + +end Elab.Command +end Lean diff --git a/Std/Util/LibraryNote.lean b/Std/Util/LibraryNote.lean new file mode 100644 index 0000000000..1428c1e641 --- /dev/null +++ b/Std/Util/LibraryNote.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2022 Gabriel Ebner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner +-/ +import Lean + +/-! +# Define the `library_note` command. +-/ + +namespace Std.Util.LibraryNote + +open Lean + +/-- A library note consists of a (short) tag and a (long) note. -/ +def LibraryNoteEntry := String × String + +/-- Environment extension supporting `library_note`. -/ +initialize libraryNoteExt : SimplePersistentEnvExtension LibraryNoteEntry (Array LibraryNoteEntry) ← + registerSimplePersistentEnvExtension { + name := `library_note + addEntryFn := Array.push + addImportedFn := Array.concatMap id + } + +/-- Extract the doc-comment from a `Syntax`. -/ +-- TODO move? +def getDocCommentContent (stx : Syntax) : String := + let val := stx[1].getAtomVal! + val.extract 0 (val.endPos - ⟨2⟩) + +open Lean Parser Command in +/-- +``` +/-- ... some explanation ... -/ +library_note "some tag" +``` +creates a new "library note", which can then be cross-referenced using +``` +-- See note [some tag] +``` +in doc-comments. +-/ +elab "library_note " title:strLit ppSpace text:docComment : command => do + modifyEnv (libraryNoteExt.addEntry · (title.1.isStrLit?.get!, getDocCommentContent text)) diff --git a/Std/Util/TermUnsafe.lean b/Std/Util/TermUnsafe.lean new file mode 100644 index 0000000000..8b81d5bc85 --- /dev/null +++ b/Std/Util/TermUnsafe.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner +-/ +import Lean + +/-! +Defines term syntax to call unsafe functions. + +``` +def cool := + unsafe (unsafeCast () : Nat) + +#eval cool +``` +-/ + +namespace Std.TermUnsafe +open Lean Meta Elab Term + +def mkAuxName (hint : Name) : TermElabM Name := + withFreshMacroScope do + let name := (← getDeclName?).getD Name.anonymous ++ hint + pure $ addMacroScope (← getMainModule) name (← getCurrMacroScope) + +elab "unsafe " t:term : term <= expectedType => do + let mut t ← elabTerm t expectedType + t ← instantiateMVars t + if t.hasExprMVar then + synthesizeSyntheticMVarsNoPostponing + t ← instantiateMVars t + if ← logUnassignedUsingErrorInfos (← getMVars t) then throwAbortTerm + t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t + let Expr.const unsafeFn unsafeLvls .. := t.getAppFn | unreachable! + let ConstantInfo.defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable! + let implName ← mkAuxName `impl + addDecl <| Declaration.defnDecl { + name := implName + type := unsafeDefn.type + levelParams := unsafeDefn.levelParams + value := ← mkOfNonempty unsafeDefn.type + hints := ReducibilityHints.opaque + safety := DefinitionSafety.safe + } + setImplementedBy implName unsafeFn + pure $ mkAppN (mkConst implName unsafeLvls) t.getAppArgs diff --git a/bors.toml b/bors.toml new file mode 100644 index 0000000000..1060ad4878 --- /dev/null +++ b/bors.toml @@ -0,0 +1,6 @@ +status = ["Build"] +use_squash_merge = true +timeout_sec = 28800 +block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR", "merge-conflict"] +delete_merged_branches = true +cut_body_after = "---" diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000000..8f84d5e471 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,13 @@ +import Lake + +open Lake DSL + +package std + +@[defaultTarget] +lean_lib Std + +@[defaultTarget] +lean_exe runLinter where + root := `scripts.runLinter + supportInterpreter := true diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000000..3a7df6c313 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2022-08-30 diff --git a/scripts/runLinter.lean b/scripts/runLinter.lean new file mode 100644 index 0000000000..7643038397 --- /dev/null +++ b/scripts/runLinter.lean @@ -0,0 +1,60 @@ +import Std.Tactic.Lint +import Std.Data.Array.Defs + +open Lean Core Elab Command Std.Tactic.Lint + +abbrev NoLints := Array (Name × Name) + +def readJsonFile (α) [FromJson α] (path : System.FilePath) : IO α := do + let _ : MonadExceptOf String IO := ⟨throw ∘ IO.userError, fun x _ => x⟩ + liftExcept <| fromJson? <|<- liftExcept <| Json.parse <|<- IO.FS.readFile path + +def writeJsonFile (α) [ToJson α] (path : System.FilePath) (a : α) : IO Unit := + IO.FS.writeFile path <| toJson a |>.pretty + +open System in +instance : ToExpr FilePath where + toTypeExpr := mkConst ``FilePath + toExpr path := mkApp (mkConst ``FilePath.mk) (toExpr path.1) + +elab "compileTimeSearchPath" : term => + return toExpr (← searchPathRef.get) + +unsafe def main (args : List String) : IO Unit := do + let (update, args) := + match args with + | "--update" :: args => (true, args) + | _ => (false, args) + let some module := + match args with + | [] => some `Std + | [mod] => Syntax.decodeNameLit s!"`{mod}" + | _ => none + | IO.eprintln "Usage: runLinter [--update] [Std.Data.Nat]" *> IO.Process.exit 1 + let nolintsFile := "scripts/nolints.json" + let nolints ← readJsonFile NoLints nolintsFile + searchPathRef.set compileTimeSearchPath + withImportModules [{module}] {} (trustLevel := 1024) fun env => + let ctx := {fileName := "", fileMap := default} + let state := {env} + Prod.fst <$> (CoreM.toIO · ctx state) do + let decls ← getDeclsInPackage `Std + let linters ← getChecks (slow := true) (extra := []) (useOnly := false) + let results ← lintCore decls linters.toArray + if update then + writeJsonFile NoLints nolintsFile <| + .qsort (lt := fun (a,b) (c,d) => a.lt c || (a == c && b.lt d)) <| + .flatten <| results.map fun (linter, decls) => + decls.fold (fun res decl _ => res.push (linter.name, decl)) #[] + let results := results.map fun (linter, decls) => + .mk linter <| nolints.foldl (init := decls) fun decls (linter', decl') => + if linter.name == linter' then decls.erase decl' else decls + let failed := results.any (!·.2.isEmpty) + if failed then + let fmtResults ← + formatLinterResults results decls (groupByFilename := true) + "in Std" (runSlowLinters := true) .medium linters.length + IO.print (← fmtResults.toString) + IO.Process.exit 1 + else + IO.print "-- Linting passed." diff --git a/test/hello.lean b/test/hello.lean new file mode 100644 index 0000000000..e69de29bb2