From 9e237f8a1224fa9f6f92f3f714bbfc6481747181 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 29 Dec 2020 15:13:14 +0100 Subject: [PATCH] feat: basic port of `leanpkg` --- nix/bootstrap.nix | 16 +++-- nix/buildLeanPackage.nix | 4 ++ nix/packages.nix | 2 +- src/Leanpkg.lean | 135 +++++++++++++++++++++++++++++++++++ src/Leanpkg/.gitignore | 1 + src/Leanpkg/Git.lean | 41 +++++++++++ src/Leanpkg/LeanVersion.lean | 27 +++++++ src/Leanpkg/Manifest.lean | 85 ++++++++++++++++++++++ src/Leanpkg/Proc.lean | 20 ++++++ src/Leanpkg/Resolve.lean | 91 +++++++++++++++++++++++ src/Leanpkg/Toml.lean | 72 +++++++++++++++++++ src/lean.mk.in | 2 +- src/shell/CMakeLists.txt | 4 ++ src/stdlib.make.in | 2 + tests/leanpkg/a/.gitignore | 1 + tests/leanpkg/a/A.lean | 1 + tests/leanpkg/a/leanpkg.toml | 3 + tests/leanpkg/b/.gitignore | 1 + tests/leanpkg/b/B.lean | 4 ++ tests/leanpkg/b/leanpkg.toml | 6 ++ 20 files changed, 512 insertions(+), 6 deletions(-) create mode 100644 src/Leanpkg.lean create mode 100644 src/Leanpkg/.gitignore create mode 100644 src/Leanpkg/Git.lean create mode 100644 src/Leanpkg/LeanVersion.lean create mode 100644 src/Leanpkg/Manifest.lean create mode 100644 src/Leanpkg/Proc.lean create mode 100644 src/Leanpkg/Resolve.lean create mode 100644 src/Leanpkg/Toml.lean create mode 100644 tests/leanpkg/a/.gitignore create mode 100644 tests/leanpkg/a/A.lean create mode 100644 tests/leanpkg/a/leanpkg.toml create mode 100644 tests/leanpkg/b/.gitignore create mode 100644 tests/leanpkg/b/B.lean create mode 100644 tests/leanpkg/b/leanpkg.toml diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 99893ee99e..81f4c1aa9f 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -1,5 +1,5 @@ { debug ? false, extraCMakeFlags ? [], - stdenv, lib, cmake, gmp, buildLeanPackage, writeShellScriptBin, runCommand, + stdenv, lib, cmake, gmp, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, ... } @ args: rec { inherit stdenv; @@ -17,7 +17,7 @@ rec { } // args // { src = args.realSrc or (lib.sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]); }); - leanc = buildCMake { + leanc-unwrapped = buildCMake { name = "leanc"; src = ../src; dontBuild = true; @@ -61,6 +61,7 @@ rec { desc = "stage${toString stage}"; build = args: buildLeanPackage.override { lean = prevStage; + leanc = leanc-unwrapped; # use same stage for retrieving dependencies lean-leanDeps = stage0; lean-final = self; @@ -72,18 +73,25 @@ rec { Init = build { name = "Init"; src = ../src; deps = []; }; Std = build { name = "Std"; src = ../src; deps = [ Init ]; }; Lean = build { name = "Lean"; src = ../src; deps = [ Init Std ]; }; + Leanpkg = build { name = "Leanpkg"; src = ../src; deps = [ Init Std Lean ]; }; inherit (Lean) emacs-dev emacs-package; mods = Init.mods // Std.mods // Lean.mods; + leanc = writeShellScriptBin "leanc" '' + ${leanc-unwrapped}/bin/leanc -L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean "$@" + ''; lean = wrapStage(stdenv.mkDerivation { name = "lean-${desc}"; buildCommand = '' mkdir -p $out/bin $out/lib/lean - ln -sf ${leancpp}/lib/lean/* ${Init.staticLib}/* ${Init.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* $out/lib/lean/ - ${leanc}/bin/leanc -x none -rdynamic -L${gmp}/lib -L$out/lib/lean -L${leancpp}/lib/lean -o $out/bin/lean + ln -sf ${leancpp}/lib/lean/* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/ + ${leanc}/bin/leanc -x none -rdynamic -o $out/bin/lean + ${leanc}/bin/leanc -x none -rdynamic ${Leanpkg.staticLib}/* -o $out/bin/leanpkg ln -s ${leanc}/bin/leanc $out/bin/ ln -s ${leanc}/include $out/ ''; }); + leanpkg = Leanpkg.executable "leanpkg"; + # lean = symlinkJoin { name = "lean"; paths = [ leanWithoutLeanpkg leanpkg ]; }; test = buildCMake { name = "lean-test-${desc}"; realSrc = lib.sourceByRegex ../. [ "src.*" "tests.*" ]; diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index 4769817ba2..a251d1dd3d 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -126,6 +126,10 @@ in rec { mkdir $out ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))} ''; + executable = name: runCommand name {} '' + mkdir -p $out/bin + ${leanc}/bin/leanc -x none -L${staticLib} -o $out/bin/${name} + ''; lean-package = writeShellScriptBin "lean" '' LEAN_PATH=${modRoot}:$LEAN_PATH ${lean-final}/bin/lean $@ diff --git a/nix/packages.nix b/nix/packages.nix index b9f42bb224..acef9bdab5 100644 --- a/nix/packages.nix +++ b/nix/packages.nix @@ -81,7 +81,7 @@ let in { inherit cc lean4-mode buildLeanPackage llvmPackages; lean = lean.stage1; - stage0check-mod = (lean.stage1.Lean.overrideArgs { lean-final = lean.stage0; }).check-mod; + stage0check-mod = (lean.stage1.Leanpkg.overrideArgs { lean-final = lean.stage0; }).check-mod; HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcCheckTarget = "$root#stage0-from-input.stage0check-mod"; srcCheckArgs = "(--override-input lean-stage0 $root\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; }); HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcCheckTarget = "$root\?rev=$(git rev-parse HEAD)#stage0check-mod"; }); temci = (import temci {}).override { doCheck = false; }; diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean new file mode 100644 index 0000000000..e13d51a879 --- /dev/null +++ b/src/Leanpkg.lean @@ -0,0 +1,135 @@ +/- +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 + +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 : String) : IO Unit := do + IO.FS.writeFile fn manifest.reprint.get! + +def configure : IO String := do + let d ← readManifest + IO.eprintln $ "configuring " ++ d.name ++ " " ++ d.version + let assg ← solveDeps d + let paths ← constructPath assg + for path in paths do + unless path == "./." do + -- TODO: share build of common dependencies + execCmd { + cmd := "leanpkg" + cwd := path + args := #["build"] + } + System.FilePath.searchPathSeparator.toString.intercalate <| paths.map (· ++ "/build") + +def build (leanArgs : List String) : IO Unit := do + let manifest ← readManifest + let path ← configure + let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ leanArgs + execCmd { + cmd := "leanmake" + cwd := manifest.effectivePath + args := #[s!"LEAN_OPTS={" ".intercalate leanArgs}", s!"LEAN_PATH={path}"] + } + +def initGitignoreContents := + "/build +" + +def initPkg (n : String) (fromNew : Bool) : IO Unit := do + IO.FS.writeFile leanpkgTomlFn s!"[package] +name = \"{n}\" +version = \"0.1\" +" + 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 + let gitEx ← IO.isDir ".git" + unless gitEx do + (do + execCmd {cmd := "git", args := #["init", "-q"]} + unless upstreamGitBranch = "master" do + execCmd {cmd := "git", args := #["checkout", "-B", upstreamGitBranch]} + ) <|> IO.println "WARNING: failed to initialize git repository" + +def init (n : String) := initPkg n false + +def usage := + "Lean package manager, version " ++ uiLeanVersionString ++ " + +Usage: leanpkg + +configure download dependencies +build [-- ] download dependencies and build *.olean files +init create a Lean package in the current directory + +See `leanpkg help ` for more information on a specific command." + +def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit + | "configure", [], [] => discard <| configure + | "build", _, leanArgs => build leanArgs + | "init", [Name], [] => init Name + | "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." + | "help", ["build"], [] => IO.println "download dependencies and build *.olean files + +Usage: + leanpkg build [-- ] + +This command invokes `Leanpkg configure` followed by +`Leanmake `, 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", ["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." + | "help", _, [] => IO.println usage + | _, _, _ => 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 + +def main (args : List String) : IO Unit := do + Lean.initSearchPath none -- HACK + let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args + Leanpkg.main cmd outerArgs innerArgs diff --git a/src/Leanpkg/.gitignore b/src/Leanpkg/.gitignore new file mode 100644 index 0000000000..b62f4dcf77 --- /dev/null +++ b/src/Leanpkg/.gitignore @@ -0,0 +1 @@ +/leanpkg/config_vars.lean diff --git a/src/Leanpkg/Git.lean b/src/Leanpkg/Git.lean new file mode 100644 index 0000000000..1203abb875 --- /dev/null +++ b/src/Leanpkg/Git.lean @@ -0,0 +1,41 @@ +/- +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.LeanVersion + +namespace Leanpkg + +def upstreamGitBranch := + if Lean.version.isRelease then + "Lean-" ++ leanVersionStringCore + else + "master" + +def gitdefaultRevision : Option String → String + | none => upstreamGitBranch + | some branch => branch + +def gitParseRevision (gitRepoDir : String) (rev : String) : IO String := do + let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepoDir} + rev.trim -- remove newline at end + +def gitHeadRevision (gitRepoDir : String) : IO String := + gitParseRevision gitRepoDir "HEAD" + +def gitParseOriginRevision (gitRepoDir : String) (rev : String) : IO String := + (gitParseRevision gitRepoDir $ "origin/" ++ rev) <|> gitParseRevision gitRepoDir rev + <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepoDir}") + +def gitLatestOriginRevision (gitRepoDir : String) (branch : Option String) : IO String := do + discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepoDir} + gitParseOriginRevision gitRepoDir (gitdefaultRevision branch) + +def gitRevisionExists (gitRepoDir : String) (rev : String) : IO Bool := do + try + discard <| gitParseRevision gitRepoDir (rev ++ "^{commit}") + true + catch _ => false + +end Leanpkg diff --git a/src/Leanpkg/LeanVersion.lean b/src/Leanpkg/LeanVersion.lean new file mode 100644 index 0000000000..6622486fd5 --- /dev/null +++ b/src/Leanpkg/LeanVersion.lean @@ -0,0 +1,27 @@ +/- +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 +-/ +namespace Leanpkg + +def leanVersionStringCore := + s!"{Lean.version.major}.{Lean.version.minor}.{Lean.version.patch}" + +def leanVersionString := + if Lean.version.isRelease then + s!"leanprover/lean:{leanVersionStringCore}" + else if Lean.version.specialDesc ≠ "" then + Lean.version.specialDesc + else + "master" + +def uiLeanVersionString := +if Lean.version.isRelease then + leanVersionStringCore +else if Lean.version.specialDesc ≠ "" then + Lean.version.specialDesc +else + s!"master ({leanVersionStringCore})" + +end Leanpkg diff --git a/src/Leanpkg/Manifest.lean b/src/Leanpkg/Manifest.lean new file mode 100644 index 0000000000..03912ee606 --- /dev/null +++ b/src/Leanpkg/Manifest.lean @@ -0,0 +1,85 @@ +/- +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.Toml +import Leanpkg.LeanVersion + +namespace Leanpkg + +inductive Source where + | path (dirName : String) : Source + | git (url rev : String) (branch : Option String) : Source + +namespace Source + +def fromToml (v : Toml.Value) : Option Source := + (do let Toml.Value.str dirName ← v.lookup "path" | none + path dirName) <|> + (do let Toml.Value.str url ← v.lookup "git" | none + let Toml.Value.str rev ← v.lookup "rev" | none + match v.lookup "branch" with + | none => git url rev none + | some (Toml.Value.str branch) => git url rev (some branch) + | _ => none) + +def toToml : Source → Toml.Value + | path dirName => Toml.Value.table [("path", Toml.Value.str dirName)] + | git url rev none => + Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)] + | git url rev (some branch) => + Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)] + +end Source + +structure Dependency where + name : String + src : Source + +structure Manifest where + name : String + version : String + leanVersion : String := leanVersionString + timeout : Option Nat := none + path : Option String := none + dependencies : List Dependency := [] + +namespace Manifest + +def effectivePath (m : Manifest) : String := + m.path.getD "." + +def fromToml (t : Toml.Value) : Option Manifest := do + let pkg ← t.lookup "package" + let Toml.Value.str n ← pkg.lookup "name" | none + let Toml.Value.str ver ← pkg.lookup "version" | none + let leanVer ← match pkg.lookup "lean_version" with + | some (Toml.Value.str leanVer) => some leanVer + | none => some leanVersionString + | _ => none + let tm ← match pkg.lookup "timeout" with + | some (Toml.Value.nat timeout) => some (some timeout) + | none => some none + | _ => none + let path ← match pkg.lookup "path" with + | some (Toml.Value.str path) => some (some path) + | none => some none + | _ => none + let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none + let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src) + return { name := n, version := ver, leanVersion := leanVer, + path := path, dependencies := deps, timeout := tm } + +def fromFile (fn : String) : IO Manifest := do + let cnts ← IO.FS.readFile fn + let toml ← Toml.parse cnts + let some manifest ← pure (fromToml toml) + | throw <| IO.userError s!"cannot read manifest from {fn}" + manifest + +end Manifest + +def leanpkgTomlFn := "leanpkg.toml" + +end Leanpkg diff --git a/src/Leanpkg/Proc.lean b/src/Leanpkg/Proc.lean new file mode 100644 index 0000000000..f62c07c2c8 --- /dev/null +++ b/src/Leanpkg/Proc.lean @@ -0,0 +1,20 @@ +/- +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 +-/ +namespace Leanpkg + +def execCmd (args : IO.Process.SpawnArgs) : IO Unit := do + let envstr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} " + let cmdstr := " ".intercalate (args.cmd :: args.args.toList) + IO.println <| "> " ++ envstr ++ + match args.cwd with + | some cwd => cmdstr ++ " # in directory " ++ cwd + | none => cmdstr + let child ← IO.Process.spawn args + let exitCode ← child.wait + if exitCode != 0 then + throw <| IO.userError <| s!"external command exited with status {exitCode}" + +end Leanpkg diff --git a/src/Leanpkg/Resolve.lean b/src/Leanpkg/Resolve.lean new file mode 100644 index 0000000000..fc379eeefe --- /dev/null +++ b/src/Leanpkg/Resolve.lean @@ -0,0 +1,91 @@ +/- +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.Manifest +import Leanpkg.Proc +import Leanpkg.Git + +namespace Leanpkg + +def Assignment := List (String × String) + +namespace Assignment +def empty : Assignment := [] + +def contains (a : Assignment) (s : String) : Bool := + (a.lookup s).isSome + +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 (fun a ⟨k, v⟩ => f a k v) i + +end Assignment + +abbrev Solver := StateT Assignment IO + +def notYetAssigned (d : String) : Solver Bool := do + ¬ (← get).contains d + +def resolvedPath (d : String) : Solver String := do + let some path ← pure ((← get).lookup d) | unreachable! + path + +-- TODO(gabriel): windows? +def resolveDir (absOrRel : String) (base : String) : String := + if absOrRel.front = '/' then + absOrRel -- absolute + else + base ++ "/" ++ absOrRel + +def materialize (relpath : String) (dep : Dependency) : Solver Unit := + match dep.src with + | Source.path dir => do + let depdir := resolveDir dir relpath + IO.println s!"{dep.name}: using local path {depdir}" + modify (·.insert dep.name depdir) + | Source.git url rev branch => do + let depdir := "build/deps/" ++ dep.name + let alreadyThere ← IO.isDir depdir + if alreadyThere then + IO.print s!"{dep.name}: trying to update {depdir} to revision {rev}" + IO.println (match branch with | none => "" | some branch => "@" ++ branch) + let hash ← gitParseOriginRevision depdir rev + let revEx ← gitRevisionExists depdir hash + unless revEx do + execCmd {cmd := "git", args := #["fetch"], cwd := depdir} + else + IO.println s!"{dep.name}: cloning {url} to {depdir}" + execCmd {cmd := "git", args := #["clone", url, depdir]} + let hash ← gitParseOriginRevision depdir rev + execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir} + modify (·.insert dep.name depdir) + +def solveDepsCore (relPath : String) (d : Manifest) : (maxDepth : Nat) → Solver Unit + | 0 => throw <| IO.userError "maximum dependency resolution depth reached" + | maxDepth + 1 => do + let deps ← d.dependencies.filterM (notYetAssigned ·.name) + deps.forM (materialize relPath) + for dep in deps do + let p ← resolvedPath dep.name + let d' ← Manifest.fromFile $ p ++ "/" ++ "leanpkg.toml" + unless d'.name = dep.name do + throw <| IO.userError <| d.name ++ " (in " ++ relPath ++ ") depends on " ++ d'.name ++ + ", but resolved dependency has name " ++ dep.name ++ " (in " ++ p ++ ")" + solveDepsCore p d' maxDepth + +def solveDeps (d : Manifest) : IO Assignment := do + let (_, assg) ← (solveDepsCore "." d 1024).run <| Assignment.empty.insert d.name "." + assg + +def constructPathCore (depname : String) (dirname : String) : IO String := do + let path ← Manifest.effectivePath (← Manifest.fromFile $ dirname ++ "/" ++ leanpkgTomlFn) + return dirname ++ "/" ++ path + +def constructPath (assg : Assignment) : IO (List String) := do + assg.reverse.mapM fun ⟨depname, dirname⟩ => constructPathCore depname dirname + +end Leanpkg diff --git a/src/Leanpkg/Toml.lean b/src/Leanpkg/Toml.lean new file mode 100644 index 0000000000..31d910a63e --- /dev/null +++ b/src/Leanpkg/Toml.lean @@ -0,0 +1,72 @@ +/- +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 Lean.Parser + +namespace Toml + +inductive Value : Type where + | str : String → Value + | nat : Nat → Value + | bool : Bool → Value + | table : List (String × Value) → Value + deriving Inhabited + +def Value.lookup : Value → String → Option Value + | Value.table cs, k => cs.lookup k + | _, _ => none + +-- TODO: custom whitespace and other inaccuracies +declare_syntax_cat val +syntax "True" : val +syntax "False" : val +syntax str : val +syntax num : val +syntax bareKey := ident -- TODO +syntax key := bareKey <|> str +declare_syntax_cat keyCat @[keyCatParser] def key' := key -- HACK: for the antiquotation +syntax keyVal := key " = " val +syntax table := "[" key "]" keyVal* +syntax inlineTable := "{" keyVal,* "}" +syntax inlineTable : val +syntax file := table* +declare_syntax_cat fileCat @[fileCatParser] def file' := file -- HACK: for the antiquotation + +open Lean + +partial def ofSyntax : Syntax → Value + | `(val|True) => Value.bool true + | `(val|False) => Value.bool false + | `(val|$s:strLit) => Value.str <| s.isStrLit?.get! + | `(val|$n:numLit) => Value.nat <| n.isNatLit?.get! + | `(val|{$[$keys:key = $values],*}) => toTable keys (values.map ofSyntax) + | `(fileCat|$[[$keys] $kvss*]*) => toTable keys <| kvss.map fun kvs => ofSyntax <| Lean.Unhygienic.run `(val|{$kvs,*}) + | stx => unreachable! + where + toKey : Syntax → String + | `(keyCat|$key:ident) => key.getId.toString + | `(keyCat|$key:strLit) => key.isStrLit?.get! + | _ => unreachable! + toTable (keys : Array Syntax) (vals : Array Value) : Value := + Value.table <| Array.toList <| keys.zipWith vals fun k v => (toKey k, v) + +open Lean.Parser + +def parse (input : String) : IO Value := do + -- HACKHACKHACK + let env ← importModules [{ module := `Leanpkg.Toml }] {} + let fileParser ← compileParserDescr (parserExtension.getState env).categories file { env := env, opts := {} } + let c := mkParserContext (mkInputContext input "") { env := env, options := {} } + let s := mkParserState input + let s := whitespace c s + let s := fileParser.fn c s + if s.hasError then + throw <| IO.userError (s.toErrorMsg c) + else if input.atEnd s.pos then + ofSyntax s.stxStack.back + else + throw <| IO.userError ((s.mkError "end of input").toErrorMsg c) + +end Toml diff --git a/src/lean.mk.in b/src/lean.mk.in index 8f583855dc..1fb910d965 100644 --- a/src/lean.mk.in +++ b/src/lean.mk.in @@ -34,7 +34,7 @@ SHELL = /usr/bin/env bash -eo pipefail all: $(OBJS) -bin: $(BIN_OUT)/$(PKG) +bin: $(BIN_OUT)/$(BIN_NAME) lib: $(LIB_OUT)/$(STATIC_LIB_NAME) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 0f521d3533..93c958ec43 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -112,3 +112,7 @@ FOREACH(T ${LEANTESTS}) COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) + +add_test(NAME leanpkgtest + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b" + COMMAND bash -c "PATH=${LEAN_BIN}:$PATH leanpkg build") diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 89451f813f..1e41c5f291 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -7,6 +7,7 @@ LEANMAKE_OPTS=\ OUT="${LIB}"\ LIB_OUT="${LIB}/lean"\ OLEAN_OUT="${LIB}/lean"\ + BIN_OUT="${CMAKE_BINARY_DIR}/bin"\ LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\ LEANC_OPTS+="${LEANC_OPTS}"\ MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ @@ -17,3 +18,4 @@ stdlib: +"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS) +"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS) +"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) + +"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg $(LEANMAKE_OPTS) LINK_OPTS="${CMAKE_EXE_LINKER_FLAGS}" diff --git a/tests/leanpkg/a/.gitignore b/tests/leanpkg/a/.gitignore new file mode 100644 index 0000000000..796b96d1c4 --- /dev/null +++ b/tests/leanpkg/a/.gitignore @@ -0,0 +1 @@ +/build diff --git a/tests/leanpkg/a/A.lean b/tests/leanpkg/a/A.lean new file mode 100644 index 0000000000..7ee5f37600 --- /dev/null +++ b/tests/leanpkg/a/A.lean @@ -0,0 +1 @@ +def name := "world" diff --git a/tests/leanpkg/a/leanpkg.toml b/tests/leanpkg/a/leanpkg.toml new file mode 100644 index 0000000000..123e4c53fb --- /dev/null +++ b/tests/leanpkg/a/leanpkg.toml @@ -0,0 +1,3 @@ +[package] +name = "a" +version = "0.1" diff --git a/tests/leanpkg/b/.gitignore b/tests/leanpkg/b/.gitignore new file mode 100644 index 0000000000..796b96d1c4 --- /dev/null +++ b/tests/leanpkg/b/.gitignore @@ -0,0 +1 @@ +/build diff --git a/tests/leanpkg/b/B.lean b/tests/leanpkg/b/B.lean new file mode 100644 index 0000000000..3d031b53f2 --- /dev/null +++ b/tests/leanpkg/b/B.lean @@ -0,0 +1,4 @@ +import A + +def main : IO Unit := + IO.println "Hello, {name}!" diff --git a/tests/leanpkg/b/leanpkg.toml b/tests/leanpkg/b/leanpkg.toml new file mode 100644 index 0000000000..4dfec95d81 --- /dev/null +++ b/tests/leanpkg/b/leanpkg.toml @@ -0,0 +1,6 @@ +[package] +name = "b" +version = "0.1" + +[dependencies] +a = { path = "../a" }