ponyup Specification (DRAFT)

[SeanTAllen]

1. Purpose

ponyup is the Pony toolchain multiplexer. It installs, selects, and removes
versioned packages of Pony development tools, managing a local directory of
installed versions and providing a single stable path for each tool's binary.

2. State Model

2.1 Filesystem State

A ponyup installation occupies a single root directory R. The structure is:

R/
  .platform            -- platform triple (e.g., "x86_64-linux-ubuntu24.04")
  .lock                -- lockfile: installed packages and selections
  bin/                 -- stable binary references (symlinks or batch shims)
  <pkg-string>/        -- one directory per installed package-version
    bin/
      <binary>...      -- actual executables

Where <pkg-string> is the fully qualified package name:
<app>-<channel>-<version>-<cpu>-<os>[-<distro>]

Example: ponyc-release-0.61.1-x86_64-linux-ubuntu24.04

2.2 Abstract State

Let the state of a ponyup installation be the tuple:

State = (Platform, Installed, Selected, Bin)

Platform : PlatformTriple | Unset
Installed : Set(Package)
Selected  : Application → Package | None    -- partial function
Bin       : BinaryName → FilePath | None     -- partial function

Where:

Package     = (Application, Channel, Version, CPU, OS, Distro)
Application = ponyc | corral | ponyup | changelog-tool
Channel     = nightly | release
Version     = string           -- semver for release, date for nightly
CPU         = x86_64 | arm64
OS          = linux | darwin | windows
Distro      = string | None    -- e.g., "ubuntu24.04", "musl"

2.3 Lockfile

The lockfile (.lock) is the persistent representation of Installed and
Selected. Each line is:

<pkg-string> [*]

The * marker denotes the selected version for that application. Lines are
grouped implicitly by application name.

2.4 Platform Triple

The platform triple is stored in .platform and represents the target
platform for package downloads. Format: <cpu>-<os>[-<distro>]

On Linux, ponyc requires a distro component. Other applications do not use it.

3. Invariants

These properties must hold at the end of every successful operation:

INV-1 (Lockfile reflects filesystem):
For every package P in Installed, the directory R/<string(P)>/ exists and
contains the expected binaries. For every package directory under R/, there
is a corresponding entry in Installed.

INV-2 (At most one selection per application):
For each application A, |{P ∈ Installed : P.application = A ∧ Selected(A) = P}| ≤ 1

INV-3 (Selection implies installed):
If Selected(A) = P then P ∈ Installed.

INV-4 (Bin references match selection):
For each application A where Selected(A) = P:

• On Unix: For each required binary B of A, Bin(B.name) is a symlink
  pointing to R/<string(P)>/bin/<B.name>.
• On Windows: For each required binary B of A, Bin(B.name + ".bat") is a
  batch file that delegates to R/<string(P)>/bin/<B.name>.exe.
• Optional binaries: If the binary exists in R/<string(P)>/bin/, a
  corresponding link/shim exists in Bin. If it does not exist, no
  link/shim is created (and any stale link from a prior version is removed).

INV-5 (No orphan bin entries):
Every entry in Bin corresponds to a binary of some selected package.

INV-6 (Platform set before install):
The update operation requires Platform ≠ Unset.

INV-7 (Distro required for ponyc on Linux):
If a package P has P.application = ponyc and P.os = linux, then
P.distro ≠ None.

4. Operations

4.1 update (sync)

Install a package, or confirm it is already installed.

Input: application name A, channel/version specifier V

Preconditions:

• Platform ≠ Unset
• A is a recognized application
• V is a valid channel name, a channel-version string (e.g., "release-0.61.1"),
  or "latest" (meaning: latest in the specified channel)

Steps:

1. Construct package identity from (A, channel, version, Platform)
2. If version is "latest", resolve to concrete version via Cloudsmith query
3. If resolved package is already in Installed: report already installed, done
4. Query Cloudsmith for download URL and expected SHA-512 checksum
5. Download archive to temporary file
6. Compute SHA-512 of downloaded file
7. Verify checksum: computed must equal server-provided checksum
8. Extract archive to R/<pkg-string>/
9. Add package to Installed
10. Auto-select: call select(P) to make this the active version

Postconditions (on success):

• P ∈ Installed
• Selected(A) = P
• INV-1 through INV-5 hold
• Downloaded archive is deleted

Error conditions:

• Network unreachable: no state change
• No matching package on Cloudsmith: no state change
• Checksum mismatch: downloaded file deleted, no state change
• Extraction failure: partial directory may remain (TODO: should this be cleaned up?)

4.2 select

Make an installed package version the active one for its application.

Input: application name A, version V

Preconditions:

• There exists P ∈ Installed with P.application = A and version matching V
• If V is "latest", at least one package for A is installed

Steps:

1. If V is "latest", resolve to the most recent installed version of A
2. Find the matching package P
3. Remove existing bin entries for application A
4. Create new bin entries (symlinks/shims) pointing to P's binaries
5. Update Selected(A) = P
6. Persist lockfile

Postconditions:

• Selected(A) = P
• INV-4 and INV-5 hold

Error conditions:

• No installed version matches: error message, no state change

4.3 remove

Remove an installed package version.

Input: application name A, version V

Preconditions:

• There exists P ∈ Installed with P.application = A and version matching V
• Selected(A) ≠ P (cannot remove the currently selected version)

Steps:

1. Delete directory R/<string(P)>/
2. Remove P from Installed
3. Persist lockfile

Postconditions:

• P ∉ Installed
• Selected(A) unchanged
• INV-1 through INV-5 hold

Error conditions:

• Package not installed: error message, no state change
• Package is currently selected: error message, no state change
• Directory deletion fails: state inconsistency (lockfile updated but directory remains?)

4.4 show

Display installed packages and optionally their remote availability.

Input: optional application name filter A, flag local

Preconditions: None (read-only operation)

Behavior:

• List all packages in Installed (filtered by A if given)
• Mark selected version with *
• If local = false: query Cloudsmith for latest available version of each
  installed application (with 5-second timeout); display if newer version exists
• No state mutation

4.5 find

Search for available packages on Cloudsmith.

Input: application name A, optional channel C, optional count N
(default varies), flag all_platforms

Preconditions: None (read-only operation)

Behavior:

• Query Cloudsmith for packages matching A and optionally C
• If all_platforms = false: filter to current Platform
• Display results as formatted table (10-second timeout)
• No state mutation

4.6 default

Set the platform triple for future operations.

Input: platform string T

Preconditions:

• T is a valid platform triple (parseable into CPU, OS, and optional Distro)

Steps:

1. Parse and validate T
2. Write T to R/.platform
3. Set Platform = T

Postconditions:

• Platform is set to the parsed triple
• .platform file contains T

5. Package Identity and Resolution

5.1 Package String Format

A package is identified by its string representation:
<app>-<channel>-<version>-<cpu>-<os>[-<distro>]

The string uniquely identifies a package within an installation.

5.2 Version Resolution

When a version is specified as "latest":

• For update: resolves via Cloudsmith query (most recent completed package)
• For select: resolves to the most recent installed version (by string sort)
• For remove: resolves to the most recent installed version

5.3 Cloudsmith Name Mapping

Ponyup package names map to Cloudsmith package names with these transformations:

• Channel suffix removed (-nightly, -release)
• x86_64 → x86-64
• linux → unknown-linux
• darwin → apple-darwin
• windows → pc-windows

5.4 Platform Parsing

Input platform strings accept target triples with optional vendor field:

• x86_64-unknown-linux-ubuntu24.04 → (x86_64, linux, "ubuntu24.04")
• arm64-apple-darwin → (arm64, darwin, None)
• x86_64-linux-ubuntu24.04 → (x86_64, linux, "ubuntu24.04") [vendor omitted]

CPU aliases: x64, amd64 → x86_64; aarch64 → arm64

Vendor field is always stripped (not stored).

6. Platform-Specific Behavior

Aspect	Unix	Windows
Archive format	.tar.gz	.zip
Extraction	tar -xzf with --strip-components=1	PowerShell Expand-Archive
Bin linking	Symlinks	.bat shim files
Executable suffix	(none)	.exe
Available apps	ponyc, corral, ponyup, changelog-tool	ponyc, corral, ponyup
Default root	$HOME/.local/share/ponyup (or XDG)	%LOCALAPPDATA%\ponyup

7. Bootstrap

The bootstrap scripts (ponyup-init.sh, ponyup-init.ps1) are responsible
for initial installation of ponyup itself. They:

1. Detect the platform (CPU, OS, distro on Linux)
2. Download the latest ponyup release from Cloudsmith
3. Verify checksum (SHA-256 for bootstrap, distinct from SHA-512 used by ponyup itself)
4. Extract to the ponyup root directory
5. Write the .platform file
6. Set up PATH (instructions or automatic)
7. Run ponyup default <platform>

Note: The bootstrap scripts are separate from ponyup itself and have their own
platform detection logic. Distro detection on Linux uses cc -dumpmachine
(glibc vs musl) and lsb_release or /etc/alpine-release.

8. Open Questions / Observations

These are areas where the current implementation's behavior is implicit or
potentially inconsistent, and where a spec could make an explicit choice:

1. Partial install cleanup: If extraction fails during update, is the
   partial directory cleaned up? The code attempts removal but doesn't guarantee
   it. Should the invariant require cleanup?

2. Lockfile atomicity: The lockfile is written by dispose() which
   overwrites the file. If the process crashes mid-write, the lockfile could be
   corrupted. Should writes be atomic (write to temp, rename)?

3. Concurrent access: What happens if two ponyup processes run
   simultaneously? The lockfile has no locking mechanism. Should it?

4. Auto-select on update: update always calls select for the newly
   installed version. Is this the desired behavior? A user installing an older
   version might not want it to become active.

5. Remove prevents removing selected version: This means to remove the last
   installed version, you must first install a different version, select it,
   then remove the old one. Is this intentional? Should there be a way to
   remove everything for an application?

6. "latest" resolution differs by operation: update resolves "latest" via
   Cloudsmith (newest available). select and remove resolve "latest" via
   installed packages (newest installed). This is reasonable but should be
   explicit.

7. Version ordering: Versions are compared by string sort (via Comparable
   on the full package string). This works for date-based nightly versions but
   may not correctly order semver release versions (e.g., "0.9.0" > "0.10.0"
   by string sort). Is this a bug?

8. No certificate validation: The SSL context disables server certificate
   verification. This is a security concern — MITM attacks could serve
   malicious binaries. The SHA-512 checksum mitigates this only if the checksum
   itself comes over a trusted channel, but both URL and checksum come from the
   same unverified connection.

9. Bootstrap checksum algorithm mismatch: Bootstrap uses SHA-256, ponyup
   itself uses SHA-512. Is this intentional? Should they align?

10. Optional binary handling on version switch: When selecting a new version,
    if the old version had an optional binary (e.g., pony-lsp) but the new one
    doesn't, is the old symlink removed? The spec says it should be (INV-4/INV-5)
    — need to verify the code does this.

11. Self-update: ponyup can install ponyup (it's a recognized application).
    What happens when the running binary replaces itself? On Unix this works
    because the old inode stays valid until the process exits. On Windows this
    may fail. Is self-update tested/supported?

12. Lockfile entry for ponyup itself: When ponyup updates itself, it adds
    an entry to the lockfile and creates a symlink. But the bootstrap also
    creates the initial binary. Is there a potential conflict between the
    bootstrapped binary and the lockfile-managed one?