chore: remove orphan file
This commit is contained in:
Sebastian Ullrich
parent
0a2d0bc3fd
commit
a3c73f5df8
1 changed files with 0 additions and 228 deletions
228
src/Leanpkg.lean
228
src/Leanpkg.lean
|
|
@ -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 <command>
|
||||
|
||||
init <name> create a Lean package in the current directory
|
||||
configure download and build dependencies
|
||||
build [<args>] configure and build *.olean files
|
||||
|
||||
See `leanpkg help <command>` 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 [<leanmake-args>] [-- <lean-args>]
|
||||
|
||||
This command invokes `leanpkg configure` followed by `leanmake <leanmake-args> LEAN_OPTS=<lean-args>`.
|
||||
If defined, the `package.timeout` configuration value is passed to Lean via its `-T` parameter.
|
||||
If no <lean-args> 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 <name>
|
||||
|
||||
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
|
||||
Loading…
Add table
Reference in a new issue