From c49b403922f66a000f17ef4f16bda3cffecd414e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 6 Apr 2026 01:51:11 +0000 Subject: [PATCH] fstar: address code review comments - document gen_rhs_expr_list and strip-components Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0a30f342-3941-4952-a54f-1bee84b022ef Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .github/workflows/fstar-extract.yml | 3 +++ fstar/RewriteCodeGen.fst | 3 +++ 2 files changed, 6 insertions(+) diff --git a/.github/workflows/fstar-extract.yml b/.github/workflows/fstar-extract.yml index ec4473ce5..1b1a5a74f 100644 --- a/.github/workflows/fstar-extract.yml +++ b/.github/workflows/fstar-extract.yml @@ -50,6 +50,9 @@ jobs: URL="https://github.com/FStarLang/FStar/releases/download/v${FSTAR_VERSION}/${ARCHIVE}" echo "Downloading F* ${FSTAR_VERSION} from ${URL}" >&2 curl -fsSL -o "/tmp/${ARCHIVE}" "${URL}" + # The F* 2026 archive has structure: ./fstar/bin/fstar.exe + # --strip-components=2 removes both './' and 'fstar/' so that + # bin/fstar.exe lands directly in $HOME/fstar/bin/fstar.exe. mkdir -p "$HOME/fstar" tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=2 echo "$HOME/fstar/bin" >> "$GITHUB_PATH" diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst index 8a4b0cbb2..b84a64574 100644 --- a/fstar/RewriteCodeGen.fst +++ b/fstar/RewriteCodeGen.fst @@ -332,6 +332,9 @@ let rec gen_rhs_expr (e: cexpr) : Tot string (decreases e) = ^ gen_rhs_expr_list args ^ ")" and gen_rhs_expr_list (es: list cexpr) : Tot string (decreases es) = + (* Comma-separated list for C++ function arguments. Empty list yields "" + so EApp fn [] produces fn_name(), which is valid C++ for zero-arg calls + (e.g. builder helper functions that take no explicit arguments). *) match es with | [] -> "" | [e] -> gen_rhs_expr e