chore(leanpkg): delete
This commit is contained in:
Leonardo de Moura
parent
41d1293b38
commit
47cd2ee61a
12 changed files with 6 additions and 1022 deletions
|
|
@ -1,3 +0,0 @@
|
|||
# leanpkg
|
||||
|
||||
`leanpkg` is the package manager for the [Lean theorem prover](https://leanprover.github.io). For more information, see [the reference](https://leanprover.github.io/reference/using_lean.html#using-the-package-manager) or `leanpkg help`.
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
builtin_path
|
||||
path ./.
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
[package]
|
||||
name = "leanpkg"
|
||||
version = "0.1"
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
import leanpkg.lean_version system.io
|
||||
|
||||
namespace leanpkg
|
||||
|
||||
def upstream_git_branch :=
|
||||
if lean.is_release then
|
||||
"lean-" ++ lean_version_string_core
|
||||
else
|
||||
"master"
|
||||
|
||||
def git_parse_revision (git_repo_dir : string) (rev : string) : io string := do
|
||||
rev ← io.cmd {cmd := "git", args := ["rev-parse", "-q", "--verify", rev], cwd := git_repo_dir},
|
||||
return rev.pop_back -- remove newline at end
|
||||
|
||||
def git_head_revision (git_repo_dir : string) : io string :=
|
||||
git_parse_revision git_repo_dir "HEAD"
|
||||
|
||||
def git_parse_origin_revision (git_repo_dir : string) (rev : string) : io string :=
|
||||
(git_parse_revision git_repo_dir $ "origin/" ++ rev) <|> git_parse_revision git_repo_dir rev
|
||||
<|> io.fail ("cannot find revision " ++ rev ++ " in repository " ++ git_repo_dir)
|
||||
|
||||
def git_latest_origin_revision (git_repo_dir : string) : io string := do
|
||||
io.cmd {cmd := "git", args := ["fetch"], cwd := git_repo_dir},
|
||||
git_parse_origin_revision git_repo_dir upstream_git_branch
|
||||
|
||||
def git_revision_exists (git_repo_dir : string) (rev : string) : io bool := do
|
||||
some _ ← optional (git_parse_revision git_repo_dir (rev ++ "^{commit}"))
|
||||
| pure ff,
|
||||
pure tt
|
||||
|
||||
end leanpkg
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
namespace leanpkg
|
||||
|
||||
def lean_version_string_core :=
|
||||
let (major, minor, patch) := lean.version in
|
||||
sformat!("{major}.{minor}.{patch}")
|
||||
|
||||
def lean_version_string :=
|
||||
if lean.is_release then
|
||||
lean_version_string_core
|
||||
else if lean.special_version_desc ≠ "" then
|
||||
lean.special_version_desc
|
||||
else
|
||||
"master"
|
||||
|
||||
def ui_lean_version_string :=
|
||||
if lean.is_release then
|
||||
lean_version_string_core
|
||||
else if lean.special_version_desc ≠ "" then
|
||||
lean.special_version_desc
|
||||
else
|
||||
"master (" ++ lean_version_string_core ++ ")"
|
||||
|
||||
end leanpkg
|
||||
|
|
@ -1,315 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
import leanpkg.resolve leanpkg.git
|
||||
|
||||
namespace leanpkg
|
||||
|
||||
def write_file (fn : string) (cnts : string) (mode := io.mode.write) : io unit := do
|
||||
h ← io.mk_file_handle fn io.mode.write,
|
||||
io.fs.write h cnts.to_char_buffer,
|
||||
io.fs.close h
|
||||
|
||||
def read_manifest : io manifest := do
|
||||
m ← manifest.from_file leanpkg_toml_fn,
|
||||
when (m.lean_version ≠ lean_version_string) $
|
||||
io.print_ln $ "\nWARNING: Lean version mismatch: installed version is " ++ lean_version_string
|
||||
++ ", but package requires " ++ m.lean_version ++ "\n",
|
||||
return m
|
||||
|
||||
def write_manifest (d : manifest) (fn := leanpkg_toml_fn) : io unit :=
|
||||
write_file fn (repr d)
|
||||
|
||||
-- TODO(gabriel): implement a cross-platform api
|
||||
def get_dot_lean_dir : io string := do
|
||||
some home ← io.env.get "HOME" | io.fail "environment variable HOME is not set",
|
||||
return $ home ++ "/.lean"
|
||||
|
||||
-- TODO(gabriel): file existence testing
|
||||
def exists_file (f : string) : io bool := do
|
||||
ch ← io.proc.spawn { cmd := "test", args := ["-f", f] },
|
||||
ev ← io.proc.wait ch,
|
||||
return $ ev = 0
|
||||
|
||||
def mk_path_file : ∀ (paths : list string), string
|
||||
| [] := "builtin_path\n"
|
||||
| (x :: xs) := mk_path_file xs ++ "path " ++ x ++ "\n"
|
||||
|
||||
def configure : io unit := do
|
||||
d ← read_manifest,
|
||||
io.put_str_ln $ "configuring " ++ d.name ++ " " ++ d.version,
|
||||
when (d.path ≠ some "src") $ io.put_str_ln "WARNING: leanpkg configurations not specifying `path = \"src\"` are deprecated.",
|
||||
assg ← solve_deps d,
|
||||
path_file_cnts ← mk_path_file <$> construct_path assg,
|
||||
write_file "leanpkg.path" path_file_cnts
|
||||
|
||||
def make (lean_args : list string) : io unit := do
|
||||
manifest ← read_manifest,
|
||||
exec_cmd {
|
||||
cmd := "lean",
|
||||
args := (match manifest.timeout with some t := ["-T", repr t] | none := [] end) ++
|
||||
["--make"] ++ manifest.effective_path ++ lean_args,
|
||||
env := [("LEAN_PATH", none)]
|
||||
}
|
||||
|
||||
def build (lean_args : list string) := configure >> make lean_args
|
||||
|
||||
def make_test (lean_args : list string) : io unit :=
|
||||
exec_cmd { cmd := "lean", args := ["--make", "test"] ++ lean_args, env := [("LEAN_PATH", none)] }
|
||||
|
||||
def test (lean_args : list string) := build lean_args >> make_test lean_args
|
||||
|
||||
def init_gitignore_contents :=
|
||||
"*.olean
|
||||
/_target
|
||||
/leanpkg.path
|
||||
"
|
||||
|
||||
def init_pkg (n : string) (from_new : bool) : io unit := do
|
||||
write_manifest { name := n, path := "src", version := "0.1" } leanpkg_toml_fn,
|
||||
src_ex ← dir_exists "src",
|
||||
when (¬src_ex) (do
|
||||
when ¬from_new $ io.put_str_ln "Move existing .lean files into the 'src' folder.",
|
||||
exec_cmd {cmd := "mkdir", args := ["src"]}),
|
||||
write_file ".gitignore" init_gitignore_contents io.mode.append,
|
||||
git_ex ← dir_exists ".git",
|
||||
when (¬git_ex) (do {
|
||||
exec_cmd {cmd := "git", args := ["init", "-q"]},
|
||||
when (upstream_git_branch ≠ "master") $
|
||||
exec_cmd {cmd := "git", args := ["checkout", "-b", upstream_git_branch]}
|
||||
} <|> io.print_ln "WARNING: failed to initialize git repository"),
|
||||
configure
|
||||
|
||||
def init (n : string) := init_pkg n false
|
||||
|
||||
-- TODO(gabriel): windows
|
||||
def basename (s : string) : string :=
|
||||
s.fold "" $ λ s c, if c = '/' then "" else s.str c
|
||||
|
||||
def add_dep_to_manifest (dep : dependency) : io unit := do
|
||||
d ← read_manifest,
|
||||
let d' := { d with dependencies := d.dependencies.filter (λ old_dep, old_dep.name ≠ dep.name) ++ [dep] },
|
||||
write_manifest d'
|
||||
|
||||
def strip_dot_git (url : string) : string :=
|
||||
if url.backn 4 = ".git" then url.popn_back 4 else url
|
||||
|
||||
def looks_like_git_url (dep : string) : bool :=
|
||||
':' ∈ dep.to_list
|
||||
|
||||
def parse_add_dep (dep : string) : io dependency :=
|
||||
if looks_like_git_url dep then
|
||||
pure { name := basename (strip_dot_git dep), src := source.git dep upstream_git_branch }
|
||||
else do
|
||||
ex ← dir_exists dep,
|
||||
if ex then
|
||||
pure { name := basename dep, src := source.path dep }
|
||||
else do
|
||||
[user, repo] ← pure $ dep.split (= '/')
|
||||
| io.fail sformat!"path '{dep}' does not exist",
|
||||
pure { name := repo, src := source.git sformat!"https://github.com/{user}/{repo}" upstream_git_branch }
|
||||
|
||||
def absolutize_dep (dep : dependency) : io dependency :=
|
||||
match dep.src with
|
||||
| source.path p := do
|
||||
cwd ← io.env.get_cwd,
|
||||
pure {src := source.path (resolve_dir p cwd), ..dep}
|
||||
| _ := pure dep
|
||||
end
|
||||
|
||||
def fixup_git_version (dir : string) : ∀ (src : source), io source
|
||||
| (source.git url _) := source.git url <$> git_head_revision dir
|
||||
| src := return src
|
||||
|
||||
def add (dep : dependency) : io unit := do
|
||||
(_, assg) ← (materialize "." dep).run assignment.empty,
|
||||
some downloaded_path ← return (assg.find dep.name),
|
||||
manif ← manifest.from_file (downloaded_path ++ "/" ++ leanpkg_toml_fn),
|
||||
src ← fixup_git_version downloaded_path dep.src,
|
||||
let dep := { dep with name := manif.name, src := src },
|
||||
add_dep_to_manifest dep,
|
||||
configure
|
||||
|
||||
def new (dir : string) := do
|
||||
ex ← dir_exists dir,
|
||||
when ex $ io.fail $ "directory already exists: " ++ dir,
|
||||
exec_cmd {cmd := "mkdir", args := ["-p", dir]},
|
||||
change_dir dir,
|
||||
init_pkg (basename dir) true
|
||||
|
||||
def upgrade_dep (assg : assignment) (d : dependency) : io dependency :=
|
||||
match d.src with
|
||||
| (source.git url rev) := (do
|
||||
some path ← return (assg.find d.name) | io.fail "unresolved dependency",
|
||||
new_rev ← git_latest_origin_revision path,
|
||||
return {d with src := source.git url new_rev})
|
||||
<|> return d
|
||||
| _ := return d
|
||||
end
|
||||
|
||||
def upgrade := do
|
||||
m ← read_manifest,
|
||||
assg ← solve_deps m,
|
||||
ds' ← m.dependencies.mmap (upgrade_dep assg),
|
||||
write_manifest {m with dependencies := ds'},
|
||||
configure
|
||||
|
||||
def usage :=
|
||||
"Lean package manager, version " ++ ui_lean_version_string ++ "
|
||||
|
||||
Usage: leanpkg <command>
|
||||
|
||||
configure download dependencies
|
||||
build [-- <lean-args>] download dependencies and build *.olean files
|
||||
test [-- <lean-args>] download dependencies, build *.olean files, and run test files
|
||||
|
||||
new <dir> create a Lean package in a new directory
|
||||
init <name> create a Lean package in the current directory
|
||||
|
||||
add <url> add a dependency from a git repository (uses latest upstream revision)
|
||||
add <dir> add a local dependency
|
||||
upgrade upgrade all git dependencies to the latest upstream version
|
||||
|
||||
install <url> install a user-wide package from git
|
||||
install <dir> install a user-wide package from a local directory
|
||||
|
||||
dump print the parsed leanpkg.toml file (for debugging)
|
||||
|
||||
See `leanpkg help <command>` for more information on a specific command."
|
||||
|
||||
def main : ∀ (cmd : string) (leanpkg_args lean_args : list string), io unit
|
||||
| "configure" [] [] := configure
|
||||
| "build" _ lean_args := build lean_args
|
||||
| "test" _ lean_args := test lean_args
|
||||
| "new" [dir] [] := new dir
|
||||
| "init" [name] [] := init name
|
||||
| "add" [dep] [] := parse_add_dep dep >>= add
|
||||
| "upgrade" [] [] := upgrade
|
||||
| "install" [dep] [] := do
|
||||
dep ← parse_add_dep dep,
|
||||
dep ← absolutize_dep dep,
|
||||
dot_lean_dir ← get_dot_lean_dir,
|
||||
exec_cmd {cmd := "mkdir", args := ["-p", dot_lean_dir]},
|
||||
let user_toml_fn := dot_lean_dir ++ "/" ++ leanpkg_toml_fn,
|
||||
ex ← exists_file user_toml_fn,
|
||||
when (¬ ex) $ write_manifest {
|
||||
name := "_user_local_packages",
|
||||
version := "1"
|
||||
} user_toml_fn,
|
||||
change_dir dot_lean_dir,
|
||||
add dep,
|
||||
build []
|
||||
| "dump" [] [] := read_manifest >>= io.print_ln ∘ repr
|
||||
| "help" ["configure"] [] := io.print_ln "Download dependencies
|
||||
|
||||
Usage:
|
||||
leanpkg configure
|
||||
|
||||
This command sets up the `_target/deps` directory and the `leanpkg.path` file.
|
||||
|
||||
For each (transitive) git dependency, the specified commit is checked out
|
||||
into a sub-directory of `_target/deps`. If there are dependencies on multiple
|
||||
versions of the same package, the version materialized is undefined.
|
||||
|
||||
The `leanpkg.path` file used to resolve Lean imports is populated with paths
|
||||
to the `src` directories of all (transitive) dependencies. No copy is made
|
||||
of local dependencies."
|
||||
| "help" ["build"] [] := io.print_ln "Download dependencies and build *.olean files
|
||||
|
||||
Usage:
|
||||
leanpkg build [-- <lean-args>]
|
||||
|
||||
This command invokes `leanpkg configure` followed by
|
||||
`lean --make src <lean-args>`, building the package's Lean files as well as
|
||||
(transitively) imported files of dependencies. If defined, the `package.timeout`
|
||||
configuration value is passed to Lean via its `-T` parameter."
|
||||
| "help" ["test"] [] := io.print_ln "Download dependencies, build *.olean files, and run test files
|
||||
|
||||
Usage:
|
||||
leanpkg test [-- <lean-args>]
|
||||
|
||||
This command invokes `leanpkg build <lean-args>` followed by
|
||||
`lean --make test <lean-args>`, executing the package's test files. A failed
|
||||
test should generate a Lean error message, which makes this command return a
|
||||
non-zero exit code."
|
||||
| "help" ["add"] [] := io.print_ln sformat!"Add a dependency
|
||||
|
||||
Usage:
|
||||
leanpkg add <local-path>
|
||||
leanpkg add <git-url>
|
||||
leanpkg add <github-user>/<github-repo>
|
||||
|
||||
Examples:
|
||||
leanpkg add ../mathlib
|
||||
leanpkg add https://github.com/leanprover/mathlib
|
||||
leanpkg add leanprover/mathlib
|
||||
|
||||
This command adds the specified local or git dependency, then calls
|
||||
`leanpkg configure`. For git dependencies, the pinned commit is
|
||||
the head of the branch `lean-<version>` (e.g. `lean-3.3.0`) on stable
|
||||
releases of Lean, or else `master` (current branch: {upstream_git_branch})."
|
||||
| "help" ["new"] [] := io.print_ln "Create a new Lean package in a new directory
|
||||
|
||||
Usage:
|
||||
leanpkg new <path>/.../<name>
|
||||
|
||||
This command creates a new Lean package named '<name>' in a new directory
|
||||
`<path>/.../<name>`. A new git repository is initialized to the branch name
|
||||
expected by `leanpkg add` (see `leanpkg help add`).
|
||||
|
||||
For converting an existing directory into a Lean package, use `leanpkg init`."
|
||||
| "help" ["init"] [] := io.print_ln "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. Existing Lean source files should be moved into the new `src`
|
||||
directory."
|
||||
| "help" ["upgrade"] [] := io.print_ln "Upgrade all git dependencies to the latest upstream version
|
||||
|
||||
Usage:
|
||||
leanpkg upgrade
|
||||
|
||||
This command fetches the remote repositories of all git dependencies and updates
|
||||
the pinned commits to the head of the respective branch (see
|
||||
`leanpkg help add`)."
|
||||
| "help" ["install"] [] := io.print_ln "Install a user-wide package
|
||||
|
||||
Usage:
|
||||
leanpkg install <local-path>
|
||||
leanpkg install <git-url>
|
||||
leanpkg install <github-user>/<github-repo>
|
||||
|
||||
This command adds a dependency to a user-wide \"meta\" package in `~/.lean`.
|
||||
For files not part of a Lean package, Lean falls back to the core library
|
||||
and this meta package for import resolution.
|
||||
|
||||
For removing or upgrading user-wide dependencies, you currently have to change
|
||||
into `~/.lean` yourself and edit the leanpkg.toml file or execute
|
||||
`leanpkg upgrade`, respectively."
|
||||
| "help" _ [] := io.print_ln usage
|
||||
| _ _ _ := io.fail usage
|
||||
|
||||
private def split_cmdline_args_core : list string → list string × list string
|
||||
| [] := ([], [])
|
||||
| (arg::args) := if arg = "--"
|
||||
then ([], args)
|
||||
else match split_cmdline_args_core args with
|
||||
| (outer_args, inner_args) := (arg::outer_args, inner_args)
|
||||
end
|
||||
|
||||
def split_cmdline_args : list string → io (string × list string × list string)
|
||||
| [] := io.fail usage
|
||||
| [cmd] := return (cmd, [], [])
|
||||
| (cmd::rest) := match split_cmdline_args_core rest with
|
||||
| (outer_args, inner_args) := return (cmd, outer_args, inner_args)
|
||||
end
|
||||
end leanpkg
|
||||
|
||||
|
||||
def main : io unit :=
|
||||
do (cmd, outer_args, inner_args) ← io.cmdline_args >>= leanpkg.split_cmdline_args,
|
||||
leanpkg.main cmd outer_args inner_args
|
||||
|
|
@ -1,114 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
import leanpkg.toml leanpkg.lean_version system.io
|
||||
|
||||
namespace leanpkg
|
||||
|
||||
inductive source
|
||||
| path (dir_name : string) : source
|
||||
| git (url rev : string) : source
|
||||
|
||||
namespace source
|
||||
|
||||
def from_toml (v : toml.value) : option source :=
|
||||
(do toml.value.str dir_name ← v.lookup "path" | none,
|
||||
return $ path dir_name) <|>
|
||||
(do toml.value.str url ← v.lookup "git" | none,
|
||||
toml.value.str rev ← v.lookup "rev" | none,
|
||||
return $ git url rev)
|
||||
|
||||
def to_toml : ∀ (s : source), toml.value
|
||||
| (path dir_name) := toml.value.table [("path", toml.value.str dir_name)]
|
||||
| (git url rev) :=
|
||||
toml.value.table [("git", toml.value.str url), ("rev", toml.value.str rev)]
|
||||
|
||||
/- TODO(Leo): has_to_string -/
|
||||
instance : has_repr source :=
|
||||
⟨λ s, repr s.to_toml⟩
|
||||
|
||||
end source
|
||||
|
||||
structure dependency :=
|
||||
(name : string) (src : source)
|
||||
|
||||
namespace dependency
|
||||
/- TODO(Leo): has_to_string -/
|
||||
instance : has_repr dependency :=
|
||||
⟨λ d, d.name ++ " = " ++ repr d.src⟩
|
||||
end dependency
|
||||
|
||||
structure manifest :=
|
||||
(name : string) (version : string)
|
||||
(lean_version : string := lean_version_string)
|
||||
(timeout : option nat := none)
|
||||
(path : option string := none)
|
||||
(dependencies : list dependency := [])
|
||||
|
||||
namespace manifest
|
||||
|
||||
def effective_path (m : manifest) : list string :=
|
||||
[match m.path with some p := p | none := "." end]
|
||||
|
||||
def from_toml (t : toml.value) : option manifest := do
|
||||
pkg ← t.lookup "package",
|
||||
toml.value.str n ← pkg.lookup "name" | none,
|
||||
toml.value.str ver ← pkg.lookup "version" | none,
|
||||
lean_ver ←
|
||||
match pkg.lookup "lean_version" with
|
||||
| some (toml.value.str lean_ver) := some lean_ver
|
||||
| none := some lean_version_string
|
||||
| _ := none
|
||||
end,
|
||||
tm ← match pkg.lookup "timeout" with
|
||||
| some (toml.value.nat timeout) := some (some timeout)
|
||||
| none := some none
|
||||
| _ := none
|
||||
end,
|
||||
path ← match pkg.lookup "path" with
|
||||
| some (toml.value.str path) := some (some path)
|
||||
| none := some none
|
||||
| _ := none
|
||||
end,
|
||||
toml.value.table deps ← t.lookup "dependencies" <|> some (toml.value.table []) | none,
|
||||
deps ← deps.mmap (λ ⟨n, src⟩, do src ← source.from_toml src,
|
||||
return $ dependency.mk n src),
|
||||
return { name := n, version := ver, lean_version := lean_ver,
|
||||
path := path, dependencies := deps, timeout := tm }
|
||||
|
||||
def to_toml (d : manifest) : toml.value :=
|
||||
let pkg := [("name", toml.value.str d.name), ("version", toml.value.str d.version),
|
||||
("lean_version", toml.value.str d.lean_version)],
|
||||
pkg := match d.path with some p := pkg ++ [("path", toml.value.str p)] | none := pkg end,
|
||||
pkg := match d.timeout with some t := pkg ++ [("timeout", toml.value.nat t)] | none := pkg end,
|
||||
deps := toml.value.table $ d.dependencies.map $ λ dep, (dep.name, dep.src.to_toml) in
|
||||
toml.value.table [("package", toml.value.table pkg), ("dependencies", deps)]
|
||||
|
||||
instance : has_repr manifest :=
|
||||
⟨λ d, repr d.to_toml⟩
|
||||
|
||||
def from_string (s : string) : option manifest :=
|
||||
match parser.run_string toml.File s with
|
||||
| sum.inr toml := from_toml toml
|
||||
| sum.inl _ := none
|
||||
end
|
||||
|
||||
def from_file (fn : string) : io manifest := do
|
||||
cnts ← io.fs.read_file fn,
|
||||
toml ←
|
||||
(match parser.run toml.File cnts with
|
||||
| sum.inl err :=
|
||||
io.fail $ "toml parse error in " ++ fn ++ "\n\n" ++ err
|
||||
| sum.inr res := return res
|
||||
end),
|
||||
some manifest ← return (from_toml toml)
|
||||
| io.fail ("cannot read manifest from " ++ fn ++ "\n\n" ++ repr toml),
|
||||
return manifest
|
||||
|
||||
end manifest
|
||||
|
||||
def leanpkg_toml_fn := "leanpkg.toml"
|
||||
|
||||
end leanpkg
|
||||
|
|
@ -1,27 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
import system.io leanpkg.toml
|
||||
open io io.proc
|
||||
|
||||
namespace leanpkg
|
||||
|
||||
def exec_cmd (args : io.process.spawn_args) : io unit := do
|
||||
let cmdstr := join " " (args.cmd :: args.args),
|
||||
io.put_str_ln $ "> " ++
|
||||
match args.cwd with
|
||||
| some cwd := cmdstr ++ " # in directory " ++ cwd
|
||||
| none := cmdstr
|
||||
end,
|
||||
ch ← spawn args,
|
||||
exitv ← wait ch,
|
||||
when (exitv ≠ 0) $ io.fail $
|
||||
"external command exited with status " ++ repr exitv
|
||||
|
||||
def change_dir (dir : string) : io unit := do
|
||||
io.put_str_ln sformat!"> cd {dir}",
|
||||
io.env.set_cwd dir
|
||||
|
||||
end leanpkg
|
||||
|
|
@ -1,106 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
import leanpkg.manifest system.io leanpkg.proc leanpkg.git
|
||||
|
||||
namespace leanpkg
|
||||
|
||||
def assignment := list (string × string)
|
||||
|
||||
namespace assignment
|
||||
def empty : assignment := []
|
||||
|
||||
def find : assignment → string → option string
|
||||
| [] s := none
|
||||
| ((k, v) :: kvs) s :=
|
||||
if k = s then some v else find kvs s
|
||||
|
||||
def contains (a : assignment) (s : string) : bool :=
|
||||
(a.find s).is_some
|
||||
|
||||
def insert (a : assignment) (k v : string) : assignment :=
|
||||
if a.contains k then a else (k, v) :: a
|
||||
|
||||
def fold {α} (i : α) (f : α → string → string → α) : assignment → α :=
|
||||
list.foldl (λ a ⟨k, v⟩, f a k v) i
|
||||
|
||||
end assignment
|
||||
|
||||
@[reducible] def solver := state_t assignment io
|
||||
instance {α : Type} : has_coe (io α) (solver α) := ⟨state_t.lift⟩
|
||||
|
||||
def not_yet_assigned (d : string) : solver bool := do
|
||||
assg ← get,
|
||||
return $ ¬ assg.contains d
|
||||
|
||||
def resolved_path (d : string) : solver string := do
|
||||
assg ← get,
|
||||
some path ← return (assg.find d) | io.fail "",
|
||||
return path
|
||||
|
||||
-- TODO(gabriel): directory existence testing
|
||||
def dir_exists (d : string) : io bool := do
|
||||
ch ← io.proc.spawn { cmd := "test", args := ["-d", d] },
|
||||
ev ← io.proc.wait ch,
|
||||
return $ ev = 0
|
||||
|
||||
-- TODO(gabriel): windows?
|
||||
def resolve_dir (abs_or_rel : string) (base : string) : string :=
|
||||
if abs_or_rel.front = '/' then
|
||||
abs_or_rel -- absolute
|
||||
else
|
||||
base ++ "/" ++ abs_or_rel
|
||||
|
||||
def materialize (relpath : string) (dep : dependency) : solver punit :=
|
||||
match dep.src with
|
||||
| (source.path dir) := do
|
||||
let depdir := resolve_dir dir relpath,
|
||||
io.put_str_ln $ dep.name ++ ": using local path " ++ depdir,
|
||||
modify $ λ assg, assg.insert dep.name depdir
|
||||
| (source.git url rev) := do
|
||||
let depdir := "_target/deps/" ++ dep.name,
|
||||
already_there ← dir_exists depdir,
|
||||
if already_there then do {
|
||||
io.put_str_ln $ dep.name ++ ": trying to update " ++ depdir ++ " to revision " ++ rev,
|
||||
hash ← git_parse_origin_revision depdir rev,
|
||||
rev_ex ← git_revision_exists depdir hash,
|
||||
when (¬rev_ex) $
|
||||
exec_cmd {cmd := "git", args := ["fetch"], cwd := depdir}
|
||||
} else do {
|
||||
io.put_str_ln $ dep.name ++ ": cloning " ++ url ++ " to " ++ depdir,
|
||||
exec_cmd {cmd := "mkdir", args := ["-p", depdir]},
|
||||
exec_cmd {cmd := "git", args := ["clone", url, depdir]}
|
||||
},
|
||||
hash ← git_parse_origin_revision depdir rev,
|
||||
exec_cmd {cmd := "git", args := ["checkout", "--detach", hash], cwd := depdir},
|
||||
modify $ λ assg, assg.insert dep.name depdir
|
||||
end
|
||||
|
||||
def solve_deps_core : ∀ (rel_path : string) (d : manifest) (max_depth : ℕ), solver unit
|
||||
| _ _ 0 := io.fail "maximum dependency resolution depth reached"
|
||||
| relpath d (max_depth + 1) := do
|
||||
deps ← monad.filter (not_yet_assigned ∘ dependency.name) d.dependencies,
|
||||
deps.mmap' (materialize relpath),
|
||||
deps.mmap' $ λ dep, do
|
||||
p ← resolved_path dep.name,
|
||||
d' ← manifest.from_file $ p ++ "/" ++ "leanpkg.toml",
|
||||
when (d'.name ≠ dep.name) $
|
||||
io.fail $ d.name ++ " (in " ++ relpath ++ ") depends on " ++ d'.name ++
|
||||
", but resolved dependency has name " ++ dep.name ++ " (in " ++ p ++ ")",
|
||||
solve_deps_core p d' max_depth
|
||||
|
||||
def solve_deps (d : manifest) : io assignment := do
|
||||
(_, assg) ← (solve_deps_core "." d 1024).run $ assignment.empty.insert d.name ".",
|
||||
return assg
|
||||
|
||||
def construct_path_core (depname : string) (dirname : string) : io (list string) :=
|
||||
list.map (λ relpath, dirname ++ "/" ++ relpath) <$>
|
||||
manifest.effective_path <$> (manifest.from_file $ dirname ++ "/" ++ leanpkg_toml_fn)
|
||||
|
||||
def construct_path (assg : assignment) : io (list string) := do
|
||||
let assg := assg.fold [] (λ xs depname dirname, (depname, dirname) :: xs),
|
||||
list.join <$> (assg.mmap $ λ ⟨depname, dirname⟩, construct_path_core depname dirname)
|
||||
|
||||
end leanpkg
|
||||
|
|
@ -1,161 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Gabriel Ebner
|
||||
-/
|
||||
import data.buffer.parser
|
||||
|
||||
-- I'd like to contribute a new naming convention:
|
||||
-- CamelCase for non-terminals.
|
||||
|
||||
def join (sep : string) : list string → string
|
||||
| [x] := x
|
||||
| [] := ""
|
||||
| (x::xs) := x ++ sep ++ join xs
|
||||
|
||||
namespace toml
|
||||
|
||||
inductive value : Type
|
||||
| str : string → value
|
||||
| nat : ℕ → value
|
||||
| bool : bool → value
|
||||
| table : list (string × value) → value
|
||||
|
||||
namespace value
|
||||
|
||||
private def escapec : char → string
|
||||
| '\"' := "\\\""
|
||||
| '\t' := "\\t"
|
||||
| '\n' := "\\n"
|
||||
| '\\' := "\\\\"
|
||||
| c := string.singleton c
|
||||
|
||||
private def escape (s : string) : string :=
|
||||
s.fold "" (λ s c, s ++ escapec c)
|
||||
|
||||
/- TODO(Leo): has_to_string -/
|
||||
private mutual def repr_core, repr_pairs
|
||||
with repr_core : value → string
|
||||
| (value.str s) := "\"" ++ escape s ++ "\""
|
||||
| (value.nat n) := repr n
|
||||
| (value.bool tt) := "true"
|
||||
| (value.bool ff) := "false"
|
||||
| (value.table cs) := "{" ++ repr_pairs cs ++ "}"
|
||||
with repr_pairs : list (string × value) → string
|
||||
| [] := ""
|
||||
| [(k, v)] := k ++ " = " ++ repr_core v
|
||||
| ((k, v)::kvs) := k ++ " = " ++ repr_core v ++ ", " ++ repr_pairs kvs
|
||||
|
||||
protected def repr : ∀ (v : value), string
|
||||
| (table cs) := join "\n" $ do (h, c) ← cs,
|
||||
match c with
|
||||
| table ds :=
|
||||
["[" ++ h ++ "]\n" ++
|
||||
join "" (do (k, v) ← ds,
|
||||
[k ++ " = " ++ repr_core v ++ "\n"])]
|
||||
| _ := ["<error> " ++ repr_core c]
|
||||
end
|
||||
| v := repr_core v
|
||||
|
||||
/- TODO(Leo): has_to_string -/
|
||||
instance : has_repr value :=
|
||||
⟨value.repr⟩
|
||||
|
||||
def lookup : value → string → option value
|
||||
| (value.table cs) k :=
|
||||
match cs.filter (λ c : string × value, c.fst = k) with
|
||||
| [] := none
|
||||
| (k,v) ::_ := some v
|
||||
end
|
||||
| _ _ := none
|
||||
|
||||
end value
|
||||
|
||||
open parser
|
||||
|
||||
def Comment : parser unit :=
|
||||
ch '#' >> many' (sat (≠ '#')) >> optional (ch '\n') >> eps
|
||||
|
||||
def Ws : parser unit :=
|
||||
decorate_error "<whitespace>" $
|
||||
many' $ one_of' " \t\x0d\n".to_list <|> Comment
|
||||
|
||||
def tok (s : string) := str s >> Ws
|
||||
|
||||
def StringChar : parser char :=
|
||||
sat (λc, c ≠ '\"' ∧ c ≠ '\\' ∧ c.val > 0x1f)
|
||||
<|> (do str "\\",
|
||||
(str "t" >> return '\t') <|>
|
||||
(str "n" >> return '\n') <|>
|
||||
(str "\\" >> return '\\') <|>
|
||||
(str "\"" >> return '\"'))
|
||||
|
||||
def BasicString : parser string :=
|
||||
str "\"" *> (many_char StringChar) <* str "\"" <* Ws
|
||||
|
||||
def String := BasicString
|
||||
|
||||
def Nat : parser nat :=
|
||||
do s ← many_char1 (one_of "0123456789".to_list),
|
||||
Ws,
|
||||
return s.to_nat
|
||||
|
||||
def Boolean : parser bool :=
|
||||
(tok "true" >> return tt) <|>
|
||||
(tok "false" >> return ff)
|
||||
|
||||
def BareKey : parser string := do
|
||||
cs ← many_char1 $ sat $ λ c, c.is_alpha ∨ c.is_digit ∨ c = '_' ∨ c = '-',
|
||||
Ws,
|
||||
return cs
|
||||
|
||||
def Key := BareKey <|> BasicString
|
||||
|
||||
section
|
||||
parameter Val : parser value
|
||||
|
||||
def KeyVal : parser (string × value) := do
|
||||
k ← Key, tok "=", v ← Val,
|
||||
return (k, v)
|
||||
|
||||
def StdTable : parser (string × value) := do
|
||||
tok "[", n ← Key, tok "]",
|
||||
cs ← many KeyVal,
|
||||
return (n, value.table cs)
|
||||
|
||||
def Table : parser (string × value) := StdTable
|
||||
|
||||
def StrVal : parser value :=
|
||||
value.str <$> String
|
||||
|
||||
def NatVal : parser value :=
|
||||
value.nat <$> Nat
|
||||
|
||||
def BoolVal : parser value :=
|
||||
value.bool <$> Boolean
|
||||
|
||||
def InlineTable : parser value :=
|
||||
tok "{" *> (value.table <$> sep_by (tok ",") KeyVal) <* tok "}"
|
||||
|
||||
end
|
||||
|
||||
def Val : parser value :=
|
||||
fix $ λ Val, StrVal <|> NatVal <|> BoolVal <|> InlineTable Val
|
||||
|
||||
def Expression := Table Val
|
||||
|
||||
def File : parser value :=
|
||||
Ws *> (value.table <$> many Expression)
|
||||
|
||||
/-
|
||||
#eval run_string File $
|
||||
"[package]\n" ++
|
||||
"name = \"sss\"\n" ++
|
||||
"version = \"0.1\"\n" ++
|
||||
"timeout = 10\n" ++
|
||||
"\n" ++
|
||||
"[dependencies]\n" ++
|
||||
"library_dev = { git = \"https://github.com/leanprover/library_dev\", rev = \"master\" }"
|
||||
-/
|
||||
|
||||
end toml
|
||||
|
|
@ -1,221 +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
|
||||
-/
|
||||
import data.buffer data.dlist
|
||||
|
||||
inductive parse_result (α : Type)
|
||||
| done (pos : ℕ) (result : α) : parse_result
|
||||
| fail (pos : ℕ) (expected : dlist string) : parse_result
|
||||
|
||||
def parser (α : Type) :=
|
||||
∀ (input : char_buffer) (start : ℕ), parse_result α
|
||||
|
||||
namespace parser
|
||||
variables {α β γ : Type}
|
||||
|
||||
protected def bind (p : parser α) (f : α → parser β) : parser β :=
|
||||
λ input pos, match p input pos with
|
||||
| parse_result.done pos a := f a input pos
|
||||
| parse_result.fail ._ pos expected := parse_result.fail β pos expected
|
||||
end
|
||||
|
||||
protected def pure (a : α) : parser α :=
|
||||
λ input pos, parse_result.done pos a
|
||||
|
||||
private lemma parser.id_map (p : parser α) : parser.bind p parser.pure = p :=
|
||||
begin
|
||||
apply funext, intro input,
|
||||
apply funext, intro pos,
|
||||
dunfold parser.bind,
|
||||
cases (p input pos); exact rfl
|
||||
end
|
||||
|
||||
private lemma parser.bind_assoc (p : parser α) (q : α → parser β) (r : β → parser γ) :
|
||||
parser.bind (parser.bind p q) r = parser.bind p (λ a, parser.bind (q a) r) :=
|
||||
begin
|
||||
apply funext, intro input,
|
||||
apply funext, intro pos,
|
||||
dunfold parser.bind,
|
||||
cases (p input pos); try {dunfold bind},
|
||||
cases (q result input pos_1); try {dunfold bind},
|
||||
all_goals {refl}
|
||||
end
|
||||
|
||||
protected def fail (msg : string) : parser α :=
|
||||
λ _ pos, parse_result.fail α pos (dlist.singleton msg)
|
||||
|
||||
instance : monad parser :=
|
||||
{ pure := @parser.pure, bind := @parser.bind }
|
||||
|
||||
instance : is_lawful_monad parser :=
|
||||
{ id_map := @parser.id_map,
|
||||
pure_bind := λ _ _ _ _, rfl,
|
||||
bind_assoc := @parser.bind_assoc }
|
||||
|
||||
instance : monad_fail parser :=
|
||||
{ fail := @parser.fail, ..parser.monad }
|
||||
|
||||
protected def failure : parser α :=
|
||||
λ _ pos, parse_result.fail α pos dlist.empty
|
||||
|
||||
protected def orelse (p q : parser α) : parser α :=
|
||||
λ input pos, match p input pos with
|
||||
| parse_result.fail ._ pos₁ expected₁ :=
|
||||
if pos₁ ≠ pos then parse_result.fail _ pos₁ expected₁ else
|
||||
match q input pos with
|
||||
| parse_result.fail ._ pos₂ expected₂ :=
|
||||
if pos₁ < pos₂ then
|
||||
parse_result.fail _ pos₁ expected₁
|
||||
else if pos₂ < pos₁ then
|
||||
parse_result.fail _ pos₂ expected₂
|
||||
else -- pos₁ = pos₂
|
||||
parse_result.fail _ pos₁ (expected₁ ++ expected₂)
|
||||
| ok := ok
|
||||
end
|
||||
| ok := ok
|
||||
end
|
||||
|
||||
instance : alternative parser :=
|
||||
{ failure := @parser.failure,
|
||||
orelse := @parser.orelse }
|
||||
|
||||
instance : inhabited (parser α) :=
|
||||
⟨parser.failure⟩
|
||||
|
||||
/-- Overrides the expected token name, and does not consume input on failure. -/
|
||||
def decorate_errors (msgs : thunk (list string)) (p : parser α) : parser α :=
|
||||
λ input pos, match p input pos with
|
||||
| parse_result.fail ._ _ expected :=
|
||||
parse_result.fail _ pos (dlist.lazy_of_list (msgs ()))
|
||||
| ok := ok
|
||||
end
|
||||
|
||||
/-- Overrides the expected token name, and does not consume input on failure. -/
|
||||
def decorate_error (msg : thunk string) (p : parser α) : parser α :=
|
||||
decorate_errors [msg ()] p
|
||||
|
||||
/-- Matches a single character satisfying the given predicate. -/
|
||||
def sat (p : char → Prop) [decidable_pred p] : parser char :=
|
||||
λ input pos,
|
||||
if h : pos < input.size then
|
||||
let c := input.read ⟨pos, h⟩ in
|
||||
if p c then
|
||||
parse_result.done (pos+1) $ input.read ⟨pos, h⟩
|
||||
else
|
||||
parse_result.fail _ pos dlist.empty
|
||||
else
|
||||
parse_result.fail _ pos dlist.empty
|
||||
|
||||
/-- Matches the empty word. -/
|
||||
def eps : parser unit := return ()
|
||||
|
||||
/-- Matches the given character. -/
|
||||
def ch (c : char) : parser unit :=
|
||||
decorate_error c.to_string $ sat (= c) >> eps
|
||||
|
||||
/-- Matches a whole char_buffer. Does not consume input in case of failure. -/
|
||||
def char_buf (s : char_buffer) : parser unit :=
|
||||
decorate_error s.to_string $ s.to_list.mmap' ch
|
||||
|
||||
/-- Matches one out of a list of characters. -/
|
||||
def one_of (cs : list char) : parser char :=
|
||||
decorate_errors (do c ← cs, return c.to_string) $
|
||||
sat (∈ cs)
|
||||
|
||||
def one_of' (cs : list char) : parser unit :=
|
||||
one_of cs >> eps
|
||||
|
||||
/-- Matches a string. Does not consume input in case of failure. -/
|
||||
def str (s : string) : parser unit :=
|
||||
decorate_error s $ s.to_list.mmap' ch
|
||||
|
||||
/-- Number of remaining input characters. -/
|
||||
def remaining : parser ℕ :=
|
||||
λ input pos, parse_result.done pos (input.size - pos)
|
||||
|
||||
/-- Matches the end of the input. -/
|
||||
def eof : parser unit :=
|
||||
decorate_error "<end-of-file>" $
|
||||
do rem ← remaining, guard $ rem = 0
|
||||
|
||||
def foldr_core (f : α → β → β) (p : parser α) (b : β) : ∀ (reps : ℕ), parser β
|
||||
| 0 := failure
|
||||
| (reps+1) := (do x ← p, xs ← foldr_core reps, return (f x xs)) <|> return b
|
||||
|
||||
/-- Matches zero or more occurrences of `p`, and folds the result. -/
|
||||
def foldr (f : α → β → β) (p : parser α) (b : β) : parser β :=
|
||||
λ input pos, foldr_core f p b (input.size - pos + 1) input pos
|
||||
|
||||
def foldl_core (f : α → β → α) : ∀ (a : α) (p : parser β) (reps : ℕ), parser α
|
||||
| a p 0 := failure
|
||||
| a p (reps+1) := (do x ← p, foldl_core (f a x) p reps) <|> return a
|
||||
|
||||
/-- Matches zero or more occurrences of `p`, and folds the result. -/
|
||||
def foldl (f : α → β → α) (a : α) (p : parser β) : parser α :=
|
||||
λ input pos, foldl_core f a p (input.size - pos + 1) input pos
|
||||
|
||||
/-- Matches zero or more occurrences of `p`. -/
|
||||
def many (p : parser α) : parser (list α) :=
|
||||
foldr list.cons p []
|
||||
|
||||
def many_char (p : parser char) : parser string :=
|
||||
list.as_string <$> many p
|
||||
|
||||
/-- Matches zero or more occurrences of `p`. -/
|
||||
def many' (p : parser α) : parser unit :=
|
||||
many p >> eps
|
||||
|
||||
/-- Matches one or more occurrences of `p`. -/
|
||||
def many1 (p : parser α) : parser (list α) :=
|
||||
list.cons <$> p <*> many p
|
||||
|
||||
def many_char1 (p : parser char) : parser string :=
|
||||
list.as_string <$> many1 p
|
||||
|
||||
/-- Matches one or more occurrences of `p`, separated by `sep`. -/
|
||||
def sep_by1 (sep : parser unit) (p : parser α) : parser (list α) :=
|
||||
list.cons <$> p <*> many (sep >> p)
|
||||
|
||||
/-- Matches zero or more occurrences of `p`, separated by `sep`. -/
|
||||
def sep_by (sep : parser unit) (p : parser α) : parser (list α) :=
|
||||
sep_by1 sep p <|> return []
|
||||
|
||||
def fix_core (F : parser α → parser α) : ∀ (max_depth : ℕ), parser α
|
||||
| 0 := failure
|
||||
| (max_depth+1) := F (fix_core max_depth)
|
||||
|
||||
/-- Fixpoint combinator satisfying `fix F = F (fix F)`. -/
|
||||
def fix (F : parser α → parser α) : parser α :=
|
||||
λ input pos, fix_core F (input.size - pos + 1) input pos
|
||||
|
||||
private def make_monospaced : char → char
|
||||
| '\n' := ' '
|
||||
| '\t' := ' '
|
||||
| '\x0d' := ' '
|
||||
| c := c
|
||||
|
||||
def mk_error_msg (input : char_buffer) (pos : ℕ) (expected : dlist string) : char_buffer :=
|
||||
let left_ctx := (input.take pos).take_right 10,
|
||||
right_ctx := (input.drop pos).take 10 in
|
||||
left_ctx.map make_monospaced ++ right_ctx.map make_monospaced ++ "\n".to_char_buffer ++
|
||||
left_ctx.map (λ _, ' ') ++ "^\n".to_char_buffer ++
|
||||
"\n".to_char_buffer ++
|
||||
"expected: ".to_char_buffer
|
||||
++ string.to_char_buffer (" | ".intercalate expected.to_list)
|
||||
++ "\n".to_char_buffer
|
||||
|
||||
/-- Runs a parser on the given input. The parser needs to match the complete input. -/
|
||||
def run (p : parser α) (input : char_buffer) : sum string α :=
|
||||
match (p <* eof) input 0 with
|
||||
| parse_result.done pos res := sum.inr res
|
||||
| parse_result.fail ._ pos expected :=
|
||||
sum.inl $ buffer.to_string $ mk_error_msg input pos expected
|
||||
end
|
||||
|
||||
/-- Runs a parser on the given input. The parser needs to match the complete input. -/
|
||||
def run_string (p : parser α) (input : string) : sum string α :=
|
||||
run p input.to_char_buffer
|
||||
|
||||
end parser
|
||||
|
|
@ -488,12 +488,12 @@ add_custom_target(
|
|||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
|
||||
)
|
||||
|
||||
add_custom_target(
|
||||
leanpkg ALL
|
||||
COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}
|
||||
DEPENDS standard_lib
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg"
|
||||
)
|
||||
# add_custom_target(
|
||||
# leanpkg ALL
|
||||
# COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}
|
||||
# DEPENDS standard_lib
|
||||
# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg"
|
||||
# )
|
||||
|
||||
add_custom_target(clean-std-lib
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue