Skip to content

[Merged by Bors] - fix(scripts/runSkimmer): only lake update skimmer #41662

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
thorimur wants to merge 1 commit into from
Closed

[Merged by Bors] - fix(scripts/runSkimmer): only lake update skimmer #41662

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
20 changes: 10 additions & 10 deletions scripts/runSkimmer.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,11 +49,11 @@ usage() {
Usage: runSkimmer.sh [[--no-update] [--on [tgts...]] | --lake-update | --init | -h | --help]

Options:
[no arguments] Run \`lake update\` in \`SideSkimmer\`, then run \`lake build <tgt>:applyCurrentTryThis\` on targets configured in \`runSkimmer.sh\`. (When refactoring mathlib, does not get mathlib's cache.)
--on [tgts...] Run \`lake update\` in \`SideSkimmer\`, then run \`lake build <tgt>:applyCurrentTryThis\` for \`tgt\` in the supplied \`tgts\`. Each `tgt` may be lake target syntax for the current package or a library or module therein. (When refactoring mathlib, does not get mathlib's cache.)
--no-update Only run \`lake build <tgts>:applyCurrentTryThis\`, without first running \`lake update\` in \`SideSkimmer\`. Applies both the default targets and those supplied with \`--on\`.
[no arguments] Run \`lake update skimmer\` in \`SideSkimmer\`, then run \`lake build <tgt>:applyCurrentTryThis\` on targets configured in \`runSkimmer.sh\`. (When refactoring mathlib, does not get mathlib's cache.)
--on [tgts...] Run \`lake update skimmer\` in \`SideSkimmer\`, then run \`lake build <tgt>:applyCurrentTryThis\` for \`tgt\` in the supplied \`tgts\`. Each `tgt` may be lake target syntax for the current package or a library or module therein. (When refactoring mathlib, does not get mathlib's cache.)
--no-update Only run \`lake build <tgts>:applyCurrentTryThis\`, without first running \`lake update skimmer\` in \`SideSkimmer\`. Applies both the default targets and those supplied with \`--on\`.
--init Set up the \`SideSkimmer\` side package. This only needs to be done when first introducing \`runSkimmer.sh\` to a new repo.
--lake-update Only run \`lake update -v\` in \`SideSkimmer\`, and if refactoring mathlib, do not get mathlib's cache while doing so.
--lake-update Only run \`lake update skimmer -v\` in \`SideSkimmer\`, and if refactoring mathlib, do not get mathlib's cache while doing so.
EOF
}

Expand Down Expand Up @@ -117,18 +117,18 @@ EOF
/lean-toolchain
EOF
# Creates toolchain, manifest, etc.
(cd "${pkg}" && lake update)
(cd "${pkg}" && lake update skimmer)
else
if [[ -f "${pkg}/lakefile.lean" && -f "${pkg}/.gitignore" ]]; then
if [[ "${lakeUpdate}" ]]; then
echo "Only running \`lake update -v\` in \`SideSkimmer\`; skipping run."
(cd "${pkg}" && lake update -v)
echo "Only running \`lake update skimmer -v\` in \`SideSkimmer\`; skipping run."
(cd "${pkg}" && lake update skimmer -v)
exit 0
fi
# Only run `lake update` if `--no-update` is not present.
# Only run `lake update skimmer` if `--no-update` is not present.
if [[ ! "${noUpdate}" ]]; then
echo "Running \`lake update\` in \`SideSkimmer\`. Use \`runSkimmer.sh --no-update\` to skip this step."
(cd "${pkg}" && lake update)
echo "Running \`lake update skimmer\` in \`SideSkimmer\`. Use \`runSkimmer.sh --no-update\` to skip this step."
(cd "${pkg}" && lake update skimmer)
elif [[ ! -f "${pkg}/lake-manifest.json" ]]; then
echo "Expected manifest at \`${pkg}/lake-manifest.json\`."
echo "Please exclude the \`--no-update\` flag to create one."
Expand Down
Loading