From cd169759469875b1a72f85f4caf3f87484f3b879 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 24 May 2024 17:32:07 -0400 Subject: [PATCH] feat: `lake pack` / `lake unpack` (#4270) Adds two new Lake commands, `lake pack` and `lake unpack`, which pack and unpack, respectively, Lake build artifacts from an archive. If a path argument is given, creates the archive specified, otherwise uses the information in a package's `buildArchive` configuration as the default. The pack command will be used by Reservoir to prepare crate-style build archives for packages. In the future, the command will also be extensible through configuration file hooks. --- src/lake/Lake/Build/Package.lean | 2 +- src/lake/Lake/CLI/Actions.lean | 15 +++++++++++---- src/lake/Lake/CLI/Help.lean | 26 ++++++++++++++++++++++++++ src/lake/Lake/CLI/Main.lean | 25 +++++++++++++++++++++---- src/lake/examples/hello/test.sh | 13 ++++++++++++- src/lake/tests/noRelease/test.sh | 5 +++-- 6 files changed, 74 insertions(+), 12 deletions(-) diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index e5e657dc69..34bb232dd6 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -71,7 +71,7 @@ def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.asy download url self.buildArchiveFile unless upToDate && (← self.buildDir.pathExists) do updateAction .fetch - logVerbose s!"unpacking {self.name}/{tag}/{self.buildArchive}" + logVerbose s!"unpacking {self.name}:{tag}:{self.buildArchive}" untar self.buildArchiveFile self.buildDir return (true, .nil) diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean index 83c4c434e5..b92ea5488b 100644 --- a/src/lake/Lake/CLI/Actions.lean +++ b/src/lake/Lake/CLI/Actions.lean @@ -19,14 +19,21 @@ def exe (name : Name) (args : Array String := #[]) (buildConfig : BuildConfig : let exeFile ← ws.runBuild exe.fetch buildConfig env exeFile.toString args -def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do +def Package.pack (pkg : Package) (file : FilePath := pkg.buildArchiveFile) : LogIO Unit := do + logInfo s!"packing {file}" + tar pkg.buildDir file + +def Package.unpack (pkg : Package) (file : FilePath := pkg.buildArchiveFile) : LogIO Unit := do + logInfo s!"unpacking {file}" + untar file pkg.buildDir + +def Package.uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do + pkg.pack + logInfo s!"uploading {tag}:{pkg.buildArchive}" let mut args := #["release", "upload", tag, pkg.buildArchiveFile.toString, "--clobber"] if let some repo := pkg.releaseRepo? then args := args.append #["-R", repo] - logInfo s!"packing {pkg.buildArchive}" - tar pkg.buildDir pkg.buildArchiveFile - logInfo s!"uploading {tag}/{pkg.buildArchive}" proc {cmd := "gh", args} def Package.resolveDriver diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index c0efc2ad54..5bc0902d57 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -26,6 +26,8 @@ COMMANDS: env ... execute a command in Lake's environment lean elaborate a Lean file in Lake's context update update dependencies and save them to the manifest + pack pack build artifacts into an archive for distribution + unpack unpack build artifacts from an distributed archive upload upload build artifacts to a GitHub release script manage and run workspace scripts scripts shorthand for `lake script list` @@ -202,6 +204,28 @@ Does NOT verify that the configured lint driver actually exists in the package or its dependencies. It merely verifies that one is specified. " +def helpPack := +"Pack build artifacts into a archive for distribution + +USAGE: + lake pack [] + +Packs the root package's `buildDir` into a gzip tar archive using `tar`. +If a path for the archive is not specified, creates a archive in the package's +Lake directory (`.lake`) named according to its `buildArchive` setting. + +Does NOT build any artifacts. It just packs the existing ones." + +def helpUnpack := +"Unpack build artifacts from a distributed archive + +USAGE: + lake unpack [] + +Unpack build artifacts from the gzip tar archive `file.tgz` into the root +package's `buildDir`. If a path for the archive is not specified, uses the +the package's `buildArchive` in its Lake directory (`.lake`)." + def helpUpload := "Upload build artifacts to a GitHub release @@ -352,6 +376,8 @@ def help : (cmd : String) → String | "init" => helpInit | "build" => helpBuild | "update" | "upgrade" => helpUpdate +| "pack" => helpPack +| "unpack" => helpUnpack | "upload" => helpUpload | "test" => helpTest | "check-test" => helpCheckTest diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 3b4eaaf5ed..65b00353b7 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -326,13 +326,28 @@ protected def update : CliM PUnit := do let toUpdate := (← getArgs).foldl (·.insert <| stringToLegalOrSimpleName ·) {} updateManifest config toUpdate +protected def pack : CliM PUnit := do + processOptions lakeOption + let file? ← takeArg? + noArgsRem do + let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions)) + let file := (FilePath.mk <$> file?).getD ws.root.buildArchiveFile + ws.root.pack file + +protected def unpack : CliM PUnit := do + processOptions lakeOption + let file? ← takeArg? + noArgsRem do + let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions)) + let file := (FilePath.mk <$> file?).getD ws.root.buildArchiveFile + ws.root.unpack file + protected def upload : CliM PUnit := do processOptions lakeOption let tag ← takeArg "release tag" - let opts ← getThe LakeOptions - let config ← mkLoadConfig opts - let ws ← loadWorkspace config - uploadRelease ws.root tag + noArgsRem do + let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions)) + ws.root.uploadRelease tag protected def setupFile : CliM PUnit := do processOptions lakeOption @@ -475,6 +490,8 @@ def lakeCli : (cmd : String) → CliM PUnit | "build" => lake.build | "update" | "upgrade" => lake.update | "resolve-deps" => lake.resolveDeps +| "pack" => lake.pack +| "unpack" => lake.unpack | "upload" => lake.upload | "setup-file" => lake.setupFile | "test" => lake.test diff --git a/src/lake/examples/hello/test.sh b/src/lake/examples/hello/test.sh index b086e2f6e4..30bf7a64a4 100755 --- a/src/lake/examples/hello/test.sh +++ b/src/lake/examples/hello/test.sh @@ -1,4 +1,5 @@ -set -ex +#!/usr/bin/env bash +set -euxo pipefail LAKE=${LAKE:-../../.lake/build/bin/lake} @@ -15,6 +16,16 @@ $LAKE -q build hello 2>&1 | diff - /dev/null # Related: https://github.com/leanprover/lean4/issues/2549 test -f lake-manifest.json +# Test pack/unpack +$LAKE pack .lake/build.tgz 2>&1 | grep --color "packing" +rm -rf .lake/build +$LAKE unpack .lake/build.tgz 2>&1 | grep --color "unpacking" +.lake/build/bin/hello +$LAKE pack 2>&1 | grep --color "packing" +rm -rf .lake/build +$LAKE unpack 2>&1 | grep --color "unpacking" +.lake/build/bin/hello + ./clean.sh $LAKE -f lakefile.toml exe hello diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh index bbef5ac68a..1190a5d380 100755 --- a/src/lake/tests/noRelease/test.sh +++ b/src/lake/tests/noRelease/test.sh @@ -45,9 +45,10 @@ EOF git -C dep tag release ($LAKE build dep:release && exit 1 || true) | grep --color "downloading" -# Test unpacking +# Test automatic cloud release unpacking mkdir -p dep/.lake/build -tar -cz -f dep/.lake/release.tgz -C dep/.lake/build . +$LAKE -d dep pack 2>&1 | grep --color "packing" +test -f dep/.lake/release.tgz echo 4225503363911572621 > dep/.lake/release.tgz.trace rmdir dep/.lake/build $LAKE build dep:release -v | grep --color "unpacking"