Containerd is a container runtime with an emphasis on simplicity, robustness, and portability. It is available as a daemon, which can manage the complete container lifecycle of its host system: image transfer and storage, container execution and supervision, low-level storage and network attachments, etc.

Package schema defines the OCI image media types, schema definitions and validation functions.

This package provides a Go library to read and manipulate checkpoint archives as created by Podman, CRI-O and containerd.

Distrobox is a fancy wrapper around Podman or Docker to create and start containers highly integrated with the hosts.

oci-image-tool is a collection of tools for working with the OCI image format specification.

A toolkit to run, read and write docker-compose.yml files with Guix machinery.

libslirp is a user-mode networking library used by virtual machines, containers or various tools.

slirp4netns provides user-mode networking ("slirp") for unprivileged network namespaces.

This package provides an implementation of Compose Spec for podman focused on being rootless and not requiring any daemon to be running.

This package provides a replacement for libslirp and VPNKit, written in pure Go. It is based on the network stack of gVisor and brings a configurable DNS server and dynamic port forwarding.

It can be used with QEMU, Hyperkit, Hyper-V and User-Mode Linux.

The binary is called gvproxy.

RootlessKit is a Linux-native implementation of "fake root" using (code user_namespaces(7)). It is used to run containers engines as an unprivileged user, known as "Rootless mode".

Buildah is a command-line tool to build OCI container images. More generally, it can be used to:

• create a working container, either from scratch or using an image as a starting point;

• create an image, either from a working container or via the instructions in a Dockerfile;

• mount a working container's root filesystem for manipulation;

• use the updated contents of a container's root filesystem as a filesystem layer to create a new image.

crun is a fast and low-memory footprint Open Container Initiative (OCI) Container Runtime fully written in C.

This package provides Container Network Interface (CNI) plugins to configure network interfaces in Linux containers.

Conmon is a monitoring program and communication tool between a container manager (like Podman or CRI-O) and an Open Container Initiative (OCI) runtime (like runc or crun) for a single container.

This package provides a tool for exploring a Docker image, layer contents, and discovering ways to shrink the size of Docker/OCI image.

Catatonit is a simple container init tool developed as a rewrite of initrs in C due to the need for static compilation of Rust binaries with musl. Inspired by other container inits like tini and dumb-init, catatonit focuses on correct signal handling, utilizing signalfd(2) for improved stability. Its main purpose is to support the key usage by docker-init: /dev/init – <your program>, with minimal additional features planned.

Podman (the POD MANager) is a tool for managing containers and images, volumes mounted into those containers, and pods made from groups of containers.

Not all commands are working out of the box due to requiring additional binaries to be present in the $PATH.

To get podman compose working, install either podman-compose or docker-compose packages.

To get podman machine working, install qemu-minimal, and openssh packages.

This package provides a tool to read and manipulate checkpoint archives as created by Podman, CRI-O and containerd.

convmv is a file renamer, that converts between different encodings, e.g. from ISO-8859-1 to UTF-8. It is particularly usefuls for files with names, that display incorrectly.

Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.

This package provides a survey of programming language semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, for a miniature example of an imperative programming language. Their encoding, the proofs of equivalence of different styles, abstract interpretation, and the proof of soundess obtained from axiomatic semantics or abstract interpretation is done in Coq. The tools can be run inside Coq, thus making them available for proof by reflection. Code can also be extracted and connected to a yacc-based parser, thanks to the use of a functor parameterized by a module type of strings. A hand-written parser is also provided in Coq, without associated proofs.

Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.