Skip to content
Open
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 .github/workflows/idris2-proof.yml
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ jobs:
run: |
set -euo pipefail
idris2 --install anytype.ipkg
idris2 --install abi.ipkg
idris2 --install src/interface/abi.ipkg
idris2 --build anytype-tests.ipkg
./build/exec/anytype-tests
idris2 --build anytype-cli.ipkg
Expand Down
4 changes: 4 additions & 0 deletions CHANGELOG.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,10 @@ explicit honesty notice that no working checker exists yet (the

==== Added

* `+README.adoc+` §"Relationship to ephapax (design reference only)":
ephapax uses anytype as a design reference only. There is no code or
build dependency (per the kernel ruling D-2026-10-12), and no soundness
proof exists for the relationship.
* Instantiated identity descriptiles (CLADE/ECOSYSTEM/ANCHOR/STATE/META)
and the AFFIRMATION honesty snapshot with the anytype identity and an
honest early-stage status; ANCHOR pins systemet upstream.
Expand Down
2 changes: 1 addition & 1 deletion Justfile
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@
@echo "Version: {{version}}"
@echo "RSR Tier: {{tier}}"
@echo "Recipes: $(just --summary | wc -w)"
@[ -f ".machine_readable/6a2/STATE.a2ml" ] && grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/6a2/STATE.a2ml | head -1 | xargs -I{} echo "Phase: {}" || true

Check failure on line 55 in Justfile

View workflow job for this annotation

GitHub Actions / Hypatia neurosymbolic scan

[hypatia] CI policy requires a retired descriptile path; align the check with .machine_readable/descriptiles/

# Run Invariant Path overlay tools for this repository
invariant-path *ARGS:
Expand Down Expand Up @@ -135,7 +135,7 @@
test *args:
@command -v idris2 >/dev/null || { echo "FAIL: idris2 not on PATH (install Idris2 0.7.0)"; exit 1; }
idris2 --install anytype.ipkg
idris2 --install abi.ipkg
idris2 --install src/interface/abi.ipkg
idris2 --build anytype-tests.ipkg
./build/exec/anytype-tests
idris2 --build anytype-cli.ipkg
Expand Down Expand Up @@ -434,7 +434,7 @@

# Update STATE.a2ml timestamp
state-touch:
@if [ -f ".machine_readable/6a2/STATE.a2ml" ]; then \

Check failure on line 437 in Justfile

View workflow job for this annotation

GitHub Actions / Hypatia neurosymbolic scan

[hypatia] CI policy requires a retired descriptile path; align the check with .machine_readable/descriptiles/
sed -i 's/last-updated = "[^"]*"/last-updated = "'"$(date +%Y-%m-%d)"'"/' .machine_readable/6a2/STATE.a2ml && \
echo "STATE.a2ml timestamp updated"; \
fi
Expand Down
20 changes: 20 additions & 0 deletions README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,26 @@ parameter (the L2 grade algebra), not a fixed feature set:
* *AffineScript* is one *product profile* of this kernel (`grade = affine + cost`),
aimed at WASM contracts and edge functions. It is downstream of anytype.

== Relationship to ephapax (design reference only)

* link:https://github.com/hyperpolymath/ephapax[*ephapax*] uses anytype as a
*design reference only*: it borrows the idea "pick the algebra, get the
discipline". It is not a downstream profile of this kernel.
* There is *no code or build dependency* in either direction. ephapax does not
import, link, vendor or pin anytype, and anytype does not depend on ephapax.
This follows the estate kernel ruling (D-2026-10-12: Agda is the family proof
kernel and Idris2 is for ABI/runtime only; cross-kernel use is port plus
ledger, and nothing is imported across kernels). Under that ruling anytype
must not become an ephapax dependency.
* *No soundness proof exists for this relationship.* Nothing here or in ephapax
shows that ephapax's typing discipline is an instance of an anytype grade
algebra, or that any anytype result carries over to ephapax. ephapax's v2 plan
keeps its {0,1,ω} usage grades separate from an anytype-style single algebra,
and records its anytype row as UNVERIFIED.
* Source: the ephapax v2 survey,
link:https://github.com/hyperpolymath/ephapax/blob/main/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc[`EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc`]
("How sibling repositories plug in" and "Cross-repo action list").

== RSR integration

This repository uses the Rhodium Standard Repository pattern: machine-readable
Expand Down
Loading