Skip to content
This repository has been archived by the owner on Aug 20, 2021. It is now read-only.

Use zstd instead of zip #398

Merged
merged 6 commits into from
Apr 16, 2020
Merged

Use zstd instead of zip #398

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
fb790e4
libkexec/klab-zip: rename to klab-compress
asymmetric Apr 13, 2020
cdbcbd5
libexec/klab-compress: using POSIX-compliant args
asymmetric Apr 13, 2020
96ef42d
libexec/klab-compress: use zstd
asymmetric Apr 13, 2020
50dd2ae
*: replace occurrencies of zip with tar
asymmetric Apr 13, 2020
156918a
libexec/klab-fetch: handle both zip and tar
asymmetric Apr 15, 2020
98bb5ad
libexec/klab-fetch: print usage on missing arg
asymmetric Apr 15, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ Remember, you must turn on the **d**ebug cells view to see these (above).
- `klab status <hash>` - Shows whether a proof has been run, and whether it was accepted or rejected.
- `klab status-js <hash>` - Shows the behaviour tree for an executed proof.
- `klab fetch <url>` - Fetches the execution trace of a proof object at the url, preparing it for local debugging.
- `klab zip <hash>` - zips up an execution trace so you can share it with a friend (or enemy).
- `klab compress <hash>` - compresses an execution trace so you can share it with a friend (or enemy).
- `klab storage <contractName>` - Guesses what the storage layout of a given contract is
- `klab report` - Generates a html report of the current project state in `out/report/index.html`.
- `klab help` - Generates this view
Expand Down
19 changes: 9 additions & 10 deletions libexec/klab-zip → libexec/klab-compress
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,15 +31,14 @@ if [ ! -d "$KLAB_OUT/log" ]; then
mkdir -p "$KLAB_OUT/log"
fi

zip -r "$KLAB_OUT/log/$spec_hash.zip" config.json

cd $KLAB_OUT
find . \
\( -wholename "*$spec_hash*" -or -wholename "*$spec_name*" \) \
-and ! -wholename "*/log/*.zip" \
-exec zip "./log/$spec_hash.zip" {} +

zip -r "log/$spec_hash.zip" \
"prelude.smt2" \
"rules.k" \
"bin_runtime.k"
\( -name "*$spec_hash*" \
-o -name "*$spec_name*" \
-o -name config.tmp.json \
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I changed this from config.json to config.tmp.json, because the former is not in $KLAB_OUT while the latter is, and this made the code cleaner (since I only have to search in one dir).

AFAICT the former is a subset of the latter, so everything should be fine.

@mhhf true story?

-o -name prelude.smt2 \
-o -name rules.k \
-o -name bin_runtime.k \) \
-a \! -name "*.tar" \
-a \! -name "*.zip" \
-exec tar --create --zstd --file "./log/$spec_hash.tar" {} +
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here we could pass the --threads=N argument to zstd, to control how many threads are used for compression, in case we deemed it necessary.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do you have a rough idea of what kind of speedup we could get from this?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On the test archive on buildbot, using -T0, 29 vs 33 seconds, so negligible. Maybe there are other bottlenecks.

19 changes: 15 additions & 4 deletions libexec/klab-fetch
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,23 @@ if [ -z "$KLAB_OUT" ]; then
KLAB_OUT=out
fi

[[ $# -eq 1 ]] || (echo >&2 "Usage: klab fetch \$URL" && exit 1)
url=$1
filename=${url##*/}

mkdir -p "$KLAB_OUT"/log
wget -c "$url" -P "$KLAB_OUT"/log/
unzip -qu "$KLAB_OUT/log/${url##*/}" -d "$KLAB_OUT"
# log the proof hash
hash=$(basename "$url" '.zip')
echo $hash > $KLAB_OUT/HEAD

case $url in
*.zip)
unzip -qu "$KLAB_OUT/log/$filename" -d "$KLAB_OUT"
;;
*)
d-xo marked this conversation as resolved.
Show resolved Hide resolved
tar xf "$KLAB_OUT/log/$filename" -C "$KLAB_OUT"
;;
esac

# remove extension
hash=${filename%%.*}
echo "Focusing on: $hash"
echo "$hash" > $KLAB_OUT/HEAD
2 changes: 1 addition & 1 deletion libexec/klab-help
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ Commands:

- klab fetch <url> - Fetches the execution trace of a proof object at the url, preparing it for local debugging.

- klab zip <hash> - zips up an execution trace so you can share it with a friend (or enemy).
- klab compress <hash> - compresses an execution trace so you can share it with a friend (or enemy).

- klab storage <contractName> - Guesses what the storage layout of a given contract is

Expand Down
4 changes: 2 additions & 2 deletions libexec/klab-prove-all
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,8 @@ export -f report

savelogs() {
local hash=$1
klab zip "$hash" > /dev/null
cp "$KLAB_OUT/log/${hash}.zip" "$KLAB_REPORT_NAME_DIR"
klab compress "$hash" > /dev/null
cp "$KLAB_OUT/log/${hash}.tar" "$KLAB_REPORT_NAME_DIR"
cp "$KLAB_OUT/log/${hash}.log" "$KLAB_REPORT_NAME_DIR"
cp "$KLAB_OUT/log/${hash}.err.log" "$KLAB_REPORT_NAME_DIR"
}
Expand Down
14 changes: 7 additions & 7 deletions libexec/klab-report
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,13 +152,13 @@ const getBadges = (cases, act) => {

const outPath = path.join(KLAB_OUT, "log", s.proofid + ".log");
const errPath = path.join(KLAB_OUT, "log", s.proofid + ".err.log");
const zipPath = path.join(KLAB_OUT, "log", s.proofid + ".zip");
const tarballPath = path.join(KLAB_OUT, "log", s.proofid + ".tar");
const gasPath = path.join(KLAB_OUT, "gas", s.proofid + ".all.json");

const lemmaPath = path.join(KLAB_OUT, "log", s.proofid + "_lemma_stats.json");
const hasOut = testPath(outPath) && read(outPath).trim() !== "";
const hasErr = testPath(errPath) && read(errPath).trim() !== "";
const hasZip = testPath(zipPath);
const hasTarball = testPath(tarballPath);
const hasGas = testPath(gasPath);

const lemma_stats = testPath(lemmaPath) && JSON.parse(read(lemmaPath)) || {};
Expand All @@ -177,11 +177,11 @@ const getBadges = (cases, act) => {

proof_info.push(td(badge(c.suffix, ((rejected || aborted) ? `${s.status} [${s.exit}]` : s.status))))

let zip = "";
if(finished && hasZip) {
zip = tr(`<td colspan="4" class="zipselect">${h(['input', `class="autoselect" type="text" value="klab fetch https://${config.host}/${config.name}/${s.proofid+'.zip'}" onfocus="this.select()"`])("")}</td>`)
let tarball = "";
if(finished && hasTarball) {
tarball = tr(`<td colspan="4" class="tarballselect">${h(['input', `class="autoselect" type="text" value="klab fetch https://${config.host}/${config.name}/${s.proofid+'.tar'}" onfocus="this.select()"`])("")}</td>`)
} else if (rejected || aborted) {
zip = tr(`<td colspan="4" class="zipselect">${h(['input', `class="autoselect" type="text" value="No log archive found"`])("")}</td>`)
tarball = tr(`<td colspan="4" class="tarballselect">${h(['input', `class="autoselect" type="text" value="No log archive found"`])("")}</td>`)
}

let lemmas = ""
Expand All @@ -191,7 +191,7 @@ const getBadges = (cases, act) => {
])
}

return h(["tr", `id="${s.spec}" class="${s.status}"`])(proof_info) + zip + lemmas
return h(["tr", `id="${s.spec}" class="${s.status}"`])(proof_info) + tarball + lemmas
})
.join('\n')
return {
Expand Down
2 changes: 1 addition & 1 deletion resources/report.css
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion resources/report.scss
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ a {
table {
border-spacing: 0px;
width: 100%;
td.zipselect {
td.tarballselect {
padding-bottom: 1em;
}
td {
Expand Down
4 changes: 2 additions & 2 deletions resources/zsh/_klab
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ _klab() {
"--evm[reduce a k term to only include evm relevant information]"
_values -C 'proofname' $(ls ${KLAB_OUT:-out}/meta/{name,data}/)
;;
focus|do-prove|get-gas|solve-gas|status|zip)
focus|do-prove|get-gas|solve-gas|status|compress)
_values -C 'proofname' $(ls ${KLAB_OUT:-out}/meta/{name,data}/)
;;
debug)
Expand Down Expand Up @@ -56,7 +56,7 @@ _klab() {
"report:generate a report"
"solve-gas:generate a simple gas kast expression based on the raw gas"
"status:display the proofstatus"
"zip:bundle a proof to a zip file"
"compress:bundle a proof into a compressed tarball"
)
_describe -t commands 'klab' subcommands
fi
Expand Down
2 changes: 1 addition & 1 deletion shell.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ pkgs.stdenv.mkDerivation {
time
unzip
wget
zip
z3
zstd
asymmetric marked this conversation as resolved.
Show resolved Hide resolved
];
shellHook = ''
export PATH=${toString ./node_modules/.bin}:${toString ./bin}:$PATH
Expand Down