Skip to content

test(idris2): port DSL + playground test suites from Racket/TS#22

Merged
hyperpolymath merged 1 commit into
mainfrom
feat/port-tests-to-idris2
May 20, 2026
Merged

test(idris2): port DSL + playground test suites from Racket/TS#22
hyperpolymath merged 1 commit into
mainfrom
feat/port-tests-to-idris2

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Estate ports 5a/11 (DSL) + 5b/11 (playground) — converts the betlang test surface to Idris2 under the cladistic `Test.Spec` harness used by ipfs-overlay, format-registrations, awesome-nickel, etc.

Originally tagged DEFERRED ("multi-week language reimpl") in the estate bimodal-rollout — pragmatic re-scoping landed it as the same content-validation + pure-logic shape that the other estate ports use, no Racket runtime required.

What ported

`tests/idris2/` (DSL — content-validation)

  • DslStructureTest — 16 unit tests: file existence, `#lang racket` declarations, SPDX coverage, primitive provides, structural substring checks across the 8 `.rkt` source files
  • DslContractsTest — 12 INVARIANT tests pinning documented contracts (ternary shape, weighted-3 enforcement, seed reproducibility, entropy bounds, 25-test `basics.rkt` coverage, `bet-parallel` list-comprehension form)

`playground/tests/idris2/` (hybrid: pure-logic + content-validation)

  • PlaygroundTernaryTest — 13 tests; inline Idris2 reimplementation of the Kleene 3-value logic (`Tri/notT/andT/orT/impliesT/betT`). De Morgan + commutativity property checks over all 9 `Tri` pairs.
  • PlaygroundProbabilityTest — 12 tests; pure-logic port of `Branch/betWeighted/betConditional/analyticEV`. mulberry32 PRNG falls back to content-validation.
  • PlaygroundStructureTest — 14 tests; SPDX + structural checks across the 4 `.ts` files and `deno.json`.

Totals

67 / 67 tests PASS on idris2 0.8.0:

  • DSL: 28 / 28 PASS
  • Playground: 39 / 39 PASS

SPDX coverage note

Only the 2 `conformance/*.rkt` files carry SPDX headers. `DslStructureTest` pins current truth (asserts those two specifically) rather than failing on absent headers across the other 6 files. Backfilling SPDX across `core/` + `lib/` + `tests/basics.rkt` is tracked separately in the estate licence-debt ledger.

Test plan

  • Local: `idris2 --build betlang-tests.ipkg` clean compile, 28 PASS
  • Local: `cd playground && idris2 --build playground-tests.ipkg` clean compile, 39 PASS
  • CI: dogfood-gate workflow picks up the new ipkg files

🤖 Generated with Claude Code

Estate ports 5a/11 + 5b/11 — converts the betlang test surface to Idris2
under the same cladistic Test.Spec harness used by ipfs-overlay,
format-registrations, awesome-nickel, etc.

tests/idris2/ (DSL, content-validation):
  - DslStructureTest    16 unit tests: file existence, #lang racket,
                        SPDX coverage, primitive provides, structural
                        substring checks across 8 .rkt source files
  - DslContractsTest    12 INVARIANT tests pinning the documented
                        contracts (ternary shape, weighted-3 enforcement,
                        seed reproducibility, entropy bounds, 25-test
                        basics coverage, parallel list-comprehension form)
  - Total 28 tests; all PASS

playground/tests/idris2/ (hybrid: pure-logic + content-validation):
  - PlaygroundTernaryTest    13 tests; inline Idris2 reimpl of the
                             Kleene 3-value logic (Tri/notT/andT/orT/
                             impliesT/betT). De Morgan + truth-table
                             property checks over all 9 pairs.
  - PlaygroundProbabilityTest 12 tests; pure-logic port of Branch/
                              betWeighted/betConditional/analyticEV.
                              mulberry32 PRNG falls back to content-
                              validation (no clean Idris2 port for the
                              bitwise-uint32 arithmetic).
  - PlaygroundStructureTest  14 tests; SPDX + structural checks across
                             the 4 .ts files and deno.json.
  - Total 39 tests; all PASS

Local build verified on idris2 0.8.0 with the standard estate
incantation (IDRIS2_PREFIX/IDRIS2_DATA/IDRIS2_PACKAGE_PATH/
LD_LIBRARY_PATH). 67/67 PASS total across both suites.

SPDX coverage note: only the 2 conformance/*.rkt files carry SPDX
headers. The DSL structure test pins current truth (asserts those
two specifically) rather than failing on absent headers across the
other 6 .rkt source files. Backfilling SPDX across core/ + lib/ +
tests/basics.rkt is filed separately as part of the licence-debt
ledger (estate-wide scaffold-placeholder sweep).

Closes the 2026-05-20 bimodal-rollout DEFERRED tags on betlang in
the estate test rollout campaign.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 0624c1e into main May 20, 2026
12 of 24 checks passed
@hyperpolymath hyperpolymath deleted the feat/port-tests-to-idris2 branch May 20, 2026 13:57
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 56 issues detected

Severity Count
🔴 Critical 9
🟠 High 18
🟡 Medium 29

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Merge artifact in root",
    "type": "stale",
    "file": "SPEC.core.scm.orig",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No permissions declaration -- add permissions: read-all",
    "type": "missing_permissions",
    "file": "comprehensive-quality.yml",
    "action": "add_permissions",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/main.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/probability.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/ternary.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/test/probability_test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/test/ternary_test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant