diff --git a/README.md b/README.md index 02737ec3e7..793b9ced8a 100644 --- a/README.md +++ b/README.md @@ -206,6 +206,10 @@ def add_zero(x): - 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. - Formatter: [bend-fmt-lsp](tools/bend-fmt-lsp), a formatting-only Bend 2 language server. +- Independent module smoke checks: `bend aggregation.bend --checkup` checks + and runs local, content-hash and named hub imports in their own scope. + Hub entries stay inside the library cache, including after path normalization + or symlink resolution; a failed entry does not stop the later checks. - 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 f262925086..7afbe62998 100755 --- a/bend2/main.ts +++ b/bend2/main.ts @@ -327,8 +327,13 @@ async function cli_file(args: string[]): Promise { // cli_checkup checks and runs each import of the file alone (Base read // once, seeded into every module that imports it); one that fails fails it. +// A hub import loads from a root that imports only it, so it resolves as any +// import does and keeps its namespace; a first parse (Base skipped) finds its +// file, to see if it imports Base, and its main is the root's main. async function cli_checkup(file: string): Promise { const base = await book_read(BASE); + const tmp = fs.mkdtempSync(path.join(os.tmpdir(), "bend-")); + const hub = path.join(tmp, "hub.bend"); 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*$/ @@ -336,13 +341,29 @@ async function cli_checkup(file: string): Promise { if (m === null) { continue; } - const at = m[1].startsWith("/") ? m[1] - : path.join(path.dirname(file), m[1]); + const at = /^(0x[0-9a-f]+|[^/]*@[^/]*)\//.test(m[1]) ? hub + : path.resolve(path.dirname(file), m[1]); + // A hub-owned root makes the loader confine every import to its cache. + const ns = at === hub ? "0x0/checkup" : ""; cli_say(1, "--- " + m[1] + " ---\n"); let code = 1; try { - const own = /^import Base$/m.test(fs.readFileSync(at, "utf8")); - code = book_run(await book_read(at, own ? base : undefined), [at]); + fs.writeFileSync(hub, "import " + m[1] + " as Hub\n"); + let seen = new Map([[BASE, ""]]); + if (at === hub) { + await Bend.book_load(Bend.book_nil(), hub, ns, seen).catch((e) => { + throw new Check_Fail(e); + }); + } + const [, , got = at] = seen.keys(); + const own = /^import Base$/m.test(fs.readFileSync(got, "utf8")); + seen = new Map(); + const book = await book_read(at, own ? base : undefined, seen, ns); + const main = book.tlds[seen.get(got) + ":main"]; + if (at === hub && main !== undefined) { + book.tlds["main"] = main; + } + code = book_run(book, [at]); } catch (e) { cli_say(2, book_err(e) + "\n"); } @@ -351,6 +372,7 @@ async function cli_checkup(file: string): Promise { bad = true; } } + fs.rmSync(tmp, { recursive: true }); if (bad) { process.exit(1); } @@ -888,13 +910,13 @@ function cli_fail(msg: string): never { // ==== async function book_read(file: string, base?: Bend.Book, - seen = new Map()): Promise { + seen = new Map(), ns = ""): Promise { const book = base === undefined ? Bend.book_nil() : book_seed(base); if (base !== undefined) { seen.set(BASE, ""); } try { - await Bend.book_load(book, file, "", seen); + await Bend.book_load(book, file, ns, seen); const laws = path.join(path.dirname(file), "LAWS.bend"); if (path.basename(file) === "PROOF.bend" && fs.existsSync(laws) && !seen.has(fs.realpathSync(laws))) { diff --git a/gates/ping.ts b/gates/ping.ts index a72189e0ac..1944a485f6 100644 --- a/gates/ping.ts +++ b/gates/ping.ts @@ -325,6 +325,42 @@ try { const got = await bend_closed(args); check("a closed reader keeps success: " + args.join(" "), got.code === 0); } + const checkup_files = { + "pure.bend": "import Base\ndef main() -> Nat:\n 5n\n", + "io.bend": "import Base\ndef main() -> IO(Unit):\n IO.print(\"hub-io\")\n", + }; + const checkup_pkg = pkg_hash(checkup_files); + const checkup_cache = path.join(TMP, "checkup-lib"); + fs.mkdirSync(path.join(checkup_cache, checkup_pkg), { recursive: true }); + fs.mkdirSync(path.join(checkup_cache, "names")); + for (const [name, text] of Object.entries(checkup_files)) { + fs.writeFileSync(path.join(checkup_cache, checkup_pkg, name), text); + } + fs.writeFileSync(path.join(checkup_cache, "names", "checkup@1.0.0.0"), checkup_pkg); + const checkup_hub = path.join(TMP, "checkup-hub.bend"); + fs.writeFileSync(checkup_hub, "import " + checkup_pkg + + "/pure.bend as Pure\nimport checkup@1.0.0.0/io.bend as Effect\n"); + const checkup_result = await bend([checkup_hub, "--checkup"], + { BEND_LIB: checkup_cache, BEND_NO_TELEMETRY: "1" }); + check("hash and named hub checkups execute pure and effectful entries", + checkup_result.code === 0 && checkup_result.out.includes("\n5n\n") + && checkup_result.out.endsWith("hub-io\n")); + const checkup_outside = path.join(TMP, "checkup-outside.bend"); + fs.writeFileSync(checkup_outside, "import Base\ndef main() -> Nat:\n 99n\n"); + fs.writeFileSync(checkup_hub, "import " + checkup_pkg + + "/../../checkup-outside.bend as Outside\nimport checkup@1.0.0.0/io.bend as Effect\n"); + const checkup_escape = await bend([checkup_hub, "--checkup"], + { BEND_LIB: checkup_cache, BEND_NO_TELEMETRY: "1" }); + check("a hub traversal fails without running the outside file; later imports run", + checkup_escape.code === 1 && !checkup_escape.out.includes("\n99n\n") + && checkup_escape.out.endsWith("hub-io\n")); + fs.unlinkSync(path.join(checkup_cache, checkup_pkg, "pure.bend")); + fs.symlinkSync(checkup_outside, path.join(checkup_cache, checkup_pkg, "pure.bend")); + fs.writeFileSync(checkup_hub, "import checkup@1.0.0.0/pure.bend as Outside\n"); + const checkup_link = await bend([checkup_hub, "--checkup"], + { BEND_LIB: checkup_cache, BEND_NO_TELEMETRY: "1" }); + check("a named hub entry cannot run through a symlink outside its cache", + checkup_link.code === 1 && !checkup_link.out.includes("\n99n\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";