-
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.
Merge pull request #3674 from mtzguido/win_prepare
Preparing for a native Windows build
- Loading branch information
Showing
21 changed files
with
315 additions
and
142 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
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
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 |
|---|---|---|
| @@ -0,0 +1,52 @@ | ||
| #!/bin/bash | ||
|
|
||
| # This is called by the Makefile *after* an installation into the | ||
| # prefix, so we add the rest of the files that go into a binary package. | ||
|
|
||
| set -eu | ||
|
|
||
| windows () { | ||
| # This seems portable enough and does not trigger an | ||
| # undefined variable error (see set -u above) if $OS | ||
| # is unset (like in linux/mac). Note: OSX's bash is usually | ||
| # old and does not support '[ -v OS ]'. | ||
| [[ "${OS:-}" = "Windows_NT" ]] | ||
| } | ||
|
|
||
| if [ $# -ne 1 ]; then | ||
| echo "Usage: $0 <prefix>" >&2 | ||
| exit 1 | ||
| fi | ||
|
|
||
| PREFIX="$1" | ||
| mkdir -p "$PREFIX" | ||
| PREFIX="$(realpath "$PREFIX")" | ||
|
|
||
| if ! [ -v FSTAR_PACKAGE_Z3 ] || ! [ "$FSTAR_PACKAGE_Z3" = false ]; then | ||
| .scripts/package_z3.sh "$PREFIX" | ||
| fi | ||
|
|
||
| if windows; then | ||
| # This dll is needed. It must be installed if we're packaging, as we | ||
| # must have run F* already, but it should probably be obtained from | ||
| # somewhere else.. | ||
| LIBGMP=$(which libgmp-10.dll) || echo "error: libgmp-10.dll not found! Carrying on..." >&2 | ||
| cp "$LIBGMP" "$PREFIX/bin" | ||
| fi | ||
|
|
||
| # License and extra files. Not there on normal installs, but present in | ||
| # package. | ||
| cp LICENSE* "$PREFIX" | ||
| cp README.md "$PREFIX" | ||
| cp INSTALL.md "$PREFIX" | ||
| cp version.txt "$PREFIX" | ||
|
|
||
| # Save the megabytes! Strip binaries | ||
| STRIP=strip | ||
|
|
||
| if windows; then | ||
| STRIP="$(pwd)/mk/winwrap.sh $STRIP" | ||
| fi | ||
|
|
||
| $STRIP "$PREFIX"/bin/* || true | ||
| $STRIP "$PREFIX"/lib/fstar/z3-*/bin/* || true |
This file was deleted.
Oops, something went wrong.
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
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
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,29 +1,117 @@ | ||
| #!/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 () { | ||
| # This seems portable enough and does not trigger an | ||
| # undefined variable error (see set -u above) if $OS | ||
| # is unset (like in linux/mac). Note: OSX's bash is usually | ||
| # old and does not support '[ -v OS ]'. | ||
| [[ "${OS:-}" = "Windows_NT" ]] | ||
| } | ||
|
|
||
| release () { | ||
| [[ -n "${FSTAR_RELEASE:-}" ]] | ||
| } | ||
|
|
||
| # 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 release; then | ||
| LEVEL=-9 | ||
| fi | ||
| $WRAP zip -q -r $LEVEL "$ATGT" . | ||
| popd >/dev/null | ||
| ;; | ||
| 7z) | ||
| TGT="$ARCHIVE.zip" | ||
| ATGT="$(realpath "$TGT")" | ||
| LEVEL= | ||
| if release; then | ||
| LEVEL=-mx9 | ||
| fi | ||
| pushd "$PREFIX" >/dev/null | ||
| $WRAP 7z $LEVEL a "$ATGT" . | ||
| popd >/dev/null | ||
| ;; | ||
| tar.gz|tgz|"") | ||
| 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 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 |
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
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
Oops, something went wrong.