Pam-mount is a PAM module to mount volumes when a user logs in. It can mount all local file systems supported by mount, as well as LUKS volumes encrypted with the user's log-in password.

This package provides a minimal seat management daemon whose task is to mediate access to shared devices, such as graphics and input, for applications that require it.

This package provides an implementation of the MAC-Telnet protocol used by RouterOS devices. It provides the following commands:

macping

Ping RouterOS devices or mactelnetd hosts.

mactelnetd

MAC-Telnet daemon.

mactelnet

MAC-Telnet client.

mndp

Discover other RouterOS devices or mactelnetd hosts.

This package provides a command line tool that can give numerous reports on memory usage on GNU/Linux systems.

GNU Rot[t]log is a program for managing log files. It is used to automatically rotate out log files when they have reached a given size or according to a given schedule. It can also be used to automatically compress and archive such logs. Rot[t]log will mail reports of its activity to the system administrator.

jtbl accepts piped JSON data from stdin and outputs a text table representation to stdout.

daemontools is a collection of tools for managing UNIX services.

The Stress Terminal UI displays graphs of the CPU frequency, utilization, temperature and power.

Jnettop is a traffic visualiser, which captures traffic going through the host it is running from and displays streams sorted by bandwidth they use.

stress-ng stress-tests a computer system by exercising both physical subsystems as operating system kernel interfaces. It can stress the CPU, cache, disk, memory, socket and pipe I/O, scheduling, and much more, in various selectable ways. This can trip hardware issues such as thermal overruns as well as operating system bugs that occur only when a system is being thrashed hard.

You can also measure test throughput rates, which can be useful to observe performance changes across different operating system releases or types of hardware. However, stress-ng is not a benchmark. Use it with caution: some of the tests can make poorly designed hardware run dangerously hot or make the whole system lock up.

Compared to its inspiration, stress, stress-ng offers many additional options such as the number of bogo operations to run, execution metrics, verification of memory and computational operations, and considerably more stress mechanisms.

Utility to convert lsof output to a graph showing FIFO and UNIX interprocess communication.

The witr (why-is-this-running), is a utility to show:

1. What is running?

2. How did it start?

3. What is keeping it running?

4. What context does it belong to?

It shows which process uses the port, and its information like process tree, working directory, user, pid, command, and so on.

Tcpdump is a command-line tool to analyze network traffic passing through the network interface controller.

The standard library aims to contain all the tools needed to write both programs and proofs easily. While we always try and write efficient code, we prioritize ease of proof over type-checking and normalization performance. If computational performance is important to you, then perhaps try agda-prelude instead.

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is not a “linear” resource: Concepts are presented as a directed graph, with links indicating dependencies.

This Emacs mode enables interactive development with Agda. It also aids the input of Unicode characters.

Agda is a dependently typed functional programming language: it has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code). Agda is also a proof assistant: it is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL.

The goal is to provide a concrete library focused on verification examples, as opposed to mathematics. The library has a good number of theorems for booleans, natural numbers, and lists. It also has trees, tries, vectors, and rudimentary IO. A number of good ideas come from Agda's standard library.

A new Categories library for Agda

A standard library for Cubical Agda, comparable to agda-stdlib but using cubical methods.

Zbarlight is a simple wrapper for the zbar library. It can read all zbar supported codes.

This package provides a Go library for rendering QR codes in terminals.

GNU Barcode is a flexible tool to produce printed barcodes from text strings. It supports a variety of encoding standards and sizing measurements. Barcodes can be output in PostScript or Encapsulated PostScript formats.

ZBar can read barcodes from various sources, such as video streams, image files, and raw intensity sensors. It supports EAN-13/UPC-A, UPC-E, EAN-8, Code 128, Code 93, Code 39, Codabar, Interleaved 2 of 5, QR Code and SQ Code. Included with the library are basic applications for decoding captured bar code images and using a video device (e.g. webcam) as a bar code scanner. For application developers, language bindings are included for C, C++ and Python as well as GUI widgets for GTK and Qt.