chore: update toolchain and dependencies

main
Henrik Böving 2022-08-09 23:30:43 +02:00
parent 583e2299b7
commit d29e14a26a
10 changed files with 27 additions and 105 deletions

View File

@ -5,6 +5,5 @@ Authors: Henrik Böving
-/ -/
import DocGen4.Process import DocGen4.Process
import DocGen4.Load import DocGen4.Load
import DocGen4.IncludeStr
import DocGen4.Output import DocGen4.Output
import DocGen4.LeanInk import DocGen4.LeanInk

View File

@ -1,57 +0,0 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
namespace DocGen4
open Lean System IO Lean.Elab.Term FS
deriving instance DecidableEq for FileType
/--
Traverse all subdirectories fo `f` to find if one satisfies `p`.
-/
partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option FilePath) := do
if (← p f) then
return f
for d in (← System.FilePath.readDir f) do
let subDir := d.path
let metadata ← subDir.metadata
if metadata.type = FileType.dir then
if let some p ← traverseDir subDir p then
return p
return none
syntax (name := includeStr) "include_str" str : term
/--
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 _ => do
let str := stx[1].isStrLit?.get!
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
| some p => pure <| some <| p / str
| none => do
let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists
pure <| foundDir.map (· / str)
then
if ←path.pathExists then
if ←path.isDir then
throwError s!"{str} is a directory"
else
let content ← FS.readFile path
pure <| mkStrLit content
else
throwError s!"{path} does not exist as a file"
else
throwError s!"No such file in whole directory: {str}"
end DocGen4

View File

@ -23,13 +23,16 @@ def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
let (leanInstall?, lakeInstall?) ← Lake.findInstall? let (leanInstall?, lakeInstall?) ← Lake.findInstall?
match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
| .ok config => | .ok config =>
let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio let ws : Lake.Workspace ← Lake.loadWorkspace config
let libraryLeanGitHash := ws.env.lean.githash |>.run Lake.MonadLog.eio
|>.toIO (λ _ => IO.userError "Failed to load Lake workspace")
let libraryLeanGitHash := ws.lakeEnv.lean.githash
if libraryLeanGitHash ≠ Lean.githash then if libraryLeanGitHash ≠ Lean.githash then
IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}" IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}"
let ctx ← Lake.mkBuildContext ws let _libs ← ws.runBuild (Lake.buildImportsAndDeps imports) false
(ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx |>.run (Lake.MonadLog.eio config.verbosity)
initSearchPath (←findSysroot) ws.leanPaths.oleanPath |>.toIO (λ _ => IO.userError "Failed to compile imports via Lake")
initSearchPath (←findSysroot) (ws.packageList.map (·.oleanDir))
pure <| Except.ok ws pure <| Except.ok ws
| .error err => | .error err =>
throw <| IO.userError err.toString throw <| IO.userError err.toString

View File

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving Authors: Henrik Böving
-/ -/
import DocGen4.Process import DocGen4.Process
import DocGen4.IncludeStr
import DocGen4.Output.ToHtmlFormat import DocGen4.Output.ToHtmlFormat
namespace DocGen4.Output namespace DocGen4.Output

View File

@ -55,20 +55,18 @@ compiler release to work with this provides a function to turn names of
declarations into (optionally positional) Github URLs. declarations into (optionally positional) Github URLs.
-/ -/
def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do
let leanHash := ws.env.lean.githash let leanHash := ws.lakeEnv.lean.githash
-- Compute a map from package names to source URL -- Compute a map from package names to source URL
let mut gitMap := Std.mkHashMap let mut gitMap := Std.mkHashMap
let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl) let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
let projectCommit ← getProjectCommit let projectCommit ← getProjectCommit
gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit) gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
for pkg in ws.packageArray do let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile
for dep in pkg.dependencies do |>.run (Lake.MonadLog.eio .normal)
let value := match dep.src with |>.toIO (λ _ => IO.userError "Failed to load lake manifest")
-- TODO: subdir handling for pkg in manifest.toArray do
| Lake.Source.git url commit _ => (getGithubBaseUrl url, commit.getD "main") let value := (getGithubBaseUrl pkg.url, pkg.rev)
-- TODO: What do we do here if linking a source is not possible? gitMap := gitMap.insert pkg.name value
| _ => ("https://example.com", "master")
gitMap := gitMap.insert dep.name value
pure λ module range => pure λ module range =>
let parts := module.components.map Name.toString let parts := module.components.map Name.toString
@ -79,8 +77,9 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange
else else
match ws.packageArray.find? (·.isLocalModule module) with match ws.packageArray.find? (·.isLocalModule module) with
| some pkg => | some pkg =>
let (baseUrl, commit) := gitMap.find! pkg.name match gitMap.find? pkg.name with
s!"{baseUrl}/blob/{commit}/{path}.lean" | some (baseUrl, commit) => s!"{baseUrl}/blob/{commit}/{path}.lean"
| none => "https://example.com"
| none => "https://example.com" | none => "https://example.com"
match range with match range with

View File

@ -39,7 +39,7 @@ instance : ValueAttr EnumAttributes where
Obtain the value of a parametric attribute for a certain name. Obtain the value of a parametric attribute for a certain name.
-/ -/
def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do
let val ← ParametricAttribute.getParam attr env decl let val ← ParametricAttribute.getParam? attr env decl
some (attr.attr.name.toString ++ " " ++ toString val) some (attr.attr.name.toString ++ " " ++ toString val)
instance : ValueAttr ParametricAttribute where instance : ValueAttr ParametricAttribute where
@ -108,7 +108,6 @@ def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind
pure <| va.getValue attr env decl pure <| va.getValue attr env decl
def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
let env ← getEnv
let mut res := #[] let mut res := #[]
for attr in attrs do for attr in attrs do
if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then

View File

@ -25,8 +25,7 @@ where
def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let mut info ← DefinitionInfo.ofDefinitionVal v let mut info ← DefinitionInfo.ofDefinitionVal v
let some className := getClassName (←getEnv) v.type | unreachable! let some className ← isClass? v.type | unreachable!
if let some instAttr ← getDefaultInstance v.name className then if let some instAttr ← getDefaultInstance v.name className then
info := { info with attrs := info.attrs.push instAttr } info := { info with attrs := info.attrs.push instAttr }
let typeNames ← getInstanceTypes v.type let typeNames ← getInstanceTypes v.type

View File

@ -26,22 +26,3 @@ require lake from git
require leanInk from git require leanInk from git
"https://github.com/hargonix/LeanInk" @ "doc-gen-json" "https://github.com/hargonix/LeanInk" @ "doc-gen-json"
module_facet docs : FilePath := fun mod => do
let some docGen4 ← findLeanExe? `«doc-gen4»
| error "no doc-gen4 executable configuration found in workspace"
let exeTarget ← docGen4.exe.recBuild
let modTarget ← mod.leanBin.recBuild
let buildDir := (← getWorkspace).root.buildDir
let docFile := mod.filePath (buildDir / "doc") "html"
let task ← show SchedulerM _ from do
exeTarget.bindAsync fun exeFile exeTrace => do
modTarget.bindSync fun _ modTrace => do
let depTrace := exeTrace.mix modTrace
buildFileUnlessUpToDate docFile depTrace do
proc {
cmd := exeFile.toString
args := #["single", mod.name.toString]
env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
}
return ActiveTarget.mk docFile task

View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-07-24 leanprover/lean4:nightly-2022-08-09

View File

@ -1,20 +1,20 @@
{"version": 1, {"version": 2,
"packages": "packages":
[{"url": "https://github.com/mhuisi/lean4-cli", [{"url": "https://github.com/mhuisi/lean4-cli",
"rev": "112b35fc348a4a18d2111ac2c6586163330b4941", "rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
"name": "Cli"}, "name": "Cli"},
{"url": "https://github.com/hargonix/LeanInk", {"url": "https://github.com/hargonix/LeanInk",
"rev": "5d0aaba8b4fceeaf3a719e014dd42ca5d02f4810", "rev": "eed51a5e121233c3d15fb14642048a9bd3e00695",
"name": "leanInk"}, "name": "leanInk"},
{"url": "https://github.com/xubaiw/Unicode.lean", {"url": "https://github.com/xubaiw/Unicode.lean",
"rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0", "rev": "25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29",
"name": "Unicode"}, "name": "Unicode"},
{"url": "https://github.com/leanprover-community/mathlib4.git", {"url": "https://github.com/leanprover-community/mathlib4.git",
"rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd", "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd",
"name": "mathlib"}, "name": "mathlib"},
{"url": "https://github.com/leanprover/lake", {"url": "https://github.com/leanprover/lake",
"rev": "a7bc6addee9fc07c0ee43d0dcb537faa41844217", "rev": "6cfb4e3fd7ff700ace8c2cfdb85056d59f321920",
"name": "lake"}, "name": "lake"},
{"url": "https://github.com/xubaiw/CMark.lean", {"url": "https://github.com/xubaiw/CMark.lean",
"rev": "8f17d13d3046c517f7f02062918d81bc69e45cce", "rev": "8c0f9c1b16ee8047813f43b1f92de471782114ff",
"name": "CMark"}]} "name": "CMark"}]}