Skip to content

AGENTS.md

Latest commit

 

History

History
136 lines (114 loc) · 6.67 KB

AGENTS.md

File metadata and controls

136 lines (114 loc) · 6.67 KB
Raw

Notes for agents and future development

The README covers consumer-facing usage. This file records maintainer knowledge: why non-obvious things are the way they are, and the workflows for changes and releases.

Layout and build pipeline

  • src/index.ts — the entire wrapper: implementation, types, and doc comments in one place. tsc emits dist/index.{js,d.ts}.
  • src/cadical.d.ts — the ONLY hand-written declaration file; types the Emscripten glue (dist/cadical.js). Copied to dist by the build.
  • src/options.generated.ts — generated by scripts/generate-options.mjs from deps/cadical/src/options.hpp; committed. Regenerate when the CaDiCaL pin changes.
  • deps/ and dist/ are gitignored. scripts/fetch-cadical.sh clones the pinned CaDiCaL tag; scripts/build-wasm.sh does everything (emcc compile + link, options generation, tsc).
  • Fast iteration: if you only changed src/*.ts, you just need npx tsc -p tsconfig.json — the emcc step is only needed when the CaDiCaL pin, exported C functions, or link flags change.

Why the C++ build is the way it is

  • CaDiCaL's ./configure compiles and RUNS feature-test binaries, which is impossible when cross-compiling to wasm. So build-wasm.sh instantiates makefile.in directly with sed and builds libcadical.a.
  • Feature macros that configure would normally probe: -DNCLOSEFROM (Emscripten's libc has no closefrom()) and -DNCONTRIB (contrib/ excluded). Do NOT define -DQUIET — it compiles out messages and would make printStatistics() print nothing.
  • src/kitten.c is C (compiled with emcc -x c); everything else is C++.
  • Adding a wrapper method for a new C function requires exporting it in the EXPORTED_FUNCTIONS list in build-wasm.sh (then re-linking).

CaDiCaL API contracts (source of a real bug class)

deps/cadical/src/cadical.hpp documents a state machine (CONFIGURING/READY/SOLVING/...) with require (...) contracts on most methods. Our build keeps contracts enabled: violating one calls C abort(), which surfaces in JS as an opaque RuntimeError: Aborted() — the real message only goes to stderr. This is why:

  • Solver options are constructor-only (set requires CONFIGURING, which is left permanently on first add/assume/solve).
  • Limits are solve() options (upstream limit is per-solve, resets on return).

Before wrapping any new C function, read its contract in cadical.hpp and design the JS API so the contract cannot be violated (preferred) or guard it in JS with a clear error.

Memory / GC invariants (do not break these)

  • _finalizerState must NEVER reference the Cadical object — the FinalizationRegistry holds it strongly, and a back-reference would make solvers uncollectable (finalizer never fires).
  • Callback function-table entries (addFunction) are GC roots. They must hold only a WeakRef trampoline to the solver, never the callback or solver directly — otherwise a callback capturing its own solver pins it forever. The real callback lives on the instance (_onTerminate / _onLearn).
  • Never cache mod.HEAP32 (or any heap view) across calls into wasm: ALLOW_MEMORY_GROWTH invalidates views on growth. Re-read at use time.
  • Symbol.dispose is wired via guarded prototype assignment + interface merging (not a class method) because on engines without the symbol a computed class key of undefined silently becomes a method named "undefined".

The options generator

scripts/generate-options.mjs parses options.hpp macro lines: OPTION( always, QUTOPT( (quiet, verbose — present because we don't build with -DQUIET), and deliberately EXCLUDES LOGOPT( (only exists in -DLOGGING builds). Range 0..1 options are typed as boolean flags.

History: v0.1.0 shipped matching only OPTION(, so Cadical.create({ quiet: true }) — the README example — threw at runtime. When touching the regex, check the macro-variant census first: grep -oE "^[A-Z]+\(" deps/cadical/src/options.hpp | sort | uniq -c and verify the parsed count matches.

Testing

  • npm test = tsc -p tsconfig.test.json (type-checks tests against the SHIPPED dist/index.d.ts — this guards the published type surface) + node --test running .ts files directly via type stripping (dev needs Node 22.18+ or 24+).
  • Tests import ../dist/index.js on purpose: they exercise the built artifact, so build before testing.
  • test/gc-check.fixture.ts is not a test; it's spawned by the suite with --expose-gc and verifies both a plain solver and one whose callback captures itself get collected and auto-disposed.
  • Browser check (manual, do when touching the glue/loading path): python3 -m http.server at repo root, open example/index.html, confirm signature + solve output.

Upgrading the CaDiCaL pin

  1. Change CADICAL_TAG in scripts/fetch-cadical.sh; rm -rf deps.
  2. npm run build — watch for new compile errors (missing libc functions get -DN... macros; check what upstream configure does).
  3. Diff src/options.generated.ts; check deps/cadical/src/ccadical.h for added/removed C API functions worth (un)wrapping.
  4. Full test + browser check + release smoke test.

Releasing

  1. npm test, clean git tree, then npm version patch|minor (commits and tags).
  2. npm publish — it will run the full build via prepack, then fail with EOTP (2FA; and OTP can't be entered interactively from agent shells). That's expected: it leaves a fresh dist/. Then ask the maintainer for an authenticator code and immediately run npm publish --ignore-scripts --otp=<code> (skipping the rebuild keeps you inside the ~30s OTP window).
  3. Smoke-test the PUBLISHED package, not the local build: in a temp dir, rm -rf node_modules package-lock.json (stale modules caused a false alarm once), npm i cadical-wasm@<new version>, and run the README examples verbatim. This exact ritual caught the v0.1.0 quiet-option bug. Registry propagation can lag a few seconds after publish.
  4. git push && git push --tags.

API design principles (keep changes consistent with these)

  • Value-oriented, not a mirror of the stateful IPASIR C API: whole clauses in, plain arrays/booleans out (addClause, model(), failedAssumptions()).
  • Placement by lifetime: fixed-for-solver-life → constructor options; scoped-to-one-call → solve() options; module-instantiation-global → createModule(options) only (the shared module is deliberately zero-config — no first-caller-wins races).
  • Unknown option names throw at runtime (for JS users) AND fail type-checking (for TS users). Keep both layers.
  • Disposal vocabulary: dispose() / disposed / Symbol.dispose, with the GC backstop as a safety net, never the primary story.