From 47cd2ee61ac3a586f547215c5e93561672af2a64 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Apr 2018 12:43:17 -0700 Subject: [PATCH] chore(leanpkg): delete --- leanpkg/README.md | 3 - leanpkg/leanpkg.path | 2 - leanpkg/leanpkg.toml | 3 - leanpkg/leanpkg/git.lean | 36 ---- leanpkg/leanpkg/lean_version.lean | 28 --- leanpkg/leanpkg/main.lean | 315 ------------------------------ leanpkg/leanpkg/manifest.lean | 114 ----------- leanpkg/leanpkg/proc.lean | 27 --- leanpkg/leanpkg/resolve.lean | 106 ---------- leanpkg/leanpkg/toml.lean | 161 --------------- library/data/buffer/parser.lean | 221 --------------------- src/CMakeLists.txt | 12 +- 12 files changed, 6 insertions(+), 1022 deletions(-) delete mode 100644 leanpkg/README.md delete mode 100644 leanpkg/leanpkg.path delete mode 100644 leanpkg/leanpkg.toml delete mode 100644 leanpkg/leanpkg/git.lean delete mode 100644 leanpkg/leanpkg/lean_version.lean delete mode 100644 leanpkg/leanpkg/main.lean delete mode 100644 leanpkg/leanpkg/manifest.lean delete mode 100644 leanpkg/leanpkg/proc.lean delete mode 100644 leanpkg/leanpkg/resolve.lean delete mode 100644 leanpkg/leanpkg/toml.lean delete mode 100644 library/data/buffer/parser.lean diff --git a/leanpkg/README.md b/leanpkg/README.md deleted file mode 100644 index 2a0a0d31aa..0000000000 --- a/leanpkg/README.md +++ /dev/null @@ -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`. diff --git a/leanpkg/leanpkg.path b/leanpkg/leanpkg.path deleted file mode 100644 index 2301f1b12c..0000000000 --- a/leanpkg/leanpkg.path +++ /dev/null @@ -1,2 +0,0 @@ -builtin_path -path ./. diff --git a/leanpkg/leanpkg.toml b/leanpkg/leanpkg.toml deleted file mode 100644 index 66053b0be8..0000000000 --- a/leanpkg/leanpkg.toml +++ /dev/null @@ -1,3 +0,0 @@ -[package] -name = "leanpkg" -version = "0.1" diff --git a/leanpkg/leanpkg/git.lean b/leanpkg/leanpkg/git.lean deleted file mode 100644 index e530042ede..0000000000 --- a/leanpkg/leanpkg/git.lean +++ /dev/null @@ -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 diff --git a/leanpkg/leanpkg/lean_version.lean b/leanpkg/leanpkg/lean_version.lean deleted file mode 100644 index 8f91c205d9..0000000000 --- a/leanpkg/leanpkg/lean_version.lean +++ /dev/null @@ -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 diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean deleted file mode 100644 index 84d6fa1dc2..0000000000 --- a/leanpkg/leanpkg/main.lean +++ /dev/null @@ -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 - -configure download dependencies -build [-- ] download dependencies and build *.olean files -test [-- ] download dependencies, build *.olean files, and run test files - -new create a Lean package in a new directory -init create a Lean package in the current directory - -add add a dependency from a git repository (uses latest upstream revision) -add add a local dependency -upgrade upgrade all git dependencies to the latest upstream version - -install install a user-wide package from git -install install a user-wide package from a local directory - -dump print the parsed leanpkg.toml file (for debugging) - -See `leanpkg help ` 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 [-- ] - -This command invokes `leanpkg configure` followed by -`lean --make src `, 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 [-- ] - -This command invokes `leanpkg build ` followed by -`lean --make test `, 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 - leanpkg add - leanpkg add / - -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-` (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 /.../ - -This command creates a new Lean package named '' in a new directory -`/.../`. 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 - -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 - leanpkg install - leanpkg install / - -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 diff --git a/leanpkg/leanpkg/manifest.lean b/leanpkg/leanpkg/manifest.lean deleted file mode 100644 index a222ae0442..0000000000 --- a/leanpkg/leanpkg/manifest.lean +++ /dev/null @@ -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 diff --git a/leanpkg/leanpkg/proc.lean b/leanpkg/leanpkg/proc.lean deleted file mode 100644 index 921e71b2f6..0000000000 --- a/leanpkg/leanpkg/proc.lean +++ /dev/null @@ -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 diff --git a/leanpkg/leanpkg/resolve.lean b/leanpkg/leanpkg/resolve.lean deleted file mode 100644 index 9e88343532..0000000000 --- a/leanpkg/leanpkg/resolve.lean +++ /dev/null @@ -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 diff --git a/leanpkg/leanpkg/toml.lean b/leanpkg/leanpkg/toml.lean deleted file mode 100644 index 341183b714..0000000000 --- a/leanpkg/leanpkg/toml.lean +++ /dev/null @@ -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"])] - | _ := [" " ++ 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 "" $ -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 diff --git a/library/data/buffer/parser.lean b/library/data/buffer/parser.lean deleted file mode 100644 index dd5e5032cb..0000000000 --- a/library/data/buffer/parser.lean +++ /dev/null @@ -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 "" $ -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 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c7292c2870..0d3729851d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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"