Kina.ai
Menu

Design · Content

Content

Code figures, reading columns, and definition lists use the same live classes as the compiler API, specification, and learning pages. Content supplies the hierarchy; the stylesheet supplies the presentation.

Code snippet

A labeled, keyboard-scrollable source figure

Use CodeSnippet for standalone source or command output that needs a caption. It composes the current .figure, .figure-label, and .codeblock styles.

ad_log_softmax.kina · restricted reverse-mode AD
let f = fn(x: tensor<F32, [2, 3], @host>) -> tensor<F32, [2, 3], @host> {
  let y = x.log_softmax(axis=1) in
  y
} in
let x = tensor<F32, [2, 3], @host> in
handle f(x) with reverseMode
label
Required caption text. Name the source and explain why the excerpt is shown.
language
Required syntax grammar: kina, mlir, shell, or intentionally unhighlighted text.
children
Required source string. Preserve meaningful indentation and omit decorative leading or trailing blank lines.
Markdown fences
Keep generated documentation inside .prose; its native prestyle is the reading-column equivalent.
Keyboard overflow
The code well is focusable and named from its caption so keyboard users can scroll long lines. Generated Markdown fences receive the same focusable treatment.

Variants

Source, emitted output, commands, logs

Set language explicitly. Pair Kina source with MLIR when readers need to compare input and lowering; use shell for commands and text for output with no syntax grammar.

Source · Kina
let x = tensor<F32, [2, 3], @host> in
x.log_softmax(axis=1)
Emitted output · MLIR
module {
  func.func @main() -> tensor<2x3xf32> {
    %0 = tensor.empty() : tensor<2x3xf32>
    return %0 : tensor<2x3xf32>
  }
}
Compiler command · shell
dune exec bin/main.exe -- \
  ../../tests/compiler/examples/ad_log_softmax.kina \
  /tmp/ad_log_softmax.mlir
Validation output · text
Checking ad_log_softmax.kina
Shape obligations: discharged
MLIR emission: complete

Prose

The shipping reading matrix

PageMast owns the page h1, so rendered Markdown drops its leading title. Wrap the remaining document in .prose. This specimen starts at h2 and exercises the current sheet through h4.

Typed tensor programs

Kina makes tensor shape and placement part of a program's type. The bootstrap compiler accepts the .kina surface and lowers typed programs to textual MLIR. Its implemented behavior is tracked on the current status page.

The compiler boundary

Kina owns the typed decoder graph, loss, automatic differentiation, and decoding semantics for StoryLM-0. Corpus loading and checkpoints remain host concerns.

What a checked program records

  • Tensor facts
    • Dtype and symbolic shape
    • Host or device placement
  • Explicit operator semantics
  • Constraints discharged during checking

Follow the evidence

  1. Read the numbered specification.
  2. Inspect a compiler-accepted example.
  3. Compare the emitted MLIR golden.

Do not infer new operator semantics from a specimen. The numbered specification is the language contract.

The current vertical slice separates language-owned work from host support.

StoryLM-0 responsibility by layer
LayerStoryLM-0 responsibility
KinaDecoder graph, loss, AD, and decoding semantics
HostTokenization, corpus loading, and checkpoints
dune exec bin/main.exe -- \
  ../../tests/compiler/examples/ad_log_softmax.kina \
  /tmp/ad_log_softmax.mlir

Definitions

Term and explanation

Use .defs when readers need to scan named concepts, modules, or API fields. Keep each term short and put the explanation in its paired definition.

Surface program
A .kina file accepted by the bootstrap parser.
Typed IR
The checked representation consumed by compiler transformations and lowering.
MLIR golden
A source-controlled snapshot used to verify the compiler's textual MLIR output.