Abs

A lean core — standard library for Lean 4, heavily inspired by Jane Street's Core.

Modules

Module	Approx Coverage	Description
Command	Done	Structured CLI parsing: flags, positional args, subcommands, tab completion
Control	Partial	Control-flow abstractions (ado)
Deriving	Partial	Custom deriving handlers (Enumerable)
Testing	Partial	Compile-time shell testing ($, promote)
Data.Seq	Done	Lazy sequences with Done/Skip/Yield state machine (~50 functions)
Data.StepFunction	Done	Piecewise-constant time→value functions with lazy steps
Data.TimingWheel	Done	Hierarchical circular-buffer alarm queue, O(1) add/remove
Time.TimeNs	Done	Nanosecond-precision time, spans, Ofday, string parsing, zone conversions
Time.Date	Done	Calendar dates, day-of-week, date arithmetic, ISO 8601 week numbering
Time.Month	Done	Month and DayOfWeek enums
Time.Zone	Done	IANA timezone support: TZif parser, transition lookup, DST handling
Time.Timezone	Done	Zone loading from /usr/share/zoneinfo/, local timezone resolution
Array	0%	Fixed-length mutable vectors
Bytes	0%	Mutable byte sequences
String	0%	Extended string operations
Substring	0%	String slices
Char	0%	Character utilities
Int	0%	Integer types and conversions
Int32	0%	32-bit integers
Int64	0%	64-bit integers
Float	0%	Floating-point operations
Sign	0%	Sign enumeration
Ordering	0%	Comparison ordering
Percent	0%	Percentage type
ByteUnits	0%	Byte quantity representation (KB, MB, GB, etc.)
Map	0%	Immutable tree-backed maps
Set	0%	Immutable tree-backed sets
Hashtbl	0%	Hash tables
HashSet	0%	Hash-backed sets
Stack	0%	Last-in-first-out stack
Queue	0%	First-in-first-out queue
Deque	0%	Double-ended queue
Fqueue	0%	Functional queue
Fdeque	0%	Functional deque
DoublyLinked	0%	Imperative doubly-linked list
Bag	0%	Unordered mutable collection
Iarray	0%	Immutable arrays
UnionFind	0%	Disjoint-set data structure
TimeFloat	0%	Time with float precision
Error	0%	Error type with backtraces
OrError	0%	Result type (success or error)
Info	0%	Structured error information
Validate	0%	Validation framework
Sexp	0%	S-expression handling
Sexpable	0%	S-expression serialization interface
Binable	0%	Binary serialization
Md5	0%	MD5 hashing
Hexdump	0%	Hex dump formatting
Pid	0%	Process identifiers
Signal	0%	Unix signals
HostAndPort	0%	Network host and port type
Gc	0%	Garbage collector control
Identifiable	0%	Types with unique identifiers
Stringable	0%	Types convertible to/from strings
Comparable	0%	Comparable types interface
Hashable	0%	Hashable types interface
Container	0%	Generic container interface
IndexedContainer	0%	Container operations with indices
Ref	0%	Mutable references
SetOnce	0%	Write-once mutable cell
Atomic	0%	Atomic reference operations
UniqueId	0%	Unique identity generation
Either	0%	Sum type
Nothing	0%	Uninhabited type
NeverReturns	0%	Type indicating function never returns
TypeEqual	0%	Compile-time type equality
Blang	0%	Boolean expression evaluation
MaybeBound	0%	Open/closed/unbounded intervals
BinarySearch	0%	Binary search over sorted collections
Quickcheck	0%	Property-based testing

Usage

Add abs as a dependency in your lakefile.lean:

require abs from git
  "https://github.com/rdavison/abs"

Then import Abs:

import Abs

open Command

def greet : Cmd :=
  Cmd.basic "greet someone" none <|
    ado
      let loud ← Param.flag "--loud" Flag.noArg " shout"
      let name ← Param.anon (CmdAnons.anonArg "NAME" ArgType.string)
    in do
      let msg := if loud then s!"Hello, {name}!".toUpper else s!"Hello, {name}!"
      IO.println msg

def main (args : List String) : IO Unit :=
  Command.run greet (argv := "greet" :: args)

Building

lake build

Testing

Cram tests

Cram tests verify CLI output at elaboration time:

import Abs

open Testing.Cram

$ .lake/build/bin/my-app World
  Hello, World!

$ .lake/build/bin/my-app --loud World
  HELLO, WORLD!

$ command runs the command via sh -c. Expected output on subsequent lines must be indented two spaces. A blank line separates test cases.

lake build Tests

When a cram test fails, the error shows the diff. To accept the actual output:

lake exe promote

Examples

examples/Command/ has five working programs:

• Basic — flags and a positional arg
• Flags — required, optional, default, boolean, listed, enum types
• Subcommands — groups, version wiring
• Anons — tuples, optional, sequences, enum-style arg types
• Nested — multi-level nesting, git-style CLI

Build and run an example:

lake build example-basic
.lake/build/bin/example-basic --loud World