From ab5bfefa57273c5db0739929f944ca55ebc9e0d9 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 10 Nov 2023 14:22:37 +0100 Subject: [PATCH 01/16] feat: per-package server options Co-authored-by: digama0 --- nix/lake-dev.in | 2 +- src/Lean/Data/KVMap.lean | 10 ++++ src/Lean/Server/FileWorker.lean | 28 ++++++---- src/Lean/Server/README.md | 2 +- src/Lean/Util/FileSetupInfo.lean | 9 ++++ src/Lean/Util/ServerOptions.lean | 81 ++++++++++++++++++++++++++++ src/lake/Lake/Build/Imports.lean | 4 +- src/lake/Lake/CLI/Main.lean | 8 +-- src/lake/Lake/CLI/Serve.lean | 30 ++++++++--- src/lake/Lake/Config/Env.lean | 2 +- src/lake/Lake/Config/LeanConfig.lean | 13 +++++ src/lake/Lake/Config/Package.lean | 15 ++++-- src/lake/README.md | 7 +-- src/lake/examples/deps/test.sh | 4 +- src/lake/tests/badImport/test.sh | 2 +- src/lake/tests/noBuild/test.sh | 6 +-- src/lake/tests/serve/test.sh | 6 +-- 17 files changed, 185 insertions(+), 44 deletions(-) create mode 100644 src/Lean/Util/FileSetupInfo.lean create mode 100644 src/Lean/Util/ServerOptions.lean diff --git a/nix/lake-dev.in b/nix/lake-dev.in index 837bc37272d8..aa8a9f710125 100644 --- a/nix/lake-dev.in +++ b/nix/lake-dev.in @@ -10,7 +10,7 @@ function pebkac() { [[ $# -gt 0 ]] || pebkac case $1 in --version) - # minimum version for `lake server` with fallback + # minimum version for `lake serve` with fallback echo 3.1.0 ;; print-paths) diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean index 67250f94aa4b..d9107b195870 100644 --- a/src/Lean/Data/KVMap.lean +++ b/src/Lean/Data/KVMap.lean @@ -190,6 +190,16 @@ def subsetAux : List (Name × DataValue) → KVMap → Bool def subset : KVMap → KVMap → Bool | ⟨m₁⟩, m₂ => subsetAux m₁ m₂ +def mergeBy (mergeFn : Name → DataValue → DataValue → DataValue) (l r : KVMap) + : KVMap := Id.run do + let mut result := l + for ⟨k, vᵣ⟩ in r do + if let some vₗ := result.find k then + result := result.insert k (mergeFn k vₗ vᵣ) + else + result := result.insert k vᵣ + return result + def eqv (m₁ m₂ : KVMap) : Bool := subset m₁ m₂ && subset m₂ m₁ diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 0c53463c0761..8ccf919c7547 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -12,7 +12,7 @@ import Lean.Environment import Lean.Data.Lsp import Lean.Data.Json.FromToJson -import Lean.Util.Paths +import Lean.Util.FileSetupInfo import Lean.LoadDynlib import Lean.Server.Utils @@ -155,11 +155,13 @@ abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO /- Worker initialization sequence. -/ section Initialization - /-- Use `lake print-paths` to compile dependencies on the fly and add them to `LEAN_PATH`. + /-- Use `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`. Compilation progress is reported to `hOut` via LSP notifications. Return the search path for - source files. -/ - partial def lakeSetupSearchPath (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do - let mut args := #["print-paths"] ++ imports.map (toString ·.module) + source files and the options for the file. -/ + partial def lakeSetupFile (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO (SearchPath × Options) := do + let some filePath := System.Uri.fileUriToPath? m.uri + | return ([], Options.empty) -- untitled files have no search path and no associated `moreServerArgs` + let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module) if m.dependencyBuildMode matches .never then args := args.push "--no-build" let cmdStr := " ".intercalate (toString lakePath :: args.toList) @@ -183,12 +185,13 @@ section Initialization let stderr ← IO.ofExcept stderr.get match (← lakeProc.wait) with | 0 => - let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?) + let Except.ok (info : FileSetupInfo) ← pure (Json.parse stdout >>= fromJson?) | throwServerError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" - initSearchPath (← getBuildDir) paths.oleanPath - paths.loadDynlibPaths.forM loadDynlib - paths.srcPath.mapM realPathNormalized - | 2 => pure [] -- no lakefile.lean + initSearchPath (← getBuildDir) info.paths.oleanPath + info.paths.loadDynlibPaths.forM loadDynlib + let pkgSearchPath ← info.paths.srcPath.mapM realPathNormalized + return (pkgSearchPath, info.setupOptions.toOptions) + | 2 => pure ([], Options.empty) -- no lakefile.lean -- error from `--no-build` | 3 => throwServerError s!"Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor.\n\n{stdout}" | _ => throwServerError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" @@ -198,6 +201,7 @@ section Initialization -- parsing should not take long, do synchronously let (headerStx, headerParserState, msgLog) ← Parser.parseHeader m.mkInputContext (headerStx, ·) <$> EIO.asTask do + let mut opts := opts let mut srcSearchPath ← initSrcSearchPath (← getBuildDir) let lakePath ← match (← IO.getEnv "LAKE") with | some path => pure <| System.FilePath.mk path @@ -211,8 +215,10 @@ section Initialization -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps -- NOTE: lake does not exist in stage 0 (yet?) if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then - let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx) hOut + let (pkgSearchPath, fileOptions) ← lakeSetupFile lakePath m (Lean.Elab.headerToImports headerStx) hOut srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath + -- file options take priority + opts := opts.mergeBy (fun _ _ fileOpt => fileOpt) fileOptions -- allow `headerEnv` to be leaked, which would live until the end of the process anyway Elab.processHeader (leakEnv := true) headerStx opts msgLog m.mkInputContext catch e => -- should be from `lake print-paths` diff --git a/src/Lean/Server/README.md b/src/Lean/Server/README.md index b6d1a0d01363..fc0426403d79 100644 --- a/src/Lean/Server/README.md +++ b/src/Lean/Server/README.md @@ -39,7 +39,7 @@ Another important consideration is the *compacted region* memory used by importe When the user has two or more files in a single dependency chain open, it is desirable for changes in imports to propagate to modules importing them. That is, when `B.lean` depends on `A.lean` and both are open, changes to `A` should eventually be observable in `B`. But a major problem with Lean 3 is how it does this much too eagerly. Often `B` will be recompiled needlessly as soon as `A` is opened, even if no changes have been made to `A`. For heavyweight modules which take up to several minutes to compile, this causes frustration when `A` is opened merely for inspection e.g. via go-to-definition. -In Lean 4, the situation is different as `.olean` artifacts are required to exist for all imported modules -- one cannot import a `.lean` file without compiling it first. In the running example, when a user opens and edits `A`, nothing is going to happen to `B`. They can continue to interact with it as if `A` kept its previous contents. But when `A` is saved with changes, users can then issue the "refresh file dependencies" command in their editor, which will restart the respective worker and use `lake print-paths` to rebuild and locate its dependencies. This being a conscious action, users will be aware of having to then wait for compilation. +In Lean 4, the situation is different as `.olean` artifacts are required to exist for all imported modules -- one cannot import a `.lean` file without compiling it first. In the running example, when a user opens and edits `A`, nothing is going to happen to `B`. They can continue to interact with it as if `A` kept its previous contents. But when `A` is saved with changes, users can then issue the "refresh file dependencies" command in their editor, which will restart the respective worker and use `lake setup-file` to rebuild and locate its dependencies. This being a conscious action, users will be aware of having to then wait for compilation. ### Worker architecture diff --git a/src/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean new file mode 100644 index 000000000000..24d4eeb5e476 --- /dev/null +++ b/src/Lean/Util/FileSetupInfo.lean @@ -0,0 +1,9 @@ +import Lean.Util.ServerOptions + +/-- +Information shared between Lake and Lean when calling `lake setup-file`. +-/ +structure Lean.FileSetupInfo where + paths : LeanPaths + setupOptions : ServerOptions + deriving FromJson, ToJson diff --git a/src/Lean/Util/ServerOptions.lean b/src/Lean/Util/ServerOptions.lean new file mode 100644 index 000000000000..8337ddc05d8c --- /dev/null +++ b/src/Lean/Util/ServerOptions.lean @@ -0,0 +1,81 @@ +import Lean.Util.Paths + +namespace Lean + +/-- Restriction of `DataValue` that covers exactly those cases that Lean is able to handle when passed via the `-D` flag. -/ +inductive ServerOptionValue where + | ofString (s : String) + | ofBool (b : Bool) + | ofNat (n : Nat) + deriving Inhabited, Repr + +def ServerOptionValue.ofDataValue? : DataValue → Option ServerOptionValue + | .ofString s => some (.ofString s) + | .ofBool b => some (.ofBool b) + | .ofNat n => some (.ofNat n) + | _ => none + +def ServerOptionValue.toDataValue : ServerOptionValue → DataValue + | .ofString s => .ofString s + | .ofBool b => .ofBool b + | .ofNat n => .ofNat n + +instance : KVMap.Value ServerOptionValue where + toDataValue := ServerOptionValue.toDataValue + ofDataValue? := ServerOptionValue.ofDataValue? + +instance : Coe String ServerOptionValue where + coe := ServerOptionValue.ofString + +instance : Coe Bool ServerOptionValue where + coe := ServerOptionValue.ofBool + +instance : Coe Nat ServerOptionValue where + coe := ServerOptionValue.ofNat + +instance : FromJson ServerOptionValue where + fromJson? + | (s : String) => Except.ok s + | (b : Bool) => Except.ok b + | (n : Nat) => Except.ok n + | _ => Except.error "invalid ServerOptionValue type" + +instance : ToJson ServerOptionValue where + toJson + | (s : String) => s + | (b : Bool) => b + | (n : Nat) => n + +/-- Options that are used by the server as if they were passed using `-D`. -/ +structure ServerOptions where + values : RBMap Name ServerOptionValue Name.cmp + deriving Inhabited, Repr + +def ServerOptions.toOptions (serverOptions : ServerOptions) : Options := Id.run do + let mut options := KVMap.empty + for ⟨name, optionValue⟩ in serverOptions.values do + options := options.insert name optionValue.toDataValue + return options + +def ServerOptions.fromOptions? (options : Options) : Option ServerOptions := do + let mut values := RBMap.empty + for ⟨name, dataValue⟩ in options do + let optionValue ← ServerOptionValue.ofDataValue? dataValue + values := values.insert name optionValue + return ⟨values⟩ + +instance : FromJson ServerOptions where + fromJson? + | Json.obj obj => do + let values ← obj.foldM (init := RBMap.empty) fun acc k v => do + let optionValue ← fromJson? v + return acc.insert k.toName optionValue + return ⟨values⟩ + | _ => Except.error "invalid ServerOptions type" + +instance : ToJson ServerOptions where + toJson options := + Json.obj <| options.values.fold (init := RBNode.leaf) fun acc k v => + acc.insert (cmp := compare) k.toString (toJson v) + +end Lean diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean index ee89e7483c06..3d944c3b83ee 100644 --- a/src/lake/Lake/Build/Imports.lean +++ b/src/lake/Lake/Build/Imports.lean @@ -6,7 +6,7 @@ Authors: Mac Malone import Lake.Build.Index /-! -Definitions to support `lake print-paths` builds. +Definitions to support `lake setup-file` builds. -/ open System @@ -46,7 +46,7 @@ def recBuildImports (imports : Array Module) /-- Builds the workspace-local modules of list of imports. -Used by `lake print-paths` to build modules for the Lean server. +Used by `lake setup-file` to build modules for the Lean server. Returns the set of module dynlibs built (so they can be loaded by the server). Builds only module `.olean` and `.ilean` files if the package is configured diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index e219110db10b..9b2ab3df390f 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -310,12 +310,14 @@ protected def upload : CliM PUnit := do noArgsRem do liftM <| uploadRelease ws.root tag |>.run (MonadLog.io opts.verbosity) -protected def printPaths : CliM PUnit := do +protected def setupFile : CliM PUnit := do processOptions lakeOption let opts ← getThe LakeOptions let loadConfig ← mkLoadConfig opts let buildConfig := mkBuildConfig opts - printPaths loadConfig (← takeArgs) buildConfig opts.verbosity + let filePath ← takeArg "file path" + let imports ← takeArgs + setupFile loadConfig filePath imports buildConfig opts.verbosity protected def clean : CliM PUnit := do processOptions lakeOption @@ -389,7 +391,7 @@ def lakeCli : (cmd : String) → CliM PUnit | "update" | "upgrade" => lake.update | "resolve-deps" => lake.resolveDeps | "upload" => lake.upload -| "print-paths" => lake.printPaths +| "setup-file" => lake.setupFile | "clean" => lake.clean | "script" => lake.script | "scripts" => lake.script.list diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 191d85860e2c..19c6b3a8a0f6 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -6,11 +6,12 @@ Authors: Mac Malone import Lake.Load import Lake.Build import Lake.Util.MainM +import Lean.Util.FileSetupInfo namespace Lake -open Lean (Json toJson fromJson? LeanPaths) +open Lean (Json toJson fromJson? LeanPaths ServerOptions searchModuleNameOfFileName FileSetupInfo) -/-- Exit code to return if `print-paths` cannot find the config file. -/ +/-- Exit code to return if `setup-file` cannot find the config file. -/ def noConfigFileCode : ExitCode := 2 /-- @@ -20,13 +21,12 @@ and falls back to plain `lean --server`. def invalidConfigEnvVar := "LAKE_INVALID_CONFIG" /-- -Build a list of imports of the package -and print the `.olean` and source directories of every used package. +Build a list of imports of a file and print the `.olean` and source directories of every used package, as well as the server options for the file. If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2). -The `print-paths` command is used internally by Lean 4 server. +The `setup-file` command is used internally by Lean 4 server. -/ -def printPaths (loadConfig : LoadConfig) (imports : List String := []) +def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String := []) (buildConfig : BuildConfig := {}) (verbosity : Verbosity := .normal) : MainM PUnit := do if (← loadConfig.configFile.pathExists) then if let some errLog := (← IO.getEnv invalidConfigEnvVar) then @@ -36,12 +36,26 @@ def printPaths (loadConfig : LoadConfig) (imports : List String := []) let ws ← MainM.runLogIO (loadWorkspace loadConfig) verbosity let dynlibs ← ws.runBuild (buildImportsAndDeps imports) buildConfig |>.run (MonadLog.eio verbosity) - IO.println <| Json.compress <| toJson { + let paths : LeanPaths := { oleanPath := ws.leanPath srcPath := ws.leanSrcPath loadDynlibPaths := dynlibs : LeanPaths } + let setupOptions : ServerOptions ← do + let some moduleName ← searchModuleNameOfFileName path ws.leanSrcPath + | pure ⟨∅⟩ + let some (pkg, module) := ws.packages.findSome? fun pkg => do + pure (pkg, ← pkg.findModule? moduleName) + | pure ⟨∅⟩ + let options := pkg.config.moreServerOptions ++ module.lib.config.moreServerOptions + |>.map fun opt => ⟨opt.name, opt.value⟩ + pure ⟨Lean.RBMap.fromArray options Lean.Name.cmp⟩ + IO.println <| Json.compress <| toJson { + paths, + setupOptions + : FileSetupInfo + } else exit noConfigFileCode @@ -55,7 +69,7 @@ def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do IO.eprint log if let some ws := ws? then let ctx := mkLakeContext ws - pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs) + pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreGlobalServerArgs) else IO.eprintln "warning: package configuration has errors, falling back to plain `lean --server`" pure (config.env.baseVars.push (invalidConfigEnvVar, log), #[]) diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index 33a884f0da11..305afc716653 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -92,7 +92,7 @@ def leanPath (env : Env) : SearchPath := /-- The Lean source search path of the environment (i.e., `LEAN_SRC_PATH`). -Combines the initial path of the environment with that of the Lake abd Lean +Combines the initial path of the environment with that of the Lake and Lean installations. -/ def leanSrcPath (env : Env) : SearchPath := diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index 9e6814f0f162..4eeddb416eaa 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -1,3 +1,5 @@ +import Lean.Util.ServerOptions + /- Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -80,6 +82,12 @@ def BuildType.leancArgs : BuildType → Array String | minSizeRel => #["-Os", "-DNDEBUG"] | release => #["-O3", "-DNDEBUG"] +/-- Option that is used by the server as if it was passed using `-D`. -/ +structure ServerOption where + name : Lean.Name + value : Lean.ServerOptionValue + deriving Inhabited, Repr + /-- Configuration options common to targets that build modules. -/ structure LeanConfig where /-- @@ -110,6 +118,11 @@ structure LeanConfig where -/ moreLeancArgs : Array String := #[] /-- + Additional options to pass to the Lean language server + (i.e., `lean --server`) launched by `lake serve`. + -/ + moreServerOptions : Array ServerOption := #[] + /-- Additional arguments to pass to `leanc` when compiling a module's C source files generated by `lean`. diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index bf70a5d7ed78..a36e5ef16fa9 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -89,9 +89,10 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where /-- Additional arguments to pass to the Lean language server - (i.e., `lean --server`) launched by `lake server`. + (i.e., `lean --server`) launched by `lake serve`, both for this package and + also for any packages browsed from this one in the same session. -/ - moreServerArgs : Array String := #[] + moreGlobalServerArgs : Array String := #[] /-- The directory containing the package's Lean source files. @@ -310,9 +311,13 @@ namespace Package @[inline] def precompileModules (self : Package) : Bool := self.config.precompileModules -/-- The package's `moreServerArgs` configuration. -/ -@[inline] def moreServerArgs (self : Package) : Array String := - self.config.moreServerArgs +/-- The package's `moreGlobalServerArgs` configuration. -/ +@[inline] def moreGlobalServerArgs (self : Package) : Array String := + self.config.moreGlobalServerArgs + +/-- The package's `moreServerOptions` configuration. -/ +@[inline] def moreServerOptions (self : Package) : Array ServerOption := + self.config.moreServerOptions /-- The package's `buildType` configuration. -/ @[inline] def buildType (self : Package) : BuildType := diff --git a/src/lake/README.md b/src/lake/README.md index 9cabf5a4b2b3..c914bdc5168d 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -165,7 +165,8 @@ Lake provides a large assortment of configuration options for packages. * `postUpdate?`: A post-`lake update` hook. The monadic action is run after a successful `lake update` execution on this package or one of its downstream dependents. Defaults to `none`. See the option's docstring for a complete example. * `precompileModules`: Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`. -* `moreServerArgs`: Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. +* `moreServerOptions`: Additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. +* `moreGlobalServerArgs`: Additional arguments to pass to `lean --server` which apply both to this package and anything else in the same server session (e.g. when browsing other packages from the same session via go-to-definition) * `buildType`: The `BuildType` of targets in the package (see [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670)). One of `debug`, `relWithDebInfo`, `minSizeRel`, or `release`. Defaults to `release`. * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. * `weakLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. Unlike `moreLeanArgs`, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild. They come *before* `moreLeanArgs`. @@ -206,7 +207,7 @@ lean_lib «target-name» where * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the library's modules. * `defaultFacets`: An `Array` of library facets to build on a bare `lake build` of the library. For example, setting this to `#[LeanLib.sharedLib]` will build the shared library facet. * `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the library's static and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source). -* `precompileModules`, `buildType`, `Args`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest) +* `precompileModules`, `buildType`, `Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest) ### Binary Executables @@ -227,7 +228,7 @@ lean_exe «target-name» where * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the executable's modules. * `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the executable. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source). * `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`. -* `precompileModules`, `buildType`, `Args`: Augments the package's corresponding configuration option. The executable's arguments come after and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest). +* `precompileModules`, `buildType`, `Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The executable's arguments come after and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest). ### External Libraries diff --git a/src/lake/examples/deps/test.sh b/src/lake/examples/deps/test.sh index 34f4ae865b6a..5117a6bb8ad0 100755 --- a/src/lake/examples/deps/test.sh +++ b/src/lake/examples/deps/test.sh @@ -11,8 +11,8 @@ $LAKE -d foo build --update ./foo/.lake/build/bin/foo ./bar/.lake/build/bin/bar -# Test print-paths works (i.e., does not error) -$LAKE -d foo print-paths A B +# Test setup-file works (i.e., does not error) +$LAKE -d foo setup-file ./foo/Foo.lean A B # Test `lake clean` test -d a/.lake/build diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh index de26391c8fc5..2d561e16ba32 100755 --- a/src/lake/tests/badImport/test.sh +++ b/src/lake/tests/badImport/test.sh @@ -11,4 +11,4 @@ LAKE=${LAKE:-../../.lake/build/bin/lake} # https://github.com/leanprover/lean4/issues/2415 ($LAKE build +X 2>&1 && exit 1 || true) | grep -F "X.lean" -($LAKE print-paths Lib.B 2>&1 && exit 1 || true) | grep -F "Lib.B" +($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep -F "Lib.B" diff --git a/src/lake/tests/noBuild/test.sh b/src/lake/tests/noBuild/test.sh index d7f32ccd7586..1d6d4a3c2853 100755 --- a/src/lake/tests/noBuild/test.sh +++ b/src/lake/tests/noBuild/test.sh @@ -9,12 +9,12 @@ set -euxo pipefail NO_BUILD_CODE=3 LAKE=${LAKE:-../../.lake/build/bin/lake} -# Test `--no-build` for print-paths and module builds (`buildUnlessUpToDate`) -$LAKE print-paths Test --no-build && exit 1 || [ $? = $NO_BUILD_CODE ] +# Test `--no-build` for setup-file and module builds (`buildUnlessUpToDate`) +$LAKE setup-file ./Irrelevant.lean Test --no-build && exit 1 || [ $? = $NO_BUILD_CODE ] test ! -f .lake/build/lib/Test.olean $LAKE build Test test -f .lake/build/lib/Test.olean -$LAKE print-paths Test --no-build +$LAKE setup-file ./Irrelevant.lean Test --no-build # Test `--no-build` for file builds (`buildFileUnlessUpToDate`) $LAKE build +Test:o --no-build && exit 1 || [ $? = $NO_BUILD_CODE ] diff --git a/src/lake/tests/serve/test.sh b/src/lake/tests/serve/test.sh index b725503d53a7..0801d3603c47 100755 --- a/src/lake/tests/serve/test.sh +++ b/src/lake/tests/serve/test.sh @@ -28,14 +28,14 @@ echo -n "$MSGS" | ${LAKE:-../../.lake/build/bin/lake} serve >/dev/null echo "tested 49" # --- -# Test that `lake print-paths` retains the error from `lake serve` +# Test that `lake setup-file` retains the error from `lake serve` # See https://github.com/leanprover/lake/issues/116 # --- -# Test that `lake print-paths` produces the error from `LAKE_INVALID_CONFIG` +# Test that `lake setup-file` produces the error from `LAKE_INVALID_CONFIG` set -x # NOTE: For some reason, using `!` here does not work on macOS -(LAKE_INVALID_CONFIG=$'foo\n' $LAKE print-paths 2>&1 && exit 1 || true) | grep foo +(LAKE_INVALID_CONFIG=$'foo\n' $LAKE setup-file ./Irrelevant.lean 2>&1 && exit 1 || true) | grep foo set +x # Test that `lake serve` produces the `Invalid Lake configuration message`. From 612f93e352297c6f9f0579d9d50005a43830a752 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 10 Nov 2023 21:03:39 +0100 Subject: [PATCH 02/16] test: use correct file uri in interactive tests --- tests/lean/interactive/1265.lean.expected.out | 4 +- tests/lean/interactive/1403.lean.expected.out | 2 +- tests/lean/interactive/1659.lean.expected.out | 10 +- tests/lean/interactive/533.lean.expected.out | 2 +- tests/lean/interactive/863.lean.expected.out | 4 +- tests/lean/interactive/amb.lean.expected.out | 4 +- .../interactive/anonHyp.lean.expected.out | 2 +- .../autoBoundIssue.lean.expected.out | 12 +- .../interactive/catHover.lean.expected.out | 12 +- .../interactive/codeaction.lean.expected.out | 4 +- .../interactive/compHeader.lean.expected.out | 2 +- .../compNamespace.lean.expected.out | 10 +- .../interactive/completion.lean.expected.out | 8 +- .../interactive/completion2.lean.expected.out | 8 +- .../interactive/completion3.lean.expected.out | 8 +- .../interactive/completion4.lean.expected.out | 8 +- .../interactive/completion5.lean.expected.out | 2 +- .../interactive/completion6.lean.expected.out | 4 +- .../interactive/completion7.lean.expected.out | 4 +- .../completionAtPrint.lean.expected.out | 2 +- .../completionDocString.lean.expected.out | 2 +- .../completionEOF.lean.expected.out | 2 +- .../completionIStr.lean.expected.out | 2 +- .../completionOption.lean.expected.out | 12 +- .../completionPrefixIssue.lean.expected.out | 2 +- .../completionPrv.lean.expected.out | 8 +- .../interactive/definition.lean.expected.out | 8 +- .../interactive/discrsIssue.lean.expected.out | 2 +- .../dotIdCompletion.lean.expected.out | 2 +- .../editAfterError.lean.expected.out | 8 +- .../editCompletion.lean.expected.out | 4 +- .../expectedTypeAsGoal.lean.expected.out | 2 +- .../fieldCompletion.lean.expected.out | 2 +- .../foldingRange.lean.expected.out | 2 +- tests/lean/interactive/goTo.lean.expected.out | 104 +++++----- .../lean/interactive/goTo2.lean.expected.out | 12 +- .../interactive/goalEOF.lean.expected.out | 2 +- .../interactive/goalIssue.lean.expected.out | 4 +- .../interactive/haveInfo.lean.expected.out | 8 +- .../interactive/highlight.lean.expected.out | 22 +-- .../lean/interactive/hover.lean.expected.out | 182 +++++++++--------- .../interactive/hoverAt.lean.expected.out | 2 +- .../hoverBinderUndescore.lean.expected.out | 12 +- .../interactive/hoverDot.lean.expected.out | 20 +- .../hoverException.lean.expected.out | 2 +- .../inWordCompletion.lean.expected.out | 4 +- .../interactive/infoIssues.lean.expected.out | 14 +- .../internalNamesIssue.lean.expected.out | 2 +- .../interactive/jumpMutual.lean.expected.out | 30 +-- .../keywordCompletion.lean.expected.out | 4 +- .../lean3HoverIssue.lean.expected.out | 14 +- .../macroGoalIssue.lean.expected.out | 2 +- .../lean/interactive/match.lean.expected.out | 8 +- .../matchPatternHover.lean.expected.out | 4 +- .../matchStxCompletion.lean.expected.out | 2 +- .../partialNamespace.lean.expected.out | 2 +- .../interactive/plainGoal.lean.expected.out | 84 ++++---- .../plainTermGoal.lean.expected.out | 28 +-- tests/lean/interactive/run.lean | 2 +- .../unterminatedDocComment.lean.expected.out | 8 +- 60 files changed, 374 insertions(+), 374 deletions(-) diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out index 787c3640f3f8..cc081a1d907e 100644 --- a/tests/lean/interactive/1265.lean.expected.out +++ b/tests/lean/interactive/1265.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://1265.lean"}, +{"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}} {"items": [{"label": "getHygieneInfo", @@ -22,7 +22,7 @@ {"value": "The underlying `Syntax` value. ", "kind": "markdown"}, "detail": "Lean.TSyntax ks → Lean.Syntax"}], "isIncomplete": true} -{"textDocument": {"uri": "file://1265.lean"}, +{"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}} {"items": [{"label": "getHygieneInfo", diff --git a/tests/lean/interactive/1403.lean.expected.out b/tests/lean/interactive/1403.lean.expected.out index 2a50da1c8824..86608a6bd9b1 100644 --- a/tests/lean/interactive/1403.lean.expected.out +++ b/tests/lean/interactive/1403.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://1403.lean"}, +{"textDocument": {"uri": "file:///1403.lean"}, "position": {"line": 1, "character": 2}} {"range": {"start": {"line": 1, "character": 2}, "end": {"line": 1, "character": 12}}, diff --git a/tests/lean/interactive/1659.lean.expected.out b/tests/lean/interactive/1659.lean.expected.out index c2fe11449b5d..cb8d2d4bae23 100644 --- a/tests/lean/interactive/1659.lean.expected.out +++ b/tests/lean/interactive/1659.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://1659.lean"}, +{"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 9, "character": 23}} {"items": [{"label": "Lean.Elab.Tactic.elabTermEnsuringType", @@ -8,13 +8,13 @@ "kind": 21, "detail": "Type"}], "isIncomplete": true} -{"textDocument": {"uri": "file://1659.lean"}, +{"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 15, "character": 23}} {"items": [{"label": "Tactic.elabTermEnsuringType", "kind": 21, "detail": "Type"}, {"label": "Term.elabTermEnsuringType", "kind": 21, "detail": "Type"}], "isIncomplete": true} -{"textDocument": {"uri": "file://1659.lean"}, +{"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 21, "character": 23}} {"items": [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, @@ -22,7 +22,7 @@ "kind": 21, "detail": "Type"}], "isIncomplete": true} -{"textDocument": {"uri": "file://1659.lean"}, +{"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 27, "character": 23}} {"items": [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, @@ -33,7 +33,7 @@ "kind": 21, "detail": "Type"}], "isIncomplete": true} -{"textDocument": {"uri": "file://1659.lean"}, +{"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}} {"items": [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index f9137c9288da..155bb3aa7edb 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://533.lean"}, +{"textDocument": {"uri": "file:///533.lean"}, "position": {"line": 4, "character": 10}} {"items": [{"label": "F", "kind": 6, "detail": "Sort ?u"}, diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out index 0dc92d70dfaa..faadde731fa1 100644 --- a/tests/lean/interactive/863.lean.expected.out +++ b/tests/lean/interactive/863.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://863.lean"}, +{"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 9, "character": 12}} {"items": [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}, @@ -6,7 +6,7 @@ "kind": 5, "detail": "[self : MonadRef] → Type"}], "isIncomplete": true} -{"textDocument": {"uri": "file://863.lean"}, +{"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 13, "character": 12}} {"items": [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}, diff --git a/tests/lean/interactive/amb.lean.expected.out b/tests/lean/interactive/amb.lean.expected.out index d231a2a7ad0e..a8048d8e715a 100644 --- a/tests/lean/interactive/amb.lean.expected.out +++ b/tests/lean/interactive/amb.lean.expected.out @@ -1,10 +1,10 @@ -{"textDocument": {"uri": "file://amb.lean"}, +{"textDocument": {"uri": "file:///amb.lean"}, "position": {"line": 17, "character": 19}} {"range": {"start": {"line": 17, "character": 19}, "end": {"line": 17, "character": 20}}, "contents": {"value": "```lean\nFoo.f (n : Nat) : Bool\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://amb.lean"}, +{"textDocument": {"uri": "file:///amb.lean"}, "position": {"line": 19, "character": 19}} {"range": {"start": {"line": 19, "character": 19}, "end": {"line": 19, "character": 20}}, diff --git a/tests/lean/interactive/anonHyp.lean.expected.out b/tests/lean/interactive/anonHyp.lean.expected.out index 5d146f6c6793..a60251092bdb 100644 --- a/tests/lean/interactive/anonHyp.lean.expected.out +++ b/tests/lean/interactive/anonHyp.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://anonHyp.lean"}, +{"textDocument": {"uri": "file:///anonHyp.lean"}, "position": {"line": 2, "character": 4}} {"rendered": "```lean\ncase succ\nn✝ : Nat\nn_ih✝ : n✝ + 1 > 0\n⊢ Nat.succ n✝ + 1 > 0\n```", diff --git a/tests/lean/interactive/autoBoundIssue.lean.expected.out b/tests/lean/interactive/autoBoundIssue.lean.expected.out index cb2d82d062c3..8c80d1d3c880 100644 --- a/tests/lean/interactive/autoBoundIssue.lean.expected.out +++ b/tests/lean/interactive/autoBoundIssue.lean.expected.out @@ -1,34 +1,34 @@ -{"textDocument": {"uri": "file://autoBoundIssue.lean"}, +{"textDocument": {"uri": "file:///autoBoundIssue.lean"}, "position": {"line": 13, "character": 21}} {"range": {"start": {"line": 13, "character": 21}, "end": {"line": 13, "character": 24}}, "goal": "k : Fin ?m\nctx : Vector Ty ?m\nty u : Ty\n⊢ Vector Ty ?m"} -{"textDocument": {"uri": "file://autoBoundIssue.lean"}, +{"textDocument": {"uri": "file:///autoBoundIssue.lean"}, "position": {"line": 16, "character": 26}} {"range": {"start": {"line": 16, "character": 26}, "end": {"line": 16, "character": 29}}, "goal": "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"} -{"textDocument": {"uri": "file://autoBoundIssue.lean"}, +{"textDocument": {"uri": "file:///autoBoundIssue.lean"}, "position": {"line": 19, "character": 20}} {"range": {"start": {"line": 19, "character": 20}, "end": {"line": 19, "character": 23}}, "goal": "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"} -{"textDocument": {"uri": "file://autoBoundIssue.lean"}, +{"textDocument": {"uri": "file:///autoBoundIssue.lean"}, "position": {"line": 24, "character": 18}} {"range": {"start": {"line": 24, "character": 18}, "end": {"line": 24, "character": 21}}, "goal": "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"} -{"textDocument": {"uri": "file://autoBoundIssue.lean"}, +{"textDocument": {"uri": "file:///autoBoundIssue.lean"}, "position": {"line": 26, "character": 18}} {"range": {"start": {"line": 26, "character": 18}, "end": {"line": 26, "character": 21}}, "goal": "aux : {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty : Ty} → HasType k ctx ty\nk : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"} -{"textDocument": {"uri": "file://autoBoundIssue.lean"}, +{"textDocument": {"uri": "file:///autoBoundIssue.lean"}, "position": {"line": 29, "character": 24}} {"range": {"start": {"line": 29, "character": 24}, "end": {"line": 29, "character": 27}}, diff --git a/tests/lean/interactive/catHover.lean.expected.out b/tests/lean/interactive/catHover.lean.expected.out index 1b3f3d24e970..51c64e75ce41 100644 --- a/tests/lean/interactive/catHover.lean.expected.out +++ b/tests/lean/interactive/catHover.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://catHover.lean"}, +{"textDocument": {"uri": "file:///catHover.lean"}, "position": {"line": 4, "character": 33}} {"range": {"start": {"line": 4, "character": 32}, "end": {"line": 4, "character": 36}}, @@ -6,7 +6,7 @@ {"value": "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://catHover.lean"}, +{"textDocument": {"uri": "file:///catHover.lean"}, "position": {"line": 4, "character": 14}} {"range": {"start": {"line": 4, "character": 14}, "end": {"line": 4, "character": 18}}, @@ -14,7 +14,7 @@ {"value": "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://catHover.lean"}, +{"textDocument": {"uri": "file:///catHover.lean"}, "position": {"line": 4, "character": 25}} {"range": {"start": {"line": 4, "character": 24}, "end": {"line": 4, "character": 29}}, @@ -22,7 +22,7 @@ {"value": "```lean\nLean.Parser.Category.index : Lean.Parser.Category\n```\n***\nIndex syntax categoy ", "kind": "markdown"}} -{"textDocument": {"uri": "file://catHover.lean"}, +{"textDocument": {"uri": "file:///catHover.lean"}, "position": {"line": 12, "character": 16}} {"range": {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 19}}, @@ -30,7 +30,7 @@ {"value": "```lean\nLean.Parser.Category.value : Lean.Parser.Category\n```\n***\nValue syntax category ", "kind": "markdown"}} -{"textDocument": {"uri": "file://catHover.lean"}, +{"textDocument": {"uri": "file:///catHover.lean"}, "position": {"line": 17, "character": 15}} {"range": {"start": {"line": 17, "character": 15}, "end": {"line": 17, "character": 19}}, @@ -38,7 +38,7 @@ {"value": "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://catHover.lean"}, +{"textDocument": {"uri": "file:///catHover.lean"}, "position": {"line": 20, "character": 9}} {"range": {"start": {"line": 20, "character": 7}, "end": {"line": 20, "character": 11}}, diff --git a/tests/lean/interactive/codeaction.lean.expected.out b/tests/lean/interactive/codeaction.lean.expected.out index 2f09c348252c..687ff34fcb9d 100644 --- a/tests/lean/interactive/codeaction.lean.expected.out +++ b/tests/lean/interactive/codeaction.lean.expected.out @@ -2,7 +2,7 @@ "kind": "quickfix", "edit": {"documentChanges": - [{"textDocument": {"version": 1, "uri": "file://codeaction.lean"}, + [{"textDocument": {"version": 1, "uri": "file:///codeaction.lean"}, "edits": [{"range": {"start": {"line": 30, "character": 4}, @@ -14,7 +14,7 @@ {"providerResultIndex": 1, "providerName": "helloProvider", "params": - {"textDocument": {"uri": "file://codeaction.lean"}, + {"textDocument": {"uri": "file:///codeaction.lean"}, "range": {"start": {"line": 30, "character": 4}, "end": {"line": 30, "character": 4}}, "context": {"diagnostics": []}}}} diff --git a/tests/lean/interactive/compHeader.lean.expected.out b/tests/lean/interactive/compHeader.lean.expected.out index 3be618a0fcf2..e616d3c9ee52 100644 --- a/tests/lean/interactive/compHeader.lean.expected.out +++ b/tests/lean/interactive/compHeader.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://compHeader.lean"}, +{"textDocument": {"uri": "file:///compHeader.lean"}, "position": {"line": 2, "character": 22}} {"items": [{"label": "veryLongNam", "kind": 6, "detail": "Sort u_1"}, diff --git a/tests/lean/interactive/compNamespace.lean.expected.out b/tests/lean/interactive/compNamespace.lean.expected.out index 78a759c773d6..68fd4113384b 100644 --- a/tests/lean/interactive/compNamespace.lean.expected.out +++ b/tests/lean/interactive/compNamespace.lean.expected.out @@ -1,21 +1,21 @@ -{"textDocument": {"uri": "file://compNamespace.lean"}, +{"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 5, "character": 12}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], "isIncomplete": true} -{"textDocument": {"uri": "file://compNamespace.lean"}, +{"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 9, "character": 12}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], "isIncomplete": true} -{"textDocument": {"uri": "file://compNamespace.lean"}, +{"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 13, "character": 11}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], "isIncomplete": true} -{"textDocument": {"uri": "file://compNamespace.lean"}, +{"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 16, "character": 16}} {"items": [{"label": "Foo.LongNamespaceExample", "kind": 9, "detail": "namespace"}], "isIncomplete": true} -{"textDocument": {"uri": "file://compNamespace.lean"}, +{"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 20, "character": 12}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out index 28419bfb8831..8963177efab2 100644 --- a/tests/lean/interactive/completion.lean.expected.out +++ b/tests/lean/interactive/completion.lean.expected.out @@ -1,16 +1,16 @@ -{"textDocument": {"uri": "file://completion.lean"}, +{"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 3, "character": 22}} {"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion.lean"}, +{"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 5, "character": 23}} {"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion.lean"}, +{"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 7, "character": 28}} {"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion.lean"}, +{"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 9, "character": 29}} {"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out index f721ab7c7164..b2620931aa7c 100644 --- a/tests/lean/interactive/completion2.lean.expected.out +++ b/tests/lean/interactive/completion2.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completion2.lean"}, +{"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 19, "character": 10}} {"items": [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, @@ -6,7 +6,7 @@ {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"}, {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion2.lean"}, +{"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}} {"items": [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, @@ -14,7 +14,7 @@ {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"}, {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion2.lean"}, +{"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}} {"items": [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, @@ -22,7 +22,7 @@ {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"}, {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion2.lean"}, +{"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 37, "character": 22}} {"items": [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out index 48ba7a29a17e..615bb214c8a4 100644 --- a/tests/lean/interactive/completion3.lean.expected.out +++ b/tests/lean/interactive/completion3.lean.expected.out @@ -1,25 +1,25 @@ -{"textDocument": {"uri": "file://completion3.lean"}, +{"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 7, "character": 9}} {"items": [{"label": "b", "kind": 5, "detail": "S → Bool"}, {"label": "x", "kind": 5, "detail": "S → Nat"}, {"label": "y", "kind": 5, "detail": "S → String"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion3.lean"}, +{"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 12, "character": 5}} {"items": [{"label": "b", "kind": 5, "detail": "S → Bool"}, {"label": "x", "kind": 5, "detail": "S → Nat"}, {"label": "y", "kind": 5, "detail": "S → String"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion3.lean"}, +{"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 16, "character": 5}} {"items": [{"label": "b", "kind": 5, "detail": "S → Bool"}, {"label": "x", "kind": 5, "detail": "S → Nat"}, {"label": "y", "kind": 5, "detail": "S → String"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion3.lean"}, +{"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 20, "character": 5}} {"items": [{"label": "x", "kind": 5, "detail": "S → Nat"}, diff --git a/tests/lean/interactive/completion4.lean.expected.out b/tests/lean/interactive/completion4.lean.expected.out index 88b2e8c18d24..67d9fc4fe530 100644 --- a/tests/lean/interactive/completion4.lean.expected.out +++ b/tests/lean/interactive/completion4.lean.expected.out @@ -1,25 +1,25 @@ -{"textDocument": {"uri": "file://completion4.lean"}, +{"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 7, "character": 4}} {"items": [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion4.lean"}, +{"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 11, "character": 10}} {"items": [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion4.lean"}, +{"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 16, "character": 11}} {"items": [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion4.lean"}, +{"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 20, "character": 21}} {"items": [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out index 38d270ac5679..b88a5e9310d6 100644 --- a/tests/lean/interactive/completion5.lean.expected.out +++ b/tests/lean/interactive/completion5.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completion5.lean"}, +{"textDocument": {"uri": "file:///completion5.lean"}, "position": {"line": 9, "character": 15}} {"items": [{"label": "b1", "kind": 5, "detail": "C → String"}, diff --git a/tests/lean/interactive/completion6.lean.expected.out b/tests/lean/interactive/completion6.lean.expected.out index d3976fb926c5..e5586b430b35 100644 --- a/tests/lean/interactive/completion6.lean.expected.out +++ b/tests/lean/interactive/completion6.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completion6.lean"}, +{"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}} {"items": [{"label": "b1", "kind": 5, "detail": "C → String"}, @@ -7,7 +7,7 @@ {"label": "f3", "kind": 5, "detail": "D → Bool"}, {"label": "toC", "kind": 5, "detail": "D → C"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion6.lean"}, +{"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}} {"items": [{"label": "b1", "kind": 5, "detail": "C → String"}, diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index f50c1efce9f1..04dd60a4ea12 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -1,8 +1,8 @@ -{"textDocument": {"uri": "file://completion7.lean"}, +{"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 6, "character": 10}} {"items": [{"label": "And", "kind": 22, "detail": "Type 1"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completion7.lean"}, +{"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 8, "character": 11}} {"items": [{"label": "left", "kind": 5, "detail": "And → Type"}, diff --git a/tests/lean/interactive/completionAtPrint.lean.expected.out b/tests/lean/interactive/completionAtPrint.lean.expected.out index 48577fdddf38..6a27b6c940d1 100644 --- a/tests/lean/interactive/completionAtPrint.lean.expected.out +++ b/tests/lean/interactive/completionAtPrint.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completionAtPrint.lean"}, +{"textDocument": {"uri": "file:///completionAtPrint.lean"}, "position": {"line": 2, "character": 25}} {"items": [{"label": "find?", diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out index 24204c8e7ceb..4521ca09a1c6 100644 --- a/tests/lean/interactive/completionDocString.lean.expected.out +++ b/tests/lean/interactive/completionDocString.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completionDocString.lean"}, +{"textDocument": {"uri": "file:///completionDocString.lean"}, "position": {"line": 0, "character": 20}} {"items": [{"label": "insertAt", diff --git a/tests/lean/interactive/completionEOF.lean.expected.out b/tests/lean/interactive/completionEOF.lean.expected.out index db1c3bdafabc..db831fc9d4fd 100644 --- a/tests/lean/interactive/completionEOF.lean.expected.out +++ b/tests/lean/interactive/completionEOF.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completionEOF.lean"}, +{"textDocument": {"uri": "file:///completionEOF.lean"}, "position": {"line": 8, "character": 9}} {"items": [{"label": "And", "kind": 21, "detail": "Type"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionIStr.lean.expected.out b/tests/lean/interactive/completionIStr.lean.expected.out index 2735770873c9..47ea662abba0 100644 --- a/tests/lean/interactive/completionIStr.lean.expected.out +++ b/tests/lean/interactive/completionIStr.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completionIStr.lean"}, +{"textDocument": {"uri": "file:///completionIStr.lean"}, "position": {"line": 5, "character": 34}} {"items": [{"label": "b1", "kind": 5, "detail": "C → String"}, diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out index 6797b7a161ce..0bdc0109fc19 100644 --- a/tests/lean/interactive/completionOption.lean.expected.out +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completionOption.lean"}, +{"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 1, "character": 17}} {"items": [{"textEdit": @@ -71,7 +71,7 @@ "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionOption.lean"}, +{"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 4, "character": 20}} {"items": [{"textEdit": @@ -98,7 +98,7 @@ "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionOption.lean"}, +{"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 7, "character": 23}} {"items": [{"textEdit": @@ -150,7 +150,7 @@ "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionOption.lean"}, +{"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 10, "character": 27}} {"items": [{"textEdit": @@ -202,7 +202,7 @@ "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionOption.lean"}, +{"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 13, "character": 17}} {"items": [{"textEdit": @@ -275,7 +275,7 @@ "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionOption.lean"}, +{"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 16, "character": 18}} {"items": [{"textEdit": diff --git a/tests/lean/interactive/completionPrefixIssue.lean.expected.out b/tests/lean/interactive/completionPrefixIssue.lean.expected.out index 4d4d4bff9408..903119b94fa4 100644 --- a/tests/lean/interactive/completionPrefixIssue.lean.expected.out +++ b/tests/lean/interactive/completionPrefixIssue.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://completionPrefixIssue.lean"}, +{"textDocument": {"uri": "file:///completionPrefixIssue.lean"}, "position": {"line": 1, "character": 64}} {"items": [{"label": "veryLongDefinitionName", "kind": 6, "detail": "Nat"}, diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index 10bcdf3c282d..87db18785039 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/tests/lean/interactive/completionPrv.lean.expected.out @@ -1,20 +1,20 @@ -{"textDocument": {"uri": "file://completionPrv.lean"}, +{"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 2, "character": 11}} {"items": [{"label": "blaBlaBoo", "kind": 21, "detail": "Nat"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionPrv.lean"}, +{"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 9, "character": 11}} {"items": [{"label": "booBoo", "kind": 21, "detail": "Nat"}, {"label": "instToBoolBool", "kind": 21, "detail": "ToBool Bool"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionPrv.lean"}, +{"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 21, "character": 5}} {"items": [{"label": "field1", "kind": 5, "detail": "S → Nat"}, {"label": "getInc", "kind": 3, "detail": "S → Nat"}], "isIncomplete": true} -{"textDocument": {"uri": "file://completionPrv.lean"}, +{"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 25, "character": 4}} {"items": [{"label": "field1", "kind": 5, "detail": "S → Nat"}, diff --git a/tests/lean/interactive/definition.lean.expected.out b/tests/lean/interactive/definition.lean.expected.out index b7d96fb33237..3b10090a62a1 100644 --- a/tests/lean/interactive/definition.lean.expected.out +++ b/tests/lean/interactive/definition.lean.expected.out @@ -1,15 +1,15 @@ -{"textDocument": {"uri": "file://definition.lean"}, +{"textDocument": {"uri": "file:///definition.lean"}, "position": {"line": 4, "character": 2}} -[{"targetUri": "file://definition.lean", +[{"targetUri": "file:///definition.lean", "targetSelectionRange": {"start": {"line": 0, "character": 10}, "end": {"line": 0, "character": 13}}, "targetRange": {"start": {"line": 0, "character": 0}, "end": {"line": 1, "character": 7}}, "originSelectionRange": {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 3}}}] -{"textDocument": {"uri": "file://definition.lean"}, +{"textDocument": {"uri": "file:///definition.lean"}, "position": {"line": 10, "character": 13}} -[{"targetUri": "file://definition.lean", +[{"targetUri": "file:///definition.lean", "targetSelectionRange": {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 5}}, "targetRange": diff --git a/tests/lean/interactive/discrsIssue.lean.expected.out b/tests/lean/interactive/discrsIssue.lean.expected.out index b09821e1e07e..e5c62054a3d0 100644 --- a/tests/lean/interactive/discrsIssue.lean.expected.out +++ b/tests/lean/interactive/discrsIssue.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://discrsIssue.lean"}, +{"textDocument": {"uri": "file:///discrsIssue.lean"}, "position": {"line": 32, "character": 18}} {"range": {"start": {"line": 32, "character": 18}, "end": {"line": 32, "character": 20}}, diff --git a/tests/lean/interactive/dotIdCompletion.lean.expected.out b/tests/lean/interactive/dotIdCompletion.lean.expected.out index 03891dd7e876..cec637cc5f0b 100644 --- a/tests/lean/interactive/dotIdCompletion.lean.expected.out +++ b/tests/lean/interactive/dotIdCompletion.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://dotIdCompletion.lean"}, +{"textDocument": {"uri": "file:///dotIdCompletion.lean"}, "position": {"line": 4, "character": 5}} {"items": [{"label": "true", "kind": 4, "detail": "Boo"}, diff --git a/tests/lean/interactive/editAfterError.lean.expected.out b/tests/lean/interactive/editAfterError.lean.expected.out index 3ad143e86cd2..17459b155201 100644 --- a/tests/lean/interactive/editAfterError.lean.expected.out +++ b/tests/lean/interactive/editAfterError.lean.expected.out @@ -1,11 +1,11 @@ -{"textDocument": {"version": 2, "uri": "file://editAfterError.lean"}, +{"textDocument": {"version": 2, "uri": "file:///editAfterError.lean"}, "contentChanges": [{"text": "s", "range": {"start": {"line": 1, "character": 10}, "end": {"line": 1, "character": 11}}}]} {"version": 2, - "uri": "file://editAfterError.lean", + "uri": "file:///editAfterError.lean", "diagnostics": [{"source": "Lean 4", "severity": 1, @@ -23,7 +23,7 @@ {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}}}]} {"version": 2, - "uri": "file://editAfterError.lean", + "uri": "file:///editAfterError.lean", "diagnostics": [{"source": "Lean 4", "severity": 1, @@ -41,7 +41,7 @@ {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}}}]} {"version": 2, - "uri": "file://editAfterError.lean", + "uri": "file:///editAfterError.lean", "diagnostics": [{"source": "Lean 4", "severity": 1, diff --git a/tests/lean/interactive/editCompletion.lean.expected.out b/tests/lean/interactive/editCompletion.lean.expected.out index d80fe93880ad..7625ab84e90e 100644 --- a/tests/lean/interactive/editCompletion.lean.expected.out +++ b/tests/lean/interactive/editCompletion.lean.expected.out @@ -1,10 +1,10 @@ -{"textDocument": {"version": 2, "uri": "file://editCompletion.lean"}, +{"textDocument": {"version": 2, "uri": "file:///editCompletion.lean"}, "contentChanges": [{"text": ".", "range": {"start": {"line": 3, "character": 21}, "end": {"line": 3, "character": 22}}}]} -{"textDocument": {"uri": "file://editCompletion.lean"}, +{"textDocument": {"uri": "file:///editCompletion.lean"}, "position": {"line": 3, "character": 22}} {"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], "isIncomplete": true} diff --git a/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out b/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out index 1c6ad9bbf7c4..c8c677973de5 100644 --- a/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out +++ b/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://expectedTypeAsGoal.lean"}, +{"textDocument": {"uri": "file:///expectedTypeAsGoal.lean"}, "position": {"line": 3, "character": 5}} {"range": {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 23}}, diff --git a/tests/lean/interactive/fieldCompletion.lean.expected.out b/tests/lean/interactive/fieldCompletion.lean.expected.out index 1c5b8158e46d..78ee05fc63f7 100644 --- a/tests/lean/interactive/fieldCompletion.lean.expected.out +++ b/tests/lean/interactive/fieldCompletion.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://fieldCompletion.lean"}, +{"textDocument": {"uri": "file:///fieldCompletion.lean"}, "position": {"line": 5, "character": 3}} {"items": [{"label": "modifiers", "kind": 5, "detail": "field"}], "isIncomplete": true} diff --git a/tests/lean/interactive/foldingRange.lean.expected.out b/tests/lean/interactive/foldingRange.lean.expected.out index e33ef5c3711b..f69f864c1969 100644 --- a/tests/lean/interactive/foldingRange.lean.expected.out +++ b/tests/lean/interactive/foldingRange.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://foldingRange.lean"}, +{"textDocument": {"uri": "file:///foldingRange.lean"}, "position": {"line": 0, "character": 2}} [{"startLine": 1, "kind": "imports", "endLine": 4}, {"startLine": 8, "kind": "imports", "endLine": 9}, diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out index ba756c710be2..316024c5f556 100644 --- a/tests/lean/interactive/goTo.lean.expected.out +++ b/tests/lean/interactive/goTo.lean.expected.out @@ -1,42 +1,42 @@ -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 11, "character": 2}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 6}}, "targetRange": {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 6}}, "originSelectionRange": {"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 6}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 11, "character": 6}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 6}}, "targetRange": {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 6}}, "originSelectionRange": {"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 6}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 14, "character": 2}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 6, "character": 2}, "end": {"line": 6, "character": 6}}, "targetRange": {"start": {"line": 6, "character": 2}, "end": {"line": 6, "character": 6}}, "originSelectionRange": {"start": {"line": 14, "character": 2}, "end": {"line": 14, "character": 6}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 16, "character": 2}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 2, "character": 10}, "end": {"line": 2, "character": 13}}, "targetRange": {"start": {"line": 2, "character": 0}, "end": {"line": 2, "character": 19}}, "originSelectionRange": {"start": {"line": 16, "character": 2}, "end": {"line": 16, "character": 5}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 20, "character": 11}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 2, "character": 10}, "end": {"line": 2, "character": 13}}, "targetRange": @@ -44,9 +44,9 @@ "originSelectionRange": {"start": {"line": 20, "character": 8}, "end": {"line": 20, "character": 11}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 28, "character": 12}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 22, "character": 10}, "end": {"line": 22, "character": 27}}, @@ -55,18 +55,18 @@ "originSelectionRange": {"start": {"line": 28, "character": 10}, "end": {"line": 28, "character": 27}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 30, "character": 2}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 3}}, "targetRange": {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 3}}, "originSelectionRange": {"start": {"line": 30, "character": 2}, "end": {"line": 30, "character": 3}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 34, "character": 14}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 9, "character": 4}, "end": {"line": 9, "character": 10}}, "targetRange": @@ -74,9 +74,9 @@ "originSelectionRange": {"start": {"line": 34, "character": 14}, "end": {"line": 34, "character": 20}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 43, "character": 7}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 36, "character": 16}, "end": {"line": 36, "character": 24}}, @@ -85,9 +85,9 @@ "originSelectionRange": {"start": {"line": 43, "character": 7}, "end": {"line": 43, "character": 11}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 43, "character": 7}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 38, "character": 26}, "end": {"line": 38, "character": 38}}, @@ -97,9 +97,9 @@ "originSelectionRange": {"start": {"line": 43, "character": 7}, "end": {"line": 43, "character": 11}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 48, "character": 28}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 46, "character": 4}, "end": {"line": 46, "character": 7}}, "targetRange": @@ -107,27 +107,27 @@ "originSelectionRange": {"start": {"line": 48, "character": 28}, "end": {"line": 48, "character": 29}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 54, "character": 2}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 52, "character": 6}, "end": {"line": 52, "character": 7}}, "targetRange": {"start": {"line": 52, "character": 6}, "end": {"line": 52, "character": 7}}, "originSelectionRange": {"start": {"line": 54, "character": 2}, "end": {"line": 54, "character": 3}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 54, "character": 6}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 57, "character": 2}, "end": {"line": 57, "character": 3}}, "targetRange": {"start": {"line": 57, "character": 2}, "end": {"line": 57, "character": 3}}, "originSelectionRange": {"start": {"line": 54, "character": 6}, "end": {"line": 54, "character": 7}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 60, "character": 7}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 59, "character": 0}, "end": {"line": 59, "character": 29}}, "targetRange": @@ -135,9 +135,9 @@ "originSelectionRange": {"start": {"line": 60, "character": 7}, "end": {"line": 60, "character": 11}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 87, "character": 16}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}}, "targetRange": @@ -145,7 +145,7 @@ "originSelectionRange": {"start": {"line": 87, "character": 7}, "end": {"line": 87, "character": 18}}}, - {"targetUri": "file://goTo.lean", + {"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}}, "targetRange": @@ -153,9 +153,9 @@ "originSelectionRange": {"start": {"line": 87, "character": 7}, "end": {"line": 87, "character": 18}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 87, "character": 12}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}}, "targetRange": @@ -163,9 +163,9 @@ "originSelectionRange": {"start": {"line": 87, "character": 7}, "end": {"line": 87, "character": 15}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 89, "character": 13}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}}, "targetRange": @@ -173,7 +173,7 @@ "originSelectionRange": {"start": {"line": 89, "character": 8}, "end": {"line": 89, "character": 16}}}, - {"targetUri": "file://goTo.lean", + {"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}}, "targetRange": @@ -181,9 +181,9 @@ "originSelectionRange": {"start": {"line": 89, "character": 8}, "end": {"line": 89, "character": 16}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 91, "character": 13}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 6}}, "targetRange": @@ -191,7 +191,7 @@ "originSelectionRange": {"start": {"line": 91, "character": 8}, "end": {"line": 91, "character": 17}}}, - {"targetUri": "file://goTo.lean", + {"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}}, "targetRange": @@ -199,9 +199,9 @@ "originSelectionRange": {"start": {"line": 91, "character": 8}, "end": {"line": 91, "character": 17}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 95, "character": 13}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}}, "targetRange": @@ -209,9 +209,9 @@ "originSelectionRange": {"start": {"line": 95, "character": 8}, "end": {"line": 95, "character": 16}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 99, "character": 13}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 68, "character": 2}, "end": {"line": 68, "character": 5}}, "targetRange": @@ -219,7 +219,7 @@ "originSelectionRange": {"start": {"line": 99, "character": 8}, "end": {"line": 99, "character": 16}}}, - {"targetUri": "file://goTo.lean", + {"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 81, "character": 0}, "end": {"line": 81, "character": 8}}, "targetRange": @@ -227,9 +227,9 @@ "originSelectionRange": {"start": {"line": 99, "character": 8}, "end": {"line": 99, "character": 16}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 103, "character": 13}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 73, "character": 4}, "end": {"line": 73, "character": 12}}, "targetRange": @@ -237,9 +237,9 @@ "originSelectionRange": {"start": {"line": 103, "character": 8}, "end": {"line": 103, "character": 16}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 108, "character": 13}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 77, "character": 2}, "end": {"line": 77, "character": 5}}, "targetRange": @@ -247,7 +247,7 @@ "originSelectionRange": {"start": {"line": 108, "character": 8}, "end": {"line": 108, "character": 16}}}, - {"targetUri": "file://goTo.lean", + {"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 83, "character": 0}, "end": {"line": 83, "character": 8}}, "targetRange": @@ -255,7 +255,7 @@ "originSelectionRange": {"start": {"line": 108, "character": 8}, "end": {"line": 108, "character": 16}}}, - {"targetUri": "file://goTo.lean", + {"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}}, "targetRange": @@ -263,9 +263,9 @@ "originSelectionRange": {"start": {"line": 108, "character": 8}, "end": {"line": 108, "character": 16}}}] -{"textDocument": {"uri": "file://goTo.lean"}, +{"textDocument": {"uri": "file:///goTo.lean"}, "position": {"line": 112, "character": 7}} -[{"targetUri": "file://goTo.lean", +[{"targetUri": "file:///goTo.lean", "targetSelectionRange": {"start": {"line": 9, "character": 4}, "end": {"line": 9, "character": 10}}, "targetRange": diff --git a/tests/lean/interactive/goTo2.lean.expected.out b/tests/lean/interactive/goTo2.lean.expected.out index 3dc760c2d105..18a74f7f9dd6 100644 --- a/tests/lean/interactive/goTo2.lean.expected.out +++ b/tests/lean/interactive/goTo2.lean.expected.out @@ -1,6 +1,6 @@ -{"textDocument": {"uri": "file://goTo2.lean"}, +{"textDocument": {"uri": "file:///goTo2.lean"}, "position": {"line": 10, "character": 15}} -[{"targetUri": "file://goTo2.lean", +[{"targetUri": "file:///goTo2.lean", "targetSelectionRange": {"start": {"line": 1, "character": 0}, "end": {"line": 1, "character": 55}}, "targetRange": @@ -8,9 +8,9 @@ "originSelectionRange": {"start": {"line": 10, "character": 11}, "end": {"line": 10, "character": 20}}}] -{"textDocument": {"uri": "file://goTo2.lean"}, +{"textDocument": {"uri": "file:///goTo2.lean"}, "position": {"line": 10, "character": 27}} -[{"targetUri": "file://goTo2.lean", +[{"targetUri": "file:///goTo2.lean", "targetSelectionRange": {"start": {"line": 2, "character": 0}, "end": {"line": 2, "character": 55}}, "targetRange": @@ -18,9 +18,9 @@ "originSelectionRange": {"start": {"line": 10, "character": 23}, "end": {"line": 10, "character": 30}}}] -{"textDocument": {"uri": "file://goTo2.lean"}, +{"textDocument": {"uri": "file:///goTo2.lean"}, "position": {"line": 10, "character": 11}} -[{"targetUri": "file://goTo2.lean", +[{"targetUri": "file:///goTo2.lean", "targetSelectionRange": {"start": {"line": 14, "character": 4}, "end": {"line": 14, "character": 5}}, "targetRange": diff --git a/tests/lean/interactive/goalEOF.lean.expected.out b/tests/lean/interactive/goalEOF.lean.expected.out index 8bb8197ac43d..aa06e923e659 100644 --- a/tests/lean/interactive/goalEOF.lean.expected.out +++ b/tests/lean/interactive/goalEOF.lean.expected.out @@ -1,3 +1,3 @@ -{"textDocument": {"uri": "file://goalEOF.lean"}, +{"textDocument": {"uri": "file:///goalEOF.lean"}, "position": {"line": 5, "character": 25}} {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]} diff --git a/tests/lean/interactive/goalIssue.lean.expected.out b/tests/lean/interactive/goalIssue.lean.expected.out index d6e35fe956db..83627f6f41b7 100644 --- a/tests/lean/interactive/goalIssue.lean.expected.out +++ b/tests/lean/interactive/goalIssue.lean.expected.out @@ -1,8 +1,8 @@ -{"textDocument": {"uri": "file://goalIssue.lean"}, +{"textDocument": {"uri": "file:///goalIssue.lean"}, "position": {"line": 2, "character": 12}} {"rendered": "```lean\nx : Nat\nthis : x + x = x + x\n⊢ 0 + x = x\n```", "goals": ["x : Nat\nthis : x + x = x + x\n⊢ 0 + x = x"]} -{"textDocument": {"uri": "file://goalIssue.lean"}, +{"textDocument": {"uri": "file:///goalIssue.lean"}, "position": {"line": 8, "character": 12}} {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```", "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]} diff --git a/tests/lean/interactive/haveInfo.lean.expected.out b/tests/lean/interactive/haveInfo.lean.expected.out index 8b7b86378966..bed3a64ebfcd 100644 --- a/tests/lean/interactive/haveInfo.lean.expected.out +++ b/tests/lean/interactive/haveInfo.lean.expected.out @@ -1,12 +1,12 @@ -{"textDocument": {"uri": "file://haveInfo.lean"}, +{"textDocument": {"uri": "file:///haveInfo.lean"}, "position": {"line": 2, "character": 4}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} -{"textDocument": {"uri": "file://haveInfo.lean"}, +{"textDocument": {"uri": "file:///haveInfo.lean"}, "position": {"line": 8, "character": 17}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} -{"textDocument": {"uri": "file://haveInfo.lean"}, +{"textDocument": {"uri": "file:///haveInfo.lean"}, "position": {"line": 15, "character": 17}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} -{"textDocument": {"uri": "file://haveInfo.lean"}, +{"textDocument": {"uri": "file:///haveInfo.lean"}, "position": {"line": 23, "character": 2}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} diff --git a/tests/lean/interactive/highlight.lean.expected.out b/tests/lean/interactive/highlight.lean.expected.out index 8feb7444c434..27c5f6e779d3 100644 --- a/tests/lean/interactive/highlight.lean.expected.out +++ b/tests/lean/interactive/highlight.lean.expected.out @@ -1,9 +1,9 @@ -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 1, "character": 23}} [{"range": {"start": {"line": 1, "character": 22}, "end": {"line": 1, "character": 26}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 5, "character": 7}} [{"range": {"start": {"line": 1, "character": 4}, "end": {"line": 1, "character": 8}}, @@ -14,7 +14,7 @@ {"range": {"start": {"line": 5, "character": 6}, "end": {"line": 5, "character": 10}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 10, "character": 3}} [{"range": {"start": {"line": 9, "character": 6}, "end": {"line": 9, "character": 9}}, @@ -22,7 +22,7 @@ {"range": {"start": {"line": 10, "character": 2}, "end": {"line": 10, "character": 5}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 15, "character": 3}} [{"range": {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 6}}, @@ -31,7 +31,7 @@ {"start": {"line": 23, "character": 16}, "end": {"line": 23, "character": 20}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 19, "character": 7}} [{"range": {"start": {"line": 14, "character": 2}, "end": {"line": 14, "character": 5}}, @@ -42,7 +42,7 @@ {"range": {"start": {"line": 23, "character": 4}, "end": {"line": 23, "character": 7}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 23, "character": 5}} [{"range": {"start": {"line": 14, "character": 2}, "end": {"line": 14, "character": 5}}, @@ -53,7 +53,7 @@ {"range": {"start": {"line": 23, "character": 4}, "end": {"line": 23, "character": 7}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 23, "character": 12}} [{"range": {"start": {"line": 22, "character": 10}, @@ -67,7 +67,7 @@ {"start": {"line": 23, "character": 24}, "end": {"line": 23, "character": 27}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 30, "character": 2}} [{"range": {"start": {"line": 28, "character": 10}, @@ -79,7 +79,7 @@ {"range": {"start": {"line": 30, "character": 2}, "end": {"line": 30, "character": 3}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 41, "character": 7}} [{"range": {"start": {"line": 34, "character": 10}, @@ -104,7 +104,7 @@ {"range": {"start": {"line": 41, "character": 7}, "end": {"line": 41, "character": 8}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 48, "character": 9}} [{"range": {"start": {"line": 45, "character": 10}, @@ -116,7 +116,7 @@ {"range": {"start": {"line": 48, "character": 9}, "end": {"line": 48, "character": 10}}, "kind": 1}] -{"textDocument": {"uri": "file://highlight.lean"}, +{"textDocument": {"uri": "file:///highlight.lean"}, "position": {"line": 53, "character": 9}} [{"range": {"start": {"line": 53, "character": 9}, "end": {"line": 53, "character": 10}}, diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 0ee83936b0e3..11bd07180dcd 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 3, "character": 8}} {"range": {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 18}}, @@ -6,7 +6,7 @@ {"value": "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 7, "character": 8}} {"range": {"start": {"line": 7, "character": 8}, "end": {"line": 7, "character": 18}}, @@ -14,7 +14,7 @@ {"value": "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 12, "character": 4}} {"range": {"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}}, @@ -22,17 +22,17 @@ {"value": "```lean\nNat.zero : Nat\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 21, "character": 2}} {"range": {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 23}}, "contents": {"value": "My tactic ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 21, "character": 8}} {"range": {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 23}}, "contents": {"value": "My tactic ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 21, "character": 13}} {"range": {"start": {"line": 21, "character": 13}, "end": {"line": 21, "character": 23}}, @@ -40,7 +40,7 @@ {"value": "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 28, "character": 6}} {"range": {"start": {"line": 28, "character": 6}, "end": {"line": 28, "character": 12}}, @@ -48,7 +48,7 @@ {"value": "```lean\nLean.Parser.Category.tactic : Lean.Parser.Category\n```\n***\n`tactic` is the builtin syntax category for tactics. These appear after\n`by` in proofs, and they are programs that take in the proof context\n(the hypotheses in scope plus the type of the term to synthesize) and construct\na term of the expected type. For example, `simp` is a tactic, used in:\n```\nexample : 2 + 2 = 4 := by simp\n```\n\n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 28, "character": 32}} {"range": {"start": {"line": 28, "character": 32}, "end": {"line": 28, "character": 36}}, @@ -56,7 +56,7 @@ {"value": "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 31, "character": 6}} {"range": {"start": {"line": 31, "character": 6}, "end": {"line": 31, "character": 12}}, @@ -64,7 +64,7 @@ {"value": "```lean\nLean.Parser.Category.tactic : Lean.Parser.Category\n```\n***\n`tactic` is the builtin syntax category for tactics. These appear after\n`by` in proofs, and they are programs that take in the proof context\n(the hypotheses in scope plus the type of the term to synthesize) and construct\na term of the expected type. For example, `simp` is a tactic, used in:\n```\nexample : 2 + 2 = 4 := by simp\n```\n\n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 31, "character": 24}} {"range": {"start": {"line": 31, "character": 23}, "end": {"line": 31, "character": 27}}, @@ -72,49 +72,49 @@ {"value": "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 36, "character": 2}} {"range": {"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 23}}, "contents": {"value": "My tactic ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 44, "character": 2}} {"range": {"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 23}}, "contents": {"value": "My tactic ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 49, "character": 16}} {"range": {"start": {"line": 49, "character": 15}, "end": {"line": 49, "character": 21}}, "contents": {"value": "```lean\nmyNota : Lean.ParserDescr\n```\n***\nMy notation ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 52, "character": 7}} {"range": {"start": {"line": 52, "character": 7}, "end": {"line": 52, "character": 15}}, "contents": {"value": "```lean\n1 : Nat\n```\n***\nMy notation ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 59, "character": 7}} {"range": {"start": {"line": 59, "character": 7}, "end": {"line": 59, "character": 15}}, "contents": {"value": "```lean\nNat\n```\n***\nMy notation ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 69, "character": 7}} {"range": {"start": {"line": 69, "character": 7}, "end": {"line": 69, "character": 16}}, "contents": {"value": "```lean\nNat\n```\n***\nMy ultimate notation ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 73, "character": 21}} {"range": {"start": {"line": 73, "character": 18}, "end": {"line": 73, "character": 25}}, "contents": {"value": "```lean\nmyInfix : Lean.TrailingParserDescr\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 73, "character": 39}} {"range": {"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}}, @@ -122,7 +122,7 @@ {"value": "```lean\nNat.add (a✝a✝¹ : Nat) : Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 77, "character": 10}} {"range": {"start": {"line": 77, "character": 7}, "end": {"line": 77, "character": 14}}, @@ -130,7 +130,7 @@ {"value": "```lean\nNat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 82, "character": 7}} {"range": {"start": {"line": 82, "character": 7}, "end": {"line": 82, "character": 8}}, @@ -138,7 +138,7 @@ {"value": "```lean\nNat : Type\n```\n***\nThe type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 87, "character": 14}} {"range": {"start": {"line": 87, "character": 14}, "end": {"line": 87, "character": 36}}, @@ -146,7 +146,7 @@ {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```\n***\nA `doSeq` is a sequence of `doElem`, the main argument after the `do` keyword and other\ndo elements that take blocks. It can either have the form `\"{\" (doElem \";\"?)* \"}\"` or\n`many1Indent (doElem \";\"?)`, where `many1Indent` ensures that all the items are at\nthe same or higher indentation level as the first line. \n***\n*import Lean.Parser.Do*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 89, "character": 30}} {"range": {"start": {"line": 89, "character": 29}, "end": {"line": 89, "character": 34}}, @@ -154,17 +154,17 @@ {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```\n***\nA `doSeq` is a sequence of `doElem`, the main argument after the `do` keyword and other\ndo elements that take blocks. It can either have the form `\"{\" (doElem \";\"?)* \"}\"` or\n`many1Indent (doElem \";\"?)`, where `many1Indent` ensures that all the items are at\nthe same or higher indentation level as the first line. \n***\n*import Lean.Parser.Do*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 92, "character": 2}} {"range": {"start": {"line": 92, "character": 0}, "end": {"line": 92, "character": 7}}, "contents": {"value": "My command ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 99, "character": 2}} {"range": {"start": {"line": 99, "character": 0}, "end": {"line": 99, "character": 7}}, "contents": {"value": "My command ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 102, "character": 16}} {"range": {"start": {"line": 102, "character": 16}, @@ -173,7 +173,7 @@ {"value": "```lean\nLean.Parser.ppSpace : Lean.Parser.Parser\n```\n***\nNo-op parser that advises the pretty printer to emit a space/soft line break. \n***\n*import Lean.Parser.Extra*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 102, "character": 24}} {"range": {"start": {"line": 102, "character": 24}, @@ -182,7 +182,7 @@ {"value": "```lean\nLean.ParserDescr.sepBy1 (p : Lean.ParserDescr) (sep : String) (psep : Lean.ParserDescr)\n (allowTrailingSep : Bool := false) : Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 102, "character": 31}} {"range": {"start": {"line": 102, "character": 31}, @@ -191,12 +191,12 @@ {"value": "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. \n***\n*import Init.Notation*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 111, "character": 2}} {"range": {"start": {"line": 111, "character": 0}, "end": {"line": 111, "character": 8}}, "contents": {"value": "My ultimate command ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 115, "character": 10}} {"range": {"start": {"line": 115, "character": 8}, @@ -205,7 +205,7 @@ {"value": "Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be\ninherited. If `e` is itself a variable called `x`, it can be elided:\n`fun y => { x := 1, y }`.\nA *structure update* of an existing value can be given via `with`:\n`{ point with x := 1 }`.\nThe structure type can be specified if not inferable:\n`{ x := 1, y := 2 : Point }`.\n", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 119, "character": 8}} {"range": {"start": {"line": 119, "character": 8}, @@ -214,84 +214,84 @@ {"value": "```lean\nid.{u} {α : Sort u} (a : α) : α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 119, "character": 10}} {"range": {"start": {"line": 119, "character": 8}, "end": {"line": 119, "character": 21}}, "contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 126, "character": 2}} {"range": {"start": {"line": 126, "character": 2}, "end": {"line": 126, "character": 3}}, "contents": {"value": "```lean\nn : Id ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 133, "character": 9}} {"range": {"start": {"line": 133, "character": 7}, "end": {"line": 133, "character": 17}}, "contents": {"value": "```lean\nfoo : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 138, "character": 7}} {"range": {"start": {"line": 138, "character": 7}, "end": {"line": 138, "character": 10}}, "contents": {"value": "```lean\nBar.foo : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 141, "character": 9}} {"range": {"start": {"line": 141, "character": 7}, "end": {"line": 141, "character": 17}}, "contents": {"value": "```lean\n_root_.foo : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 144, "character": 4}} {"range": {"start": {"line": 144, "character": 4}, "end": {"line": 144, "character": 7}}, "contents": {"value": "```lean\nBar.bar : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 147, "character": 10}} {"range": {"start": {"line": 147, "character": 10}, "end": {"line": 147, "character": 13}}, "contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 147, "character": 17}} {"range": {"start": {"line": 147, "character": 17}, "end": {"line": 147, "character": 19}}, "contents": {"value": "```lean\nBar.Foo.mk (hi : ℕ) : Foo\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 150, "character": 2}} {"range": {"start": {"line": 150, "character": 2}, "end": {"line": 150, "character": 4}}, "contents": {"value": "```lean\nBar.Foo.hi (self : Foo) : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 153, "character": 10}} {"range": {"start": {"line": 153, "character": 10}, "end": {"line": 153, "character": 13}}, "contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 155, "character": 4}} {"range": {"start": {"line": 155, "character": 4}, "end": {"line": 155, "character": 6}}, "contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 158, "character": 2}} {"range": {"start": {"line": 158, "character": 0}, "end": {"line": 158, "character": 8}}, "contents": {"value": "```lean\nBar.instToStringNat : ToString ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 160, "character": 9}} {"range": {"start": {"line": 160, "character": 9}, "end": {"line": 160, "character": 10}}, "contents": {"value": "```lean\nBar.f : ToString ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 163, "character": 10}} {"range": {"start": {"line": 163, "character": 10}, @@ -299,26 +299,26 @@ "contents": {"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 166, "character": 4}} {"range": {"start": {"line": 166, "character": 4}, "end": {"line": 166, "character": 11}}, "contents": {"value": "```lean\nBar.foo.bar : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 166, "character": 8}} {"range": {"start": {"line": 166, "character": 4}, "end": {"line": 166, "character": 11}}, "contents": {"value": "```lean\nBar.foo.bar : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 173, "character": 6}} {"range": {"start": {"line": 173, "character": 6}, "end": {"line": 173, "character": 7}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 176, "character": 4}} -[{"targetUri": "file://hover.lean", +[{"targetUri": "file:///hover.lean", "targetSelectionRange": {"start": {"line": 173, "character": 6}, "end": {"line": 173, "character": 7}}, @@ -328,26 +328,26 @@ "originSelectionRange": {"start": {"line": 176, "character": 4}, "end": {"line": 176, "character": 5}}}] -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 176, "character": 4}} {"range": {"start": {"line": 176, "character": 4}, "end": {"line": 176, "character": 5}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 180, "character": 12}} {"range": {"start": {"line": 180, "character": 11}, "end": {"line": 180, "character": 33}}, "contents": {"value": "enable the 'unused variables' linter", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 183, "character": 8}} {"range": {"start": {"line": 183, "character": 8}, "end": {"line": 183, "character": 9}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 186, "character": 8}} -[{"targetUri": "file://hover.lean", +[{"targetUri": "file:///hover.lean", "targetSelectionRange": {"start": {"line": 183, "character": 8}, "end": {"line": 183, "character": 9}}, @@ -357,18 +357,18 @@ "originSelectionRange": {"start": {"line": 186, "character": 8}, "end": {"line": 186, "character": 9}}}] -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 186, "character": 8}} {"range": {"start": {"line": 186, "character": 8}, "end": {"line": 186, "character": 9}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 191, "character": 25}} {"range": {"start": {"line": 191, "character": 25}, "end": {"line": 191, "character": 26}}, "contents": {"value": "```lean\nn : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 194, "character": 2}} {"range": {"start": {"line": 194, "character": 0}, "end": {"line": 194, "character": 9}}, @@ -376,7 +376,7 @@ {"value": "`declModifiers` is the collection of modifiers on a declaration:\n* a doc comment `/-- ... -/`\n* a list of attributes `@[attr1, attr2]`\n* a visibility specifier, `private` or `protected`\n* `noncomputable`\n* `unsafe`\n* `partial` or `nonrec`\n\nAll modifiers are optional, and have to come in the listed order.\n\n`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed\non the same line as the declaration. It is used for declarations nested inside other syntax,\nsuch as inductive constructors, structure projections, and `let rec` / `where` definitions. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 200, "character": 2}} {"range": {"start": {"line": 200, "character": 2}, @@ -385,7 +385,7 @@ {"value": "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 203, "character": 28}} {"range": {"start": {"line": 203, "character": 27}, @@ -394,12 +394,12 @@ {"value": "```lean\nId ℕ\n```\n***\nParentheses, used for grouping expressions (e.g., `a * (b + c)`).\nCan also be used for creating simple functions when combined with `·`. Here are some examples:\n - `(· + 1)` is shorthand for `fun x => x + 1`\n - `(· + ·)` is shorthand for `fun x y => x + y`\n - `(f · a b)` is shorthand for `fun x => f x a b`\n - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n - also applies to other parentheses-like notations such as `(·, 1)`\n", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 206, "character": 8}} {"range": {"start": {"line": 206, "character": 8}, "end": {"line": 206, "character": 9}}, "contents": {"value": "```lean\n?m\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 206, "character": 10}} {"range": {"start": {"line": 206, "character": 8}, @@ -408,48 +408,48 @@ {"value": "```lean\n?m x✝¹ x✝\n```\n***\n`a + b` computes the sum of `a` and `b`.\nThe meaning of this notation is type-dependent. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 215, "character": 28}} {"range": {"start": {"line": 215, "character": 28}, "end": {"line": 215, "character": 29}}, "contents": {"value": "```lean\nx : α\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 217, "character": 28}} {"range": {"start": {"line": 217, "character": 28}, "end": {"line": 217, "character": 29}}, "contents": {"value": "```lean\nα\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 219, "character": 31}} {"range": {"start": {"line": 219, "character": 31}, "end": {"line": 219, "character": 32}}, "contents": {"value": "```lean\nx : α\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 222, "character": 22}} {"range": {"start": {"line": 222, "character": 22}, "end": {"line": 222, "character": 32}}, "contents": {"value": "my_intro tactic ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 222, "character": 31}} {"range": {"start": {"line": 222, "character": 31}, "end": {"line": 222, "character": 32}}, "contents": {"value": "```lean\nα\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 229, "character": 22}} {"range": {"start": {"line": 229, "character": 22}, "end": {"line": 229, "character": 32}}, "contents": {"value": "my_intro tactic ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 232, "character": 8}} {"range": {"start": {"line": 232, "character": 8}, "end": {"line": 232, "character": 9}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 235, "character": 4}} {"range": {"start": {"line": 235, "character": 4}, "end": {"line": 235, "character": 8}}, @@ -457,7 +457,7 @@ {"value": "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 238, "character": 4}} {"range": {"start": {"line": 238, "character": 4}, "end": {"line": 238, "character": 8}}, @@ -465,24 +465,24 @@ {"value": "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 238, "character": 9}} {"range": {"start": {"line": 238, "character": 9}, "end": {"line": 238, "character": 10}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 242, "character": 8}} {"range": {"start": {"line": 242, "character": 8}, "end": {"line": 242, "character": 9}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 244, "character": 12}} {"range": {"start": {"line": 244, "character": 12}, "end": {"line": 244, "character": 13}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 246, "character": 4}} {"range": {"start": {"line": 246, "character": 4}, "end": {"line": 246, "character": 8}}, @@ -490,7 +490,7 @@ {"value": "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 249, "character": 9}} {"range": {"start": {"line": 249, "character": 9}, @@ -499,13 +499,13 @@ {"value": "```lean\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 249, "character": 11}} {"range": {"start": {"line": 249, "character": 11}, "end": {"line": 249, "character": 13}}, "contents": {"value": "```lean\nih : True\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 254, "character": 6}} {"range": {"start": {"line": 254, "character": 4}, "end": {"line": 254, "character": 9}}, @@ -513,7 +513,7 @@ {"value": "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 254, "character": 15}} {"range": {"start": {"line": 254, "character": 13}, @@ -522,7 +522,7 @@ {"value": "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 257, "character": 6}} {"range": {"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}}, @@ -530,7 +530,7 @@ {"value": "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 257, "character": 17}} {"range": {"start": {"line": 257, "character": 15}, @@ -539,7 +539,7 @@ {"value": "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 260, "character": 27}} {"range": {"start": {"line": 260, "character": 27}, @@ -548,7 +548,7 @@ {"value": "```lean\nInhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α\n```\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 260, "character": 28}} {"range": {"start": {"line": 260, "character": 28}, @@ -557,7 +557,7 @@ {"value": "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 266, "character": 2}} {"range": {"start": {"line": 266, "character": 2}, "end": {"line": 266, "character": 3}}, @@ -565,25 +565,25 @@ {"value": "```lean\nlet x :=\n match 0 with\n | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 269, "character": 4}} {"range": {"start": {"line": 269, "character": 4}, "end": {"line": 269, "character": 8}}, "contents": {"value": "```lean\nauto (o : ℕ := by exact 1) : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 274, "character": 22}} {"range": {"start": {"line": 274, "character": 22}, "end": {"line": 274, "character": 23}}, "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 274, "character": 13}} {"range": {"start": {"line": 274, "character": 13}, "end": {"line": 274, "character": 15}}, "contents": {"value": "```lean\n_e : 1 = x\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 280, "character": 13}} {"range": {"start": {"line": 280, "character": 13}, @@ -592,7 +592,7 @@ {"value": "```lean\nList.nil.{u} {α : Type u} : List α\n```\n***\n`[]` is the empty list. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 282, "character": 13}} {"range": {"start": {"line": 282, "character": 11}, @@ -601,7 +601,7 @@ {"value": "```lean\nList.cons.{u} {α : Type u} (head : α) (tail : List α) : List α\n```\n***\nIf `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the\nlist whose first element is `a` and with `l` as the rest of the list. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 284, "character": 18}} {"range": {"start": {"line": 284, "character": 17}, @@ -610,7 +610,7 @@ {"value": "```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 287, "character": 26}} {"range": {"start": {"line": 287, "character": 25}, @@ -619,7 +619,7 @@ {"value": "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, +{"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 287, "character": 19}} {"range": {"start": {"line": 287, "character": 19}, diff --git a/tests/lean/interactive/hoverAt.lean.expected.out b/tests/lean/interactive/hoverAt.lean.expected.out index 3634be3173bd..8a129ccea466 100644 --- a/tests/lean/interactive/hoverAt.lean.expected.out +++ b/tests/lean/interactive/hoverAt.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://hoverAt.lean"}, +{"textDocument": {"uri": "file:///hoverAt.lean"}, "position": {"line": 8, "character": 18}} {"range": {"start": {"line": 8, "character": 17}, "end": {"line": 8, "character": 34}}, diff --git a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out b/tests/lean/interactive/hoverBinderUndescore.lean.expected.out index 5fdb8faa989a..c53f87cf026a 100644 --- a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out +++ b/tests/lean/interactive/hoverBinderUndescore.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://hoverBinderUndescore.lean"}, +{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"}, "position": {"line": 1, "character": 5}} {"range": {"start": {"line": 1, "character": 5}, "end": {"line": 1, "character": 6}}, @@ -6,7 +6,7 @@ {"value": "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverBinderUndescore.lean"}, +{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"}, "position": {"line": 1, "character": 7}} {"range": {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 8}}, @@ -14,7 +14,7 @@ {"value": "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverBinderUndescore.lean"}, +{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"}, "position": {"line": 6, "character": 6}} {"range": {"start": {"line": 6, "character": 6}, "end": {"line": 6, "character": 7}}, @@ -22,7 +22,7 @@ {"value": "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverBinderUndescore.lean"}, +{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"}, "position": {"line": 6, "character": 8}} {"range": {"start": {"line": 6, "character": 8}, "end": {"line": 6, "character": 9}}, @@ -30,7 +30,7 @@ {"value": "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverBinderUndescore.lean"}, +{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"}, "position": {"line": 11, "character": 6}} {"range": {"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 7}}, @@ -38,7 +38,7 @@ {"value": "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverBinderUndescore.lean"}, +{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"}, "position": {"line": 11, "character": 8}} {"range": {"start": {"line": 11, "character": 8}, "end": {"line": 11, "character": 9}}, diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index 09f0cb0da501..844b67da3b4b 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -1,20 +1,20 @@ -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 8, "character": 11}} {"range": {"start": {"line": 8, "character": 7}, "end": {"line": 8, "character": 14}}, "contents": {"value": "```lean\nFoo.foo : Foo\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 12, "character": 7}} {"range": {"start": {"line": 12, "character": 7}, "end": {"line": 12, "character": 10}}, "contents": {"value": "```lean\nFoo.foo : Foo\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 12, "character": 11}} {"range": {"start": {"line": 12, "character": 11}, "end": {"line": 12, "character": 13}}, "contents": {"value": "```lean\nFoo.f₁ (self : Foo) : Nat\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 12, "character": 14}} {"range": {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}}, @@ -22,13 +22,13 @@ {"value": "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 16, "character": 11}} {"range": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 13}}, "contents": {"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 16, "character": 14}} {"range": {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}}, @@ -36,13 +36,13 @@ {"value": "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 19, "character": 13}} {"range": {"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 15}}, "contents": {"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 19, "character": 16}} {"range": {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}}, @@ -50,13 +50,13 @@ {"value": "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 22, "character": 14}} {"range": {"start": {"line": 22, "character": 14}, "end": {"line": 22, "character": 16}}, "contents": {"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hoverDot.lean"}, +{"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 22, "character": 17}} {"range": {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}}, diff --git a/tests/lean/interactive/hoverException.lean.expected.out b/tests/lean/interactive/hoverException.lean.expected.out index f692d42901ae..af093fa3a839 100644 --- a/tests/lean/interactive/hoverException.lean.expected.out +++ b/tests/lean/interactive/hoverException.lean.expected.out @@ -1,3 +1,3 @@ -{"textDocument": {"uri": "file://hoverException.lean"}, +{"textDocument": {"uri": "file:///hoverException.lean"}, "position": {"line": 2, "character": 14}} null diff --git a/tests/lean/interactive/inWordCompletion.lean.expected.out b/tests/lean/interactive/inWordCompletion.lean.expected.out index 45517b167606..08fdc098945d 100644 --- a/tests/lean/interactive/inWordCompletion.lean.expected.out +++ b/tests/lean/interactive/inWordCompletion.lean.expected.out @@ -1,11 +1,11 @@ -{"textDocument": {"uri": "file://inWordCompletion.lean"}, +{"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 5, "character": 10}} {"items": [{"label": "gfabc", "kind": 3, "detail": "Nat → Nat"}, {"label": "gfacc", "kind": 3, "detail": "Nat → Nat"}, {"label": "gfadc", "kind": 3, "detail": "Nat → Nat"}], "isIncomplete": true} -{"textDocument": {"uri": "file://inWordCompletion.lean"}, +{"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 13, "character": 14}} {"items": [{"label": "gfabc", "kind": 3, "detail": "Nat → Nat"}, diff --git a/tests/lean/interactive/infoIssues.lean.expected.out b/tests/lean/interactive/infoIssues.lean.expected.out index d7012c79dc1e..699aff477070 100644 --- a/tests/lean/interactive/infoIssues.lean.expected.out +++ b/tests/lean/interactive/infoIssues.lean.expected.out @@ -1,9 +1,9 @@ -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 3, "character": 2}} {"rendered": "```lean\nx y : Nat\nh : x = y\nthis : y = x\n⊢ 0 + x = y + 0\n```", "goals": ["x y : Nat\nh : x = y\nthis : y = x\n⊢ 0 + x = y + 0"]} -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 13, "character": 33}} {"rendered": "```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + (0 + Nat.succ n✝)\n```\n---\n```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + Nat.succ n✝\n```\n---\n```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = Nat.succ n✝\n```", @@ -11,30 +11,30 @@ ["p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + (0 + Nat.succ n✝)", "p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + Nat.succ n✝", "p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = Nat.succ n✝"]} -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 13, "character": 36}} {"rendered": "```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + (0 + Nat.succ n✝)\n```\n---\n```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + Nat.succ n✝\n```", "goals": ["p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + (0 + Nat.succ n✝)", "p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + Nat.succ n✝"]} -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 15, "character": 2}} {"rendered": "```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```", "goals": ["case right\np : Prop\nx : Nat\n⊢ p"]} -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 25, "character": 35}} {"rendered": "```lean\np : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (y + 1))\n```\n---\n```lean\np : Prop\nx y : Nat\n⊢ y + 1 = 0 + (y + 1)\n```", "goals": ["p : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (y + 1))", "p : Prop\nx y : Nat\n⊢ y + 1 = 0 + (y + 1)"]} -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 25, "character": 9}} {"rendered": "```lean\np : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (0 + (y + 1)))\n```", "goals": ["p : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (0 + (y + 1)))"]} -{"textDocument": {"uri": "file://infoIssues.lean"}, +{"textDocument": {"uri": "file:///infoIssues.lean"}, "position": {"line": 27, "character": 2}} {"rendered": "```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```", "goals": ["case right\np : Prop\nx : Nat\n⊢ p"]} diff --git a/tests/lean/interactive/internalNamesIssue.lean.expected.out b/tests/lean/interactive/internalNamesIssue.lean.expected.out index 2a72302a7453..f71d1926f9c2 100644 --- a/tests/lean/interactive/internalNamesIssue.lean.expected.out +++ b/tests/lean/interactive/internalNamesIssue.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://internalNamesIssue.lean"}, +{"textDocument": {"uri": "file:///internalNamesIssue.lean"}, "position": {"line": 9, "character": 11}} {"items": [{"label": "bla", "kind": 3, "detail": "Nat → Nat"}, diff --git a/tests/lean/interactive/jumpMutual.lean.expected.out b/tests/lean/interactive/jumpMutual.lean.expected.out index 79da0eaabb27..3e531b9212e5 100644 --- a/tests/lean/interactive/jumpMutual.lean.expected.out +++ b/tests/lean/interactive/jumpMutual.lean.expected.out @@ -1,27 +1,27 @@ -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 6, "character": 23}} [] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 7, "character": 17}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 10, "character": 2}, "end": {"line": 10, "character": 3}}, "targetRange": {"start": {"line": 10, "character": 2}, "end": {"line": 10, "character": 3}}, "originSelectionRange": {"start": {"line": 7, "character": 17}, "end": {"line": 7, "character": 18}}}] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 7, "character": 11}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 16, "character": 4}, "end": {"line": 16, "character": 5}}, "targetRange": {"start": {"line": 16, "character": 4}, "end": {"line": 16, "character": 5}}, "originSelectionRange": {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 12}}}] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 13, "character": 13}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 10, "character": 2}, "end": {"line": 10, "character": 3}}, "targetRange": @@ -29,9 +29,9 @@ "originSelectionRange": {"start": {"line": 13, "character": 13}, "end": {"line": 13, "character": 14}}}] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 13, "character": 19}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 2, "character": 4}, "end": {"line": 2, "character": 5}}, "targetRange": @@ -39,9 +39,9 @@ "originSelectionRange": {"start": {"line": 13, "character": 19}, "end": {"line": 13, "character": 20}}}] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 20, "character": 17}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 17, "character": 10}, "end": {"line": 17, "character": 11}}, @@ -51,9 +51,9 @@ "originSelectionRange": {"start": {"line": 20, "character": 17}, "end": {"line": 20, "character": 18}}}] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 22, "character": 2}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 17, "character": 10}, "end": {"line": 17, "character": 11}}, @@ -62,9 +62,9 @@ "end": {"line": 17, "character": 11}}, "originSelectionRange": {"start": {"line": 22, "character": 2}, "end": {"line": 22, "character": 3}}}] -{"textDocument": {"uri": "file://jumpMutual.lean"}, +{"textDocument": {"uri": "file:///jumpMutual.lean"}, "position": {"line": 22, "character": 8}} -[{"targetUri": "file://jumpMutual.lean", +[{"targetUri": "file:///jumpMutual.lean", "targetSelectionRange": {"start": {"line": 2, "character": 4}, "end": {"line": 2, "character": 5}}, "targetRange": diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out index 001ac9cc1492..09fc8e78963c 100644 --- a/tests/lean/interactive/keywordCompletion.lean.expected.out +++ b/tests/lean/interactive/keywordCompletion.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://keywordCompletion.lean"}, +{"textDocument": {"uri": "file:///keywordCompletion.lean"}, "position": {"line": 4, "character": 10}} {"items": [{"label": "bin", "kind": 21, "detail": "Type 1"}, @@ -7,7 +7,7 @@ {"label": "binrel%", "kind": 14, "detail": "keyword"}, {"label": "binrel_no_prop%", "kind": 14, "detail": "keyword"}], "isIncomplete": true} -{"textDocument": {"uri": "file://keywordCompletion.lean"}, +{"textDocument": {"uri": "file:///keywordCompletion.lean"}, "position": {"line": 4, "character": 13}} {"items": [{"label": "binop_lazy%", "kind": 14, "detail": "keyword"}], "isIncomplete": true} diff --git a/tests/lean/interactive/lean3HoverIssue.lean.expected.out b/tests/lean/interactive/lean3HoverIssue.lean.expected.out index 98836ec33b29..e3e7a1992c3f 100644 --- a/tests/lean/interactive/lean3HoverIssue.lean.expected.out +++ b/tests/lean/interactive/lean3HoverIssue.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 0, "character": 55}} {"range": {"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}}, @@ -6,12 +6,12 @@ {"value": "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 0, "character": 52}} {"range": {"start": {"line": 0, "character": 52}, "end": {"line": 0, "character": 53}}, "contents": {"value": "```lean\nh : x = y\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 4, "character": 46}} {"range": {"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}}, @@ -19,7 +19,7 @@ {"value": "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 7, "character": 54}} {"range": {"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}}, @@ -27,7 +27,7 @@ {"value": "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 7, "character": 65}} {"range": {"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}}, @@ -35,12 +35,12 @@ {"value": "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*", "kind": "markdown"}} -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 7, "character": 70}} {"range": {"start": {"line": 7, "character": 70}, "end": {"line": 7, "character": 71}}, "contents": {"value": "```lean\nh : x = y\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://lean3HoverIssue.lean"}, +{"textDocument": {"uri": "file:///lean3HoverIssue.lean"}, "position": {"line": 7, "character": 72}} {"range": {"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}}, diff --git a/tests/lean/interactive/macroGoalIssue.lean.expected.out b/tests/lean/interactive/macroGoalIssue.lean.expected.out index 18356b79d984..b87a4c2da1e6 100644 --- a/tests/lean/interactive/macroGoalIssue.lean.expected.out +++ b/tests/lean/interactive/macroGoalIssue.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://macroGoalIssue.lean"}, +{"textDocument": {"uri": "file:///macroGoalIssue.lean"}, "position": {"line": 2, "character": 2}} {"rendered": "```lean\nn : Nat\nthis : n = 0 + n\n⊢ True\n```", "goals": ["n : Nat\nthis : n = 0 + n\n⊢ True"]} diff --git a/tests/lean/interactive/match.lean.expected.out b/tests/lean/interactive/match.lean.expected.out index 5e4555b01db0..55e628339f95 100644 --- a/tests/lean/interactive/match.lean.expected.out +++ b/tests/lean/interactive/match.lean.expected.out @@ -1,22 +1,22 @@ -{"textDocument": {"uri": "file://match.lean"}, +{"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 6, "character": 11}} {"items": [{"label": "fn1", "kind": 5, "detail": "S → Nat"}, {"label": "name", "kind": 5, "detail": "S → String"}, {"label": "value", "kind": 5, "detail": "S → Bool"}], "isIncomplete": true} -{"textDocument": {"uri": "file://match.lean"}, +{"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 10, "character": 10}} {"items": [{"label": "fn1", "kind": 5, "detail": "S → Nat"}, {"label": "name", "kind": 5, "detail": "S → String"}, {"label": "value", "kind": 5, "detail": "S → Bool"}], "isIncomplete": true} -{"textDocument": {"uri": "file://match.lean"}, +{"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 14, "character": 2}} {"rendered": "```lean\nx : Nat\n⊢ 0 + x = x\n```", "goals": ["x : Nat\n⊢ 0 + x = x"]} -{"textDocument": {"uri": "file://match.lean"}, +{"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 16, "character": 9}} {"rendered": "```lean\nx : Nat\n⊢ 0 + 0 = 0\n```", "goals": ["x : Nat\n⊢ 0 + 0 = 0"]} diff --git a/tests/lean/interactive/matchPatternHover.lean.expected.out b/tests/lean/interactive/matchPatternHover.lean.expected.out index 799033404567..392d9bc4ff18 100644 --- a/tests/lean/interactive/matchPatternHover.lean.expected.out +++ b/tests/lean/interactive/matchPatternHover.lean.expected.out @@ -1,9 +1,9 @@ -{"textDocument": {"uri": "file://matchPatternHover.lean"}, +{"textDocument": {"uri": "file:///matchPatternHover.lean"}, "position": {"line": 13, "character": 7}} {"range": {"start": {"line": 13, "character": 7}, "end": {"line": 13, "character": 9}}, "contents": {"value": "```lean\nas : HList β is✝\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://matchPatternHover.lean"}, +{"textDocument": {"uri": "file:///matchPatternHover.lean"}, "position": {"line": 13, "character": 17}} {"range": {"start": {"line": 13, "character": 17}, "end": {"line": 13, "character": 18}}, diff --git a/tests/lean/interactive/matchStxCompletion.lean.expected.out b/tests/lean/interactive/matchStxCompletion.lean.expected.out index 08c2d30bcc53..427e2a554ec0 100644 --- a/tests/lean/interactive/matchStxCompletion.lean.expected.out +++ b/tests/lean/interactive/matchStxCompletion.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://matchStxCompletion.lean"}, +{"textDocument": {"uri": "file:///matchStxCompletion.lean"}, "position": {"line": 8, "character": 9}} {"items": [{"label": "b1", "kind": 5, "detail": "C → String"}, diff --git a/tests/lean/interactive/partialNamespace.lean.expected.out b/tests/lean/interactive/partialNamespace.lean.expected.out index cf4173bfc650..3bf39b6dcfc1 100644 --- a/tests/lean/interactive/partialNamespace.lean.expected.out +++ b/tests/lean/interactive/partialNamespace.lean.expected.out @@ -1,4 +1,4 @@ -{"textDocument": {"uri": "file://partialNamespace.lean"}, +{"textDocument": {"uri": "file:///partialNamespace.lean"}, "position": {"line": 0, "character": 2}} [{"selectionRange": {"start": {"line": 0, "character": 0}, "end": {"line": 2, "character": 0}}, diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out index 2e8a471fb116..26e30f872add 100644 --- a/tests/lean/interactive/plainGoal.lean.expected.out +++ b/tests/lean/interactive/plainGoal.lean.expected.out @@ -1,107 +1,107 @@ -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 0, "character": 20}} {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```", "goals": ["α : Sort ?u\n⊢ α → α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 0, "character": 21}} {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```", "goals": ["α : Sort ?u\n⊢ α → α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 3, "character": 2}} {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```", "goals": ["α : Sort ?u\n⊢ α → α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 3, "character": 3}} {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", "goals": ["α : Sort ?u\na : α\n⊢ α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 7, "character": 3}} {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", "goals": ["α : Sort ?u\na : α\n⊢ α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 10, "character": 20}} {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```", "goals": ["α : Sort ?u\n⊢ α → α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 15, "character": 9}} {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```", "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 17, "character": 5}} {"rendered": "```lean\ncase succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```", "goals": ["case succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 21, "character": 9}} {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", "goals": ["α : Sort ?u\na : α\n⊢ α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 21, "character": 10}} {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", "goals": ["α : Sort ?u\na : α\n⊢ α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 21, "character": 11}} {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", "goals": ["α : Sort ?u\na : α\n⊢ α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 27, "character": 3}} {"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```", "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 27, "character": 9}} {"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m\n```", "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 27, "character": 13}} {"rendered": "no goals", "goals": []} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 34, "character": 3}} {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```", "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 40, "character": 3}} {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```\n---\n```lean\ncase succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```", "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero", "case succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 44, "character": 3}} {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```\n---\n```lean\ncase succ\nn✝ : Nat\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```", "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero", "case succ\nn✝ : Nat\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 48, "character": 3}} {"rendered": "```lean\na b : Nat\n⊢ a = b\n```", "goals": ["a b : Nat\n⊢ a = b"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 51, "character": 20}} {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```", "goals": ["α : Sort ?u\n⊢ α → α"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 55, "character": 3}} {"rendered": "```lean\nα : Sort ?u\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```", "goals": ["α : Sort ?u\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 61, "character": 3}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 63, "character": 3}} {"rendered": "```lean\ncase right\n⊢ False\n```", "goals": ["case right\n⊢ False"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 68, "character": 3}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 70, "character": 3}} {"rendered": "```lean\ncase right\n⊢ False\n```", "goals": ["case right\n⊢ False"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 78, "character": 29}} {"rendered": "```lean\nt a n✝ : Nat\nn_ih✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * Nat.succ n✝\n```\n---\n```lean\nt a n✝ : Nat\nn_ih✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```\n---\n```lean\nt a n✝ : Nat\nn_ih✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```", @@ -109,65 +109,65 @@ ["t a n✝ : Nat\nn_ih✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * Nat.succ n✝", "t a n✝ : Nat\nn_ih✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)", "t a n✝ : Nat\nn_ih✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 82, "character": 53}} {"rendered": "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```", "goals": ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 82, "character": 54}} {"rendered": "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```", "goals": ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 86, "character": 38}} {"rendered": "no goals", "goals": []} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 89, "character": 39}} null -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 93, "character": 16}} {"rendered": "```lean\ncase left\n⊢ True\n```\n---\n```lean\ncase right\n⊢ False\n```", "goals": ["case left\n⊢ True", "case right\n⊢ False"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 97, "character": 8}} {"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 99, "character": 4}} {"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 101, "character": 2}} {"rendered": "no goals", "goals": []} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 106, "character": 4}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 108, "character": 2}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 113, "character": 4}} {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 115, "character": 2}} null -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 120, "character": 2}} {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 124, "character": 17}} {"rendered": "```lean\np q : Prop\nhp : p\nhq : q\nthis : q ∧ p\n⊢ p ∧ q\n```", "goals": ["p q : Prop\nhp : p\nhq : q\nthis : q ∧ p\n⊢ p ∧ q"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 128, "character": 18}} {"rendered": "```lean\np q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)\n```", "goals": ["p q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 133, "character": 3}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 133, "character": 4}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} {"textDocument": {"uri": "file://plainGoal.lean"}, diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out index 1e85669f5614..96a2f368b90e 100644 --- a/tests/lean/interactive/plainTermGoal.lean.expected.out +++ b/tests/lean/interactive/plainTermGoal.lean.expected.out @@ -1,69 +1,69 @@ -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 2, "character": 14}} {"range": {"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 51}}, "goal": "⊢ 0 < 2"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 2, "character": 15}} {"range": {"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}}, "goal": "⊢ 0 < 1"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 2, "character": 16}} {"range": {"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}}, "goal": "⊢ 0 < 1"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 2, "character": 31}} {"range": {"start": {"line": 2, "character": 31}, "end": {"line": 2, "character": 51}}, "goal": "⊢ 1 < 2"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 2, "character": 48}} {"range": {"start": {"line": 2, "character": 32}, "end": {"line": 2, "character": 50}}, "goal": "⊢ 1 < 2"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 11, "character": 10}} {"range": {"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 19}}, "goal": "y : Int\n⊢ Option Unit"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 16, "character": 17}} {"range": {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}}, "goal": "m n : Nat\n⊢ ?m m n < n"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 16, "character": 18}} {"range": {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}}, "goal": "m n : Nat\n⊢ ?m m n < n"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 20, "character": 18}} {"range": {"start": {"line": 20, "character": 18}, "end": {"line": 20, "character": 23}}, "goal": "⊢ True"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 24, "character": 2}} {"range": {"start": {"line": 24, "character": 2}, "end": {"line": 24, "character": 74}}, "goal": "⊢ ∀ (n : Nat), n < n + 42"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 24, "character": 6}} {"range": {"start": {"line": 24, "character": 6}, "end": {"line": 24, "character": 7}}, "goal": "⊢ Nat"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 30, "character": 6}} {"range": {"start": {"line": 30, "character": 6}, "end": {"line": 30, "character": 18}}, "goal": "n : Nat\n⊢ ∀ (n m : Nat), n + m = m + n"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 32, "character": 8}} {"range": {"start": {"line": 32, "character": 8}, "end": {"line": 32, "character": 26}}, "goal": "n : Nat\n⊢ n < n + 1"} -{"textDocument": {"uri": "file://plainTermGoal.lean"}, +{"textDocument": {"uri": "file:///plainTermGoal.lean"}, "position": {"line": 35, "character": 14}} {"range": {"start": {"line": 35, "character": 14}, "end": {"line": 35, "character": 15}}, diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean index b640fe3399e9..5b56d44f203d 100644 --- a/tests/lean/interactive/run.lean +++ b/tests/lean/interactive/run.lean @@ -42,7 +42,7 @@ def ident : Parsec Name := do return xs.foldl Name.mkStr $ head partial def main (args : List String) : IO Unit := do - let uri := s!"file://{args.head!}" + let uri := s!"file:///{args.head!}" Ipc.runWith (←IO.appPath) #["--server"] do let capabilities := { textDocument? := some { diff --git a/tests/lean/interactive/unterminatedDocComment.lean.expected.out b/tests/lean/interactive/unterminatedDocComment.lean.expected.out index 69cbfa37d294..9d2e52d62615 100644 --- a/tests/lean/interactive/unterminatedDocComment.lean.expected.out +++ b/tests/lean/interactive/unterminatedDocComment.lean.expected.out @@ -1,8 +1,8 @@ -{"textDocument": {"version": 2, "uri": "file://unterminatedDocComment.lean"}, +{"textDocument": {"version": 2, "uri": "file:///unterminatedDocComment.lean"}, "contentChanges": [{"text": "/", "range": {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 3}}}]} -{"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []} -{"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []} -{"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []} +{"version": 2, "uri": "file:///unterminatedDocComment.lean", "diagnostics": []} +{"version": 2, "uri": "file:///unterminatedDocComment.lean", "diagnostics": []} +{"version": 2, "uri": "file:///unterminatedDocComment.lean", "diagnostics": []} From 7670b07843531733251193922c2abeb3a9bf362d Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 10 Nov 2023 21:08:33 +0100 Subject: [PATCH 03/16] refactor: style and Lean.Util import --- src/Lean/Util.lean | 2 +- src/lake/Lake/CLI/Serve.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean index 24f282e8312c..f80586041328 100644 --- a/src/Lean/Util.lean +++ b/src/Lean/Util.lean @@ -24,5 +24,5 @@ import Lean.Util.ReplaceLevel import Lean.Util.FoldConsts import Lean.Util.SCC import Lean.Util.OccursCheck -import Lean.Util.Paths import Lean.Util.HasConstCache +import Lean.Util.FileSetupInfo diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 19c6b3a8a0f6..6692a1dbea5e 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -9,7 +9,7 @@ import Lake.Util.MainM import Lean.Util.FileSetupInfo namespace Lake -open Lean (Json toJson fromJson? LeanPaths ServerOptions searchModuleNameOfFileName FileSetupInfo) +open Lean /-- Exit code to return if `setup-file` cannot find the config file. -/ def noConfigFileCode : ExitCode := 2 From 40034ebed170d730c4a8561120822c895a07ff07 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Tue, 14 Nov 2023 10:41:10 +0100 Subject: [PATCH 04/16] fix: adjust math template --- src/lake/Lake/CLI/Init.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 0bf963281a68..7a2481d8fa9e 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -93,13 +93,16 @@ def mathConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL -def moreServerArgs := #[ - \"-Dpp.unicode.fun=true\", -- pretty-prints `fun a ↦ b` - \"-Dpp.proofs.withType=false\" +def moreServerOptions : Array ServerOption := #[ + ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` + ⟨`pp.proofs.withType, false⟩ ] -- These settings only apply during `lake build`, but not in VSCode editor. -def moreLeanArgs := moreServerArgs +def moreLeanArgs := #[ + \"-Dpp.unicode.fun=true\", -- pretty-prints `fun a ↦ b` + \"-Dpp.proofs.withType=false\" +] -- These are additional settings which do not affect the lake hash, -- so they can be enabled in CI and disabled locally or vice versa. @@ -112,7 +115,7 @@ def weakLeanArgs : Array String := #[] package {pkgName} where - moreServerArgs := moreServerArgs + moreServerOptions := moreServerOptions -- add any package configuration options here require mathlib from git From f6d64a79763144b4d5ed2fc41a16b06da1ac3607 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Tue, 14 Nov 2023 10:55:48 +0100 Subject: [PATCH 05/16] chore: deprecate moreServerArgs instead of removing it --- src/lake/Lake/Config/Package.lean | 10 +++++++++- src/lake/Lake/Load/Package.lean | 2 ++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index a36e5ef16fa9..85a1307ded9e 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -88,11 +88,19 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where precompileModules : Bool := false /-- + **Deprecated in favor of `moreGlobalServerArgs`.** Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`, both for this package and also for any packages browsed from this one in the same session. -/ - moreGlobalServerArgs : Array String := #[] + moreServerArgs : Array String := #[] + + /-- + Additional arguments to pass to the Lean language server + (i.e., `lean --server`) launched by `lake serve`, both for this package and + also for any packages browsed from this one in the same session. + -/ + moreGlobalServerArgs : Array String := moreServerArgs /-- The directory containing the package's Lean source files. diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index 52d75cfc235d..460fe5621a17 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/src/lake/Lake/Load/Package.lean @@ -110,6 +110,8 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package := -- Deprecation warnings unless self.config.manifestFile.isNone do logWarning s!"{self.name}: package configuration option `manifestFile` is deprecated" + unless self.config.moreServerArgs.isEmpty do + logWarning s!"{self.name}: package configuration option `moreServerArgs` is deprecated in favor of `moreGlobalServerArgs`" -- Fill in the Package return {self with From 2188cbd87cfece01f7db34a849b4114f1afb749a Mon Sep 17 00:00:00 2001 From: mhuisi Date: Tue, 14 Nov 2023 11:30:11 +0100 Subject: [PATCH 06/16] feat: converting `ServerOption` to cli arg --- src/Lean/Util/ServerOptions.lean | 6 ++++++ src/lake/Lake/CLI/Init.lean | 5 +---- src/lake/Lake/Config/LeanConfig.lean | 4 ++++ 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/Lean/Util/ServerOptions.lean b/src/Lean/Util/ServerOptions.lean index 8337ddc05d8c..51447a08aa32 100644 --- a/src/Lean/Util/ServerOptions.lean +++ b/src/Lean/Util/ServerOptions.lean @@ -46,6 +46,12 @@ instance : ToJson ServerOptionValue where | (b : Bool) => b | (n : Nat) => n +/-- Formats the server option value as a CLI flag argument. -/ +def ServerOptionValue.asCliFlagValue : (v : ServerOptionValue) → String + | (s : String) => s!"\"{s}\"" + | (b : Bool) => toString b + | (n : Nat) => toString n + /-- Options that are used by the server as if they were passed using `-D`. -/ structure ServerOptions where values : RBMap Name ServerOptionValue Name.cmp diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 7a2481d8fa9e..8d992b052789 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -99,10 +99,7 @@ def moreServerOptions : Array ServerOption := #[ ] -- These settings only apply during `lake build`, but not in VSCode editor. -def moreLeanArgs := #[ - \"-Dpp.unicode.fun=true\", -- pretty-prints `fun a ↦ b` - \"-Dpp.proofs.withType=false\" -] +def moreLeanArgs := moreServerOptions.map ServerOption.asCliArg -- These are additional settings which do not affect the lake hash, -- so they can be enabled in CI and disabled locally or vice versa. diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index 4eeddb416eaa..e7b05abac80c 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -88,6 +88,10 @@ structure ServerOption where value : Lean.ServerOptionValue deriving Inhabited, Repr +/-- Formats the server option as a CLI argument using the `-D` flag. -/ +def ServerOption.asCliArg (o : ServerOption) : String := + s!"-D{o.name}={o.value.asCliFlagValue}" + /-- Configuration options common to targets that build modules. -/ structure LeanConfig where /-- From 49b484cd42090bbf8eedf8ca90cd22548295dae5 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Tue, 14 Nov 2023 11:43:08 +0100 Subject: [PATCH 07/16] chore: adjust deprecation warning to be more helpful --- src/lake/Lake/Load/Package.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index 460fe5621a17..7aa855e7fb79 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/src/lake/Lake/Load/Package.lean @@ -111,7 +111,7 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package := unless self.config.manifestFile.isNone do logWarning s!"{self.name}: package configuration option `manifestFile` is deprecated" unless self.config.moreServerArgs.isEmpty do - logWarning s!"{self.name}: package configuration option `moreServerArgs` is deprecated in favor of `moreGlobalServerArgs`" + logWarning s!"{self.name}: package configuration option `moreServerArgs` is deprecated in favor of `moreServerOptions`" -- Fill in the Package return {self with From e6762456f635e003a5e713aabf805b8727828a05 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 16 Nov 2023 16:47:47 +0100 Subject: [PATCH 08/16] feat: lake `leanOptions` config entry --- src/Lean/Util/FileSetupInfo.lean | 4 +- .../{ServerOptions.lean => LeanOptions.lean} | 54 +++++++++---------- src/lake/Lake/CLI/Init.lean | 8 +-- src/lake/Lake/CLI/Serve.lean | 8 ++- src/lake/Lake/Config/LeanConfig.lean | 20 ++++--- src/lake/Lake/Config/LeanLib.lean | 25 ++++++++- src/lake/Lake/Config/Module.lean | 3 ++ src/lake/Lake/Config/Package.lean | 6 ++- src/lake/README.md | 7 +-- 9 files changed, 82 insertions(+), 53 deletions(-) rename src/Lean/Util/{ServerOptions.lean => LeanOptions.lean} (50%) diff --git a/src/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean index 24d4eeb5e476..50f5405d68cd 100644 --- a/src/Lean/Util/FileSetupInfo.lean +++ b/src/Lean/Util/FileSetupInfo.lean @@ -1,9 +1,9 @@ -import Lean.Util.ServerOptions +import Lean.Util.LeanOptions /-- Information shared between Lake and Lean when calling `lake setup-file`. -/ structure Lean.FileSetupInfo where paths : LeanPaths - setupOptions : ServerOptions + setupOptions : LeanOptions deriving FromJson, ToJson diff --git a/src/Lean/Util/ServerOptions.lean b/src/Lean/Util/LeanOptions.lean similarity index 50% rename from src/Lean/Util/ServerOptions.lean rename to src/Lean/Util/LeanOptions.lean index 51447a08aa32..f1e03c78b2f4 100644 --- a/src/Lean/Util/ServerOptions.lean +++ b/src/Lean/Util/LeanOptions.lean @@ -3,83 +3,83 @@ import Lean.Util.Paths namespace Lean /-- Restriction of `DataValue` that covers exactly those cases that Lean is able to handle when passed via the `-D` flag. -/ -inductive ServerOptionValue where +inductive LeanOptionValue where | ofString (s : String) | ofBool (b : Bool) | ofNat (n : Nat) deriving Inhabited, Repr -def ServerOptionValue.ofDataValue? : DataValue → Option ServerOptionValue +def LeanOptionValue.ofDataValue? : DataValue → Option LeanOptionValue | .ofString s => some (.ofString s) | .ofBool b => some (.ofBool b) | .ofNat n => some (.ofNat n) | _ => none -def ServerOptionValue.toDataValue : ServerOptionValue → DataValue +def LeanOptionValue.toDataValue : LeanOptionValue → DataValue | .ofString s => .ofString s | .ofBool b => .ofBool b | .ofNat n => .ofNat n -instance : KVMap.Value ServerOptionValue where - toDataValue := ServerOptionValue.toDataValue - ofDataValue? := ServerOptionValue.ofDataValue? +instance : KVMap.Value LeanOptionValue where + toDataValue := LeanOptionValue.toDataValue + ofDataValue? := LeanOptionValue.ofDataValue? -instance : Coe String ServerOptionValue where - coe := ServerOptionValue.ofString +instance : Coe String LeanOptionValue where + coe := LeanOptionValue.ofString -instance : Coe Bool ServerOptionValue where - coe := ServerOptionValue.ofBool +instance : Coe Bool LeanOptionValue where + coe := LeanOptionValue.ofBool -instance : Coe Nat ServerOptionValue where - coe := ServerOptionValue.ofNat +instance : Coe Nat LeanOptionValue where + coe := LeanOptionValue.ofNat -instance : FromJson ServerOptionValue where +instance : FromJson LeanOptionValue where fromJson? | (s : String) => Except.ok s | (b : Bool) => Except.ok b | (n : Nat) => Except.ok n - | _ => Except.error "invalid ServerOptionValue type" + | _ => Except.error "invalid LeanOptionValue type" -instance : ToJson ServerOptionValue where +instance : ToJson LeanOptionValue where toJson | (s : String) => s | (b : Bool) => b | (n : Nat) => n -/-- Formats the server option value as a CLI flag argument. -/ -def ServerOptionValue.asCliFlagValue : (v : ServerOptionValue) → String +/-- Formats the lean option value as a CLI flag argument. -/ +def LeanOptionValue.asCliFlagValue : (v : LeanOptionValue) → String | (s : String) => s!"\"{s}\"" | (b : Bool) => toString b | (n : Nat) => toString n -/-- Options that are used by the server as if they were passed using `-D`. -/ -structure ServerOptions where - values : RBMap Name ServerOptionValue Name.cmp +/-- Options that are used by Lean as if they were passed using `-D`. -/ +structure LeanOptions where + values : RBMap Name LeanOptionValue Name.cmp deriving Inhabited, Repr -def ServerOptions.toOptions (serverOptions : ServerOptions) : Options := Id.run do +def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do let mut options := KVMap.empty - for ⟨name, optionValue⟩ in serverOptions.values do + for ⟨name, optionValue⟩ in leanOptions.values do options := options.insert name optionValue.toDataValue return options -def ServerOptions.fromOptions? (options : Options) : Option ServerOptions := do +def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do let mut values := RBMap.empty for ⟨name, dataValue⟩ in options do - let optionValue ← ServerOptionValue.ofDataValue? dataValue + let optionValue ← LeanOptionValue.ofDataValue? dataValue values := values.insert name optionValue return ⟨values⟩ -instance : FromJson ServerOptions where +instance : FromJson LeanOptions where fromJson? | Json.obj obj => do let values ← obj.foldM (init := RBMap.empty) fun acc k v => do let optionValue ← fromJson? v return acc.insert k.toName optionValue return ⟨values⟩ - | _ => Except.error "invalid ServerOptions type" + | _ => Except.error "invalid LeanOptions type" -instance : ToJson ServerOptions where +instance : ToJson LeanOptions where toJson options := Json.obj <| options.values.fold (init := RBNode.leaf) fun acc k v => acc.insert (cmp := compare) k.toString (toJson v) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 8d992b052789..057638f3ec6b 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -93,14 +93,11 @@ def mathConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL -def moreServerOptions : Array ServerOption := #[ +def leanOptions : Array LeanOption := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` ⟨`pp.proofs.withType, false⟩ ] --- These settings only apply during `lake build`, but not in VSCode editor. -def moreLeanArgs := moreServerOptions.map ServerOption.asCliArg - -- These are additional settings which do not affect the lake hash, -- so they can be enabled in CI and disabled locally or vice versa. -- Warning: Do not put any options here that actually change the olean files, @@ -112,7 +109,7 @@ def weakLeanArgs : Array String := #[] package {pkgName} where - moreServerOptions := moreServerOptions + leanOptions := leanOptions -- add any package configuration options here require mathlib from git @@ -120,7 +117,6 @@ require mathlib from git @[default_target] lean_lib {libRoot} where - moreLeanArgs := moreLeanArgs weakLeanArgs := weakLeanArgs -- add any library configuration options here " diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 6692a1dbea5e..de1f497743b2 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -42,14 +42,12 @@ def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String loadDynlibPaths := dynlibs : LeanPaths } - let setupOptions : ServerOptions ← do + let setupOptions : LeanOptions ← do let some moduleName ← searchModuleNameOfFileName path ws.leanSrcPath | pure ⟨∅⟩ - let some (pkg, module) := ws.packages.findSome? fun pkg => do - pure (pkg, ← pkg.findModule? moduleName) + let some module := ws.findModule? moduleName | pure ⟨∅⟩ - let options := pkg.config.moreServerOptions ++ module.lib.config.moreServerOptions - |>.map fun opt => ⟨opt.name, opt.value⟩ + let options := module.serverOptions.map fun opt => ⟨opt.name, opt.value⟩ pure ⟨Lean.RBMap.fromArray options Lean.Name.cmp⟩ IO.println <| Json.compress <| toJson { paths, diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index e7b05abac80c..1dd8cd4dcf78 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -1,4 +1,4 @@ -import Lean.Util.ServerOptions +import Lean.Util.LeanOptions /- Copyright (c) 2022 Mac Malone. All rights reserved. @@ -82,14 +82,14 @@ def BuildType.leancArgs : BuildType → Array String | minSizeRel => #["-Os", "-DNDEBUG"] | release => #["-O3", "-DNDEBUG"] -/-- Option that is used by the server as if it was passed using `-D`. -/ -structure ServerOption where +/-- Option that is used by Lean as if it was passed using `-D`. -/ +structure LeanOption where name : Lean.Name - value : Lean.ServerOptionValue + value : Lean.LeanOptionValue deriving Inhabited, Repr -/-- Formats the server option as a CLI argument using the `-D` flag. -/ -def ServerOption.asCliArg (o : ServerOption) : String := +/-- Formats the lean option as a CLI argument using the `-D` flag. -/ +def LeanOption.asCliArg (o : LeanOption) : String := s!"-D{o.name}={o.value.asCliFlagValue}" /-- Configuration options common to targets that build modules. -/ @@ -100,6 +100,12 @@ structure LeanConfig where -/ buildType : BuildType := .release /-- + Additional options to pass to both the Lean language server + (i.e., `lean --server`) launched by `lake serve` and to `lean` + when compiling a module's Lean source files. + -/ + leanOptions : Array LeanOption := #[] + /-- Additional arguments to pass to `lean` when compiling a module's Lean source files. -/ @@ -125,7 +131,7 @@ structure LeanConfig where Additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. -/ - moreServerOptions : Array ServerOption := #[] + moreServerOptions : Array LeanOption := #[] /-- Additional arguments to pass to `leanc` when compiling a module's C source files generated by `lean`. diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index 50995f6549bf..bb72de0b22c5 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -87,6 +87,20 @@ Is true if either the package or the library have `precompileModules` set. @[inline] def nativeFacets (self : LeanLib) : Array (ModuleFacet (BuildJob FilePath)) := self.config.nativeFacets +/-- +The arguments to pass to `lean --server` when running the Lean language server. +`serverOptions` is the the accumulation of: +- the package's `leanOptions` +- the library's `leanOptions` +- the package's `moreServerOptions` +- the library's `moreServerOptions` +-/ +@[inline] def serverOptions (self : LeanLib) : Array LeanOption := + self.pkg.leanOptions + ++ self.config.leanOptions + ++ self.pkg.moreServerOptions + ++ self.config.moreServerOptions + /-- The build type for modules of this library. That is, the minimum of package's `buildType` and the library's `buildType`. @@ -103,10 +117,17 @@ then the default (which is C for now). Backend.orPreferLeft self.config.backend self.pkg.backend /-- The arguments to pass to `lean` when compiling the library's Lean files. -That is, the package's `moreLeanArgs` plus the library's `moreLeanArgs`. +`leanArgs` is the accumulation of: +- the package's `leanOptions` +- the library's `leanOptions` +- the package's `moreLeanArgs` +- the library's `moreLeanArgs` -/ @[inline] def leanArgs (self : LeanLib) : Array String := - self.pkg.moreLeanArgs ++ self.config.moreLeanArgs + self.pkg.leanOptions.map (·.asCliArg) + ++ self.config.leanOptions.map (·.asCliArg) + ++ self.pkg.moreLeanArgs + ++ self.config.moreLeanArgs /-- The arguments to weakly pass to `lean` when compiling the library's Lean files. diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index b4e7845b7845..9038d5d749a0 100644 --- a/src/lake/Lake/Config/Module.lean +++ b/src/lake/Lake/Config/Module.lean @@ -101,6 +101,9 @@ def dynlibSuffix := "-1" @[inline] def dynlibFile (self : Module) : FilePath := self.pkg.nativeLibDir / nameToSharedLib self.dynlibName +@[inline] def serverOptions (self : Module) : Array LeanOption := + self.lib.serverOptions + @[inline] def buildType (self : Module) : BuildType := self.lib.buildType diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 85a1307ded9e..c1605107f8ad 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -324,7 +324,7 @@ namespace Package self.config.moreGlobalServerArgs /-- The package's `moreServerOptions` configuration. -/ -@[inline] def moreServerOptions (self : Package) : Array ServerOption := +@[inline] def moreServerOptions (self : Package) : Array LeanOption := self.config.moreServerOptions /-- The package's `buildType` configuration. -/ @@ -335,6 +335,10 @@ namespace Package @[inline] def backend (self : Package) : Backend := self.config.backend +/-- The package's `leanOptions` configuration. -/ +@[inline] def leanOptions (self : Package) : Array LeanOption := + self.config.leanOptions + /-- The package's `moreLeanArgs` configuration. -/ @[inline] def moreLeanArgs (self : Package) : Array String := self.config.moreLeanArgs diff --git a/src/lake/README.md b/src/lake/README.md index c914bdc5168d..5c2d246b9c52 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -165,9 +165,10 @@ Lake provides a large assortment of configuration options for packages. * `postUpdate?`: A post-`lake update` hook. The monadic action is run after a successful `lake update` execution on this package or one of its downstream dependents. Defaults to `none`. See the option's docstring for a complete example. * `precompileModules`: Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`. -* `moreServerOptions`: Additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. -* `moreGlobalServerArgs`: Additional arguments to pass to `lean --server` which apply both to this package and anything else in the same server session (e.g. when browsing other packages from the same session via go-to-definition) +* `moreServerOptions`: An `Array` of additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. +* `moreGlobalServerArgs`: An `Array` of additional arguments to pass to `lean --server` which apply both to this package and anything else in the same server session (e.g. when browsing other packages from the same session via go-to-definition) * `buildType`: The `BuildType` of targets in the package (see [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670)). One of `debug`, `relWithDebInfo`, `minSizeRel`, or `release`. Defaults to `release`. +* `leanOptions`: Additional options to pass to both the Lean language server (i.e., `lean --server`) launched by `lake serve` and to `lean` while compiling Lean source files. * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. * `weakLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. Unlike `moreLeanArgs`, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild. They come *before* `moreLeanArgs`. * `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes some flags based on the `buildType`, but you can change this by, for example, adding `-O0` and `-UNDEBUG`. @@ -207,7 +208,7 @@ lean_lib «target-name» where * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the library's modules. * `defaultFacets`: An `Array` of library facets to build on a bare `lake build` of the library. For example, setting this to `#[LeanLib.sharedLib]` will build the shared library facet. * `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the library's static and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source). -* `precompileModules`, `buildType`, `Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest) +* `precompileModules`, `buildType`, `leanOptions`, `Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest) ### Binary Executables From 431b0544aeed96f2dcf0288e0ccaebc1567090f3 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 16 Nov 2023 19:15:13 +0100 Subject: [PATCH 09/16] refactor: arg order --- src/lake/Lake/Config/LeanLib.lean | 14 ++++---------- src/lake/Lake/Config/Package.lean | 8 ++++---- 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index bb72de0b22c5..a3a1d953bc8e 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -91,15 +91,12 @@ Is true if either the package or the library have `precompileModules` set. The arguments to pass to `lean --server` when running the Lean language server. `serverOptions` is the the accumulation of: - the package's `leanOptions` -- the library's `leanOptions` - the package's `moreServerOptions` +- the library's `leanOptions` - the library's `moreServerOptions` -/ @[inline] def serverOptions (self : LeanLib) : Array LeanOption := - self.pkg.leanOptions - ++ self.config.leanOptions - ++ self.pkg.moreServerOptions - ++ self.config.moreServerOptions + self.pkg.moreServerOptions ++ self.config.moreServerOptions /-- The build type for modules of this library. @@ -119,15 +116,12 @@ then the default (which is C for now). The arguments to pass to `lean` when compiling the library's Lean files. `leanArgs` is the accumulation of: - the package's `leanOptions` -- the library's `leanOptions` - the package's `moreLeanArgs` +- the library's `leanOptions` - the library's `moreLeanArgs` -/ @[inline] def leanArgs (self : LeanLib) : Array String := - self.pkg.leanOptions.map (·.asCliArg) - ++ self.config.leanOptions.map (·.asCliArg) - ++ self.pkg.moreLeanArgs - ++ self.config.moreLeanArgs + self.pkg.moreLeanArgs ++ self.config.moreLeanArgs /-- The arguments to weakly pass to `lean` when compiling the library's Lean files. diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index c1605107f8ad..39314fcb8e11 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -323,9 +323,9 @@ namespace Package @[inline] def moreGlobalServerArgs (self : Package) : Array String := self.config.moreGlobalServerArgs -/-- The package's `moreServerOptions` configuration. -/ +/-- The package's `moreServerOptions` configuration appended to its `leanOptions` configuration. -/ @[inline] def moreServerOptions (self : Package) : Array LeanOption := - self.config.moreServerOptions + self.config.leanOptions ++ self.config.moreServerOptions /-- The package's `buildType` configuration. -/ @[inline] def buildType (self : Package) : BuildType := @@ -339,9 +339,9 @@ namespace Package @[inline] def leanOptions (self : Package) : Array LeanOption := self.config.leanOptions -/-- The package's `moreLeanArgs` configuration. -/ +/-- The package's `moreLeanArgs` configuration appended to its `leanOptions` configuration. -/ @[inline] def moreLeanArgs (self : Package) : Array String := - self.config.moreLeanArgs + self.config.leanOptions.map (·.asCliArg) ++ self.config.moreLeanArgs /-- The package's `weakLeanArgs` configuration. -/ @[inline] def weakLeanArgs (self : Package) : Array String := From 843721eabafca4742d030e9140a319eb637eaa38 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 17 Nov 2023 11:39:18 +0100 Subject: [PATCH 10/16] fix: don't forget the library `leanOptions` --- src/lake/Lake/Config/LeanLib.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index a3a1d953bc8e..fcda7a5534fe 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -96,7 +96,7 @@ The arguments to pass to `lean --server` when running the Lean language server. - the library's `moreServerOptions` -/ @[inline] def serverOptions (self : LeanLib) : Array LeanOption := - self.pkg.moreServerOptions ++ self.config.moreServerOptions + self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions /-- The build type for modules of this library. @@ -112,6 +112,7 @@ then the default (which is C for now). -/ @[inline] def backend (self : LeanLib) : Backend := Backend.orPreferLeft self.config.backend self.pkg.backend + /-- The arguments to pass to `lean` when compiling the library's Lean files. `leanArgs` is the accumulation of: @@ -121,7 +122,7 @@ The arguments to pass to `lean` when compiling the library's Lean files. - the library's `moreLeanArgs` -/ @[inline] def leanArgs (self : LeanLib) : Array String := - self.pkg.moreLeanArgs ++ self.config.moreLeanArgs + self.pkg.moreLeanArgs ++ self.config.leanOptions.map (·.asCliArg) ++ self.config.moreLeanArgs /-- The arguments to weakly pass to `lean` when compiling the library's Lean files. From 42065bff029fe1e91a61760d7321dfb4cfdf9681 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Mon, 20 Nov 2023 13:40:29 +0100 Subject: [PATCH 11/16] doc: missing headers --- src/Lean/Util/FileSetupInfo.lean | 5 +++++ src/Lean/Util/LeanOptions.lean | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean index 50f5405d68cd..0560f80a6c8c 100644 --- a/src/Lean/Util/FileSetupInfo.lean +++ b/src/Lean/Util/FileSetupInfo.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Marc Huisinga +-/ import Lean.Util.LeanOptions /-- diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean index f1e03c78b2f4..f52d48814f94 100644 --- a/src/Lean/Util/LeanOptions.lean +++ b/src/Lean/Util/LeanOptions.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Marc Huisinga +-/ import Lean.Util.Paths namespace Lean From bad3e4343ad18695eaff9917ca33ecb8a87bfa65 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Tue, 21 Nov 2023 10:18:02 +0100 Subject: [PATCH 12/16] test: fix new tests with wrong uri --- tests/lean/interactive/plainGoal.lean.expected.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out index 26e30f872add..40fa13fb654f 100644 --- a/tests/lean/interactive/plainGoal.lean.expected.out +++ b/tests/lean/interactive/plainGoal.lean.expected.out @@ -170,12 +170,12 @@ null {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 133, "character": 4}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 139, "character": 34}} {"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 142, "character": 34}} {"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]} -{"textDocument": {"uri": "file://plainGoal.lean"}, +{"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 145, "character": 34}} {"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]} From 5fbecc33ef5f947fd349510f1c118775d79e635f Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 23 Nov 2023 11:23:16 +0100 Subject: [PATCH 13/16] test: fix new tests with wrong uri --- tests/lean/interactive/rename.lean.expected.out | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/lean/interactive/rename.lean.expected.out b/tests/lean/interactive/rename.lean.expected.out index bf4b7aec4b8b..1d63331904e8 100644 --- a/tests/lean/interactive/rename.lean.expected.out +++ b/tests/lean/interactive/rename.lean.expected.out @@ -1,19 +1,19 @@ -{"textDocument": {"uri": "file://rename.lean"}, +{"textDocument": {"uri": "file:///rename.lean"}, "position": {"line": 5, "character": 14}} null -{"textDocument": {"uri": "file://rename.lean"}, +{"textDocument": {"uri": "file:///rename.lean"}, "position": {"line": 5, "character": 14}, "newName": "blue"} {"changes": {}} -{"textDocument": {"uri": "file://rename.lean"}, +{"textDocument": {"uri": "file:///rename.lean"}, "position": {"line": 9, "character": 10}, "newName": "Bar"} {"changes": {}} -{"textDocument": {"uri": "file://rename.lean"}, +{"textDocument": {"uri": "file:///rename.lean"}, "position": {"line": 23, "character": 6}, "newName": "z"} {"changes": {}} -{"textDocument": {"uri": "file://rename.lean"}, +{"textDocument": {"uri": "file:///rename.lean"}, "position": {"line": 30, "character": 12}, "newName": "X"} {"changes": {}} From 550832649ac328e5606a2c05b832befe92db7d8f Mon Sep 17 00:00:00 2001 From: mhuisi Date: Sat, 25 Nov 2023 17:45:14 +0100 Subject: [PATCH 14/16] refactor: post merge cleanup --- src/Lean/Server/FileWorker.lean | 49 +++++++++++++++------------------ 1 file changed, 22 insertions(+), 27 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index c5862b92e760..a265c40e8acd 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -164,13 +164,13 @@ abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO /- Worker initialization sequence. -/ section Initialization - structure LakePrintPathsResult where + structure LakeSetupFileResult where spawnArgs : Process.SpawnArgs exitCode : UInt32 stdout : String stderr : String - partial def runLakeSetupFile (lakePath : System.FilePath) (m : DocumentMeta) (filePath : System.FilePath) (imports : Array Import) (hOut : FS.Stream) : IO LakePrintPathsResult := do + partial def runLakeSetupFile (lakePath : System.FilePath) (m : DocumentMeta) (filePath : System.FilePath) (imports : Array Import) (hOut : FS.Stream) : IO LakeSetupFileResult := do let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module) if m.dependencyBuildMode matches .never then args := args.push "--no-build" @@ -199,11 +199,24 @@ section Initialization /-- Use `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`. Compilation progress is reported to `hOut` via LSP notifications. Return the search path for source files and the options for the file. -/ - partial def lakeSetupFile (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO (SearchPath × Options) := do + partial def setupFile (m : DocumentMeta) (hOut : FS.Stream) (headerStx : Syntax) : IO (SearchPath × Options) := do + let invalidLakeSetup := (← initSrcSearchPath, Options.empty) let some filePath := System.Uri.fileUriToPath? m.uri - | return ([], Options.empty) -- untitled files have no search path and no associated options + | return invalidLakeSetup + + -- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps + -- NOTE: lake does not exist in stage 0 (yet?) + if filePath.fileName == "lakefile.lean" then + return invalidLakeSetup + + let lakePath ← determineLakePath + if !(← System.FilePath.pathExists lakePath) then + return invalidLakeSetup + + let imports := Lean.Elab.headerToImports headerStx let result ← runLakeSetupFile lakePath m filePath imports hOut let cmdStr := " ".intercalate (toString result.spawnArgs.cmd :: result.spawnArgs.args.toList) + match result.exitCode with | 0 => let Except.ok (info : FileSetupInfo) ← pure (Json.parse result.stdout >>= fromJson?) @@ -211,33 +224,15 @@ section Initialization initSearchPath (← getBuildDir) info.paths.oleanPath info.paths.loadDynlibPaths.forM loadDynlib let pkgSearchPath ← info.paths.srcPath.mapM realPathNormalized - return (pkgSearchPath, info.setupOptions.toOptions) - | 2 => pure ([], Options.empty) -- no lakefile.lean + return (← initSrcSearchPath pkgSearchPath, info.setupOptions.toOptions) + | 2 => pure invalidLakeSetup -- no lakefile.lean -- error from `--no-build` | 3 => throwServerError s!"Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor.\n\n{result.stdout}" | _ => throwServerError s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}" - def setupSrcSearchPathAndObtainOptions (m : DocumentMeta) (hOut : FS.Stream) (headerStx : Syntax) : IO (SearchPath × Options) := do - let invalidLakeSetup := (← initSrcSearchPath, Options.empty) - let some path := System.Uri.fileUriToPath? m.uri - | return invalidLakeSetup - - -- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps - -- NOTE: lake does not exist in stage 0 (yet?) - if path.fileName == "lakefile.lean" then - return invalidLakeSetup - - let lakePath ← determineLakePath - if !(← System.FilePath.pathExists lakePath) then - return invalidLakeSetup - - let imports := Lean.Elab.headerToImports headerStx - let (pkgSearchPath, options) ← lakeSetupFile lakePath m imports hOut - return (← initSrcSearchPath pkgSearchPath, options) - def buildHeaderEnv (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (headerStx : Syntax) : IO (Environment × MessageLog × SearchPath × Options) := do - let (headerEnv, msgLog, srcSearchPath) ← - match ← EIO.toIO' <| setupSrcSearchPathAndObtainOptions m hOut headerStx with + let (headerEnv, msgLog, srcSearchPath, opts) ← + match ← EIO.toIO' <| setupFile m hOut headerStx with | .ok (srcSearchPath, fileOptions) => -- file options take priority let opts := opts.mergeBy (fun _ _ fileOpt => fileOpt) fileOptions @@ -255,7 +250,7 @@ section Initialization catch _ => pure () - return (headerEnv, msgLog, srcSearchPath) + return (headerEnv, msgLog, srcSearchPath, opts) def buildCommandState (m : DocumentMeta) From ae0aebae93a4132898cfcbf26b12989af8783bac Mon Sep 17 00:00:00 2001 From: mhuisi Date: Sat, 25 Nov 2023 20:43:33 +0100 Subject: [PATCH 15/16] refactor: clean up horrible setup-file control flow --- src/Lean/Server/FileWorker.lean | 122 ++++++--------------- src/Lean/Server/FileWorker/SetupFile.lean | 123 ++++++++++++++++++++++ src/Lean/Server/ImportCompletion.lean | 2 +- 3 files changed, 158 insertions(+), 89 deletions(-) create mode 100644 src/Lean/Server/FileWorker/SetupFile.lean diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index a265c40e8acd..c6f21bb207e1 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -22,6 +22,7 @@ import Lean.Server.References import Lean.Server.FileWorker.Utils import Lean.Server.FileWorker.RequestHandling import Lean.Server.FileWorker.WidgetRequests +import Lean.Server.FileWorker.SetupFile import Lean.Server.Rpc.Basic import Lean.Widget.InteractiveDiagnostic import Lean.Server.ImportCompletion @@ -163,85 +164,16 @@ abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO /- Worker initialization sequence. -/ section Initialization - - structure LakeSetupFileResult where - spawnArgs : Process.SpawnArgs - exitCode : UInt32 - stdout : String - stderr : String - - partial def runLakeSetupFile (lakePath : System.FilePath) (m : DocumentMeta) (filePath : System.FilePath) (imports : Array Import) (hOut : FS.Stream) : IO LakeSetupFileResult := do - let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module) - if m.dependencyBuildMode matches .never then - args := args.push "--no-build" - let spawnArgs : Process.SpawnArgs := { - stdin := Process.Stdio.null - stdout := Process.Stdio.piped - stderr := Process.Stdio.piped - cmd := lakePath.toString - args - } - let lakeProc ← Process.spawn spawnArgs - -- progress notification: reports latest stderr line - let rec processStderr (acc : String) : IO String := do - let line ← lakeProc.stderr.getLine - if line == "" then - return acc - else - publishDiagnostics m #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.information, message := line }] hOut - processStderr (acc ++ line) - let stderr ← IO.asTask (processStderr "") Task.Priority.dedicated - let stdout := String.trim (← lakeProc.stdout.readToEnd) - let stderr ← IO.ofExcept stderr.get - let exitCode ← lakeProc.wait - return ⟨spawnArgs, exitCode, stdout, stderr⟩ - - /-- Use `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`. - Compilation progress is reported to `hOut` via LSP notifications. Return the search path for - source files and the options for the file. -/ - partial def setupFile (m : DocumentMeta) (hOut : FS.Stream) (headerStx : Syntax) : IO (SearchPath × Options) := do - let invalidLakeSetup := (← initSrcSearchPath, Options.empty) - let some filePath := System.Uri.fileUriToPath? m.uri - | return invalidLakeSetup - - -- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps - -- NOTE: lake does not exist in stage 0 (yet?) - if filePath.fileName == "lakefile.lean" then - return invalidLakeSetup - - let lakePath ← determineLakePath - if !(← System.FilePath.pathExists lakePath) then - return invalidLakeSetup - - let imports := Lean.Elab.headerToImports headerStx - let result ← runLakeSetupFile lakePath m filePath imports hOut - let cmdStr := " ".intercalate (toString result.spawnArgs.cmd :: result.spawnArgs.args.toList) - - match result.exitCode with - | 0 => - let Except.ok (info : FileSetupInfo) ← pure (Json.parse result.stdout >>= fromJson?) - | throwServerError s!"invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}" - initSearchPath (← getBuildDir) info.paths.oleanPath - info.paths.loadDynlibPaths.forM loadDynlib - let pkgSearchPath ← info.paths.srcPath.mapM realPathNormalized - return (← initSrcSearchPath pkgSearchPath, info.setupOptions.toOptions) - | 2 => pure invalidLakeSetup -- no lakefile.lean - -- error from `--no-build` - | 3 => throwServerError s!"Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor.\n\n{result.stdout}" - | _ => throwServerError s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}" - - def buildHeaderEnv (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (headerStx : Syntax) : IO (Environment × MessageLog × SearchPath × Options) := do - let (headerEnv, msgLog, srcSearchPath, opts) ← - match ← EIO.toIO' <| setupFile m hOut headerStx with - | .ok (srcSearchPath, fileOptions) => - -- file options take priority - let opts := opts.mergeBy (fun _ _ fileOpt => fileOpt) fileOptions + def buildHeaderEnv (m : DocumentMeta) (headerStx : Syntax) (fileSetupResult : FileSetupResult) : IO (Environment × MessageLog) := do + let (headerEnv, msgLog) ← + match fileSetupResult.kind with + | .success | .noLakefile => -- allows `headerEnv` to be leaked, which would live until the end of the process anyway - let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) headerStx opts MessageLog.empty m.mkInputContext - pure (headerEnv, msgLog, srcSearchPath, opts) - | .error e => - let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := e.toString } - pure (← mkEmptyEnvironment, msgs, ← initSrcSearchPath, opts) + Elab.processHeader (leakEnv := true) headerStx fileSetupResult.fileOptions MessageLog.empty m.mkInputContext + | .importsOutOfDate => + mkErrorEnvironment "Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor." + | .error msg => + mkErrorEnvironment msg let mut headerEnv := headerEnv try @@ -250,7 +182,12 @@ section Initialization catch _ => pure () - return (headerEnv, msgLog, srcSearchPath, opts) + return (headerEnv, msgLog) + + where + mkErrorEnvironment (errorMsg : String) : IO (Environment × MessageLog) := do + let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := errorMsg } + return (← mkEmptyEnvironment, msgs) def buildCommandState (m : DocumentMeta) @@ -277,24 +214,33 @@ section Initialization } { Elab.Command.mkState headerEnv headerMsgLog opts with infoState := headerInfoState } - def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) + def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (globalOptions : Options) (hasWidgets : Bool) : IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do -- parsing should not take long, do synchronously let (headerStx, headerParserState, parseMsgLog) ← Parser.parseHeader m.mkInputContext (headerStx, ·) <$> EIO.asTask do - let (headerEnv, envMsgLog, srcSearchPath, opts) ← buildHeaderEnv m hOut opts headerStx + let imports := Lean.Elab.headerToImports headerStx + let fileSetupResult ← setupFile m imports fun stderrLine => + let progressDiagnostic := { + range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩ + severity? := DiagnosticSeverity.information + message := stderrLine + } + publishDiagnostics m #[progressDiagnostic] hOut + let fileSetupResult := fileSetupResult.addGlobalOptions globalOptions + let (headerEnv, envMsgLog) ← buildHeaderEnv m headerStx fileSetupResult let headerMsgLog := parseMsgLog.append envMsgLog - let cmdState := buildCommandState m headerStx headerEnv headerMsgLog opts + let cmdState := buildCommandState m headerStx headerEnv headerMsgLog fileSetupResult.fileOptions let headerSnap := { - beginPos := 0 - stx := headerStx - mpState := headerParserState - cmdState := cmdState + beginPos := 0 + stx := headerStx + mpState := headerParserState + cmdState := cmdState interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets) - tacticCache := (← IO.mkRef {}) + tacticCache := (← IO.mkRef {}) } publishDiagnostics m headerSnap.diagnostics.toArray hOut - return (headerSnap, srcSearchPath) + return (headerSnap, fileSetupResult.srcSearchPath) def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) : IO (WorkerContext × WorkerState) := do diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean new file mode 100644 index 000000000000..514037820f46 --- /dev/null +++ b/src/Lean/Server/FileWorker/SetupFile.lean @@ -0,0 +1,123 @@ +import Init.System.IO +import Lean.Server.Utils +import Lean.Util.FileSetupInfo +import Lean.Util.LakePath +import Lean.LoadDynlib + +namespace Lean.Server.FileWorker + +open IO + +structure LakeSetupFileOutput where + spawnArgs : Process.SpawnArgs + exitCode : UInt32 + stdout : String + stderr : String + +partial def runLakeSetupFile + (m : DocumentMeta) + (lakePath filePath : System.FilePath) + (imports : Array Import) + (handleStderr : String → IO Unit) + : IO LakeSetupFileOutput := do + let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module) + if m.dependencyBuildMode matches .never then + args := args.push "--no-build" + let spawnArgs : Process.SpawnArgs := { + stdin := Process.Stdio.null + stdout := Process.Stdio.piped + stderr := Process.Stdio.piped + cmd := lakePath.toString + args + } + let lakeProc ← Process.spawn spawnArgs + + let rec processStderr (acc : String) : IO String := do + let line ← lakeProc.stderr.getLine + if line == "" then + return acc + else + handleStderr line + processStderr (acc ++ line) + let stderr ← IO.asTask (processStderr "") Task.Priority.dedicated + + let stdout := String.trim (← lakeProc.stdout.readToEnd) + let stderr ← IO.ofExcept stderr.get + let exitCode ← lakeProc.wait + return ⟨spawnArgs, exitCode, stdout, stderr⟩ + +inductive FileSetupResultKind where + | success + | noLakefile + | importsOutOfDate + | error (msg : String) + +structure FileSetupResult where + kind : FileSetupResultKind + srcSearchPath : SearchPath + fileOptions : Options + +def FileSetupResult.ofSuccess (pkgSearchPath : SearchPath) (fileOptions : Options) + : IO FileSetupResult := do return { + kind := FileSetupResultKind.success + srcSearchPath := ← initSrcSearchPath pkgSearchPath, + fileOptions +} + +def FileSetupResult.ofNoLakefile : IO FileSetupResult := do return { + kind := FileSetupResultKind.noLakefile + srcSearchPath := ← initSrcSearchPath + fileOptions := Options.empty +} + +def FileSetupResult.ofImportsOutOfDate : IO FileSetupResult := do return { + kind := FileSetupResultKind.importsOutOfDate + srcSearchPath := ← initSrcSearchPath + fileOptions := Options.empty +} + +def FileSetupResult.ofError (msg : String) : IO FileSetupResult := do return { + kind := FileSetupResultKind.error msg + srcSearchPath := ← initSrcSearchPath + fileOptions := Options.empty +} + +def FileSetupResult.addGlobalOptions (result : FileSetupResult) (globalOptions : Options) + : FileSetupResult := + let fileOptions := globalOptions.mergeBy (fun _ _ fileOpt => fileOpt) result.fileOptions + { result with fileOptions := fileOptions } + +/-- Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`. +Compilation progress is reported to `handleStderr`. Returns the search path for +source files and the options for the file. -/ +partial def setupFile (m : DocumentMeta) (imports : Array Import) (handleStderr : String → IO Unit) : IO FileSetupResult := do + let some filePath := System.Uri.fileUriToPath? m.uri + | return ← FileSetupResult.ofNoLakefile -- untitled files have no lakefile + + -- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps + -- NOTE: lake does not exist in stage 0 (yet?) + if filePath.fileName == "lakefile.lean" then + return ← FileSetupResult.ofNoLakefile -- the lakefile itself has no lakefile + + let lakePath ← determineLakePath + if !(← System.FilePath.pathExists lakePath) then + return ← FileSetupResult.ofNoLakefile + + let result ← runLakeSetupFile m lakePath filePath imports handleStderr + + let cmdStr := " ".intercalate (toString result.spawnArgs.cmd :: result.spawnArgs.args.toList) + + match result.exitCode with + | 0 => + let Except.ok (info : FileSetupInfo) := Json.parse result.stdout >>= fromJson? + | return ← FileSetupResult.ofError s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}" + initSearchPath (← getBuildDir) info.paths.oleanPath + info.paths.loadDynlibPaths.forM loadDynlib + let pkgSearchPath ← info.paths.srcPath.mapM realPathNormalized + FileSetupResult.ofSuccess pkgSearchPath info.setupOptions.toOptions + | 2 => -- exit code for lake reporting that there is no lakefile + FileSetupResult.ofNoLakefile + | 3 => -- exit code for `--no-build` + FileSetupResult.ofImportsOutOfDate + | _ => + FileSetupResult.ofError s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}" diff --git a/src/Lean/Server/ImportCompletion.lean b/src/Lean/Server/ImportCompletion.lean index 25a0fe19edb5..0d2723ece4a3 100644 --- a/src/Lean/Server/ImportCompletion.lean +++ b/src/Lean/Server/ImportCompletion.lean @@ -97,7 +97,7 @@ def collectAvailableImportsFromLake : IO (Option AvailableImports) := do let exitCode ← lakeProc.wait match exitCode with | 0 => - let Except.ok (availableImports : AvailableImports) ← pure (Json.parse stdout >>= fromJson?) + let Except.ok (availableImports : AvailableImports) := Json.parse stdout >>= fromJson? | throw <| IO.userError s!"invalid output from `lake available-imports`:\n{stdout}" return availableImports | _ => From e01dee661e8afe7b82935a5a6b59f777c6a78999 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Sat, 25 Nov 2023 20:48:47 +0100 Subject: [PATCH 16/16] doc: forgot the file header again --- src/Lean/Server/FileWorker/SetupFile.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean index 514037820f46..3ecb20bcaf06 100644 --- a/src/Lean/Server/FileWorker/SetupFile.lean +++ b/src/Lean/Server/FileWorker/SetupFile.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich, Marc Huisinga +-/ import Init.System.IO import Lean.Server.Utils import Lean.Util.FileSetupInfo