mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
134 lines
3.7 KiB
Lean4
134 lines
3.7 KiB
Lean4
module
|
||
|
||
meta import Lean.ErrorExplanation
|
||
import Lean.Meta.Basic
|
||
import all Lean.Language.Basic
|
||
open Lean Meta
|
||
|
||
/-!
|
||
# Error explanation non-interactive elaboration tests
|
||
|
||
Tests the elaborators for `register_error_explanation` and named-error macros.
|
||
-/
|
||
|
||
/-! ## Name and metadata -/
|
||
|
||
def dummyMetadata : ErrorExplanation.Metadata := {
|
||
summary := "A removed error"
|
||
sinceVersion := "4.21.0"
|
||
}
|
||
|
||
/-- Example -/
|
||
register_error_explanation lean.foo {
|
||
summary := "A removed error."
|
||
sinceVersion := "4.0.0"
|
||
removedVersion? := "4.21.0"
|
||
}
|
||
|
||
/-- error: Cannot add explanation: An error explanation already exists for `lean.foo` -/
|
||
#guard_msgs in
|
||
/-- Duplicate -/
|
||
register_error_explanation lean.foo dummyMetadata
|
||
|
||
/--
|
||
error: Invalid name `TopLevelName`: Error explanation names must have two components
|
||
|
||
Note: The first component of an error explanation name identifies the package from which the error originates, and the second identifies the error itself.
|
||
-/
|
||
#guard_msgs in
|
||
/-- Invalid -/
|
||
register_error_explanation TopLevelName dummyMetadata
|
||
|
||
macro "register_bad_error_explanation" : command =>
|
||
`(/-- -/ register_error_explanation Lean.MacroScoped { summary := "", sinceVersion := "" })
|
||
/--
|
||
error: Invalid name `Lean.MacroScoped✝`: Error explanations cannot have inaccessible names. This error often occurs when an error explanation is generated using a macro.
|
||
-/
|
||
#guard_msgs in
|
||
register_bad_error_explanation
|
||
|
||
/-- Example -/
|
||
register_error_explanation lean.bar {
|
||
summary := "An error."
|
||
sinceVersion := "4.21.0"
|
||
}
|
||
|
||
/-- warning: The error name `lean.foo` was removed in Lean version 4.21.0 and should not be used. -/
|
||
#guard_msgs in
|
||
example : MetaM Unit := throwNamedError lean.foo "Error"
|
||
|
||
example : MetaM Unit := throwNamedError lean.bar "foo"
|
||
|
||
/-! ## Message data tests -/
|
||
|
||
def logErrorNames (x : MetaM Unit) : MetaM Unit := do
|
||
Core.setMessageLog {}
|
||
x
|
||
let log ← Core.getMessageLog
|
||
let mut newLog := {}
|
||
for msg in log.toArray do
|
||
newLog := newLog.add <|
|
||
if let some errorName := msg.errorName? then
|
||
{ msg with data := m!"({errorName}) " ++ msg.data }
|
||
else
|
||
msg
|
||
Core.setMessageLog newLog
|
||
|
||
/--
|
||
error: (lean.bar) Logged error
|
||
---
|
||
error: (lean.bar) Logged error with ref
|
||
---
|
||
warning: (lean.bar) Logged warning
|
||
---
|
||
warning: (lean.bar) Logged warning with ref
|
||
-/
|
||
#guard_msgs in
|
||
run_meta logErrorNames do
|
||
logNamedError lean.bar m!"Logged error"
|
||
logNamedErrorAt (← getRef) lean.bar m!"Logged error with ref"
|
||
logNamedWarning lean.bar m!"Logged warning"
|
||
logNamedWarningAt (← getRef) lean.bar m!"Logged warning with ref"
|
||
|
||
/-- error: (lean.bar) Thrown error -/
|
||
#guard_msgs in
|
||
run_meta logErrorNames do
|
||
try
|
||
throwNamedError lean.bar "Thrown error"
|
||
catch e =>
|
||
logError e.toMessageData
|
||
|
||
/-- error: (lean.bar) Thrown error with ref -/
|
||
#guard_msgs in
|
||
run_meta logErrorNames do
|
||
try
|
||
throwNamedErrorAt (← getRef) lean.bar "Thrown error with ref"
|
||
catch e =>
|
||
logError e.toMessageData
|
||
|
||
/-! # Message name in serialized output -/
|
||
|
||
def withReportedOutput (x : MetaM α) : MetaM Unit := do
|
||
Core.resetMessageLog
|
||
discard <| x
|
||
let (res, fileName) ← IO.FS.withIsolatedStreams do
|
||
let msgs := (← getThe Core.State).messages
|
||
let fileName := msgs.toList[0]!.fileName
|
||
discard <| Language.reportMessages msgs {} false {} 0
|
||
pure fileName
|
||
Core.resetMessageLog
|
||
-- We need to omit the path to the file, since that's host-dependent; also drop line
|
||
-- number to avoid noise
|
||
let dropped := res.splitOn fileName |>.map (fun (s : String) => s.dropWhile (· != ' '))
|
||
logInfo ("".toSlice.intercalate dropped)
|
||
|
||
/--
|
||
info: error(lean.bar): function is noncomputable
|
||
warning(lean.bar): function is noncomputable
|
||
-/
|
||
#guard_msgs in
|
||
run_meta withReportedOutput do
|
||
let msg := "function is noncomputable"
|
||
logNamedError lean.bar msg
|
||
logNamedWarning lean.bar msg
|