From a3c73f5df8e6d426cf36853b33e8ebbf58c2aa8a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 16 Mar 2022 10:25:05 +0100 Subject: [PATCH] chore: remove orphan file --- src/Leanpkg.lean | 228 ----------------------------------------------- 1 file changed, 228 deletions(-) delete mode 100644 src/Leanpkg.lean diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean deleted file mode 100644 index b7e15e4c51..0000000000 --- a/src/Leanpkg.lean +++ /dev/null @@ -1,228 +0,0 @@ -/- -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gabriel Ebner, Sebastian Ullrich --/ -import Leanpkg.Resolve -import Leanpkg.Git -import Leanpkg.Build -import Lean.Util.Paths - -open System - -namespace Leanpkg - -def readManifest : IO Manifest := do - let m ← Manifest.fromFile leanpkgTomlFn - if m.leanVersion ≠ leanVersionString then - IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString - ++ ", but package requires " ++ m.leanVersion ++ "\n" - return m - -def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do - IO.FS.writeFile fn manifest.reprint.get! - -def lockFileName : System.FilePath := ⟨".leanpkg-lock"⟩ - -partial def withLockFile (x : IO α) : IO α := do - acquire - try - x - finally - IO.FS.removeFile lockFileName - where - acquire (firstTime := true) := - try - -- TODO: lock file should ideally contain PID - if !System.Platform.isWindows then - discard <| IO.FS.Handle.mkPrim lockFileName "wx" - else - -- `x` mode doesn't seem to work on Windows even though it's listed at - -- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160 - -- ...? Let's use the slightly racy approach then. - if ← lockFileName.pathExists then - throw <| IO.Error.alreadyExists none 0 "" - discard <| IO.FS.Handle.mk lockFileName IO.FS.Mode.write - catch - | IO.Error.alreadyExists .. => do - if firstTime then - IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockFileName}' if stuck)" - IO.sleep (ms := 300) - acquire (firstTime := false) - | e => throw e - -def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do - let entries ← pkg.readDir - match entries.filter (FilePath.extension ·.fileName == "lean") with - | #[rootFile] => pure <| FilePath.withExtension rootFile.fileName "" |>.toString - | #[] => throw <| IO.userError s!"no '.lean' file found in {← IO.FS.realPath "."}" - | _ => throw <| IO.userError s!"{← IO.FS.realPath "."} must contain a unique '.lean' file as the package root" - -structure Configuration extends Lean.LeanPaths := - moreDeps : List FilePath - -def configure : IO Configuration := do - let d ← readManifest - IO.eprintln $ "configuring " ++ d.name ++ " " ++ d.version - let assg ← solveDeps d - let paths ← constructPath assg - let mut moreDeps := [leanpkgTomlFn] - for path in paths do - unless path == FilePath.mk "." / "." do - -- build recursively - -- TODO: share build of common dependencies - execCmd { - cmd := (← IO.appPath).toString - cwd := path - args := #["build"] - } - moreDeps := (path / Build.buildPath / (← getRootPart path).toString |>.withExtension "olean") :: moreDeps - return { - oleanPath := paths.map (· / Build.buildPath) - srcPath := paths - moreDeps - } - -def execMake (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLockFile do - let manifest ← readManifest - let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ cfg.leanArgs - let mut spawnArgs := { - cmd := "sh" - cwd := manifest.effectivePath - args := #["-c", s!"\"{← IO.appDir}/leanmake\" PKG={cfg.pkg} LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{cfg.leanPath}\" {" ".intercalate makeArgs} MORE_DEPS+=\"{" ".intercalate (cfg.moreDeps.map toString)}\" >&2"] - } - execCmd spawnArgs - -def buildImports (imports : List String) (leanArgs : List String) : IO UInt32 := do - unless ← leanpkgTomlFn.pathExists do - return 2 - let manifest ← readManifest - let cfg ← configure - let imports := imports.map (·.toName) - let root ← getRootPart - let localImports := imports.filter (·.getRoot == root) - if localImports != [] then - let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.oleanPath.toString, moreDeps := cfg.moreDeps } - if ← FilePath.pathExists "Makefile" then - let oleans := localImports.map fun i => Lean.modToFilePath "build" i "olean" |>.toString - execMake oleans buildCfg - else - Build.buildModules buildCfg localImports - IO.println <| Lean.Json.compress <| Lean.toJson cfg.toLeanPaths - return 0 - -def build (makeArgs leanArgs : List String) : IO Unit := do - let cfg ← configure - let root ← getRootPart - let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.oleanPath.toString, moreDeps := cfg.moreDeps } - if makeArgs != [] || (← FilePath.pathExists "Makefile") then - execMake makeArgs buildCfg - else - Build.buildModules buildCfg [root] - -def initGitignoreContents := - "/build -" - -def initPkg (n : String) (fromNew : Bool) : IO Unit := do - IO.FS.writeFile leanpkgTomlFn s!"[package] -name = \"{n}\" -version = \"0.1\" -lean_version = \"{leanVersionString}\" -" - 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) - h.putStr initGitignoreContents - unless ← System.FilePath.isDir ⟨".git"⟩ do - (do - execCmd {cmd := "git", args := #["init", "-q"]} - unless upstreamGitBranch = "master" do - execCmd {cmd := "git", args := #["checkout", "-B", upstreamGitBranch]} - ) <|> IO.eprintln "WARNING: failed to initialize git repository" - -def init (n : String) := initPkg n false - -def usage := - "Lean package manager, version " ++ uiLeanVersionString ++ " - -Usage: leanpkg - -init create a Lean package in the current directory -configure download and build dependencies -build [] configure and build *.olean files - -See `leanpkg help ` for more information on a specific command." - -def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO UInt32 - | "init", [Name], [] => init Name *> pure 0 - | "configure", [], [] => configure *> pure 0 - | "print-paths", leanpkgArgs, leanArgs => buildImports leanpkgArgs leanArgs - | "build", makeArgs, leanArgs => build makeArgs leanArgs *> pure 0 - | "help", ["configure"], [] => IO.println "Download dependencies - -Usage: - leanpkg configure - -This command sets up the `build/deps` directory. - -For each (transitive) git dependency, the specified commit is checked out -into a sub-directory of `build/deps`. If there are dependencies on multiple -versions of the same package, the version materialized is undefined. No copy -is made of local dependencies." *> pure 0 - | "help", ["build"], [] => IO.println "download dependencies and build *.olean files - -Usage: - leanpkg build [] [-- ] - -This command invokes `leanpkg configure` followed by `leanmake LEAN_OPTS=`. -If defined, the `package.timeout` configuration value is passed to Lean via its `-T` parameter. -If no are given, only .olean files will be produced in `build/`. If `lib` or `bin` -is passed instead, the extracted C code is compiled with `c++` and a static library in `build/lib` -or an executable in `build/bin`, respectively, is created. `leanpkg build bin` requires a declaration -of name `main` in the root namespace, which must return `IO Unit` or `IO UInt32` (the exit code) and -may accept the program's command line arguments as a `List String` parameter. - -NOTE: building and linking dependent libraries currently has to be done manually, e.g. -``` -$ (cd a; leanpkg build lib) -$ (cd b; leanpkg build bin LINK_OPTS=../a/build/lib/libA.a) -```" *> pure 0 - | "help", ["init"], [] => IO.println "Create a new Lean package in the current directory - -Usage: - leanpkg init - -This command creates a new Lean package with the given name in the current -directory." *> pure 0 - | "help", _, [] => IO.println usage *> pure 0 - | _, _, _ => throw <| IO.userError usage - -private def splitCmdlineArgsCore : List String → List String × List String - | [] => ([], []) - | (arg::args) => if arg == "--" - then ([], args) - else - let (outerArgs, innerArgs) := splitCmdlineArgsCore args - (arg::outerArgs, innerArgs) - -def splitCmdlineArgs : List String → IO (String × List String × List String) -| [] => throw <| IO.userError usage -| [cmd] => return (cmd, [], []) -| (cmd::rest) => - let (outerArgs, innerArgs) := splitCmdlineArgsCore rest - return (cmd, outerArgs, innerArgs) - -end Leanpkg - -unsafe def main (args : List String) : IO UInt32 := do - try - Lean.enableInitializersExecution - Lean.initSearchPath (← Lean.getBuildDir) - let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args - IO.eprintln "warning: leanpkg has been deprecated in favor of Lake (https://github.com/leanprover/lake) and will be removed in the next release." - Leanpkg.main cmd outerArgs innerArgs - catch e => - IO.eprintln e -- avoid "uncaught exception: ..." - pure 1