feat: termBeforeBy builtin parser

src/Lean/Parser/Term.lean

@@ -116,6 +116,12 @@ namespace Term
 def byTactic' := leading_parser
   "by " >> Tactic.tacticSeqIndentGt
 
+/-- `termBeforeBy` is defined as `withForbidden("by", term)`, which will parse a term but
+disallows `by` outside of a bracketing construct. This is used for parsers like `show p by ...`
+or `suffices p by ...`, where we do not want `p by ...` to be parsed as an application of `p` to a
+`by` block, which would otherwise be allowed. -/
+def termBeforeBy := withForbidden "by" termParser
+
 -- TODO: rename to e.g. `afterSemicolonOrLinebreak`
 def optSemicolon (p : Parser) : Parser :=
   ppDedent $ semicolonOrLinebreak >> ppLine >> p
@@ -214,10 +220,10 @@ def showRhs := fromTerm <|> byTactic'
 /-- A `sufficesDecl` represents everything that comes after the `suffices` keyword:
 an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
 @[builtin_doc] def sufficesDecl := leading_parser
-  (atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termParser >> ppSpace >> showRhs
+  (atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termBeforeBy >> ppSpace >> showRhs
 @[builtin_term_parser] def «suffices» := leading_parser:leadPrec
   withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
-@[builtin_term_parser] def «show»     := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
+@[builtin_term_parser] def «show»     := leading_parser:leadPrec "show " >> termBeforeBy >> ppSpace >> showRhs
 /--
 `@x` disables automatic insertion of implicit parameters of the constant `x`.
 `@e` for any term `e` also disables the insertion of implicit lambdas at this position.
@@ -444,7 +450,7 @@ def letEqnsDecl := leading_parser (withAnonymousAntiquot := false)
   -- Remark: we disable anonymous antiquotations here to make sure
   -- anonymous antiquotations (e.g., `$x`) are not `letDecl`
   notFollowedBy (nonReservedSymbol "rec") "rec" >>
-  (letPatDecl true <|> letIdDecl <|> letPatDecl <|> letEqnsDecl)
+  withoutForbidden (letPatDecl true <|> letIdDecl <|> letPatDecl <|> letEqnsDecl)
 /--
 `+nondep` elaborates as a nondependent `let`, a `have` expression.
 -/
@@ -1036,6 +1042,7 @@ builtin_initialize
   register_parser_alias attrKind
   register_parser_alias optSemicolon
   register_parser_alias structInstFields
+  register_parser_alias termBeforeBy
 
 end Parser
 end Lean

src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;