Skip to content

Commit

Permalink
chore: bump to latest nightly and Verso (#290)
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen authored Feb 6, 2025
1 parent 4ac3704 commit 50706bb
Show file tree
Hide file tree
Showing 10 changed files with 14 additions and 10 deletions.
2 changes: 2 additions & 0 deletions Manual/BasicTypes/Int.lean
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ open Manual.FFIDocType

open Verso.Genre Manual

set_option maxHeartbeats 300000

#doc (Manual) "Integers" =>
%%%
tag := "Int"
Expand Down
2 changes: 2 additions & 0 deletions Manual/Classes/BasicClasses.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ open Manual
open Verso.Genre
open Verso.Genre.Manual

set_option maxHeartbeats 300000

#doc (Manual) "Basic Classes" =>
%%%
tag := "basic-classes"
Expand Down
4 changes: 2 additions & 2 deletions Manual/Meta/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ def ValDesc.nat [Monad m] [MonadError m] : ValDesc m Nat where
| .num n => pure n.getNat
| other => throwError "Expected string, got {repr other}"

def ValDesc.inlinesString : ValDesc m (FileMap × Array Syntax) where
def ValDesc.inlinesString : ValDesc m (FileMap × TSyntaxArray `inline) where
description := m!"a string that contains a sequence of inline elements"
get
| .str s => open Lean.Parser in do
Expand All @@ -40,7 +40,7 @@ def ValDesc.inlinesString : ValDesc m (FileMap × Array Syntax) where
if s'.allErrors.isEmpty then
if s'.stxStack.size = 1 then
match s'.stxStack.back with
| .node _ _ contents => pure (FileMap.ofString input, contents)
| .node _ _ contents => pure (FileMap.ofString input, contents.map (⟨·⟩))
| other => throwError "Unexpected syntax from Verso parser. Expected a node, got {other}"
else throwError "Unexpected internal stack size from Verso parser. Expected 1, got {s'.stxStack.size}"
else
Expand Down
4 changes: 2 additions & 2 deletions Manual/Meta/Example.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ def Block.example (name : Option String) : Block where
data := ToJson.toJson (name, (none : Option Tag))

structure ExampleConfig where
description : FileMap × Array Syntax
description : FileMap × TSyntaxArray `inline
/-- Name for refs -/
tag : Option String := none
keep : Bool := false
Expand All @@ -44,7 +44,7 @@ def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α → m β)
out := out.qsort (fun (i, _) (j, _) => i < j)
return out.map (·.2)

def isLeanBlock : Syntax → CoreM Bool
def isLeanBlock : TSyntax `block → CoreM Bool
| `(block|```$nameStx:ident $_args*|$_contents:str```) => do
let name ← realizeGlobalConstNoOverloadWithInfo nameStx
return name == ``lean
Expand Down
2 changes: 1 addition & 1 deletion Manual/Meta/Figure.lean
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ def Block.figure (name : Option String) : Block where
data := ToJson.toJson (name, (none : Option Tag))

structure FigureConfig where
caption : FileMap × Array Syntax
caption : FileMap × TSyntaxArray `inline
/-- Name for refs -/
name : Option String := none

Expand Down
2 changes: 1 addition & 1 deletion Manual/Meta/LakeToml.lean
Original file line number Diff line number Diff line change
Expand Up @@ -796,7 +796,7 @@ def lakeToml : DirectiveExpander

discard <| expectString "elaborated configuration" expectedStr v (useLine := (·.any (!·.isWhitespace)))

contents.mapM elabBlock
contents.mapM (elabBlock ⟨·⟩)

@[role_expander tomlField]
def tomlFieldInline : RoleExpander
Expand Down
2 changes: 1 addition & 1 deletion Manual/Meta/Syntax.lean
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ structure FreeSyntaxConfig where
name : Name
«open» : Bool := true
label : String := "syntax"
title : Option (FileMap × Array Syntax) := none
title : Option (FileMap × TSyntaxArray `inline) := none

structure SyntaxConfig extends FreeSyntaxConfig where
aliases : List Name := []
Expand Down
2 changes: 1 addition & 1 deletion Manual/Tactics/Reference.lean
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ set_option pp.rawOnError true

set_option linter.unusedVariables false


set_option maxHeartbeats 300000

#doc (Manual) "Tactic Reference" =>
%%%
Expand Down
2 changes: 1 addition & 1 deletion lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "b79b06e8a36f249c0bb8f778518c231b204cbde8",
"rev": "f7423ce560d2b39bca9e67ca355aed2b2a6d39be",
"name": "verso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.17.0-rc1
leanprover/lean4:nightly-2025-02-06

0 comments on commit 50706bb

Please sign in to comment.