chore: work with newer Lean core

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/subverso.git",
    "type": "git",
    "subDir": null,
-   "rev": "771681e14ea506d41aa0c6969ba3a34727d64ab0",
+   "rev": "9f51556e14f14fbf7880b69e3cb1654e60ab66a2",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc1
+leanprover/lean4:nightly-2024-04-07

src/verso-blog/Verso/Genre/Blog.lean

@@ -66,7 +66,7 @@ def html : DirectiveExpander
 def blob : DirectiveExpander
   | #[.anon (.name blobName)], stxs => do
     if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
-    let actualName ← resolveGlobalConstNoOverloadWithInfo blobName
+    let actualName ← realizeGlobalConstNoOverloadWithInfo blobName
     let val ← ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
     pure #[val]
   | _, _ => throwUnsupportedSyntax
@@ -75,7 +75,7 @@ def blob : DirectiveExpander
 def inlineBlob : RoleExpander
   | #[.anon (.name blobName)], stxs => do
     if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
-    let actualName ← resolveGlobalConstNoOverloadWithInfo blobName
+    let actualName ← realizeGlobalConstNoOverloadWithInfo blobName
     let val ← ``(Inline.other (Blog.InlineExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
     pure #[val]
   | _, _ => throwUnsupportedSyntax
@@ -312,7 +312,7 @@ structure LeanBlockConfig where
   name : Option Name := none
   error : Option Bool := none
 
-def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : ArgParse m LeanBlockConfig :=
+def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanBlockConfig :=
   LeanBlockConfig.mk <$> .positional `exampleContext .ident <*> .named `show .bool true <*> .named `keep .bool true <*> .named `name .name true <*> .named `error .bool true
 
 @[code_block_expander leanInit]
@@ -405,7 +405,7 @@ structure LeanOutputConfig where
   severity : Option MessageSeverity
   summarize : Bool
 
-def LeanOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : ArgParse m LeanOutputConfig :=
+def LeanOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanOutputConfig :=
   LeanOutputConfig.mk <$> .positional `name output <*> .named `severity sev true <*> ((·.getD false) <$> .named `summarize .bool true)
 where
   output : ValDesc m Ident := {
@@ -420,7 +420,7 @@ where
     description := open MessageSeverity in m!"The expected severity: '{``error}', '{``warning}', or '{``information}'",
     get := open MessageSeverity in fun
       | .name b => do
-        let b' ← resolveGlobalConstNoOverloadWithInfo b
+        let b' ← realizeGlobalConstNoOverloadWithInfo b
         if b' == ``MessageSeverity.error then pure MessageSeverity.error
         else if b' == ``MessageSeverity.warning then pure MessageSeverity.warning
         else if b' == ``MessageSeverity.information then pure MessageSeverity.information
@@ -490,7 +490,7 @@ where
 
 open Lean Elab Command in
 elab "#defineLexerBlock" blockName:ident " ← " lexerName:ident : command => do
-  let lexer ← resolveGlobalConstNoOverloadWithInfo lexerName
+  let lexer ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo lexerName
   elabCommand <| ← `(@[code_block_expander $blockName]
     def $blockName : Doc.Elab.CodeBlockExpander
       | #[], str => do

src/verso/Verso/Doc/ArgParse.lean

@@ -23,8 +23,6 @@ structure ValDesc (α) where
   description : MessageData
   get : ArgVal → m α
 
-
-
 inductive ArgParse (m) : Type → Type 1 where
   | fail (stx? : Option Syntax) (message? : Option MessageData) : ArgParse m α
   | pure (val : α) : ArgParse m α
@@ -150,13 +148,13 @@ where
     return none
 end
 
-variable {m} [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m]
+variable {m} [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] [MonadLiftT CoreM m]
 
 def ValDesc.bool : ValDesc m Bool where
   description := m!"{true} or {false}"
   get
     | .name b => do
-      let b' ← resolveGlobalConstNoOverloadWithInfo b
+      let b' ← liftM <| realizeGlobalConstNoOverloadWithInfo b
       if b' == ``true then pure true
       else if b' == ``false then pure false
       else throwErrorAt b "Expected 'true' or 'false'"

src/verso/Verso/Doc/Concrete.lean

@@ -81,11 +81,19 @@ where
 @[combinator_formatter completeDocument] def completeDocument.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
 
-partial def findGenre [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m Unit
-  | `($g:ident) => discard <| resolveGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument
-  | `(($e)) => findGenre e
+open Lean.Elab Command in
+partial def findGenreCmd : Syntax → Lean.Elab.Command.CommandElabM Unit
+  | `($g:ident) => discard <| liftTermElabM <| realizeGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument
+  | `(($e)) => findGenreCmd e
   | _ => pure ()
 
+open Lean.Elab Term in
+partial def findGenreTm : Syntax → TermElabM Unit
+  | `($g:ident) => discard <| realizeGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument
+  | `(($e)) => findGenreTm e
+  | _ => pure ()
+
+
 def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM.State) : m Unit := do
   for r in internalRefs st'.linkDefs st.linkRefs do
     for stx in r.syntax do
@@ -95,7 +103,7 @@ def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM.
       pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
 
 elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:document ":::::::" : command => open Lean Elab Command PartElabM DocElabM in do
-  findGenre genre
+  findGenreCmd genre
   let endTok :=
     match ← getRef with
     | .node _ _ t =>
@@ -122,7 +130,7 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu
 
 
 elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do
-  findGenre genre
+  findGenreTm genre
   let endPos := eof.raw.getTailPos?.get!
   let .node _ _ blocks := text.raw
     | dbg_trace "nope {ppSyntax text.raw}" throwUnsupportedSyntax
@@ -162,7 +170,7 @@ def currentDocName [Monad m] [MonadEnv m] : m Name := do
 
 
 elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eoi : command => open Lean Elab Term Command PartElabM DocElabM in do
-  findGenre genre
+  findGenreCmd genre
   if eof.raw.isMissing then
     throwError "Syntax error prevents processing document"
   else

src/verso/Verso/Doc/Elab.lean

@@ -95,7 +95,7 @@ def _root_.Verso.Syntax.role.expand : InlineExpander
       withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
         let ⟨.node _ _ subjectArr⟩ := subjects
           | throwUnsupportedSyntax
-        let name ← resolveGlobalConstNoOverloadWithInfo name
+        let name ← realizeGlobalConstNoOverloadWithInfo name
         let exp ← roleExpandersFor name
         let argVals ← parseArgs args
         for e in exp do
@@ -292,7 +292,7 @@ def _root_.Verso.Syntax.block_role.expand : BlockExpander := fun block =>
   match block with
   | `(block|block_role{$name $args*}) => do
     withRef block <| withFreshMacroScope <| withIncRecDepth <| do
-      let name ← resolveGlobalConstNoOverloadWithInfo name
+      let name ← realizeGlobalConstNoOverloadWithInfo name
       let exp ← blockRoleExpandersFor name
       let argVals ← parseArgs args
       for e in exp do
@@ -394,7 +394,7 @@ def _root_.Verso.Syntax.blockquote.expand : BlockExpander
 @[block_expander Verso.Syntax.codeblock]
 def _root_.Verso.Syntax.codeblock.expand : BlockExpander
   | `<low|(Verso.Syntax.codeblock (column ~(.atom _ _col)) ~_open ~(.node _ `null #[nameStx, .node _ `null argsStx]) ~(.atom info contents) ~_close )> => do
-      let name ← resolveGlobalConstNoOverloadWithInfo nameStx
+      let name ← realizeGlobalConstNoOverloadWithInfo nameStx
       let exp ← codeBlockExpandersFor name
       -- TODO typed syntax here
       let args ← parseArgs <| argsStx.map (⟨·⟩)
@@ -417,7 +417,7 @@ def _root_.Verso.Syntax.codeblock.expand : BlockExpander
 @[block_expander Verso.Syntax.directive]
 def _root_.Verso.Syntax.directive.expand : BlockExpander
   | `<low|(Verso.Syntax.directive  ~_open ~nameStx ~(.node _ `null argsStx) ~_fake ~_fake' ~(.node _ `null contents) ~_close )> => do
-    let name ← resolveGlobalConstNoOverloadWithInfo nameStx
+    let name ← realizeGlobalConstNoOverloadWithInfo nameStx
     let exp ← directiveExpandersFor name
     -- TODO typed syntax here
     let args ← parseArgs <| argsStx.map (⟨·⟩)

src/verso/Verso/Doc/Elab/ExpanderAttribute.lean

@@ -15,7 +15,7 @@ unsafe def mkDocExpanderAttrUnsafe (attrName typeName : Name) (descr : String) (
     descr := descr,
     valueTypeName := typeName,
     evalKey := fun _ stx => do
-      Elab.resolveGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
       -- return (← Attribute.Builtin.getIdent stx).getId
   } attrDeclName
 

src/verso/Verso/Method.lean

@@ -49,7 +49,7 @@ def elabMethodDecl : CommandElab := fun stx => do
       | .node info ``method args => pure (some (.node info ``Parser.Command.declaration args))
       | _ => pure none
     let decl' := open Parser.Command in
-      Syntax.node .none ``declaration #[decl[0][0], .node .none ``«def» decl[0].args[1:7]]
+      Syntax.node .none ``declaration #[decl[0][0], .node .none ``definition decl[0].args[1:7]]
     elabCommand decl'
 where
   inRoot : Name → Name