diff --git a/GNUmakefile b/GNUmakefile index 6342e5b7c6..a8ea2d849e 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -1,5 +1,8 @@ TESTS = $(wildcard test/*.lean) +# Ensure that panics actually cause the tests to fail +export LEAN_ABORT_ON_PANIC=1 + .PHONY: all build test lint all: build test diff --git a/Std/Linter/UnreachableTactic.lean b/Std/Linter/UnreachableTactic.lean index 1da37ef564..d526c359af 100644 --- a/Std/Linter/UnreachableTactic.lean +++ b/Std/Linter/UnreachableTactic.lean @@ -94,8 +94,11 @@ def unreachableTacticLinter : Linter where run := withSetOptionIn fun stx => do if (← get).messages.hasErrors then return let cats := (Parser.parserExtension.getState (← getEnv)).categories - let tactics := cats.find! `tactic |>.kinds - let convs := cats.find! `conv |>.kinds + -- These lookups may fail when the linter is run in a fresh, empty environment + let some tactics := Parser.ParserCategory.kinds <$> cats.find? `tactic + | return + let some convs := Parser.ParserCategory.kinds <$> cats.find? `conv + | return let trees ← getInfoTrees let go : M Unit := do getTactics (← ignoreTacticKindsRef.get) (fun k => tactics.contains k || convs.contains k) stx diff --git a/test/lint_empty.lean b/test/lint_empty.lean new file mode 100644 index 0000000000..831a66895a --- /dev/null +++ b/test/lint_empty.lean @@ -0,0 +1,45 @@ +import Std +import Lean.Elab + +set_option linter.all true + +/-- Some syntax to elaborate in a fresh env -/ +def natDef : String := +"prelude + +inductive Nat where + | zero + | succ (n : Nat) : Nat + +def id (x : α) := x +" + +open Lean Parser Elab in +/-- +Test that the linters imported from Std all work when run on a declaration in an empty environment. + +This runs the linters because there's a global IO.Ref that contains them, rather than having them +be in a field of the environment itself, precisely so they can run in situations like this. However, +a linter that assumes it's run in an environment with the Lean prelude available may use of things +like `find!` and `get!` in linters, with the result that the linter panics. + +This test elaborates the definition of the natural numbers and the identity function in a fresh +environment with all linters enabled. Running the tests in an environment with `LEAN_ABORT_ON_PANIC` +set ensures that the linters can at least run. +-/ +elab "#testInEmptyEnv" : command => do + let context := mkInputContext natDef "test" + let (header, state, msgs) ← parseHeader context + let opts := Options.empty |>.setBool `linter.all true + let (env, msgs) ← processHeader header opts msgs context + if msgs.hasErrors then + for msg in msgs.toList do logMessage msg + liftM (m := IO) <| throw <| IO.userError "Errors in header" + let cmdState := Command.mkState env msgs + let s ← IO.processCommands context state cmdState + for t in s.commandState.infoState.trees do + pushInfoTree t + for msg in s.commandState.messages.toList do + logMessage msg + +#testInEmptyEnv