Skip to content
Closed
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
36 changes: 3 additions & 33 deletions .github/CODEOWNERS
Original file line number Diff line number Diff line change
@@ -1,34 +1,4 @@
# SPDX-License-Identifier: MPL-2.0
# CODEOWNERS - Define code review assignments for GitHub
# See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners

# Default: sole maintainer for all files
* @hyperpolymath

# Security-sensitive files require explicit ownership
SECURITY.md @hyperpolymath
.github/workflows/ @hyperpolymath
.machine_readable/ @hyperpolymath
contractiles/ @hyperpolymath

# License files
LICENSE @hyperpolymath
LICENSES/ @hyperpolymath

# Configuration
.gitignore @hyperpolymath
.github/ @hyperpolymath

# Documentation
README* @hyperpolymath
CONTRIBUTING* @hyperpolymath
CODE_OF_CONDUCT* @hyperpolymath
GOVERNANCE* @hyperpolymath
MAINTAINERS* @hyperpolymath
CHANGELOG* @hyperpolymath
ROADMAP* @hyperpolymath

# Build and CI
Justfile @hyperpolymath
Makefile @hyperpolymath
*.sh @hyperpolymath
# Solo-maintained hyperpolymath repo: no owner lines by policy.
# See hyperpolymath/standards CODEOWNERS-POLICY.adoc (Rule 1).
# Sole-maintainer review is moot; SPDX headers carry attribution.
2 changes: 1 addition & 1 deletion .machine_readable/contractiles/dust/Dustfile.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ to new repositories.
- description: No references to betlang in generic template files
- run: test -z "$(grep -r 'betlang' machine-readable-design/ 2>/dev/null)"
- severity: warning
- notes: Generic templates should use {{PROJECT_NAME}} or similar placeholders
- notes: Generic templates should use BetLang or similar placeholders

### version-sync-checked
- description: Version in canonical-directory-structure matches .machine_readable/contractiles
Expand Down
17 changes: 17 additions & 0 deletions 0-AI-MANIFEST.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -67,3 +67,20 @@ license: MPL-2.0
2. Read `.machine_readable/STATE.scm` for current progress
3. Read `.machine_readable/META.scm` for architecture decisions
4. Read `.machine_readable/ECOSYSTEM.scm` for ecosystem context

<!-- BEGIN requires-initialisation -->

## PRIORITY ACTION — this repository is not fully initialised

4 substitution token(s) still have no value. **Read
`REQUIRES_INITIALISATION.md` in the repository root before doing anything
else here** — it lists every outstanding token, what it means, and which
files it belongs in.

Do not fabricate values for them, and do not delete the sections that
contain them to quiet a gate. They are unfilled because they need a
decision, not because they were overlooked. Resolve what you legitimately
can, leave the rest, and delete `REQUIRES_INITIALISATION.md` only when
nothing outstanding remains.

<!-- END requires-initialisation -->
4 changes: 2 additions & 2 deletions ABI-FFI-README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
{{~ Aditionally delete this line and fill out the template below ~}}

# {{PROJECT}} ABI/FFI Documentation
# BETLANG ABI/FFI Documentation

## Overview

Expand Down Expand Up @@ -251,7 +251,7 @@ gcc -o example example.c -l{{project}} -L./zig-out/lib
### From Idris2

```idris
import {{PROJECT}}.ABI.Foreign
import BETLANG.ABI.Foreign

main : IO ()
main = do
Expand Down
47 changes: 0 additions & 47 deletions ARCHITECTURE.md

This file was deleted.

2 changes: 1 addition & 1 deletion PROOF-NEEDS.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ trusted-base-reduction policy and must be registered in
Template ABI removed — was creating a false impression of formal
verification. The removed files (`Types.idr`, `Layout.idr`,
`Foreign.idr`) contained only RSR template scaffolding with unresolved
`{{PROJECT}}`/`{{AUTHOR}}` placeholders and no domain-specific proofs.
`BETLANG`/`Jonathan D.A. Jewell` placeholders and no domain-specific proofs.

When this project needs formal ABI verification (obligations **ABI-1..5**
above, Phase 3), create domain-specific Idris2 proofs following the
Expand Down
70 changes: 70 additions & 0 deletions REQUIRES_INITIALISATION.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

# REQUIRES INITIALISATION

**This repository is not finished being set up.** 4 substitution token(s) across 2 file(s) still have no value.

## Why this is not already done

This repo was created from `hyperpolymath/rsr-template-repo`. The mint
(`just repo-init`) fills every token that has a single mechanical answer —
owner, repo, author, dates, licence, branch — and it has done so here.

The tokens below are the ones it *deliberately cannot* answer. They need a
decision or a fact that exists only in your head: what this project is for,
what command builds it, which port the service listens on, whether a PGP key
is held at all. The template's own token vocabulary says as much — you cannot
sensibly answer "required invariants" in a thirty-second bootstrap.

They were left **visibly unfilled on purpose**. The alternatives were both
worse: inventing plausible values would put confident falsehoods into a
security policy and an architecture document, and silently deleting the
sections would hide the fact that a decision is owed. A visible gap is
honest; a fabricated answer is not.

## Do not delete this file until every item below is resolved

This file is the only marker that the work is outstanding. Deleting it early
does not finish the setup, it just conceals it — and the next person or agent
to arrive will reasonably assume the repo is complete.

- **If you are a person:** delete this file yourself once the last item is done.
- **If you are an agent:** resolve what you legitimately can, leave the rest,
and delete this file only when no token below remains anywhere in the tree.
Do not delete it to make a gate go green.

Re-running the estate top-up tool will remove this file automatically once
nothing is outstanding, so the safest way to finish is to fix the tokens and
let the check confirm it.

## What is needed, and where it goes

### `{{FILE}}`

Appears in:

- `Justfile`

### `{{INPUT}}`

Appears in:

- `julia-backend/Justfile`

### `{{OUTPUT}}`

Appears in:

- `julia-backend/Justfile`

### `{{TARGET}}`

Appears in:

- `Justfile`

---

Generated by the estate top-up pass. Rationale and the governing rulings are
in `hyperpolymath/standards`; the token vocabulary is
`.machine_readable/ai/PLACEHOLDERS.adoc` in `rsr-template-repo`.
2 changes: 1 addition & 1 deletion ffi/zig/build.zig
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// {{PROJECT}} FFI Build Configuration
// BETLANG FFI Build Configuration

const std = @import("std");

Expand Down
4 changes: 2 additions & 2 deletions ffi/zig/src/main.zig
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// {{PROJECT}} FFI Implementation
// BETLANG FFI Implementation

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Quality: Placeholder filled with "BETLANG" contradicts canonical "BetLang"

The PR says the project name was taken from the README H1, but that H1 is "BetLang" (mixed case), yet {{PROJECT}} was filled with all-caps "BETLANG" in ffi/zig/src/main.zig, playground/ffi/zig/src/main.zig, ffi/zig/build.zig, ABI-FFI-README.md and PROOF-NEEDS.md. Notably the Dustfile edit in this same PR correctly uses "BetLang", so the PR is internally inconsistent. The rest of the tree (julia-backend/src/BetLang.jl, proofs/BetLang.lean, README) uses "BetLang". Recommend normalizing these fills to "BetLang" to match the canonical name; the Idris import import BETLANG.ABI.Foreign in ABI-FFI-README.md is especially misleading since the module is named BetLang elsewhere.

Was this helpful? React with 👍 / 👎

//
// This module implements the C-compatible FFI declared in src/abi/Foreign.idr
// All types and layouts must match the Idris2 ABI definitions.
Expand All @@ -10,7 +10,7 @@ const std = @import("std");

// Version information (keep in sync with project)
const VERSION = "0.1.0";
const BUILD_INFO = "{{PROJECT}} built with Zig " ++ @import("builtin").zig_version_string;
const BUILD_INFO = "BETLANG built with Zig " ++ @import("builtin").zig_version_string;

/// Thread-local error storage
threadlocal var last_error: ?[]const u8 = null;
Expand Down
2 changes: 1 addition & 1 deletion ffi/zig/test/integration_test.zig
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// {{PROJECT}} Integration Tests
// BETLANG Integration Tests
//
// These tests verify that the Zig FFI correctly implements the Idris2 ABI

Expand Down
2 changes: 1 addition & 1 deletion playground/ffi/zig/build.zig
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// {{PROJECT}} FFI Build Configuration
// BETLANG FFI Build Configuration

const std = @import("std");

Expand Down
4 changes: 2 additions & 2 deletions playground/ffi/zig/src/main.zig
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// {{PROJECT}} FFI Implementation
// BETLANG FFI Implementation
//
// This module implements the C-compatible FFI declared in src/abi/Foreign.idr
// All types and layouts must match the Idris2 ABI definitions.
Expand All @@ -10,7 +10,7 @@ const std = @import("std");

// Version information (keep in sync with project)
const VERSION = "0.1.0";
const BUILD_INFO = "{{PROJECT}} built with Zig " ++ @import("builtin").zig_version_string;
const BUILD_INFO = "BETLANG built with Zig " ++ @import("builtin").zig_version_string;

/// Thread-local error storage
threadlocal var last_error: ?[]const u8 = null;
Expand Down
2 changes: 1 addition & 1 deletion playground/ffi/zig/test/integration_test.zig
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// {{PROJECT}} Integration Tests
// BETLANG Integration Tests
//
// These tests verify that the Zig FFI correctly implements the Idris2 ABI

Expand Down
Loading