From 619873c842738d5ecd4bdad50db7470176b831c0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 27 May 2021 15:34:25 +0200 Subject: [PATCH] feat: make System.FilePath opaque --- src/Init/System/FilePath.lean | 72 +++++++++++++++++----------- src/Lean/Data/Lsp/Ipc.lean | 6 +-- src/Lean/Environment.lean | 6 +-- src/Lean/Parser/Module.lean | 5 +- src/Lean/Server/FileWorker.lean | 17 +++---- src/Lean/Server/Utils.lean | 2 +- src/Lean/Server/Watchdog.lean | 8 ++-- src/Lean/Util/Path.lean | 35 +++++++------- src/Leanpkg.lean | 23 ++++----- src/Leanpkg/Git.lean | 26 +++++----- src/Leanpkg/Manifest.lean | 22 +++++---- src/Leanpkg/Proc.lean | 2 +- src/Leanpkg/Resolve.lean | 11 ++--- tests/lean/filePath.lean | 6 +-- tests/lean/readDir.lean.expected.out | 2 +- 15 files changed, 132 insertions(+), 111 deletions(-) diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 5b7b77b1c8..4bdae56b71 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -1,18 +1,28 @@ /- Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude import Init.System.Platform import Init.Data.String.Basic +import Init.Data.Repr +import Init.Data.ToString.Basic namespace System --- TODO: make opaque? -abbrev FilePath := String +open Platform + +structure FilePath where + toString : String + deriving Inhabited, DecidableEq + +instance : Repr FilePath where + reprPrec p := Repr.addAppParen ("FilePath.mk " ++ repr p.toString) + +instance : ToString FilePath where + toString p := p.toString namespace FilePath -open Platform /-- The character that separates directories. In the case where more than one character is possible, `pathSeparator` is the 'ideal' one. -/ def pathSeparator : Char := @@ -22,18 +32,11 @@ def pathSeparator : Char := def pathSeparators : List Char := if isWindows then ['\\', '/'] else ['/'] -/-- The character that is used to separate the entries in the $PATH (or %PATH%) environment variable. -/ -def searchPathSeparator : Char := - if isWindows then ';' else ':' - -def splitSearchPath (s : String) : List String := - s.split (fun c => searchPathSeparator == c) - /-- File extension character -/ def extSeparator : Char := '.' -def exeSuffix : String := -if isWindows then ".exe" else "" +def exeExtension : String := + if isWindows then "exe" else "" /-- Case-insensitive file system -/ def isCaseInsensitive : Bool := isWindows || isOSX @@ -41,15 +44,15 @@ def isCaseInsensitive : Bool := isWindows || isOSX -- TODO: normalize `a/`, `a//b`, etc. def normalize (p : FilePath) (normalizeCase := isCaseInsensitive) : FilePath := if pathSeparators.length == 1 && !normalizeCase then p - else p.map fun c => + else ⟨p.toString.map fun c => if pathSeparators.contains c then pathSeparator else if normalizeCase then c.toLower - else c + else c⟩ -- the following functions follow the names and semantics from Rust's `std::path::Path` def isAbsolute (p : FilePath) : Bool := - pathSeparators.contains p.front || (isWindows && p.bsize >= 1 && p[1] == ':') + pathSeparators.contains p.toString.front || (isWindows && p.toString.bsize >= 1 && p.toString[1] == ':') def isRelative (p : FilePath) : Bool := !p.isAbsolute @@ -58,25 +61,24 @@ def join (p sub : FilePath) : FilePath := if sub.isAbsolute then sub else - p ++ pathSeparator.toString ++ sub + ⟨p.toString ++ pathSeparator.toString ++ sub.toString⟩ instance : Div FilePath where div := FilePath.join --- when `FilePath` is opaque ---instance : HDiv FilePath String FilePath where --- hDiv := FilePath.join +instance : HDiv FilePath String FilePath where + hDiv p sub := FilePath.join p ⟨sub⟩ private def posOfLastSep (p : FilePath) : Option String.Pos := - p.revFind pathSeparators.contains + p.toString.revFind pathSeparators.contains def parent (p : FilePath) : Option FilePath := - p.extract 0 <$> posOfLastSep p + FilePath.mk <$> p.toString.extract 0 <$> posOfLastSep p def fileName (p : FilePath) : Option String := let lastPart := match posOfLastSep p with - | some sepPos => p.extract (sepPos + 1) p.bsize - | none => p + | some sepPos => p.toString.extract (sepPos + 1) p.toString.bsize + | none => p.toString if lastPart.isEmpty || lastPart == "." || lastPart == ".." then none else some lastPart /-- Extracts the stem (non-extension) part of `p.fileName`. -/ @@ -96,7 +98,7 @@ def extension (p : FilePath) : Option String := def withFileName (p : FilePath) (fname : String) : FilePath := match p.parent with - | none => fname + | none => ⟨fname⟩ | some p => p / fname def withExtension (p : FilePath) (ext : String) : FilePath := @@ -105,11 +107,27 @@ def withExtension (p : FilePath) (ext : String) : FilePath := | some stem => p.withFileName (if ext.isEmpty then stem else stem ++ "." ++ ext) def components (p : FilePath) : List String := - p.normalize (normalizeCase := false) |>.splitOn pathSeparator.toString + p.normalize (normalizeCase := false) |>.toString.splitOn pathSeparator.toString end FilePath def mkFilePath (parts : List String) : FilePath := - String.intercalate FilePath.pathSeparator.toString parts + ⟨String.intercalate FilePath.pathSeparator.toString parts⟩ + +abbrev SearchPath := List FilePath + +namespace SearchPath + +/-- The character that is used to separate the entries in the $PATH (or %PATH%) environment variable. -/ +protected def separator : Char := + if isWindows then ';' else ':' + +def parse (s : String) : SearchPath := + s.split (fun c => SearchPath.separator == c) |>.map FilePath.mk + +def toString (path : SearchPath) : String := + SearchPath.separator.toString.intercalate (path.map FilePath.toString) + +end SearchPath end System diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean index 7469cf43cf..615bbddb8f 100644 --- a/src/Lean/Data/Lsp/Ipc.lean +++ b/src/Lean/Data/Lsp/Ipc.lean @@ -69,11 +69,11 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : | _ => loop loop -def runWith (cmd : String) (args : Array String := #[]) (test : IpcM α) : IO α := do +def runWith (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) : IO α := do let proc ← Process.spawn { toStdioConfig := ipcStdioConfig - cmd := cmd + cmd := lean.toString args := args } ReaderT.run test proc -end Lean.Lsp.Ipc \ No newline at end of file +end Lean.Lsp.Ipc diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 0006cf7aae..8aeb8a2641 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -466,9 +466,9 @@ instance : Inhabited ModuleData := ⟨{imports := arbitrary, constants := arbitrary, entries := arbitrary }⟩ @[extern 3 "lean_save_module_data"] -constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit +constant saveModuleData (fname : @& System.FilePath) (m : ModuleData) : IO Unit @[extern 2 "lean_read_module_data"] -constant readModuleData (fname : @& String) : IO (ModuleData × CompactedRegion) +constant readModuleData (fname : @& System.FilePath) : IO (ModuleData × CompactedRegion) /-- Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in @@ -508,7 +508,7 @@ def mkModuleData (env : Environment) : IO ModuleData := do } @[export lean_write_module] -def writeModule (env : Environment) (fname : String) : IO Unit := do +def writeModule (env : Environment) (fname : System.FilePath) : IO Unit := do let modData ← mkModuleData env; saveModuleData fname modData private partial def getEntriesFor (mod : ModuleData) (extId : Name) (i : Nat) : Array EnvExtensionEntry := diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index b853ef4cf2..f12cd4929f 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -116,16 +116,15 @@ partial def testParseModuleAux (env : Environment) (inputCtx : InputContext) (s parse s msgs stxs def testParseModule (env : Environment) (fname contents : String) : IO Syntax := do - let fname ← IO.realPath fname let inputCtx := mkInputContext contents fname let (header, state, messages) ← parseHeader inputCtx let cmds ← testParseModuleAux env inputCtx state messages #[] let stx := Syntax.node `Lean.Parser.Module.module #[header, mkListNode cmds] pure stx.updateLeading -def testParseFile (env : Environment) (fname : String) : IO Syntax := do +def testParseFile (env : Environment) (fname : System.FilePath) : IO Syntax := do let contents ← IO.FS.readFile fname - testParseModule env fname contents + testParseModule env fname.toString contents end Parser end Lean diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index aa4725b76e..db00a50371 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -152,12 +152,12 @@ section Initialization /-- Use `leanpkg print-paths` to compile dependencies on the fly and add them to `LEAN_PATH`. Compilation progress is reported to `hOut` via LSP notifications. Return the search path for source files. -/ - partial def leanpkgSetupSearchPath (leanpkgPath : String) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do + partial def leanpkgSetupSearchPath (leanpkgPath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do let leanpkgProc ← Process.spawn { stdin := Process.Stdio.null stdout := Process.Stdio.piped stderr := Process.Stdio.piped - cmd := leanpkgPath + cmd := leanpkgPath.toString args := #["print-paths"] ++ imports.map (toString ·.module) } -- progress notification: report latest stderr line @@ -176,9 +176,9 @@ section Initialization | [""] => pure [] -- e.g. no leanpkg.toml | [leanPath, leanSrcPath] => let sp ← getBuiltinSearchPath let sp ← addSearchPathFromEnv sp - let sp ← parseSearchPath leanPath sp + let sp := System.SearchPath.parse leanPath ++ sp searchPathRef.set sp - let srcPath := parseSearchPath leanSrcPath + let srcPath := System.SearchPath.parse leanSrcPath srcPath.mapM realPathNormalized | _ => throw <| IO.userError s!"unexpected output from `leanpkg print-paths`:\n{stdout}\nstderr:\n{stderr}" else @@ -189,11 +189,12 @@ section Initialization let inputCtx := Parser.mkInputContext m.text.source "" let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with - | some path => pure <| (path : System.FilePath) / "bin" / s!"leanpkg{System.FilePath.exeSuffix}" - | _ => pure <| (← appDir) / s!"leanpkg{System.FilePath.exeSuffix}" + | some path => pure <| System.FilePath.mk path / "bin" / "leanpkg" + | _ => pure <| (← appDir) / "leanpkg" + let leanpkgPath := leanpkgPath.withExtension System.FilePath.exeExtension let mut srcSearchPath := [(← appDir) / ".." / "lib" / "lean" / "src"] if let some p := (← IO.getEnv "LEAN_SRC_PATH") then - srcSearchPath := srcSearchPath ++ parseSearchPath p + srcSearchPath := srcSearchPath ++ System.SearchPath.parse p let (headerEnv, msgLog) ← try -- NOTE: leanpkg does not exist in stage 0 (yet?) if (← System.FilePath.pathExists leanpkgPath) then @@ -411,7 +412,7 @@ section RequestHandling let mod? ← ci.runMetaM i.lctx <| findModuleOf? n let modUri? ← match mod? with | some modName => - let modFname? ← st.srcSearchPath.findWithExt ".lean" modName + let modFname? ← st.srcSearchPath.findWithExt "lean" modName pure <| modFname?.map toFileUri | none => pure <| some doc.meta.uri diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index 72a32fb9f9..a0d29c4a33 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -92,7 +92,7 @@ def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := d /-- Transform the given path to a file:// URI. -/ def toFileUri (fname : System.FilePath) : Lsp.DocumentUri := - let fname := fname.normalize + let fname := fname.normalize.toString let fname := if System.Platform.isWindows then fname.map fun c => if c == '\\' then '/' else c else diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 190303b4ad..dbfa4d2c31 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -178,7 +178,7 @@ section ServerM /-- We store these to pass them to workers. -/ initParams : InitializeParams editDelay : Nat - workerPath : String + workerPath : System.FilePath abbrev ServerM := ReaderT ServerContext IO @@ -234,7 +234,7 @@ section ServerM let headerAst ← parseHeaderAst m.text.source let workerProc ← Process.spawn { toStdioConfig := workerCfg - cmd := st.workerPath + cmd := st.workerPath.toString args := #["--worker"] ++ st.args.toArray } let pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap) @@ -553,9 +553,9 @@ def initAndRunWatchdogAux : ServerM Unit := do def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do let mut workerPath ← IO.appPath if let some path := (←IO.getEnv "LEAN_SYSROOT") then - workerPath := s!"{path}/bin/lean{System.FilePath.exeSuffix}" + workerPath := System.FilePath.mk path / "bin" / "lean" |>.withExtension System.FilePath.exeExtension if let some path := (←IO.getEnv "LEAN_WORKER_PATH") then - workerPath := path + workerPath := System.FilePath.mk path let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap) let i ← maybeTee "wdIn.txt" false i let o ← maybeTee "wdOut.txt" true o diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index 1ad2dd0450..d6e6ffbe7a 100644 --- a/src/Lean/Util/Path.lean +++ b/src/Lean/Util/Path.lean @@ -13,33 +13,32 @@ import Lean.Data.Name namespace Lean open System -def realPathNormalized (p : FilePath) : IO String := do +def realPathNormalized (p : FilePath) : IO FilePath := do (← IO.realPath p).normalize +variable (base : FilePath) in def modPathToFilePath : Name → FilePath | Name.str p h _ => modPathToFilePath p / h - | Name.anonymous => "" + | Name.anonymous => base | Name.num p _ _ => panic! "ill-formed import" -abbrev SearchPath := List FilePath +/-- A `.olean' search path. -/ +abbrev SearchPath := System.SearchPath namespace SearchPath /-- If the package of `mod` can be found in `sp`, return the path with extension -`ext` (`.lean` or `.olean`) corresponding to `mod`. Otherwise, return `none.` -/ +`ext` (`lean` or `olean`) corresponding to `mod`. Otherwise, return `none.` -/ def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do let pkg := mod.getRoot.toString let root? ← sp.findM? fun p => - (p / pkg).isDir <||> (p / (pkg ++ ext)).pathExists - return root?.map (· ++ modPathToFilePath mod ++ ext) + (p / pkg).isDir <||> ((p / pkg).withExtension ext).pathExists + return root?.map (modPathToFilePath · mod |>.withExtension ext) end SearchPath builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {} -def parseSearchPath (path : String) (sp : SearchPath := ∅) : SearchPath := - System.FilePath.splitSearchPath path ++ sp - @[extern c inline "LEAN_IS_STAGE0"] private constant isStage0 (u : Unit) : Bool @@ -55,12 +54,12 @@ def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do let val ← IO.getEnv "LEAN_PATH" match val with | none => pure sp - | some val => parseSearchPath val sp + | some val => pure <| SearchPath.parse val ++ sp @[export lean_init_search_path] def initSearchPath (path : Option String := none) : IO Unit := match path with - | some path => searchPathRef.set <| parseSearchPath path + | some path => searchPathRef.set <| SearchPath.parse path | none => do let sp ← getBuiltinSearchPath let sp ← addSearchPathFromEnv sp @@ -68,10 +67,10 @@ def initSearchPath (path : Option String := none) : IO Unit := partial def findOLean (mod : Name) : IO FilePath := do let sp ← searchPathRef.get - if let some fname ← sp.findWithExt ".olean" mod then + if let some fname ← sp.findWithExt "olean" mod then return fname else - let pkg : FilePath := mod.getRoot.toString + let pkg := FilePath.mk mod.getRoot.toString let mut msg := s!"unknown package '{pkg}'" let rec maybeThisOne dir := do if ← (pkg / dir).isDir then @@ -92,13 +91,13 @@ def moduleNameOfFileName (fname : FilePath) (rootDir : Option FilePath) : IO Nam | some rootDir => pure rootDir | none => IO.currentDir let mut rootDir ← realPathNormalized rootDir - if !rootDir.endsWith System.FilePath.pathSeparator.toString then - rootDir := rootDir ++ System.FilePath.pathSeparator.toString - if !rootDir.isPrefixOf fname.normalize then + if !rootDir.toString.endsWith System.FilePath.pathSeparator.toString then + rootDir := ⟨rootDir.toString ++ System.FilePath.pathSeparator.toString⟩ + if !rootDir.toString.isPrefixOf fname.normalize.toString then throw $ IO.userError s!"input file '{fname}' must be contained in root directory ({rootDir})" -- NOTE: use `fname` instead of `fname.normalize` to preserve casing on all platforms - let fnameSuffix := fname.drop rootDir.length - let modNameStr := System.FilePath.withExtension fnameSuffix "" + let fnameSuffix := fname.toString.drop rootDir.toString.length + let modNameStr := FilePath.mk fnameSuffix |>.withExtension "" let modName := modNameStr.components.foldl Name.mkStr Name.anonymous pure modName diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean index 0edc72edd4..3b3ac66f5a 100644 --- a/src/Leanpkg.lean +++ b/src/Leanpkg.lean @@ -6,6 +6,8 @@ Authors: Gabriel Ebner, Sebastian Ullrich import Leanpkg.Resolve import Leanpkg.Git +open System + namespace Leanpkg def readManifest : IO Manifest := do @@ -15,10 +17,10 @@ def readManifest : IO Manifest := do ++ ", but package requires " ++ m.leanVersion ++ "\n" return m -def writeManifest (manifest : Lean.Syntax) (fn : String) : IO Unit := do +def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do IO.FS.writeFile fn manifest.reprint.get! -def lockFileName : System.FilePath := ".leanpkg-lock" +def lockFileName : System.FilePath := ⟨".leanpkg-lock"⟩ partial def withLockFile (x : IO α) : IO α := do acquire @@ -57,18 +59,17 @@ def configure : IO Configuration := do let assg ← solveDeps d let paths ← constructPath assg for path in paths do - unless path == "./." do + unless path == FilePath.mk "." / "." do -- build recursively -- TODO: share build of common dependencies execCmd { - cmd := (← IO.appPath) + cmd := (← IO.appPath).toString cwd := path args := #["build"] } - let sep := System.FilePath.searchPathSeparator.toString return { - leanPath := sep.intercalate <| paths.map (· / "build") - leanSrcPath := sep.intercalate paths + leanPath := SearchPath.toString <| paths.map (fun (p : FilePath) => p / "build") + leanSrcPath := paths.toString } def execMake (makeArgs leanArgs : List String) (leanPath : String) : IO Unit := withLockFile do @@ -90,7 +91,7 @@ def buildImports (imports : List String) (leanArgs : List String) : IO Unit := d -- TODO: shoddy check let localImports := imports.filter fun i => i.getRoot.toString.toLower == manifest.name.toLower if localImports != [] then - let oleans := localImports.map fun i => s!"\"build{Lean.modPathToFilePath i}.olean\"" + let oleans := localImports.map fun i => Lean.modPathToFilePath ⟨"build"⟩ i |>.withExtension "olean" |>.toString execMake oleans leanArgs cfg.leanPath IO.println cfg.leanPath IO.println cfg.leanSrcPath @@ -108,12 +109,12 @@ name = \"{n}\" version = \"0.1\" lean_version = \"{leanVersionString}\" " - IO.FS.writeFile s!"{n.capitalize}.lean" "def main : IO Unit := + IO.FS.writeFile ⟨s!"{n.capitalize}.lean"⟩ "def main : IO Unit := IO.println \"Hello, world!\" " - let h ← IO.FS.Handle.mk ".gitignore" IO.FS.Mode.append (bin := false) + let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false) h.putStr initGitignoreContents - unless ← System.FilePath.isDir ".git" do + unless ← System.FilePath.isDir ⟨".git"⟩ do (do execCmd {cmd := "git", args := #["init", "-q"]} unless upstreamGitBranch = "master" do diff --git a/src/Leanpkg/Git.lean b/src/Leanpkg/Git.lean index a2ebcdcc8f..55ce109228 100644 --- a/src/Leanpkg/Git.lean +++ b/src/Leanpkg/Git.lean @@ -5,6 +5,8 @@ Authors: Gabriel Ebner, Sebastian Ullrich -/ import Leanpkg.LeanVersion +open System + namespace Leanpkg def upstreamGitBranch := @@ -14,24 +16,24 @@ def gitdefaultRevision : Option String → String | none => upstreamGitBranch | some branch => branch -def gitParseRevision (gitRepoDir : String) (rev : String) : IO String := do - let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepoDir} +def gitParseRevision (gitRepo : FilePath) (rev : String) : IO String := do + let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepo} rev.trim -- remove newline at end -def gitHeadRevision (gitRepoDir : String) : IO String := - gitParseRevision gitRepoDir "HEAD" +def gitHeadRevision (gitRepo : FilePath) : IO String := + gitParseRevision gitRepo "HEAD" -def gitParseOriginRevision (gitRepoDir : String) (rev : String) : IO String := - (gitParseRevision gitRepoDir $ "origin/" ++ rev) <|> gitParseRevision gitRepoDir rev - <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepoDir}") +def gitParseOriginRevision (gitRepo : FilePath) (rev : String) : IO String := + (gitParseRevision gitRepo $ "origin/" ++ rev) <|> gitParseRevision gitRepo rev + <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepo}") -def gitLatestOriginRevision (gitRepoDir : String) (branch : Option String) : IO String := do - discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepoDir} - gitParseOriginRevision gitRepoDir (gitdefaultRevision branch) +def gitLatestOriginRevision (gitRepo : FilePath) (branch : Option String) : IO String := do + discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepo} + gitParseOriginRevision gitRepo (gitdefaultRevision branch) -def gitRevisionExists (gitRepoDir : String) (rev : String) : IO Bool := do +def gitRevisionExists (gitRepo : FilePath) (rev : String) : IO Bool := do try - discard <| gitParseRevision gitRepoDir (rev ++ "^{commit}") + discard <| gitParseRevision gitRepo (rev ++ "^{commit}") true catch _ => false diff --git a/src/Leanpkg/Manifest.lean b/src/Leanpkg/Manifest.lean index 362e91c4ef..50caaafe4e 100644 --- a/src/Leanpkg/Manifest.lean +++ b/src/Leanpkg/Manifest.lean @@ -6,17 +6,19 @@ Authors: Gabriel Ebner, Sebastian Ullrich import Leanpkg.Toml import Leanpkg.LeanVersion +open System + namespace Leanpkg inductive Source where - | path (dirName : String) : Source + | path (dir : System.FilePath) : Source | git (url rev : String) (branch : Option String) : Source namespace Source def fromToml (v : Toml.Value) : Option Source := - (do let Toml.Value.str dirName ← v.lookup "path" | none - path dirName) <|> + (do let Toml.Value.str dir ← v.lookup "path" | none + path ⟨dir⟩) <|> (do let Toml.Value.str url ← v.lookup "git" | none let Toml.Value.str rev ← v.lookup "rev" | none match v.lookup "branch" with @@ -25,7 +27,7 @@ def fromToml (v : Toml.Value) : Option Source := | _ => none) def toToml : Source → Toml.Value - | path dirName => Toml.Value.table [("path", Toml.Value.str dirName)] + | path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)] | git url rev none => Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)] | git url rev (some branch) => @@ -42,13 +44,13 @@ structure Manifest where version : String leanVersion : String := leanVersionString timeout : Option Nat := none - path : Option String := none + path : Option FilePath := none dependencies : List Dependency := [] namespace Manifest -def effectivePath (m : Manifest) : String := - m.path.getD "." +def effectivePath (m : Manifest) : FilePath := + m.path.getD ⟨"."⟩ def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do let pkg ← t.lookup "package" @@ -63,7 +65,7 @@ def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do | none => some none | _ => none let path ← match pkg.lookup "path" with - | some (Toml.Value.str path) => some (some path) + | some (Toml.Value.str path) => some (some ⟨path⟩) | none => some none | _ => none let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none @@ -71,7 +73,7 @@ def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do return { name := n, version := ver, leanVersion := leanVer, path := path, dependencies := deps, timeout := tm } -def fromFile (fn : String) : IO Manifest := do +def fromFile (fn : System.FilePath) : IO Manifest := do let cnts ← IO.FS.readFile fn let toml ← Toml.parse cnts let some manifest ← pure (fromToml toml) @@ -80,6 +82,6 @@ def fromFile (fn : String) : IO Manifest := do end Manifest -def leanpkgTomlFn : System.FilePath := "leanpkg.toml" +def leanpkgTomlFn : System.FilePath := ⟨"leanpkg.toml"⟩ end Leanpkg diff --git a/src/Leanpkg/Proc.lean b/src/Leanpkg/Proc.lean index aeb5c05b44..cd4db43195 100644 --- a/src/Leanpkg/Proc.lean +++ b/src/Leanpkg/Proc.lean @@ -10,7 +10,7 @@ def execCmd (args : IO.Process.SpawnArgs) : IO Unit := do let cmdstr := " ".intercalate (args.cmd :: args.args.toList) IO.eprintln <| "> " ++ envstr ++ match args.cwd with - | some cwd => cmdstr ++ " # in directory " ++ cwd + | some cwd => s!"{cmdstr} # in directory {cwd}" | none => cmdstr let child ← IO.Process.spawn args let exitCode ← child.wait diff --git a/src/Leanpkg/Resolve.lean b/src/Leanpkg/Resolve.lean index 2e0f9e235c..57f76c1b02 100644 --- a/src/Leanpkg/Resolve.lean +++ b/src/Leanpkg/Resolve.lean @@ -43,7 +43,7 @@ def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit := IO.eprintln s!"{dep.name}: using local path {depdir}" modify (·.insert dep.name depdir) | Source.git url rev branch => do - let depdir : FilePath := "build" / "deps" / dep.name + let depdir := FilePath.mk "build" / "deps" / dep.name if ← depdir.isDir then IO.eprint s!"{dep.name}: trying to update {depdir} to revision {rev}" IO.eprintln (match branch with | none => "" | some branch => "@" ++ branch) @@ -53,7 +53,7 @@ def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit := execCmd {cmd := "git", args := #["fetch"], cwd := depdir} else IO.eprintln s!"{dep.name}: cloning {url} to {depdir}" - execCmd {cmd := "git", args := #["clone", url, depdir]} + execCmd {cmd := "git", args := #["clone", url, depdir.toString]} let hash ← gitParseOriginRevision depdir rev execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir} modify (·.insert dep.name depdir) @@ -67,15 +67,14 @@ def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Sol let p ← resolvedPath dep.name let d' ← Manifest.fromFile $ p / "leanpkg.toml" unless d'.name = dep.name do - throw <| IO.userError <| d.name ++ " (in " ++ relPath ++ ") depends on " ++ d'.name ++ - ", but resolved dependency has name " ++ dep.name ++ " (in " ++ p ++ ")" + throw <| IO.userError s!"{d.name} (in {relPath}) depends on {d'.name}, but resolved dependency has name {dep.name} (in {p})" solveDepsCore p d' maxDepth def solveDeps (d : Manifest) : IO Assignment := do - let (_, assg) ← (solveDepsCore "." d 1024).run <| Assignment.empty.insert d.name "." + let (_, assg) ← (solveDepsCore ⟨"."⟩ d 1024).run <| Assignment.empty.insert d.name ⟨"."⟩ assg -def constructPathCore (depname : String) (dirname : FilePath) : IO String := do +def constructPathCore (depname : String) (dirname : FilePath) : IO FilePath := do let path ← Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn) return dirname / path diff --git a/tests/lean/filePath.lean b/tests/lean/filePath.lean index e35389bfd0..ee4915ada5 100644 --- a/tests/lean/filePath.lean +++ b/tests/lean/filePath.lean @@ -2,7 +2,7 @@ open System open System.Platform def norm (f : FilePath) : String := - f.map fun c => if c == '\\' then '/' else c + f.toString.map fun c => if c == '\\' then '/' else c #eval FilePath.isAbsolute (if isWindows then "C:\\foo" else "/foo") #eval FilePath.isAbsolute "a/b" @@ -11,9 +11,9 @@ def norm (f : FilePath) : String := #eval norm <| ("a" : FilePath) / "b" / "c" #eval norm <| ("a" : FilePath) / "/b/c" -#eval FilePath.parent "a/b" +#eval norm <$> FilePath.parent "a/b" #eval norm <$> FilePath.parent "a/b/c" -#eval FilePath.parent "a" +#eval norm <$> FilePath.parent "a" #eval FilePath.fileName "a/b" diff --git a/tests/lean/readDir.lean.expected.out b/tests/lean/readDir.lean.expected.out index 12fed7ab46..902f0ec25e 100644 --- a/tests/lean/readDir.lean.expected.out +++ b/tests/lean/readDir.lean.expected.out @@ -1 +1 @@ -#[{ root := "Reformat", fileName := "Input.lean" }] +#[{ root := FilePath.mk "Reformat", fileName := "Input.lean" }]