Merge pull request #55 from leanprover/update-lean

update compiler and lake
main
Henrik Böving 2022-06-19 16:46:26 +02:00 committed by GitHub
commit e485bec9a6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 65 additions and 43 deletions

View File

@ -32,9 +32,9 @@ Provides a way to include the contents of a file at compile time as a String.
This is used to include things like the CSS and JS in the binary so we
don't have to carry them around as files.
-/
@[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do
@[termElab includeStr] def includeStrImpl : TermElab := λ stx _ => do
let str := stx[1].isStrLit?.get!
let srcPath := (FilePath.mk (← read).fileName)
let srcPath := FilePath.mk $ ←getFileName
let currentDir ← IO.currentDir
-- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory.
if let some path ← match srcPath.parent with

View File

@ -21,18 +21,19 @@ as well as all the dependencies.
-/
def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
let (leanInstall?, lakeInstall?) ← Lake.findInstall?
let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO'
match res with
| Except.ok (ws, options) =>
let lean := leanInstall?.get!
match Lake.Cli.mkLakeConfig {leanInstall?, lakeInstall?} with
| Except.ok config =>
let ws ← Lake.LogT.run Lake.MonadLog.eio (Lake.loadWorkspace config)
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 := lakeInstall?.get!
let lake := config.lakeInstall
let ctx ← Lake.mkBuildContext ws lean lake
ws.root.buildImportsAndDeps imports |>.run Lake.LogMethods.eio ctx
ws.root.buildImportsAndDeps imports |>.run Lake.MonadLog.eio ctx
initSearchPath (←findSysroot) ws.leanPaths.oleanPath
pure $ Except.ok (ws, lean.githash)
| Except.error rc => pure $ Except.error rc
| Except.error err =>
throw $ IO.userError err.toString
/--
Load a list of modules from the current Lean search path into an `Environment`
@ -40,8 +41,15 @@ to process for documentation.
-/
def load (imports : List Name) : IO Process.AnalyzerResult := do
let env ← importModules (List.map (Import.mk · false) imports) Options.empty
-- TODO parameterize maxHeartbeats
IO.println "Processing modules"
Prod.fst <$> Meta.MetaM.toIO Process.process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
let config := {
-- TODO: parameterize maxHeartbeats
maxHeartbeats := 100000000,
options := ⟨[(`pp.tagAppFns, true)]⟩,
-- TODO: Figure out whether this could cause some bugs
fileName := default,
fileMap := default,
}
Prod.fst <$> Meta.MetaM.toIO Process.process config { env := env} {} {}
end DocGen4

View File

@ -63,7 +63,7 @@ def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option
for pkg in ws.packageArray do
for dep in pkg.dependencies do
let value := match dep.src with
| Lake.Source.git url commit => (getGithubBaseUrl url, commit)
| Lake.Source.git url commit => (getGithubBaseUrl url, commit.getD "main")
-- TODO: What do we do here if linking a source is not possible?
| _ => ("https://example.com", "master")
gitMap := gitMap.insert dep.name value
@ -75,7 +75,7 @@ def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option
let basic := if root == `Lean root == `Init root == `Std then
s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
else
match ws.packageForModule? module with
match ws.packageArray.find? (·.isLocalModule module) with
| some pkg =>
let (baseUrl, commit) := gitMap.find! pkg.name
s!"{baseUrl}/blob/{commit}/{path}.lean"

View File

@ -78,7 +78,7 @@ def order (l r : ModuleMember) : Bool :=
def getName : ModuleMember → Name
| docInfo i => i.getName
| modDoc i => Name.anonymous
| modDoc _ => Name.anonymous
def getDocString : ModuleMember → Option String
| docInfo i => i.getDocString
@ -102,7 +102,13 @@ def process : MetaM AnalyzerResult := do
for cinfo in env.constants.toList do
try
let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
let config := {
maxHeartbeats := 5000000,
options := ←getOptions,
fileName := ←getFileName,
fileMap := ←getFileMap
}
let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) config { env := env} {} {}
if let some dinfo ← analysis then
let some modidx := env.getModuleIdxFor? dinfo.getName | unreachable!
let moduleName := env.allImportedModuleNames.get! modidx

View File

@ -76,7 +76,7 @@ structure TheoremInfo extends Info
deriving Inhabited
/--
Information about a `constant` declaration.
Information about an `opaque` declaration.
-/
structure OpaqueInfo extends Info where
/--
@ -84,7 +84,7 @@ structure OpaqueInfo extends Info where
-/
value : CodeWithInfos
/--
A value of partial is interpreted as this constant being part of a partial def
A value of partial is interpreted as this opaque being part of a partial def
since the actual definition for a partial def is hidden behind an inaccessible value.
-/
unsafeInformation : DefinitionSafety

View File

@ -46,7 +46,7 @@ def getName : DocInfo → Name
def getKind : DocInfo → String
| axiomInfo _ => "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo _ => "constant"
| opaqueInfo _ => "opaque"
| definitionInfo _ => "def"
| instanceInfo _ => "instance"
| inductiveInfo _ => "inductive"
@ -165,8 +165,8 @@ def getKindDescription : DocInfo → String
| theoremInfo _ => "theorem"
| opaqueInfo i =>
match i.unsafeInformation with
| DefinitionSafety.safe => "constant"
| DefinitionSafety.unsafe => "unsafe constant"
| DefinitionSafety.safe => "opaque"
| DefinitionSafety.unsafe => "unsafe opaque"
| DefinitionSafety.partial => "partial def"
| definitionInfo i => Id.run do
if i.hints.isAbbrev then

View File

@ -1,25 +1,27 @@
import Lake
open Lake DSL
package «doc-gen4» {
-- add configuration options here
package «doc-gen4»
lean_lib DocGen4
@[defaultTarget]
lean_exe «doc-gen4» {
root := `Main
supportInterpreter := true
dependencies := #[
{
name := `CMark
src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4fa0f8864502dc9e661d437be842d29d708"
},
{
name := `Unicode
src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64"
},
{
name := `Cli
src := Source.git "https://github.com/mhuisi/lean4-cli" "159a20e5e165b1bbe070594b5969d8147241bb04"
},
{
name := `lake
src := Source.git "https://github.com/leanprover/lake" "cb0eab4cbcfe58090b3c739e1e90982804597704"
}
]
}
require CMark from git
"https://github.com/xubaiw/CMark.lean" @ "b3848a9c7781b3a0dda4d78b62a7f15a7941462d"
require Unicode from git
"https://github.com/hargonix/Unicode.lean" @ "6a9614063815061150e34503db1140f09ea9edb6"
require Cli from git
"https://github.com/hargonix/lean4-cli" @ "f8fe306d00b31cdfcf5d24e6c0d050e34bec6bb0"
require lake from git
"https://github.com/leanprover/lake" @ "12e2463b35829368a59d18a5504dd2f73ac1621d"
require leanInk from git
"https://github.com/leanprover/LeanInk" @ "0a160d91458c1873937449a7c78d25b34b8686df"

View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-05-27
leanprover/lean4:nightly-2022-06-17

View File

@ -376,7 +376,7 @@ main h2, main h3, main h4, main h5, main h6 {
border-top: 2px solid #8fe388;
}
.axiom, .constant {
.axiom, .opaque {
border-left: 10px solid #f44708;
border-top: 2px solid #f44708;
}
@ -417,7 +417,7 @@ main h2, main h3, main h4, main h5, main h6 {
box-shadow: 0 0 0 1px hsla(115, 62%, calc(100% - 5%*(var(--fn) + 1)));
border-radius: 5px;
}
.axiom .fn:hover, .constant .fn:hover {
.axiom .fn:hover, .opaque .fn:hover {
background-color: hsla(16, 94%, calc(100% - 5%*var(--fn)));
box-shadow: 0 0 0 1px hsla(16, 94%, calc(100% - 5%*(var(--fn) + 1)));
border-radius: 5px;
@ -542,10 +542,16 @@ a:hover {
}
.gh_link {
float: right;
margin-left: 10px;
}
.ink_link {
float: right;
margin-left: 20px;
}
.docfile h2, .note h2 {
margin-block-start: 3px;
margin-block-end: 0px;