feat: debug_assert! (#7256)

This PR introduces the `assert!` variant `debug_assert!` that is
activated when compiled with `buildType` `debug`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>

src/Lean/Elab/BuiltinNotation.lean

@@ -201,12 +201,27 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
 
 @[builtin_macro Lean.Parser.Term.assert]  def expandAssert : Macro
   | `(assert! $cond; $body) =>
-    -- TODO: support for disabling runtime assertions
     match cond.raw.reprint with
     | some code => `(if $cond then $body else panic! ("assertion violation: " ++ $(quote code)))
     | none => `(if $cond then $body else panic! ("assertion violation"))
   | _ => Macro.throwUnsupported
 
+register_builtin_option debugAssertions : Bool := {
+  defValue := false
+  descr := "enable `debug_assert!` statements\
+    \n\
+    \nDefaults to `false` unless the Lake `buildType` is `debug`."
+}
+
+@[builtin_term_elab Lean.Parser.Term.debugAssert]  def elabDebugAssert : TermElab :=
+  adaptExpander fun
+    | `(Parser.Term.debugAssert| debug_assert! $cond; $body) => do
+      if debugAssertions.get (← getOptions) then
+        `(assert! $cond; $body)
+      else
+        return body
+    | _ => throwUnsupportedSyntax
+
 @[builtin_macro Lean.Parser.Term.dbgTrace]  def expandDbgTrace : Macro
   | `(dbg_trace $arg:interpolatedStr; $body) => `(dbgTrace (s! $arg) fun _ => $body)
   | `(dbg_trace $arg:term; $body)            => `(dbgTrace (toString $arg) fun _ => $body)

src/Lean/Elab/Do.lean

@@ -1036,6 +1036,9 @@ def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := withRef action <| wit
   else if action.getKind == ``Parser.Term.doAssert then
     let cond := action[1]
     `(assert! $cond; $k)
+  else if action.getKind == ``Parser.Term.doDebugAssert then
+    let cond := action[1]
+    `(debugAssert| debug_assert! $cond; $k)
   else
     let action ← withRef action ``(($action : $((←read).m) PUnit))
     ``(Bind.bind $action (fun (_ : PUnit) => $k))
@@ -1765,6 +1768,8 @@ mutual
             return mkSeq doElem (← doSeqToCode doElems)
           else if k == ``Parser.Term.doAssert then
             return mkSeq doElem (← doSeqToCode doElems)
+          else if k == ``Parser.Term.doDebugAssert then
+            return mkSeq doElem (← doSeqToCode doElems)
           else if k == ``Parser.Term.doNested then
             let nestedDoSeq := doElem[1]
             doSeqToCode (getDoSeqElems nestedDoSeq ++ doElems)

src/Lean/Parser/Do.lean

@@ -51,7 +51,7 @@ def notFollowedByRedefinedTermToken :=
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
-      "do" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
+      "do" <|> "dbg_trace" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
 @[builtin_doElem_parser] def doLet      := leading_parser
@@ -200,6 +200,12 @@ It should only be used for debugging.
 -/
 @[builtin_doElem_parser] def doAssert    := leading_parser:leadPrec
   "assert! " >> termParser
+/--
+`debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
+with debug assertions enabled (see the `debugAssertions` option).
+-/
+@[builtin_doElem_parser] def doDebugAssert := leading_parser:leadPrec
+  "debug_assert! " >> termParser
 
 /-
 We use `notFollowedBy` to avoid counterintuitive behavior.

src/Lean/Parser/Term.lean

@@ -998,6 +998,12 @@ interpolated string literal) to stderr. It should only be used for debugging.
 /-- `assert! cond` panics if `cond` evaluates to `false`. -/
 @[builtin_term_parser] def assert := leading_parser:leadPrec
   withPosition ("assert! " >> termParser) >> optSemicolon termParser
+/--
+`debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
+with debug assertions enabled (see the `debugAssertions` option).
+-/
+@[builtin_term_parser] def debugAssert := leading_parser:leadPrec
+  withPosition ("debug_assert! " >> termParser) >> optSemicolon termParser
 
 def macroArg       := termParser maxPrec
 def macroDollarArg := leading_parser "$" >> termParser 10

src/lake/Lake/Config/LeanConfig.lean

@@ -233,3 +233,12 @@ structure LeanConfig where
   -/
   plugins : TargetArray Dynlib := #[]
 deriving Inhabited, Repr
+
+/-- The options to pass to `lean` based on the build type. -/
+def BuildType.leanOptions : BuildType → Array LeanOption
+| debug => #[{ name := `debugAssertions, value := true }]
+| _ => #[]
+
+/-- The arguments to pass to `lean` based on the build type. -/
+def BuildType.leanArgs (t : BuildType) : Array String :=
+  t.leanOptions.map (·.asCliArg)

src/lake/Lake/Config/LeanLib.lean

@@ -100,23 +100,24 @@ Otherwise, falls back to the package's.
 @[inline] def nativeFacets (self : LeanLib) (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
   self.config.nativeFacets shouldExport
 
+/--
+The build type for modules of this library.
+That is, the minimum of package's `buildType` and the library's  `buildType`.
+-/
+@[inline] def buildType (self : LeanLib) : BuildType :=
+  min self.pkg.buildType self.config.buildType
+
 /--
 The arguments to pass to `lean --server` when running the Lean language server.
 `serverOptions` is the accumulation of:
+- the build type's `leanOptions`
 - the package's `leanOptions`
 - the package's `moreServerOptions`
 - the library's `leanOptions`
 - the library's `moreServerOptions`
 -/
 @[inline] def serverOptions (self : LeanLib) : Array LeanOption :=
-  self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions
-
-/--
-The build type for modules of this library.
-That is, the minimum of package's `buildType` and the library's  `buildType`.
--/
-@[inline] def buildType (self : LeanLib) : BuildType :=
-  min self.pkg.buildType self.config.buildType
+  self.buildType.leanOptions ++ self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions
 
 /--
 The backend type for modules of this library.
@@ -143,13 +144,14 @@ The targets of the package plus the targets of the library (in that order).
 /--
 The arguments to pass to `lean` when compiling the library's Lean files.
 `leanArgs` is the accumulation of:
+- the build type's `leanArgs`
 - the package's `leanOptions`
 - the package's `moreLeanArgs`
 - the library's `leanOptions`
 - the library's `moreLeanArgs`
 -/
 @[inline] def leanArgs (self : LeanLib) : Array String :=
-  self.pkg.moreLeanArgs ++ self.config.leanOptions.map (·.asCliArg) ++ self.config.moreLeanArgs
+  self.buildType.leanArgs ++ self.pkg.moreLeanArgs ++ self.config.leanOptions.map (·.asCliArg) ++ self.config.moreLeanArgs
 
 /--
 The arguments to weakly pass to `lean` when compiling the library's Lean files.

tests/lean/1021.lean.expected.out

@@ -1,7 +1,7 @@
 some
   {
     range :=
-      { pos := { line := 202, column := 0 }, charUtf16 := 0, endPos := { line := 208, column := 31 },
+      { pos := { line := 202, column := 0 }, charUtf16 := 0, endPos := { line := 207, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
       { pos := { line := 202, column := 46 }, charUtf16 := 46, endPos := { line := 202, column := 58 },

tests/pkg/debug/Main.lean

@@ -0,0 +1,4 @@
+def main : IO Unit := do
+  assert! true
+  --debug_assert! true
+  debug_assert! false

tests/pkg/debug/lakefile.toml

@@ -0,0 +1,10 @@
+name = "debug"
+
+[[lean_exe]]
+name = "release"
+root = "Main"
+
+[[lean_exe]]
+name = "debug"
+root = "Main"
+buildType = "debug"

tests/pkg/debug/test.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+rm -rf .lake/build
+# should succeed
+lake exe release || exit 1
+# should fail
+lake exe debug && exit 1
+exit 0