Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .claude/CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ package definitions (not metadata files) and must NOT be deleted.
| **Guile Scheme** | Guix package definitions (`guix.scm`, `manifests/*.scm`) | `.scm` metadata files are deprecated — see below |
| **Bash/POSIX Shell** | Build scripts, CI glue | Keep minimal |
| **AffineScript** | TEA sources in `src/ui/tea/`; static shell in `src/ui/public/` | The compile pipeline is unavailable; `build-ui` fails explicitly |
| **Bun** | Estate JavaScript runtime | The legacy serve recipes still require migration; open `src/ui/public/prove.html` directly for the working static UI |
| **Bun** | Estate JavaScript runtime | `just serve-ui` serves the static shell via `scripts/serve-static.js` (Bun) |
| **JavaScript** | Build tooling only (Tailwind config, test harness) | Not for business logic |
| **OCaml** | AffineScript compiler host | Decision locked — AffineScript selected for UI |
| **Nickel** | Configuration language | Used across `configs/`, `echidna-playground/contractiles/k9/`, `.machine_readable/`, `echidnabot/config/` (11+ `.ncl` files) |
Expand Down
2 changes: 1 addition & 1 deletion .echidnabot.toml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ coq = { enabled = true, priority = "low" }
lean = { enabled = true, priority = "low" }

[provers.idris2]
package_file = "src/abi/echidna.ipkg"
package_file = "src/abi/echidnaabi.ipkg"
source_dirs = ["src/abi"]
totality_required = true
coverage_required = true
Expand Down
2 changes: 1 addition & 1 deletion .github/CODEOWNERS
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

# Core prover backends
/src/rust/provers/ @hyperpolymath
/src/rust/core.rs @hyperpolymath
/src/rust/lib.rs @hyperpolymath
/src/rust/dispatch.rs @hyperpolymath

# ML layer
Expand Down
91 changes: 91 additions & 0 deletions .github/ISSUE_TEMPLATE/bug_report.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
# SPDX-License-Identifier: CC-BY-SA-4.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
{
name: "Bug report",
description: "Something behaves differently from what it claims to do.",
labels: [
"bug",
"needs-triage",
],
body: [
{
type: "markdown",
attributes: {
value: "Please report what you **observed**, not what you inferred. A command and\nits actual output is worth more than a description of the problem.\n",
},
},
{
type: "textarea",
id: "what-happened",
attributes: {
label: "What happened",
description: "The observed behaviour, with the exact command and its output.",
placeholder: "$ just verify\nerror: ...\n",
render: "shell",
},
validations: {
required: true,
},
},
{
type: "textarea",
id: "expected",
attributes: {
label: "What you expected instead",
},
validations: {
required: true,
},
},
{
type: "textarea",
id: "repro",
attributes: {
label: "Minimal reproduction",
description: "The shortest sequence that reproduces it from a clean checkout.",
},
validations: {
required: true,
},
},
{
type: "input",
id: "version",
attributes: {
label: "Version / commit",
description: "Output of `git rev-parse --short HEAD`.",
},
validations: {
required: true,
},
},
{
type: "textarea",
id: "environment",
attributes: {
label: "Environment",
description: "OS, and the output of `just --version` and `mise current` if relevant.",
},
validations: {
required: false,
},
},
{
type: "checkboxes",
id: "checks",
attributes: {
label: "Before submitting",
options: [
{
label: "I have reported observed output rather than a summary of it.",
required: true,
},
{
label: "This is not a security vulnerability (those go via a private advisory).",
required: true,
},
],
},
},
],
}
20 changes: 20 additions & 0 deletions .github/ISSUE_TEMPLATE/config.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
# SPDX-License-Identifier: CC-BY-SA-4.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
#
# Issue chooser configuration. Blank issues stay enabled so that reports which
# fit neither form are not silently discouraged.
{
blank_issues_enabled: true,
contact_links: [
{
name: "Security vulnerability",
url: "https://github.com/hyperpolymath/echidna/security/advisories/new",
about: "Report privately via a security advisory. Do NOT open a public issue.",
},
{
name: "Question or support request",
url: "https://github.com/hyperpolymath/echidna/discussions",
about: "Ask a question. See .github/SUPPORT.md for what to expect.",
},
],
}
60 changes: 60 additions & 0 deletions .github/ISSUE_TEMPLATE/feature_request.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
# SPDX-License-Identifier: CC-BY-SA-4.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
{
name: "Feature request",
description: "Propose a capability this project does not yet have.",
labels: [
"enhancement",
"needs-triage",
],
body: [
{
type: "textarea",
id: "problem",
attributes: {
label: "The problem",
description: "What are you unable to do today? Describe the situation, not the solution.",
},
validations: {
required: true,
},
},
{
type: "textarea",
id: "proposal",
attributes: {
label: "Proposed change",
},
validations: {
required: true,
},
},
{
type: "textarea",
id: "alternatives",
attributes: {
label: "Alternatives considered",
description: "Including doing nothing — say why that is insufficient.",
},
validations: {
required: false,
},
},
{
type: "dropdown",
id: "scope",
attributes: {
label: "Scope",
description: "Would this change the template's shape, and therefore every repo minted from it?",
options: [
"Repo-local — affects only this project",
"Template-wide — would propagate to minted repos",
"Not sure",
],
},
validations: {
required: true,
},
},
],
}
2 changes: 1 addition & 1 deletion SECURITY.md → .github/SECURITY.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@ Report vulnerabilities privately using [GitHub Security Advisories](https://gith
If GitHub is unavailable, contact the maintainer at j.d.a.jewell@open.ac.uk.
Do not disclose vulnerabilities in public issues.

The full policy, supported versions, requested report details, and response timelines are maintained in [SECURITY.adoc](SECURITY.adoc).
The full policy, supported versions, requested report details, and response timelines are maintained in [SECURITY.adoc](../SECURITY.adoc).
7 changes: 7 additions & 0 deletions .github/SUPPORT.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
# Support

For questions, help, and community discussion:

- GitHub Discussions: https://github.com/hyperpolymath/echidna/discussions
- GitHub Issues: https://github.com/hyperpolymath/echidna/issues
- Documentation: See README.adoc in the root directory.
67 changes: 32 additions & 35 deletions .github/canonical-references/prover-counts.yml
Original file line number Diff line number Diff line change
Expand Up @@ -13,38 +13,35 @@
#
# Rule format documented in the upstream step comment.

id: prover-counts
description: |
Bare prover counts (variants vs impl files vs advertised vs core)
in narrative-carrying top-level docs must defer to
docs/PROVER_COUNT.adoc so they cannot drift. Patterns are anchored
with (^|[[:space:]]) so neighbours like Tier-1, v1.2.3, port 8081
don't false-positive.

patterns:
- '(^|[[:space:]])[0-9]+[[:space:]]+prover[[:space:]]+backends?\b'
- '(^|[[:space:]])[0-9]+[[:space:]]*-[[:space:]]*prover[[:space:]]+core\b'
- '(^|[[:space:]])[0-9]+[[:space:]]+core[[:space:]]+(backends?|provers?)\b'
- '(^|[[:space:]])[0-9]+[[:space:]]+(backends?|provers?)[[:space:]]+(operational|advertised|implemented|available|across|total)\b'
- '(^|[[:space:]])[0-9]+[[:space:]]+ProverKind[[:space:]]+variants?\b'
- '(^|[[:space:]])[0-9]+[[:space:]]+backend[[:space:]]+implementation[[:space:]]+files?\b'
- '(^|[[:space:]])[0-9]+/[0-9]+[[:space:]]+(backends?|provers?)\b'

canonical_pointer: docs/PROVER_COUNT.adoc

scope:
include:
- README.md
- README.adoc
- EXPLAINME.adoc
- CLAUDE.md
- CONTRIBUTING.md
- ../../.github/CONTRIBUTING.md
- QUICKSTART-USER.adoc
- QUICKSTART-DEV.adoc
- QUICKSTART-MAINTAINER.adoc
- RSR_COMPLIANCE.adoc
- SECURITY.md
- MAINTAINERS.adoc
- AUTHORS.adoc
- CODE_OF_CONDUCT.adoc
{
id: "prover-counts",
description: "Bare prover counts (variants vs impl files vs advertised vs core)\nin narrative-carrying top-level docs must defer to\ndocs/PROVER_COUNT.adoc so they cannot drift. Patterns are anchored\nwith (^|[[:space:]]) so neighbours like Tier-1, v1.2.3, port 8081\ndon't false-positive.\n",
patterns: [
"(^|[[:space:]])[0-9]+[[:space:]]+prover[[:space:]]+backends?\\b",
"(^|[[:space:]])[0-9]+[[:space:]]*-[[:space:]]*prover[[:space:]]+core\\b",
"(^|[[:space:]])[0-9]+[[:space:]]+core[[:space:]]+(backends?|provers?)\\b",
"(^|[[:space:]])[0-9]+[[:space:]]+(backends?|provers?)[[:space:]]+(operational|advertised|implemented|available|across|total)\\b",
"(^|[[:space:]])[0-9]+[[:space:]]+ProverKind[[:space:]]+variants?\\b",
"(^|[[:space:]])[0-9]+[[:space:]]+backend[[:space:]]+implementation[[:space:]]+files?\\b",
"(^|[[:space:]])[0-9]+/[0-9]+[[:space:]]+(backends?|provers?)\\b",
],
canonical_pointer: "docs/PROVER_COUNT.adoc",
scope: {
include: [
"README.md",
"README.adoc",
"EXPLAINME.adoc",
"CLAUDE.md",
"CONTRIBUTING.md",
"../../.github/CONTRIBUTING.md",
"QUICKSTART-USER.adoc",
"QUICKSTART-DEV.adoc",
"QUICKSTART-MAINTAINER.adoc",
"RSR_COMPLIANCE.adoc",
"SECURITY.adoc",
"MAINTAINERS.adoc",
"AUTHORS.adoc",
"CODE_OF_CONDUCT.adoc",
],
},
}
89 changes: 89 additions & 0 deletions .github/copilot-instructions.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
<!--
Comment thread
hyperpolymath marked this conversation as resolved.
Fixed
SPDX-License-Identifier: CC-BY-SA-4.0
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
<!-- Authoritative source: docs/practice/AI-CONVENTIONS.adoc -->

# Copilot Instructions

## Before Writing Code

- Read `.machine_readable/descriptiles/` (STATE, META, ECOSYSTEM) for canonical
file locations. echidna has not yet migrated these into a `*_chora.deed`.
- State files (.a2ml) live in `.machine_readable/` ONLY, never the root.

## License

- SPDX: `MPL-2.0` on all new files.
- Never use AGPL-3.0.
- Copyright: `Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>`

## Code Style

- Use descriptive variable names.
- Annotate and document all files.
- Add SPDX header to every source file.
- Use `just` for build/test/lint commands.

## Banned Patterns

- Idris2: no `believe_me`, no `assert_total`
- Haskell: no `unsafeCoerce`, no `unsafePerformIO`
- OCaml: no `Obj.magic`
- Coq: no `Admitted`
- Lean: no `sorry`
- Rust: no `transmute` unless FFI with `// SAFETY:` comment

## JavaScript / TypeScript runtimes

Ordered preference (`standards/3-practice/LANGUAGE-POLICY.adoc` §1) — reach for the first
that can do the job:

1. **Bun** — default for all new work. Runs compiled ESM/JS directly, no bundler
step. Uses an npm-compatible `package.json` plus `bun.lock`; both are
expected, not anti-patterns.
2. **pnpm** — only where an upstream toolchain requires `node_modules`.
3. **npm** — last resort. Permitted, never preferred; a deliberate, noted choice.

**Deno is being removed**, not grandfathered. Owner ruling 2026-08-26: *"deno is
to go and bun is the way we are going, put it first everywhere unless not
possible and explain why if not."* Existing Deno projects migrate to Bun; where
Bun genuinely cannot be used, document the reason in the repo.

**TypeScript is not the language for new application code — AffineScript is.**
`LANGUAGE-POLICY.adoc` §1.2, ruled 2026-08-25, separates two questions the older
text ran together: *runtime* is Bun (where `.ts` runs at all, Bun runs it), while
the *language* target is AffineScript. TypeScript is permitted only where
AffineScript cannot reach — the same narrow, transitional carve-out JavaScript
holds for MCP protocol glue and runtime APIs. ReScript remains banned; its
migration destination is AffineScript.

## Banned Languages

- No Go (use Rust)
- No Python (use Julia or Rust)
- No Nix (use Guix)
- No Deno for new work — being removed estate-wide; use Bun (owner ruling 2026-08-26)
- No ReScript (`LANGUAGE-POLICY.adoc` §3) — migrate to AffineScript

## Containers

- Use Podman, never Docker.
- Name the file `Containerfile`, never `Dockerfile`.
- Base image: `cgr.dev/chainguard/wolfi-base:latest`.

## ABI/FFI

- ABI definitions in Idris2 (`src/abi/`, package `src/abi/echidnaabi.ipkg`).
- FFI implementations in Zig (`ffi/zig/`, `src/zig_ffi/`).
- echidna keeps its own ABI/FFI layout rather than the template's interface tree.

## State Files

The retired STATE/META/ECOSYSTEM/AGENTIC/CLADE `.a2ml` files must not be
recreated anywhere; their content is in the repo deed (`*_chora.deed`) and
`docs/status/ROADMAP.adoc`.

Never create NEUROSYM.a2ml or PLAYBOOK.a2ml in the repo root.
They belong in `.machine_readable/` only.
22 changes: 16 additions & 6 deletions .github/copilot/coding-agent.yml
Original file line number Diff line number Diff line change
@@ -1,6 +1,16 @@
mcp_servers:
boj-server:
command: npx
args: ["-y", "@hyperpolymath/boj-server@latest"]
env:
BOJ_URL: http://localhost:7700
# SPDX-License-Identifier: MPL-2.0
# Copilot coding-agent MCP servers, launched with bunx (Bun is the estate
# JavaScript runtime).
{
mcp_servers: {
boj-server: {
command: "bunx",
args: [
"@hyperpolymath/boj-server@latest",
],
env: {
BOJ_URL: "http://localhost:7700",
},
},
},
}
Loading
Loading