Skip to content

linting: add shellcheck support for shell script linting #1329

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

Open
L-series wants to merge 2 commits into
base: main
Choose a base branch
from
+47 −24
Open

linting: add shellcheck support for shell script linting #1329

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
465153e
linting: add shelcheck for shell script lint
L-series Dec 1, 2025
5624f82
linting: shell: fix shellcheck warnings
L-series Dec 1, 2025
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
8 changes: 4 additions & 4 deletions META.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@ VAL=$(cat $META |
cut -d ":" -f 2 | tr -d ' ')

# More robust extraction using yq
if (which yq 2>&1 >/dev/null); then
if (which yq >/dev/null 2>&1); then
QUERY=".implementations | .[] | select(.name==\"$1\") | .\"$2\""
echo "cat $META | yq "$QUERY" -r"
echo "cat $META | yq \"$QUERY\" -r"
VAL_JQ=$(cat $META | yq "$QUERY" -r)

if [[ $VAL_JQ != $VAL ]]; then
if [[ $VAL_JQ != "$VAL" ]]; then
echo "ERROR parsing metadata file $META"
exit 1
fi
Expand All @@ -41,5 +41,5 @@ if [[ $INPUT != "" ]]; then
exit 0
fi
else
echo $VAL
echo "$VAL"
fi
3 changes: 2 additions & 1 deletion nix/util.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,8 @@ rec {

inherit (pkgs)
nixpkgs-fmt
shfmt;
shfmt
shellcheck;

inherit (pkgs.python3Packages)
mpmath sympy black pyparsing pyyaml;
Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/list_proofs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@
# which are those containing a *harness.c file.

ROOT=$(git rev-parse --show-toplevel)
cd $ROOT
cd "$ROOT" || exit
ls -1 proofs/cbmc/**/*harness.c | cut -d '/' -f 3
2 changes: 1 addition & 1 deletion proofs/hol_light/arm/list_proofs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@
# we have a spec and proof in HOL-Light.

ROOT=$(git rev-parse --show-toplevel)
cd $ROOT
cd "$ROOT" || exit
ls -1 proofs/hol_light/arm/mlkem/*.S | cut -d '/' -f 5 | sed 's/\.S//'
13 changes: 7 additions & 6 deletions proofs/hol_light/arm/proofs/build-proof.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ output_path=$3
output_dir=$(dirname "$output_path")
[ -d "$output_dir" ] || mkdir -p "$output_dir"

export HOLLIGHT_DIR="$(dirname ${hol_sh_cmd})"
HOLLIGHT_DIR="$(dirname "${hol_sh_cmd}")"
export HOLLIGHT_DIR
if [ ! -f "${HOLLIGHT_DIR}/hol_lib.cmxa" ]; then
echo "hol_lib.cmxa does not exist in HOLLIGHT_DIR('${HOLLIGHT_DIR}')."
echo "Did you compile HOL Light with HOLLIGHT_USE_MODULE set to 1?"
Expand All @@ -50,20 +51,20 @@ echo "Generating a template .ml that loads the file...: ${template_ml}"
echo "check_axioms ();;"
echo 'let proof_end_time = Unix.time();;'
echo 'Printf.printf "Running time: %f sec, Start unixtime: %f, End unixtime: %f\n" (proof_end_time -. proof_start_time) proof_start_time proof_end_time;;'
) >>${template_ml}
) >>"${template_ml}"

inlined_prefix="$(mktemp)"
inlined_ml="${inlined_prefix}.ml"
inlined_cmx="${inlined_prefix}.cmx"
(cd "${S2N_BIGNUM_DIR}" && HOLLIGHT_LOAD_PATH=${ROOT} ocaml ${HOLLIGHT_DIR}/inline_load.ml "${template_ml}" "${inlined_ml}")
(cd "${S2N_BIGNUM_DIR}" && HOLLIGHT_LOAD_PATH=${ROOT} ocaml "${HOLLIGHT_DIR}"/inline_load.ml "${template_ml}" "${inlined_ml}")

# Give a large stack size.
OCAMLRUNPARAM=l=2000000000 \
ocamlopt.byte -pp "$(${hol_sh_cmd} -pp)" -I "${HOLLIGHT_DIR}" -I +unix -c \
hol_lib.cmxa ${inlined_ml} -o ${inlined_cmx} -w -a
hol_lib.cmxa "${inlined_ml}" -o "${inlined_cmx}" -w -a
ocamlfind ocamlopt -package zarith,unix -linkpkg hol_lib.cmxa \
-I "${HOLLIGHT_DIR}" ${inlined_cmx} \
-I "${HOLLIGHT_DIR}" "${inlined_cmx}" \
-o "${output_path}"

# Remove the intermediate files to save disk space
rm -f ${inlined_cmx} ${template_ml} ${inlined_ml}
rm -f "${inlined_cmx}" "${template_ml}" "${inlined_ml}"
16 changes: 9 additions & 7 deletions scripts/format
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,6 @@ ROOT="$(realpath "$(dirname "$0")"/../)"
# Standard color definitions
GREEN="\033[32m"
RED="\033[31m"
BLUE="\033[94m"
BOLD="\033[1m"
NORMAL="\033[0m"

# utility
Expand All @@ -29,29 +27,33 @@ error()
}

info "Formatting nix files"
if ! command -v nixpkgs-fmt 2>&1 >/dev/null; then
if ! command -v nixpkgs-fmt >/dev/null 2>&1; then
error "nixpkgs-fmt not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi

nixpkgs-fmt "$ROOT"

info "Formatting shell scripts"
if ! command -v shfmt 2>&1 >/dev/null; then
if ! command -v shfmt >/dev/null 2>&1; then
error "shfmt not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi
shfmt -s -w -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/))

# Find all scripts in the repo
ALL_FILES=$(git grep -l '' :/)
SHELL_SCRIPTS=$(echo "$ALL_FILES" | xargs shfmt -f)
Comment on lines +44 to +45
Copy link
Contributor

@hanno-becker hanno-becker Dec 17, 2025

Choose a reason for hiding this comment

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

What about this:

SHELL_SCRIPTS=$(git grep -l '' :/ | sed "s/^/'/;s/$/'/" | tr '\n' ' ' | xargs -L 1 shfmt -f)

This produces a newline separated list of shell script filesnames while invoking shfmt -f only once.

SHELL_SCRIPTS=$(git grep -l '' :/ | xargs -I {} shfmt -f '{}')

achieves the same thing but is much slower because it invokes shfmt -f once per file.

And then you can do

echo "$SHELL_SCRIPTS" | xargs -L 1 shfmt -s -l -i 2 -ci -fn

for the formatting, I believe (due to the small number of shell scripts, it doesn't matter that there are multiple invocations here, though you could do the same munging as above to reduce it to one invocation).

Copy link
Contributor Author

@L-series L-series Dec 19, 2025

Choose a reason for hiding this comment

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

Hmm, personally I prefer the second alternative because it is somehow easier to understand. It comes at a slight performance cost yes, however it is marginal in the grand scheme.

First implementation :

git grep -l '' :/  0,01s user 0,02s system 254% cpu 0,012 total
sed "s/^/'/;s/$/'/"  0,00s user 0,00s system 29% cpu 0,011 total
tr '\n' ' '  0,00s user 0,00s system 11% cpu 0,011 total
xargs -L 1 shfmt -f  0,01s user 0,01s system 30% cpu 0,063 total

Second implementation:

git grep -l '' :/  0,01s user 0,02s system 251% cpu 0,011 total
xargs -I {} shfmt -f '{}'  0,48s user 1,01s system 115% cpu 1,285 total

shfmt -s -l -i 2 -ci -fn $SHELL_SCRIPTS

info "Formatting python scripts"
if ! command -v black 2>&1 >/dev/null; then
if ! command -v black >/dev/null 2>&1; then
error "black not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi
black --include "(scripts/tests|scripts/simpasm|scripts/cfify|scripts/autogen|scripts/check-namespace|\.py$)" "$ROOT"

info "Formatting c files"
if ! command -v clang-format 2>&1 >/dev/null; then
if ! command -v clang-format >/dev/null 2>&1; then
error "clang-format not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi
Expand Down
27 changes: 23 additions & 4 deletions scripts/lint
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,6 @@ fi
# Standard color definitions
GREEN="\033[32m"
RED="\033[31m"
BLUE="\033[94m"
BOLD="\033[1m"
NORMAL="\033[0m"

info()
Expand Down Expand Up @@ -106,15 +104,36 @@ gh_error_simple()
fi
}

run-shellcheck()
{
if ! command -v shellcheck >/dev/null; then
gh_error_simple "Shellcheck missing" "shellcheck is not installed"
error "Lint shellcheck"
SUCCESS=false
gh_summary_failure "Lint shellcheck"
return 0
fi

checkerr "Lint shellcheck" "$(shellcheck --severity=warning $SHELL_SCRIPTS)"
}

# Formatting
SUCCESS=true

# Get list of shell scripts for linting
ALL_FILES=$(git grep -l '' :/)
SHELL_SCRIPTS=$(echo "$ALL_FILES" | xargs shfmt -f)

gh_group_start "Linting nix files with nixpkgs-fmt"
checkerr "Lint nix" "$(nixpkgs-fmt --check "$ROOT")"
gh_group_end

gh_group_start "Linting shell scripts with shfmt"
checkerr "Lint shell" "$(shfmt -s -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/)))"
checkerr "Lint shell" "$(echo $SHELL_SCRIPTS | xargs shfmt -s -l -i 2 -ci -fn)"
gh_group_end

gh_group_start "Linting shell scripts with shellcheck"
run-shellcheck
gh_group_end

gh_group_start "Linting python scripts with black"
Expand All @@ -130,7 +149,7 @@ fi
gh_group_end

gh_group_start "Linting c files with clang-format"
checkerr "Lint C" "$(clang-format $(git ls-files ":/*.c" ":/*.h") --Werror --dry-run 2>&1 | grep "error:" | cut -d ':' -f 1,2 | tr ':' ' ')"
checkerr "Lint C" "$(clang-format "$(git ls-files ":/*.c" ":/*.h")" --Werror --dry-run 2>&1 | grep "error:" | cut -d ':' -f 1,2 | tr ':' ' ')"
gh_group_end

check-eol-dry-run()
Expand Down