Repository navigation
Expand file tree
/
Copy path0-AI-MANIFEST.a2ml
More file actions
119 lines (104 loc) · 5.02 KB
/
Copy path0-AI-MANIFEST.a2ml
File metadata and controls
119 lines (104 loc) · 5.02 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
; SPDX-License-Identifier: MPL-2.0
; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
;
; 0-AI-MANIFEST.a2ml — Universal AI entry point for GNPL
; Media-Type: application/a2ml
(manifest
(identity
(name "GNPL")
(full-name "Glyph Narration & Projection Language")
(version "0.3.0")
(repo "https://github.com/hyperpolymath/gnpl")
(license "MPL-2.0")
(author "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>")
(parent-project "lithoglyph")
(coordination-repository "nextgen-databases"))
(purpose
"Lithoglyph's narration/projection language. Where a query language answers
'what is true in the store?', GNPL answers 'what account does this evidence
support, told from whose stance, with what warrant, and what rival accounts
does the same evidence also support?' — for forensic histories, counterfactual
paths, plural meanings, and synchronic/diachronic evidence interpretation.
IMPLEMENTED: a direct-evidence narration fragment in src/Gnpl/, with a
projection parser, versioned evidence import, CLI, focalization, checked
warrants, ordered accounts, a limited rival relation and hypothetical
withdrawal. The snapshot importer is not a live Lithoglyph adapter.
Private selection, type validation and storage code remains under its
historical source namespace. It is not a second public language or a
prescribed lowering target. See docs/narration-slice.adoc and
docs/executable-boundary.adoc for the executable contracts.")
(caveat-for-agents
"A green incomplete-proof gate does not establish an axiom-free repository.
The new narration kernel depends only on Lean/Std. Its default-build audit
requires Lean to report only propext for narrate and the two scoped theorems.
Private substrate modules retain separate assumptions, including floating-
point equality. Historical proof-debt totals are not a current inventory.
Imported attribution, audience and scores are trusted inputs; checked
support is not proof of external truth or authenticated source provenance.")
(canonical-locations
(agent-instructions ".machine_readable/descriptiles/AGENTIC.a2ml")
(state ".machine_readable/descriptiles/STATE.a2ml")
(meta ".machine_readable/descriptiles/META.a2ml")
(ecosystem ".machine_readable/descriptiles/ECOSYSTEM.a2ml")
(playbook ".machine_readable/descriptiles/PLAYBOOK.a2ml")
(neurosym ".machine_readable/descriptiles/NEUROSYM.a2ml")
(roadmap ".machine_readable/ROADMAP.a2ml")
(proof-debt "docs/proof-debt.adoc")
(design-theory "docs/THEORY.adoc")
(design-application "docs/LITHOGLYPH.adoc")
(architecture "ARCHITECTURE.adoc")
(governance "GOVERNANCE.adoc")
(build "lakefile.lean")
(test "lakefile.lean") ;; @[test_driver] script test
(proof-gate "scripts/check-lean-proofs.sh")
(container-build "Containerfile")
(container-deploy "selur-compose.yml")
(spec "spec/")
(ffi-bridge "bridge/")
(abi "src/GQLdt/ABI/")
(lean-entry "src/Gnpl.lean"))
;; Commands that reproduce every claim this manifest makes.
(evidence
(build "lake build")
(test "lake test") ;; 5 suites; 35 narration and 26 private-substrate checks
(bridge "cd bridge && zig build && zig build test")
(proof-gate "lake build 2>&1 | tee lake-build.log && ./scripts/check-lean-proofs.sh --build-log lake-build.log"))
(tech-stack
(primary "Lean 4")
(lean-version "v4.15.0")
(mathlib-version "v4.15.0")
(ffi "Zig")
(config "Nickel")
(container-runtime "Podman"))
(architecture
(lean4-core
(description "Narration kernel plus private validation/storage modules")
(location "src/")
(entry "src/Gnpl.lean"))
(bridge
(description "Experimental Zig FFI bridge for storage operations")
(location "bridge/"))
(cli
(description "GNPL narration and hypothetical withdrawal CLI")
(location "src/GnplMain.lean"))
(vscode-extension
(description "VS Code language support")
(location "vscode-extension/")))
(critical-invariants
(rule "SCM files ONLY in .machine_readable/ — never root")
(rule "No sorry in Lean 4 proofs — hard invariant")
(rule "All proofs must be constructive where possible")
(rule "Container runtime is Podman — never Docker")
(rule "Completion claims require honest audit")))
<!-- BEGIN requires-initialisation -->
## PRIORITY ACTION — this repository is not fully initialised
4 substitution token(s) still have no value. **Read
`REQUIRES_INITIALISATION.adoc` 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.adoc` only when
nothing outstanding remains.
<!-- END requires-initialisation -->