Generated packages

lungo generate --<language>_out=DIR writes a package that holds the program (as C, or for TypeScript as WebAssembly) and its API in the language. It builds with the language’s own tools and runs on the lungo runtime, which it takes from the lungo release (or a local distribution) at exactly the version that generated it. The Rust output is described in generated code and Lean types in Rust.

Below, the program’s id is its name as a C identifier (polyglot for a Lake package polyglot).

Names

An exported declaration is named after the shortest suffix of its Lean name that no other declaration of its kind ends with: Geometry.Shape.area is area, unless another function also ends with area, in which case both keep one more component (shape_area, other_area). The suffix is converted to the language’s conventions (snake_case in C and Python, UpperCamelCase for Go and all types, lowerCamelCase for Swift and TypeScript members) and escaped where it is a keyword.

A function whose name comes out the same as a type’s (or a constructor’s, or a descriptor’s) keeps one more component, as two functions ending alike do; the type keeps its name. In Go, where both are UpperCamelCase in one package, Gate.acquire beside the type Acquire is GateAcquire. Two functions that would still get the same name (foo and Foo), or two types, are an error (LNG0107) naming both: rename one in Lean.

Lean types

Numbers are checked when they cross into Lean: a negative Nat, a Go int32 out of a UInt16’s range, a string that is not valid Unicode, a nil value of an inductive type are rejected (see errors), never truncated. An Option whose values can themselves be None/null (Option (Option α), Option Unit) is Some(value) (Python, TypeScript) where it is some. A structure that contains itself by value (through options, pairs or other structures) is a pointer in Go and a final class in Swift. Values Lean cannot give a language type (IO actions stored as data, a Type, a value of a type the program does not describe) are opaque: handles that keep the Lean value alive until they are closed or collected.

Opaque types

An inductive type whose values Lean code alone can make (one with a proof among its fields, say, like a structure of a value and the proof that it is well formed) is opaque: its values cross as handles, which the program’s functions make and read. It is still a type of its own: Wf in Go is struct{ lungo.Opaque }, a subclass of lungo_py.Opaque in Python, a struct in Swift, a subclass of Opaque in TypeScript, so one opaque type’s value cannot be passed where another’s is expected. Type parameters of an opaque type are not part of its binding type. Types that are not inductive, or have indices, are plain opaque values.

Layout fingerprints

Every named type records its layout fingerprint: <Name>Fingerprint (Go), <Class>.__lungo_fingerprint__ (Python), <Type>.lungoFingerprint (Swift), leanTypes["<Lean name>"].fingerprint (TypeScript), <ID>_<TYPE>_FINGERPRINT (C), and lungo::LeanLayout::FINGERPRINT in Rust. A package using another’s type as an extern type checks it before it runs.

A polymorphic function takes a type descriptor for each type parameter, first: Size(lungo.NatType, tree) (Go), size(lungo_py.NAT, tree) (Python), size(Lungo.nat, tree) (Swift), p.size(L.NAT, tree) (TypeScript), polyglot_size(nat_type, tree, &result, &error) (C). Each named type has a descriptor function (TreeType(a), tree_type(a), Tree.lungoType(a), treeType(a), polyglot_tree_type(a)).

Errors

A function whose result is Unit returns nothing (only its error) in Go, Swift and TypeScript.

Facilities

The externs the host implements are the operations of the program’s facilities, which its Lean code declares (@[lungo_facility "ns.name"], @[lungo_operation C]; see how to call host code from Lean). Each facility is one type in the language, named after the last component of its identifier (polyglot.scaler is Scaler), with one method per operation, and the host installs an implementation of each:

Every facility the program’s linked modules declare must be installed, whether or not a given call reaches it, so a program fails at its first call rather than in the middle of one. A facility’s documentation comment names the assumptions the program’s claims make of the host’s implementation; the program cannot check them. A method whose Lean type is pure must answer the same arguments the same way: Lean may evaluate a call once and keep the value.

Async exports

An export returning Lungo.Async.Program Op α asks the host to perform operations of the async facility over Op as it runs, and waits for each answer. It is an asynchronous function of the language taking a handler first: an object with one method per constructor of Op, which takes the constructor’s fields and returns (or resolves to) the answer.

A program given up is released by the runtime, and the call fails with the method’s error (or the cancellation). lungo.Outstanding() (Go), lungo_py.outstanding() (Python), lungoOutstanding() (Swift), p.outstanding() (TypeScript, per program) and lungo_async_outstanding() (C) count the programs waiting for an answer: zero once every call has completed. A process may end with programs waiting.

Assurance

Every package carries the program’s assurance document, assurance.json, the same file for every language, and reads it as the language’s types:

Each reader refuses a document of another schema version, or with a field it does not know or lacks, at any depth (details).

Threads

The program may be called from any number of threads at once (Go goroutines, Python threads, Swift tasks and queues, C threads); calls release the Python GIL. Host functions may be called on any thread, including threads Lean’s tasks run on. WebAssembly has one thread: Lean’s tasks run when they are spawned, and the program cannot use child processes, sockets, signals or timers (LNG0408).

One process has one lungo runtime and one host: the support library of its language. The C value API’s host functions and another language’s support library cannot be used in the same process.

C

CMakeLists.txt          the library <id> (target <id>::<id>) and the runtime
include/<id>.h          the API
src/<id>.c
program/                the program: lungo.h, <id>_program.h, <id>_program.c,
                        <id>_boundary.c, modules/*.c

The CMake project downloads the runtime archive of the lungo release for the target, checks its SHA-256 digest (URL_HASH), and links its static library (lungo::runtime). With -D<ID>_FETCH_LUNGO=OFF it uses an installed runtime instead (find_package(lungo <version> EXACT); CMAKE_PREFIX_PATH or lungo_DIR locates it); -D<ID>_LUNGO_TARGET=<triple> chooses the archive when the target cannot be inferred. Include it with add_subdirectory.

Every value is a lungo_value * of the C API. The API adds, per type, its descriptor (<id>_<type>_type(...)), a constructor function per constructor (<id>_<type>_<ctor>(fields…), taking ownership of the fields), a macro of each constructor’s index (<ID>_<TYPE>_<CTOR>) and an accessor per field (<id>_<type>_<field>(v), or <id>_<type>_<ctor>_<field>(v) for types of several constructors); per function int32_t <id>_<function>(type arguments…, arguments…, lungo_value **result, lungo_error **error) (an async export takes lungo_step *step instead of result); <id>_implement_<facility>_<operation>(f, ctx, drop); <id>_assurance_json(); <id>_initialize() and <id>_run_main(argc, argv). Objective-C uses the same API (see Swift).

Go

<id>.go                 the package (cgo)
*.c, *.h                the program; module files are module_<stem>_lean.c

The package imports github.com/machinefabric/lungo-go and requires exactly the module version of the lungo release that generated it (const _ = lungo.EnforceVersion<version> does not compile with another). The module carries the runtime for linux/amd64, linux/arm64, darwin/amd64, darwin/arm64 and windows/amd64 and links it once per binary. Build with cgo enabled and a C compiler (on Windows, MinGW-w64 GCC). The package name is the program’s id (option package).

Functions return (T, error); types are Go types with a descriptor function each (PointType(), TreeType[A](typeA)); Set<Facility>(impl) installs each facility; async exports take a context.Context and a handler; Assurance() is the assurance document; RunMain(args) (int, error) runs main.

Python

pyproject.toml          scikit-build-core; requires lungo-py
CMakeLists.txt          builds the program as the shared library of the package
program/
src/<package>/__init__.py, py.typed

pip install DIR builds a wheel (py3-none-<platform>: the program is a shared library loaded with ctypes, not a CPython extension, so one wheel serves every Python 3). It depends on exactly the lungo-py of the release, which carries the runtime. Functions are module functions (async exports are async def); types are frozen dataclasses; set_<facility>(impl) installs each facility; ASSURANCE is the assurance document; run_main(args) runs main.

Swift

Package.swift           depends on lungo-swift at exactly the release's version
Sources/<Module>Program/  the program and the C API (include/<id>.h: for C and Objective-C)
Sources/<Module>/<Module>.swift

The package has two products: <Module> (the Swift API) and <Module>Program (the C API, which Objective-C imports with @import <Module>Program;). lungo-swift provides LungoKit and the runtime as an XCFramework (macOS 12 and later, iOS 15 and later, the iOS simulator). Functions are module functions that throw (async exports are async throws); types are structs and indirect enums; set<Facility>(_:) installs each facility; assurance is the assurance document; runMain(_:) runs main.

TypeScript

package.json            depends on lungo-ts at exactly the release's version
index.js, index.d.ts    ES module and its declarations
program.wasm            the program and the runtime, for wasm32-wasip1

lungo generate links program.wasm with the pinned wasi-sdk. await load(options) instantiates it (on Node.js 20 and later with node:wasi; in browsers with lungo-ts’s BrowserWasi, or any WASI given as options.wasi) and returns an object whose methods are the program’s functions (async exports return promises); options.facilities implements the facilities, and ASSURANCE is the assurance document. Programs using primitives WebAssembly lacks cannot be generated (LNG0408).

Embedded packages

A library that already is a package in its language (a Python distribution, an npm package, a Swift package, or a CMake project) embeds the program in it with the generator option embed instead of depending on a package of the program’s own. lungo owns the output directory and replaces it as a whole, so it is a directory of the host’s, never its root. The host’s manifest provides what the generated one would have: