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 generate and make verify first fetch and build the pinned Jerboa generator runtime from dependencies.lock.json into vendor/jerboa; sibling checkouts are not used. 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.

VERSION is the jerboa-android generator package version and must match jpkg.sexp. Generated app (version-code ...) and (version-name ...) values belong to the emitted Android project and are intentionally independent.

The pinned Jerboa checkout is managed by scripts/fetch-jerboa.sh. The script reads generator_runtime from dependencies.lock.json with Python's JSON parser, fetches that exact commit into vendor/jerboa, verifies both the commit and tree, rejects dirty dependency checkouts, and builds the upstream runtime before generation. scripts/run-jandroid.sh uses the resulting runtime cache, which is keyed on the full pinned dependency tree, lock file, Jerboa tool version, platform, architecture, and runtime build flags.

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))
• (launcher-activity "com.example.app.MailActivity") selects a typed launcher class in the app package.
• (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")
• (android-test-dependency "androidx.work:work-testing:2.11.2")
• (test-instrumentation-runner "androidx.test.runner.AndroidJUnitRunner")
• (verification-metadata "relative/path/gradle-verification-metadata.xml")
• (fragment "relative/path.ss")
• (client original-tactics)
• (typed-kotlin-file "relative/File.kt" (typed-library ...))
• (typed-android-test-kotlin-file "relative/Test.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.

fragment reads another Jerboa file that defines:

(def fragment
  '((typed-kotlin-file "com/example/Extra.kt"
      (typed-library (com example extra)
        (export answer)
        (def (answer) : String "ok")))))

Fragments are expanded into the app spec before generation. They are useful for large typed generated source sets that should stay outside 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. For an app-owned launcher, put the Activity class in a typed module at the path matching its package and class name, then set launcher-activity to that fully qualified name. The generator verifies that the launcher is inside the app package and supplied by a typed-kotlin-file, points the manifest at it, and omits the placeholder MainActivity source. 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)))))

typed-android-test-kotlin-file writes its library under app/src/androidTest/java for instrumented tests. Main and androidTest libraries are type-checked together as one same-package module set (main first), so test libraries can call declarations that the main typed-kotlin-file forms export — including externs declared with (kotlin-class Name) and (extern ...). Pair it with (test-instrumentation-runner "..."), which sets testInstrumentationRunner in the generated app build script, and (android-test-dependency "group:name:version"), which adds androidTestImplementation coordinates under the same exact-version and verification-metadata rules as dependency. tests/fixtures/typed-worker-app.ss is a complete WorkManager example: a typed Worker subclass, a scheduler using PeriodicWorkRequest.Builder with a Class token, and an androidTest that proves registration and invocation through WorkManagerTestInitHelper (run it with make worker-smoke).

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. An app may select one XML verification manifest using verification-metadata; its path is confined to the app-spec directory, rejects traversal and symlinks, and is copied into the generated Gradle project. With no app-owned manifest, the pinned generator manifest remains the default. 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 are rejected outside dedicated adversarial fixtures.

CI Runners

CI infrastructure is documented in docs/ci-runners.md. Short version: linux-amd64 jobs run on ssh build@infra1 (runner infra1-linux-amd64); freebsd-amd64 jobs run on biggus jails. The old bhyve ubuntu-server VM on biggus is decommissioned — never start it.