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

@@ -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)
 

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

src/lake/Lake/CLI/Help.lean

@@ -26,6 +26,8 @@ COMMANDS:
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           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 <tag>          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 [<file.tgz>]
+
+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 [<file.tgz>]
+
+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

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

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

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"