TOML🔗

Lake.Toml is commonly used for configuration files. Lean 4 provides a module for working with Lake.Toml. This chapter covers how to create, manipulate, and persist Lake.Toml data in Lean.

Working with TOML in Lean requires understanding two primary types:

• Table: This is essentially a map (dictionary) of keys to values. When you parse a TOML string, you get a Table.

• Value: This is an inductive type that can be a string, integer, boolean, array, or another table.

  • Why Value is important: A Table maps keys to values, but those values could be of any type (a string, then a number, then a nested table). In Lean, a map must have a single type for its values. Value acts as a "wrapper" or "box" that lets us store different types of data in the same Table.

• Syntax and .missing: Most TOML types in Lean carry a Lean.Syntax object. This is used to track the exact location of the value in the source file for better error reporting.

  • Why .missing is important: When we create TOML values programmatically (not from a file), there is no "source line" to point to. We use Lean.Syntax.missing (or the shorthand .missing) to satisfy the type system without providing a fake source location.

Working with Lake.Toml is not as straightforward as working with Json, but the following sections provide the necessary tools to handle TOML data effectively.

1. Parsing TOML
2. Accessing and Modifying TOML
3. Nested TOML & Arrays of Tables
4. Reading and Writing TOML Files
5. JSON and TOML Conversion
6. Working with lakefile.toml