chore: update lean nightly

main
Henrik Böving 2022-07-03 15:35:21 +02:00
parent 1f6ab11ead
commit 351cbc56b6
4 changed files with 14 additions and 12 deletions

View File

@ -23,13 +23,13 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str
let (leanInstall?, lakeInstall?) ← Lake.findInstall?
match Lake.Cli.mkLakeConfig {leanInstall?, lakeInstall?} with
| Except.ok config =>
let ws ← Lake.LogT.run Lake.MonadLog.eio (Lake.loadWorkspace config)
let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio
let lean := config.leanInstall
if lean.githash ≠ Lean.githash then
IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}"
let lake := config.lakeInstall
let ctx ← Lake.mkBuildContext ws lean lake
ws.root.buildImportsAndDeps imports |>.run Lake.MonadLog.eio ctx
(ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx
initSearchPath (←findSysroot) ws.leanPaths.oleanPath
pure $ Except.ok (ws, lean.githash)
| Except.error err =>

View File

@ -97,9 +97,9 @@ syntax jsxElement : jsxChild
scoped syntax:max jsxElement : term
def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
def translateAttrs (attrs : Array (TSyntax `DocGen4.Jsx.jsxAttr)) : MacroM (TSyntax `term) := do
let mut as ← `(#[])
for attr in attrs do
for attr in attrs.map TSyntax.raw do
as ← match attr with
| `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
let n ← match n with
@ -115,13 +115,13 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
| _ => Macro.throwUnsupported
return as
private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × Syntax):= do
private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × (TSyntax `term)):= do
unless n.getId == m.getId do
withRef m <| Macro.throwError s!"Leading and trailing part of tags don't match: '{n}', '{m}'"
let mut cs ← `(#[])
for child in children do
cs ← match child with
| `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t[0].getAtomVal!)))
| `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t.raw[0].getAtomVal!)))
-- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
| `(jsxChild|{$t}) => `(($cs).push ($t : Html))
| `(jsxChild|[$t]) => `($cs ++ ($t : Array Html))
@ -132,7 +132,9 @@ private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : Mac
macro_rules
| `(<$n $attrs* />) => do
`(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[])
let kind := quote (toString n.getId)
let attrs ← translateAttrs attrs
`(Html.element $kind true $attrs #[])
| `(<$n $attrs* >$children*</$m>) => do
let (tag, children) ← htmlHelper n children m
`(Html.element $(quote tag) true $(← translateAttrs attrs) $children)

View File

@ -12,16 +12,16 @@ lean_exe «doc-gen4» {
}
require CMark from git
"https://github.com/xubaiw/CMark.lean" @ "b3848a9c7781b3a0dda4d78b62a7f15a7941462d"
"https://github.com/xubaiw/CMark.lean" @ "192939e27263b0932700ade3442e1bf2ce67c3a6"
require Unicode from git
"https://github.com/hargonix/Unicode.lean" @ "603450c82cf5066c6db6df0e8ee115f93d71f5fb"
"https://github.com/hargonix/Unicode.lean" @ "b73232aeefd6391951f9bd256e3dc4ec937c7238"
require Cli from git
"https://github.com/hargonix/lean4-cli" @ "f8fe306d00b31cdfcf5d24e6c0d050e34bec6bb0"
"https://github.com/mhuisi/lean4-cli" @ "f7590ce072b0321752a7b9942892d0104dee4036"
require lake from git
"https://github.com/leanprover/lake" @ "12e2463b35829368a59d18a5504dd2f73ac1621d"
"https://github.com/leanprover/lake" @ "401e738e4ca989ced8d9bb0cf7f66be9133fc435"
require leanInk from git
"https://github.com/hargonix/LeanInk" @ "doc-gen"

View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-06-24
leanprover/lean4:nightly-2022-06-30