diff --git a/nix/lake-dev.in b/nix/lake-dev.in index 837bc37272..aa8a9f7101 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 67250f94aa..d9107b1958 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 744ee694d5..c6f21bb207 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -11,7 +11,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 @@ -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,84 +164,16 @@ abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO /- Worker initialization sequence. -/ section Initialization - - structure LakePrintPathsResult where - spawnArgs : Process.SpawnArgs - exitCode : UInt32 - stdout : String - stderr : String - - partial def runLakePrintPaths (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO LakePrintPathsResult := do - let mut args := #["print-paths"] ++ 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⟩ - - /-- Uses `lake print-paths` to compile dependencies on the fly and adds them to `LEAN_PATH`. - Compilation progress is reported to `hOut` via LSP notifications. Returns the search path for - source files. -/ - partial def lakeSetupSearchPath (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do - let result ← runLakePrintPaths lakePath m imports hOut - let cmdStr := " ".intercalate (toString result.spawnArgs.cmd :: result.spawnArgs.args.toList) - match result.exitCode with - | 0 => - let Except.ok (paths : LeanPaths) ← pure (Json.parse result.stdout >>= fromJson?) - | throwServerError s!"invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}" - initSearchPath (← getBuildDir) paths.oleanPath - paths.loadDynlibPaths.forM loadDynlib - paths.srcPath.mapM realPathNormalized - | 2 => pure [] -- 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 setupSrcSearchPath (m : DocumentMeta) (hOut : FS.Stream) (headerStx : Syntax) : IO SearchPath := do - let some path := System.Uri.fileUriToPath? m.uri - | return ← initSrcSearchPath - - -- 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 ← initSrcSearchPath - - let lakePath ← determineLakePath - if !(← System.FilePath.pathExists lakePath) then - return ← initSrcSearchPath - - let imports := Lean.Elab.headerToImports headerStx - let pkgSearchPath ← lakeSetupSearchPath lakePath m imports hOut - return ← initSrcSearchPath pkgSearchPath - - def buildHeaderEnv (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (headerStx : Syntax) : IO (Environment × MessageLog × SearchPath) := do - let (headerEnv, msgLog, srcSearchPath) ← - match ← EIO.toIO' <| setupSrcSearchPath m hOut headerStx with - | .ok srcSearchPath => + 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) - | .error e => - let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := e.toString } - pure (← mkEmptyEnvironment, msgs, ← initSrcSearchPath) + 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 @@ -249,7 +182,12 @@ section Initialization catch _ => pure () - return (headerEnv, msgLog, srcSearchPath) + 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) @@ -276,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) ← 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 0000000000..3ecb20bcaf --- /dev/null +++ b/src/Lean/Server/FileWorker/SetupFile.lean @@ -0,0 +1,128 @@ +/- +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 +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 25a0fe19ed..0d2723ece4 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 | _ => diff --git a/src/Lean/Server/README.md b/src/Lean/Server/README.md index b6d1a0d013..fc0426403d 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.lean b/src/Lean/Util.lean index 24f282e831..f805860413 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/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean new file mode 100644 index 0000000000..0560f80a6c --- /dev/null +++ b/src/Lean/Util/FileSetupInfo.lean @@ -0,0 +1,14 @@ +/- +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 + +/-- +Information shared between Lake and Lean when calling `lake setup-file`. +-/ +structure Lean.FileSetupInfo where + paths : LeanPaths + setupOptions : LeanOptions + deriving FromJson, ToJson diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean new file mode 100644 index 0000000000..f52d48814f --- /dev/null +++ b/src/Lean/Util/LeanOptions.lean @@ -0,0 +1,92 @@ +/- +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 + +/-- Restriction of `DataValue` that covers exactly those cases that Lean is able to handle when passed via the `-D` flag. -/ +inductive LeanOptionValue where + | ofString (s : String) + | ofBool (b : Bool) + | ofNat (n : Nat) + deriving Inhabited, Repr + +def LeanOptionValue.ofDataValue? : DataValue → Option LeanOptionValue + | .ofString s => some (.ofString s) + | .ofBool b => some (.ofBool b) + | .ofNat n => some (.ofNat n) + | _ => none + +def LeanOptionValue.toDataValue : LeanOptionValue → DataValue + | .ofString s => .ofString s + | .ofBool b => .ofBool b + | .ofNat n => .ofNat n + +instance : KVMap.Value LeanOptionValue where + toDataValue := LeanOptionValue.toDataValue + ofDataValue? := LeanOptionValue.ofDataValue? + +instance : Coe String LeanOptionValue where + coe := LeanOptionValue.ofString + +instance : Coe Bool LeanOptionValue where + coe := LeanOptionValue.ofBool + +instance : Coe Nat LeanOptionValue where + coe := LeanOptionValue.ofNat + +instance : FromJson LeanOptionValue where + fromJson? + | (s : String) => Except.ok s + | (b : Bool) => Except.ok b + | (n : Nat) => Except.ok n + | _ => Except.error "invalid LeanOptionValue type" + +instance : ToJson LeanOptionValue where + toJson + | (s : String) => s + | (b : Bool) => b + | (n : Nat) => n + +/-- 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 Lean as if they were passed using `-D`. -/ +structure LeanOptions where + values : RBMap Name LeanOptionValue Name.cmp + deriving Inhabited, Repr + +def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do + let mut options := KVMap.empty + for ⟨name, optionValue⟩ in leanOptions.values do + options := options.insert name optionValue.toDataValue + return options + +def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do + let mut values := RBMap.empty + for ⟨name, dataValue⟩ in options do + let optionValue ← LeanOptionValue.ofDataValue? dataValue + values := values.insert name optionValue + return ⟨values⟩ + +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 LeanOptions type" + +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) + +end Lean diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean index ee89e7483c..3d944c3b83 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/Init.lean b/src/lake/Lake/CLI/Init.lean index 0bf963281a..057638f3ec 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 moreServerArgs := #[ - \"-Dpp.unicode.fun=true\", -- pretty-prints `fun a ↦ b` - \"-Dpp.proofs.withType=false\" +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 := moreServerArgs - -- 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 - moreServerArgs := moreServerArgs + 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/Main.lean b/src/lake/Lake/CLI/Main.lean index e219110db1..9b2ab3df39 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 191d85860e..de1f497743 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 -/-- 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,24 @@ 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 : LeanOptions ← do + let some moduleName ← searchModuleNameOfFileName path ws.leanSrcPath + | pure ⟨∅⟩ + let some module := ws.findModule? moduleName + | pure ⟨∅⟩ + 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, + setupOptions + : FileSetupInfo + } else exit noConfigFileCode @@ -55,7 +67,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 33a884f0da..305afc7166 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 9e6814f0f1..1dd8cd4dcf 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -1,3 +1,5 @@ +import Lean.Util.LeanOptions + /- Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -80,6 +82,16 @@ def BuildType.leancArgs : BuildType → Array String | minSizeRel => #["-Os", "-DNDEBUG"] | release => #["-O3", "-DNDEBUG"] +/-- Option that is used by Lean as if it was passed using `-D`. -/ +structure LeanOption where + name : Lean.Name + value : Lean.LeanOptionValue + deriving Inhabited, Repr + +/-- 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. -/ structure LeanConfig where /-- @@ -88,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. -/ @@ -110,6 +128,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 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 50995f6549..fcda7a5534 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -87,6 +87,17 @@ 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 package's `moreServerOptions` +- the library's `leanOptions` +- the library's `moreServerOptions` +-/ +@[inline] def serverOptions (self : LeanLib) : Array LeanOption := + self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions + /-- The build type for modules of this library. That is, the minimum of package's `buildType` and the library's `buildType`. @@ -101,12 +112,17 @@ 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. -That is, the package's `moreLeanArgs` plus the library's `moreLeanArgs`. +`leanArgs` is the accumulation of: +- the package's `leanOptions` +- the package's `moreLeanArgs` +- the library's `leanOptions` +- 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. diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index b4e7845b78..9038d5d749 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 bf70a5d7ed..39314fcb8e 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -88,11 +88,20 @@ 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 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 := #[] + /-- + 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. Defaults to the package's directory. @@ -310,9 +319,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 appended to its `leanOptions` configuration. -/ +@[inline] def moreServerOptions (self : Package) : Array LeanOption := + self.config.leanOptions ++ self.config.moreServerOptions /-- The package's `buildType` configuration. -/ @[inline] def buildType (self : Package) : BuildType := @@ -322,9 +335,13 @@ namespace Package @[inline] def backend (self : Package) : Backend := self.config.backend -/-- The package's `moreLeanArgs` configuration. -/ +/-- The package's `leanOptions` configuration. -/ +@[inline] def leanOptions (self : Package) : Array LeanOption := + self.config.leanOptions + +/-- 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 := diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index 52d75cfc23..7aa855e7fb 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 `moreServerOptions`" -- Fill in the Package return {self with diff --git a/src/lake/README.md b/src/lake/README.md index 9cabf5a4b2..5c2d246b9c 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -165,8 +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`. -* `moreServerArgs`: Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. +* `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`. @@ -206,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`: 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 @@ -227,7 +229,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 34f4ae865b..5117a6bb8a 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 de26391c8f..2d561e16ba 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 d7f32ccd75..1d6d4a3c28 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 b725503d53..0801d3603c 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`. diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out index 787c3640f3..cc081a1d90 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 2a50da1c88..86608a6bd9 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 c2fe11449b..cb8d2d4bae 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 f9137c9288..155bb3aa7e 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 0dc92d70df..faadde731f 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 d231a2a7ad..a8048d8e71 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 5d146f6c67..a60251092b 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 cb2d82d062..8c80d1d3c8 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 1b3f3d24e9..51c64e75ce 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 2f09c34825..687ff34fcb 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 3be618a0fc..e616d3c9ee 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 78a759c773..68fd411338 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 28419bfb88..8963177efa 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 f721ab7c71..b2620931aa 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 48ba7a29a1..615bb214c8 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 88b2e8c18d..67d9fc4fe5 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 38d270ac56..b88a5e9310 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 d3976fb926..e5586b430b 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 f50c1efce9..04dd60a4ea 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 48577fdddf..6a27b6c940 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 24204c8e7c..4521ca09a1 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 db1c3bdafa..db831fc9d4 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 2735770873..47ea662abb 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 6797b7a161..0bdc0109fc 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 4d4d4bff94..903119b94f 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 10bcdf3c28..87db187850 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 b7d96fb332..3b10090a62 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 b09821e1e0..e5c62054a3 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 03891dd7e8..cec637cc5f 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 3ad143e86c..17459b1552 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 d80fe93880..7625ab84e9 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 1c6ad9bbf7..c8c677973d 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 1c5b8158e4..78ee05fc63 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 e33ef5c371..f69f864c19 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 ba756c710b..316024c5f5 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 3dc760c2d1..18a74f7f9d 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 8bb8197ac4..aa06e923e6 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 d6e35fe956..83627f6f41 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 8b7b863789..bed3a64ebf 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 8feb7444c4..27c5f6e779 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 0ee83936b0..11bd07180d 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 3634be3173..8a129ccea4 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 5fdb8faa98..c53f87cf02 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 09f0cb0da5..844b67da3b 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 f692d42901..af093fa3a8 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 45517b1676..08fdc09894 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 d7012c79dc..699aff4770 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 2a72302a74..f71d1926f9 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 79da0eaabb..3e531b9212 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 001ac9cc14..09fc8e7896 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 98836ec33b..e3e7a1992c 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 18356b79d9..b87a4c2da1 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 5e4555b01d..55e628339f 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 7990334045..392d9bc4ff 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 08c2d30bcc..427e2a554e 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 cf4173bfc6..3bf39b6dcf 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 2e8a471fb1..40fa13fb65 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,73 +109,73 @@ ["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"}, +{"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"]} diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out index 1e85669f56..96a2f368b9 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/rename.lean.expected.out b/tests/lean/interactive/rename.lean.expected.out index bf4b7aec4b..1d63331904 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": {}} diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean index b640fe3399..5b56d44f20 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 69cbfa37d2..9d2e52d626 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": []}