pyproject.toml

[project]
name = "vera"
version = "0.1.0"
description = "Vera: a programming language designed for LLMs, with full contracts, algebraic effects, and typed slot references"
readme = "README.md"
license = "MIT"
requires-python = ">=3.11"
authors = [
    { name = "Alasdair Allan", email = "alasdair@babilim.co.uk" },
]
classifiers = [
    "Development Status :: 2 - Pre-Alpha",
    "Intended Audience :: Developers",
    "Programming Language :: Python :: 3",
    "Programming Language :: Python :: 3.11",
    "Programming Language :: Python :: 3.12",
    "Topic :: Software Development :: Compilers",
]
dependencies = [
    "lark>=1.3.1",
    # `>=4.15.5` matches the macOS 15+ baseline structurally: 4.15.5 is the
    # first z3-solver release tagged `macosx_15_0_arm64` (earlier releases
    # were `macosx_13_0_arm64`).  Pinning >=4.15.5 makes the platform support
    # decision explicit in dep resolution — older macOS / older glibc users
    # get a clear "no matching distribution" error instead of a cryptic
    # source-build failure 20 minutes later.  See README §Supported platforms.
    "z3-solver>=4.15.5",
    # Floor rationale: `>=45.0.0` was the first wasmtime-py release whose
    # host-import trampoline catches `BaseException` rather than `Exception`
    # (bytecodealliance/wasmtime-py#337).  Vera relies on this so a
    # `KeyboardInterrupt` raised inside a host import (IO.sleep /
    # IO.read_char) unwinds the wasm call safely and re-raises in
    # Python instead of escaping into Rust with an undefined ABI
    # return value (libmalloc SIGABRT, #595).  The exit-130 mapping in
    # `execute()` depends on the raw re-raise; do not lower this pin
    # below 45 without restoring the per-host-import `_VeraExit(130)`
    # guards removed in #599.
    # Raised to `>=46.0.1` for GHSA-4ch3-9j33-3pmj (a wasmtime-wasi
    # FilePerms bypass on hard-link/rename destinations; 45.0.0 is in the
    # affected range).  The core backport is 45.0.3, but wasmtime-py never
    # tagged a 45.0.x patch — 46.0.1 is the only patched binding release.
    # Vera's own WASI host is not exploitable (it preopens with the
    # default READ_WRITE FilePerms, so there is nothing to bypass); the
    # bump keeps the resolved floor off a CVE-affected release for
    # embedders who restrict perms.
    "wasmtime>=46.0.1",
]

[project.urls]
Homepage = "https://veralang.dev"
Documentation = "https://veralang.dev"
Repository = "https://github.com/aallan/vera"
Issues = "https://github.com/aallan/vera/issues"
Changelog = "https://github.com/aallan/vera/blob/main/CHANGELOG.md"

[project.optional-dependencies]
# Both pure-Python; not gated by check_wheel_availability.py (which
# reads project.dependencies only — optional extras are exempt by
# design, see README §Supported platforms).
lsp = [
    "pygls>=2.0",
    "lsprotocol>=2023.0",
]
dev = [
    "pytest>=9.1.1",
    "pytest-cov>=7.1.0",
    "pytest-xdist>=3.6",
    "mypy>=2.1.0",
    "ruff>=0.15.20",
    "pre-commit>=4.6.0",
    "pip-licenses>=5.5.5",
    # Self-referential extra: dev pulls in [lsp] so CI's single
    # `pip install -e ".[dev]"` can run tests/test_lsp.py without a
    # second pin list to keep in sync (PEP 508 extras self-reference;
    # supported by pip >= 21.2 and uv).
    "vera[lsp]",
]
mutation = [
    # Mutation testing (#387).  Kept separate from [dev] so the
    # everyday gate stays lean; `pip install -e ".[mutation]"` pulls
    # the full test deps via [dev] plus the mutation engine.  mutmut
    # was chosen over cosmic-ray: its coverage-guided test selection
    # is ~90x faster on this Z3/WASM suite, and its copy-based model
    # never mutates the working tree in place.  See MUTATION.md.
    "vera[dev]",
    "mutmut>=3.6",
    "pytest-timeout>=2.4",
    # scripts/mutation_report.py renders the per-module chart with matplotlib;
    # optional at runtime (the script skips the PNG if it is absent), but
    # pinned here so `pip install -e ".[mutation]"` produces the chart.
    "matplotlib>=3.7",
]

[project.scripts]
vera = "vera.cli:main"

[tool.setuptools.packages.find]
include = ["vera*"]

[tool.setuptools.package-data]
"vera" = ["*.lark"]
"vera.browser" = ["*.mjs"]

[build-system]
requires = ["setuptools>=83.0.0"]
build-backend = "setuptools.build_meta"

[tool.pytest.ini_options]
testpaths = ["tests"]
# Stress tests (#596) are skipped from the default per-PR pytest
# run.  They exercise programs at scale (10K-element arrays,
# 1K-deep recursion, 100K Map mutations, etc.) to catch
# scale-dependent codegen/runtime bugs of the #570/#515/#593
# class.  Run via `pytest -m stress`, or as part of the nightly
# CI workflow.
markers = [
    "stress: scale-dependent regression tests (#596); skipped by default, run via -m stress or nightly CI",
]
addopts = "-m 'not stress'"

[tool.mutmut]
# Mutation testing (#387).  See MUTATION.md for the full runbook.
# Mutate the whole compiler by default; scope a single sweep to one
# module with `only_mutate`.
source_paths = ["vera/"]
# Soundness core (#387 first pass).  The whole-tree sweep is deferred:
# codegen/api.py's ~3,500-line execute() makes mutmut inline a 774 MB
# mutant file it can't index — impractical until #421 decomposes it.
# The big wasm/calls_*.py files (28-67 MB) are likewise out of this pass.
only_mutate = [
    "vera/verifier.py",
    "vera/smt.py",
    "vera/checker/*",
    "vera/obligations/*",
]
# mutmut copies tests/ + config but nothing else by default; the
# in-process oracle also reads these repo files (the example round-trips in
# test_codegen_infrastructure / _effects / _strings; test_errors'
# error-display-sync against README / docs / spec), so the ./mutants/ copy
# needs them or pytest errors at collection.
also_copy = ["examples/", "README.md", "docs/", "spec/"]
# `mutmut run` copies the project to ./mutants/ and runs the suite there,
# so the working tree is never mutated in place.
use_setproctitle = false  # required on macOS (mutmut PR #450)
# Z3 / wasmtime headroom: a generous per-test cap so a slow-but-solvable
# mutant is not misread as an unkillable timeout survivor.
pytest_add_cli_args = ["--timeout=300"]
# In-process oracle (positive selection).  Only these suites build Vera
# programs inline (or from examples/, copied above) and exercise the
# compiler in-process, so they work inside the ./mutants/ copy and can
# kill mutants.  Deliberately omitted: subprocess / Node suites
# (test_conformance / test_cli / test_browser spawn a fresh `vera` that
# imports the UN-mutated package) and tooling suites (test_check_* /
# test_build_site exercise scripts/, not vera/, and read repo files the
# copy lacks).  Code reached only through the omitted suites is reported
# "not checked", not a weak test — see MUTATION.md "Oracle".
pytest_add_cli_args_test_selection = [
    "tests/test_verifier_contracts.py",
    "tests/test_verifier_nat_obligations.py",
    "tests/test_verifier_primitive_ops.py",
    "tests/test_verifier_calls_modules.py",
    "tests/test_verifier_adt_decreases.py",
    "tests/test_verifier_refinements.py",
    "tests/test_verifier_shadow_audits.py",
    "tests/test_verifier_mutation_obligations.py",
    "tests/test_verifier_mutation_gates_smt.py",
    "tests/test_verifier_coverage.py",
    "tests/test_obligations.py",
    "tests/test_checker_types.py",
    "tests/test_checker_patterns.py",
    "tests/test_checker_functions.py",
    "tests/test_checker_effects.py",
    "tests/test_checker_modules.py",
    "tests/test_checker_errors.py",
    "tests/test_checker_builtins_collections.py",
    "tests/test_checker_builtins_strings.py",
    "tests/test_codegen_expressions.py",
    "tests/test_codegen_calls.py",
    "tests/test_codegen_infrastructure.py",
    "tests/test_codegen_interpolation.py",
    "tests/test_codegen_effects.py",
    "tests/test_codegen_data_types.py",
    "tests/test_codegen_arrays.py",
    "tests/test_codegen_refinements.py",
    "tests/test_codegen_strings.py",
    "tests/test_codegen_string_builtins.py",
    "tests/test_codegen_numeric.py",
    "tests/test_codegen_io.py",
    "tests/test_codegen_collections.py",
    "tests/test_codegen_json.py",
    "tests/test_codegen_decimal.py",
    "tests/test_codegen_host_effects.py",
    "tests/test_codegen_nat_guards.py",
    "tests/test_codegen_translator_fixes.py",
    "tests/test_codegen_gc_alloc.py",
    "tests/test_codegen_gc_rooting.py",
    "tests/test_codegen_gc_reclamation.py",
    "tests/test_codegen_contracts.py",
    "tests/test_codegen_monomorphize.py",
    "tests/test_codegen_closures.py",
    "tests/test_codegen_modules.py",
    "tests/test_codegen_coverage.py",
    "tests/test_wasm.py",
    "tests/test_wasm_coverage.py",
    "tests/test_monomorphize_differential.py",
    "tests/test_lsp.py",
    "tests/test_parser.py",
    "tests/test_ast.py",
    "tests/test_formatter.py",
    "tests/test_types.py",
    "tests/test_errors.py",
    "tests/test_tester.py",
    "tests/test_tester_coverage.py",
    "tests/test_markdown.py",
    "tests/test_resolver.py",
    "tests/test_prelude.py",
    "tests/test_walker_defensive_branches_597.py",
    "tests/test_execute_characterization.py",
]

[tool.mypy]
python_version = "3.11"
strict = true

[[tool.mypy.overrides]]
# Lark transformer methods are dynamically named callbacks that take
# untyped `args` lists — strict annotations are impractical here.
module = "vera.transform"
disallow_untyped_defs = false
disallow_any_generics = false
no_implicit_reexport = false
warn_return_any = false

[[tool.mypy.overrides]]
# z3-solver does not ship py.typed or stubs.
module = "z3.*"
ignore_missing_imports = true

[[tool.mypy.overrides]]
# wasmtime does not ship complete type stubs.
module = "wasmtime.*"
ignore_missing_imports = true

[[tool.mypy.overrides]]
# pygls ships partial typing; lsprotocol is typed but the override is
# defensive for transitive attrs.  CI runs mypy strict over vera/lsp/.
module = ["pygls.*", "lsprotocol.*"]
ignore_missing_imports = true

[[tool.mypy.overrides]]
# pygls' @server.feature(...) decorator is untyped, which strict mode
# rejects on every handler registration.  Same narrow-exception shape
# as the vera.transform override above.
module = "vera.lsp.server"
disallow_untyped_decorators = false

[[tool.mypy.overrides]]
# Checker mixin classes reference attributes (self.env, self._error, etc.)
# that live on the composed TypeChecker class in core.py.  Mypy cannot
# resolve these across mixin boundaries, so we suppress attr-defined and
# the resulting no-any-return errors in the mixin modules.
module = [
    "vera.checker.resolution",
    "vera.checker.modules",
    "vera.checker.registration",
    "vera.checker.expressions",
    "vera.checker.calls",
    "vera.checker.control",
]
disable_error_code = ["attr-defined", "no-any-return", "has-type"]

[[tool.mypy.overrides]]
# WASM mixin classes reference attributes (self.string_pool, self.alloc_local,
# etc.) that live on the composed WasmContext class in context.py.  Same
# mixin pattern as the checker modules above.
module = [
    "vera.wasm.context",
    "vera.wasm.inference",
    "vera.wasm.operators",
    "vera.wasm.calls",
    "vera.wasm.calls_arrays",
    "vera.wasm.calls_containers",
    "vera.wasm.calls_encoding",
    "vera.wasm.calls_handlers",
    "vera.wasm.calls_markup",
    "vera.wasm.calls_math",
    "vera.wasm.calls_parsing",
    "vera.wasm.calls_strings",
    "vera.wasm.closures",
    "vera.wasm.data",
]
disable_error_code = ["attr-defined", "no-any-return", "has-type"]

[[tool.mypy.overrides]]
# Codegen mixin classes reference attributes (self._fn_sigs, self.string_pool,
# etc.) that live on the composed CodeGenerator class in core.py.  Same
# mixin pattern as the checker and wasm modules above.
module = [
    "vera.codegen.modules",
    "vera.codegen.registration",
    "vera.codegen.monomorphize",
    "vera.codegen.functions",
    "vera.codegen.closures",
    "vera.codegen.contracts",
    "vera.codegen.assembly",
    "vera.codegen.compilability",
]
disable_error_code = ["attr-defined", "no-any-return", "has-type"]