standards/a2ml/README.a2ml at main · hyperpolymath/standards · GitHub

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
120
121
122
123
124
125
126
127
128
# A2ML (Attested Markup Language)

@abstract:
A2ML is a lightweight, Djot-like markup that compiles into a typed, attested core.
It keeps authoring simple while allowing strong guarantees when you want them.

This repository is a satellite of the Hyperpolymath standards hub.
@end

## Why A2ML

- Lightweight authoring with progressive strictness (lax → checked → attested)
- Strong guarantees: required sections, resolved references, unique IDs
- Opaque payloads preserved byte-for-byte for absolute fidelity
- Renderer portability across HTML/Markdown/PDF pipelines

## Quick Start (Module 0)

@opaque(lang="a2ml", id="quick-start-example"):
# A2ML Overview

@abstract:
A2ML is a typed, attested markup format. It verifies structure and references.
@end

## Claims
- Required sections must exist.
- References must resolve.

@refs:
[1] Attested Markup Language Spec (draft)
@end
@end

## Documents

### Specification

- **Spec**: SPEC.a2ml - Surface Grammar + Typed Core
- **Quickstart**: docs/QUICKSTART.adoc - Module 0 Quickstart + FAQ
- **Modules**: docs/MODULES.adoc - Syntax Modules (Opt-in)
- **Grammar**: docs/GRAMMAR.adoc - Grammar Appendix

### Implementation

- **Conformance**: docs/CONFORMANCE.adoc - Conformance + Test Vectors
- **Conformance Plan**: docs/CONFORMANCE-PLAN-v1.adoc - v1 Conformance Plan
- **Web Rendering**: docs/WEB-RENDERING.adoc - Web Rendering Options

### Registration

- **IANA Media Type**: docs/IANA-MEDIA-TYPE.a2ml - IANA Media Type Draft
- **Comparison**: docs/COMPARISON.adoc - Comparison Matrix
- **Citations**: docs/CITATIONS.adoc - Citation Guide

## Prototypes

### Web Implementations

- **ReScript Web**: prototype/rescript/README.adoc
- **ReScript + WASM**: prototype/wasm/README.adoc
- **ddraig-ssg**: prototype/ddraig/DemoBuild.idr - Static site generator demo

### TUI

- **Ada/SPARK TUI**: prototype/ada-tui/docs/README.adoc - Terminal UI (prototype)

## Idris2 Core

The formal core is implemented in Idris2 with dependent types and proofs.

- **TypedCore**: src/A2ML/TypedCore.idr - Core types with invariants
- **Proofs**: src/A2ML/Proofs.idr - Uniqueness and resolution proofs
- **Parser**: src/A2ML/Parser.idr - Total parser (no partial functions)
- **Converters**: src/A2ML/Converters.idr - Format converters (Markdown, HTML, Djot, LaTeX, PlainText)
- **Tests**: src/A2ML/Tests.idr - 29 comprehensive tests

### Tooling

- **CLI**: cli/a2ml-cli.idr - Command-line validator and converter
- **REPL**: repl/A2ML-REPL.idr - Interactive development environment
- **LSP**: lsp/A2ML-LSP.adoc - Language Server Protocol architecture
- **Documentation**: docs/TOOLING.adoc - Complete tooling guide
- **Idris2 Core**: docs/IDRIS2-CORE.adoc - Core implementation details

## Core Tests

Run Idris2 core tests:

@opaque(lang="bash"):
just core-tests
@end

## CLI

- **CLI Documentation**: docs/CLI.adoc
- **Man Page**: docs/a2ml.1
- **Packaging**: docs/PACKAGING.adoc

Build CLI:

@opaque(lang="bash"):
just package-cli
@end

## Release Notes

- **v0.1.0**: RELEASE-NOTES-v0.1.0.adoc
- **v0.5.0**: RELEASE-NOTES-v0.5.0.adoc
- **v0.6.0**: RELEASE-NOTES-v0.6.0.adoc

## Announcement

- **Announcement Draft**: docs/ANNOUNCEMENT.adoc
- **State of A2ML**: docs/STATE-OF-A2ML.adoc
- **v1.0.0 Criteria**: docs/V1-CRITERIA.adoc

## Status

- Draft specification, v0.7.0
- Prototype parser + CLI + REPL + LSP architecture available
- Idris2 core with dependent types and formal proofs
- 29 core tests passing
- Format converters: Markdown, HTML, Djot, LaTeX, PlainText

## License

PMPL-1.0-or-later. See LICENSE.