Conky is a lightweight system monitor for X that displays operating system statistics (CPU, disk, and memory usage, etc.) and more on the desktop.

An EFL user interface for the connman connection manager.

Connman provides a daemon for managing Internet connections. The Connection Manager is designed to be slim and to use as few resources as possible. It is fully modular system that can be extended through plug-ins. The plug-in approach allows for easy adaption and modification for various use cases. Connman implements DNS resolving and caching, DHCP clients for both IPv4 and IPv6, link-local IPv4 address handling and tethering (IP connection sharing) to clients via USB, ethernet, WiFi, cellular and Bluetooth.

Cmst is a Qt based frontend for the connman connection manager. This package also provides a systemtray icon.

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

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

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.

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.

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

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

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.

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 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.

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

passt implements a thin layer between guest and host, that only implements what's strictly needed to pretend processes are running locally. The TCP adaptation doesn't keep per-connection packet buffers, and reflects observed sending windows and acknowledgements between the two sides. This TCP adaptation is needed as passt runs without the CAP_NET_RAW capability: it can't create raw IP sockets on the pod, and therefore needs to map packets at Layer-2 to Layer-4 sockets offered by the host kernel.

Also provides pasta, which similarly to slirp4netns, provides networking to containers by creating a tap interface available to processes in the namespace, and mapping network traffic outside the namespace using native Layer-4 sockets.

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

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

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.

Cook is a tool for constructing files. It is given a set of files to create, and recipes of how to create them. In any non-trivial program there will be prerequisites to performing the actions necessary to creating any file, such as include files. Cook provides a mechanism to define these.

Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why3 software verification plateform or as an automatic tactic for the Coq proof assistant.

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

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.

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel.