jerboa-android

jerboa-android is an early Android project generator for Jerboa.

The first target is deliberately small: read a quoted Jerboa app spec from a .ss file and emit a plain Kotlin/Android Gradle project. Jerboa runs at build time on the developer machine; the generated APK contains ordinary Android code.

Quick Start

make verify
make clean generate

make verify runs the release-required adversarial and supply-chain checks. make ssd-compile performs the heavier generated-Android compile with the repository-pinned Gradle and JDK artifacts. See SECURITY.md for the trust boundaries and release policy.

The generated counter project is written to build/counter.

Use make apk to regenerate it and build with the authenticated, pinned Gradle and JDK artifacts.

The generated project defaults to Android Gradle Plugin 8.13.2 and Kotlin 2.0.21, because those versions are already used by the larger game app. Specs can override both versions.

App Spec Shape

Specs are valid Jerboa files that define a quoted app value:

(import (jerboa prelude))

(def app
  '(android-app
     (id "org.jerboa.counter")
     (name "Jerboa Counter")
     (version-code 1)
     (version-name "0.1.0")
     (screen Main
       (state count 0)
       (column
         (text "Count: " count)
         (button "Increment" (set count (+ count 1)))))))

Current supported view forms:

• (column child ...)
• (row child ...)
• (text part ...)
• (button label action ...)
• (spacer height)
• (small-text part ...)

Current supported action form:

• (set state expression)

Current supported expression forms:

• strings, numbers, booleans, symbols
• binary +, -, *, /

Android project metadata supported by the generator:

• (id "com.example.app")
• (name "Display Name")
• (root-name "GradleRootName")
• (compile-sdk 35), (build-tools-version "36.0.0"), (min-sdk 26), (target-sdk 35)
• (version-code 10), (version-name "0.1.9")
• (android-gradle-plugin "8.13.2"), (kotlin-version "2.0.21")
• (jvm-toolchain 17)
• (gradle-property "android.useAndroidX" "true")
• (permission "android.permission.INTERNET")
• (permission "android.permission.READ_EXTERNAL_STORAGE" (max-sdk 32))
• (allow-backup #t), (uses-cleartext-traffic #t)
• (theme "@android:style/Theme.Material.NoActionBar")
• (ndk-version "28.2.13676358"), (abi-filter "arm64-v8a")
• (asset-dir "relative/path")
• (jni-lib-dir "relative/path")
• (dependency "androidx.documentfile:documentfile:1.1.0")
• (kotlin-source-dir "relative/path")
• (fragment "relative/path.ss")
• (client original-tactics)
• (typed-kotlin-file "relative/File.kt" (typed-library ...))

asset-dir and jni-lib-dir copy directory contents into the generated Android project. This lets app repos keep only Jerboa specs and binary assets under source control while Kotlin remains generated output.

kotlin-source-dir is a migration bridge for existing apps. It copies existing Kotlin source into the generated project after the default generated MainActivity.kt, so a large app can move to Jerboa-owned Android project generation before each view is rewritten as higher-level Jerboa forms.

fragment reads another Jerboa file that defines:

(def fragment
  '((kotlin-file "com/example/Extra.kt" "package com.example\n...")))

Large fragments can use line lists instead of one string:

(def fragment
  '((kotlin-file-lines "com/example/Extra.kt"
      ("package com.example"
       ""
       "class Extra"))))

Fragments are expanded into the app spec before generation. They are useful for large generated source sets that should stay in .ss files instead of the main app spec.

typed-kotlin-file emits a normal Typed Jerboa typed-library through the upstream (jerboa typed kotlin) backend. Use it for new generated Kotlin instead of kotlin-file, kotlin-file-lines, or kotlin-source-dir. When generated records need JVM/Android types, add structured imports before the library form:

(typed-kotlin-file "com/example/Pick.kt"
  (kotlin-imports (android net Uri))
  (typed-library (com example)
    (export make-Pick Pick? Pick-uri)
    (type Uri)
    (record Pick ((uri : Uri)))))

client expands a named generator-owned template from templates/<name>.ss. The original-tactics and ssd-review clients are composed exclusively from typed Jerboa libraries. Their generated Kotlin is backend output, not source text stored in .ss strings. scripts/check-no-raw-kotlin.sh enforces that invariant for both production clients.

All source paths are relative to the app specification and may not contain symbolic links. Output paths are descriptor-relative, no-follow, exclusive creates; generation intentionally fails if a target already exists. Dependency coordinates must use an exact group:name:version (no +, ranges, latest, or snapshot selectors). Generated projects include strict Gradle verification metadata for the reviewed graph; adding a dependency also requires a reviewed checksum update (or an application-owned verification manifest) before Gradle will execute the build. The generated settings also constrain known-vulnerable transitive build dependencies to the reviewed versions recorded in dependencies.lock.json.

The ssd-review client keeps remote synchronization disabled by default. A deployment must locally provision an HTTPS origin, SPKI SHA-256 pin, and bearer token; remote identifiers are hashed into local filenames and all HTTP, ZIP, entry-count, expansion-ratio, and storage budgets are enforced. The precise configuration and limits are documented in SECURITY.md.

Production Client Policy

New production Android code must use typed-kotlin-file or a typed named client module. Raw kotlin-file, kotlin-file-lines, and kotlin-source-dir forms remain only as compatibility features for generic generator fixtures; they are not permitted in Original Space Tactics or SSD Review.