diff --git a/README.md b/README.md index 02737ec3e..66fa9b4ee 100644 --- a/README.md +++ b/README.md @@ -205,6 +205,8 @@ def add_zero(x): - Paper: [BendRT: A Parallel Runtime for CPUs and GPUs](paper/BendRT.pdf). - Formalization: [bendtt.lean](bend2/bendtt.lean), the kernel of `--verdict` and its proofs, in Lean. - Benches: [bench/](bench), every bench used to make the charts above. +- Module smoke checks: `bend aggregation.bend --checkup` checks and runs + each aliased import independently, including lines with trailing `#` comments. - Formatter: [bend-fmt-lsp](tools/bend-fmt-lsp), a formatting-only Bend 2 language server. - Community language server: [bend2-lsp](https://github.com/don2e4/bend2-lsp), with formatting, diagnostics, and hover. - Community workshop: [Bend 2 pocket workshop](https://np.github.io/bend-workshop/), the checker and JS compiler in one HTML page, with goals and proof tools, phone first. diff --git a/bend2/main.ts b/bend2/main.ts index f26292508..f8bd19127 100755 --- a/bend2/main.ts +++ b/bend2/main.ts @@ -331,7 +331,7 @@ async function cli_checkup(file: string): Promise { const base = await book_read(BASE); let bad = false; for (const raw of fs.readFileSync(file, "utf8").split("\n")) { - const m = /^import\s+(\S+)\s+as\s+[A-Za-z_][A-Za-z0-9_]*\s*$/ + const m = /^import\s+(\S+)\s+as\s+[A-Za-z_][A-Za-z0-9_]*\s*(?:#.*)?$/ .exec(raw.trim()); if (m === null) { continue; diff --git a/gates/ping.ts b/gates/ping.ts index a72189e0a..20378bf39 100644 --- a/gates/ping.ts +++ b/gates/ping.ts @@ -325,6 +325,13 @@ try { const got = await bend_closed(args); check("a closed reader keeps success: " + args.join(" "), got.code === 0); } + fs.writeFileSync(checkup, "import ./bad.bend as Bad # must still fail\n"); + fs.writeFileSync(good_checkup, "import ./sum.bend as Good # must still run\n"); + const comment_bad = await bend([checkup, "--checkup"]); + const comment_good = await bend([good_checkup, "--checkup"]); + check("import comments preserve checkup rejection and execution", + comment_bad.code === 1 && comment_good.code === 0 + && comment_good.out.endsWith("5n\n")); const two = "import Base\ndef two() -> Nat:\n 2n\n"; const use = (at: string) => "import Base\nimport ./" + at + " as T\ndef main() -> Nat:\n T.two\n";