-
Notifications
You must be signed in to change notification settings - Fork 236
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
mk-package.sh: windows fixes (7z, paths, etc)
- Loading branch information
Showing
1 changed file
with
85 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,34 +1,109 @@ | ||
#!/bin/bash | ||
|
||
set -eu | ||
|
||
# This will just create a tar.gz or zip out of a directory. | ||
# You may want to look at src-install.sh and bin-install.sh | ||
# that generate the layouts for a source and binary package, | ||
# and are then packaged up with this script. | ||
|
||
if [ $# -ne 2 ]; then | ||
echo "usage: $0 <install_root> <package_basename>" >&2 | ||
echo "Default format is tar.gz. Optionally set FSTAR_PACKAGE_FORMAT=zip to generate a zip instead." >&2 | ||
echo "Output filename is <package_basename> + proper extension." >&2 | ||
exit 1 | ||
exec >&2 | ||
echo "usage: $0 <install_root> <package_basename>" | ||
echo "The archive format and command used depends on the system and installed tools," | ||
echo "see script for details." | ||
echo "Optionally set FSTAR_PACKAGE_FORMAT to: " | ||
echo " - 'zip': create a .zip via 'zip' command" | ||
echo " - '7z': create a .zip via '7z' command" | ||
echo " - 'tar.gz': create a .tar.gz, via calling" | ||
echo "Output filename is <package_basename> + proper extension" | ||
echo "If FSTAR_RELEASE is non-empty, we use maximum compression." | ||
exit 1 | ||
fi | ||
|
||
PREFIX="$1" | ||
ARCHIVE="$2" | ||
|
||
windows () { | ||
[ -v OS ] && [ "$OS" = "Windows_NT" ] | ||
} | ||
|
||
# Computes a (hopefully) sensible default for the current system | ||
detect_format () { | ||
if windows; then | ||
# Github actions runner do not have 'zip' | ||
if which zip > /dev/null; then | ||
FSTAR_PACKAGE_FORMAT=zip | ||
elif which 7z > /dev/null; then | ||
FSTAR_PACKAGE_FORMAT=7z | ||
else | ||
echo "error: no zip or 7z command found." >&2 | ||
exit 1 | ||
fi | ||
else | ||
FSTAR_PACKAGE_FORMAT=tar.gz | ||
fi | ||
} | ||
|
||
# If unset, pick a default for the system. | ||
if ! [ -v FSTAR_PACKAGE_FORMAT ]; then | ||
detect_format | ||
fi | ||
|
||
# Fix for stupid path confustion in windows | ||
if windows; then | ||
WRAP=$(pwd)/mk/winwrap.sh | ||
else | ||
WRAP= | ||
fi | ||
|
||
case $FSTAR_PACKAGE_FORMAT in | ||
zip) | ||
TGT="$ARCHIVE.zip" | ||
TGT="$(realpath "$TGT")" | ||
pushd "$PREFIX" | ||
zip -q -r -9 "$TGT" . | ||
popd | ||
ATGT="$(realpath "$TGT")" | ||
pushd "$PREFIX" >/dev/null | ||
LEVEL= | ||
if [ -v FSTAR_RELEASE ]; then | ||
LEVEL=-9 | ||
fi | ||
$WRAP zip -q -r $LEVEL "$ATGT" . | ||
popd >/dev/null | ||
;; | ||
tar.gz|tgz|"") | ||
7z) | ||
TGT="$ARCHIVE.zip" | ||
ATGT="$(realpath "$TGT")" | ||
LEVEL= | ||
if [ -v FSTAR_RELEASE ]; then | ||
LEVEL=-mx9 | ||
fi | ||
pushd "$PREFIX" >/dev/null | ||
$WRAP 7z $LEVEL a "$ATGT" . | ||
popd >/dev/null | ||
;; | ||
tar.gz|tgz) | ||
# -h: resolve symlinks | ||
tar czf "$ARCHIVE.tar.gz" -h -C "$PREFIX" . | ||
TGT="$ARCHIVE.tar.gz" | ||
$WRAP tar cf "$ARCHIVE.tar" -h -C "$PREFIX" . | ||
LEVEL= | ||
if [ -v FSTAR_RELEASE ]; then | ||
LEVEL=-9 | ||
fi | ||
$WRAP gzip -f $LEVEL "$ARCHIVE.tar" | ||
;; | ||
*) | ||
echo "unrecognized FSTAR_PACKAGE_FORMAT: $FSTAR_PACKAGE_FORMAT" >&2 | ||
exit 1 | ||
;; | ||
esac | ||
|
||
if ! [ -f "$TGT" ] ; then | ||
echo "error: something seems wrong, archive '$TGT' not found?" >&2 | ||
exit 1 | ||
fi | ||
|
||
# bytes=$(stat -c%s "$TGT") | ||
# echo "Wrote $TGT" ($bytes bytes)" | ||
# ^ Does not work in Mac (no -c option for stat) | ||
|
||
echo "Wrote $TGT" | ||
ls -l "$TGT" || true |