From d6313593f30839686725b4249f1da10fa0498af4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 4 Jul 2026 05:03:25 +0000 Subject: [PATCH] refactor: rename the HexAll umbrella to Hex so users can import Hex Rename the aggregator umbrella library (and its root module) from HexAll to Hex, so downstream code requiring `hex` simply writes `import Hex`. Update the lakefile target and the module docstring to match. Rework the README: fold the separate Mathlib-free and Mathlib-layer tables into one three-column table keyed by component, move the `require` snippet up into a Quickstart section with a short worked example (exact integer determinant and an LLL short vector), link to the manual, and correct the released-repo links to their leanprover/ homes. Co-Authored-By: Claude Opus 4.8 (1M context) --- HexAll.lean => Hex.lean | 4 +-- README.md | 77 +++++++++++++++++++++++++---------------- lakefile.toml | 4 +-- 3 files changed, 51 insertions(+), 34 deletions(-) rename HexAll.lean => Hex.lean (77%) diff --git a/HexAll.lean b/Hex.lean similarity index 77% rename from HexAll.lean rename to Hex.lean index fd9914b..b452e5b 100644 --- a/HexAll.lean +++ b/Hex.lean @@ -10,11 +10,11 @@ public import HexLLLMathlib public section /-! -`hex` — convenience aggregator for the released hex libraries. +`Hex` — convenience aggregator for the released hex libraries. Requiring `hex` pulls in the whole released `hex-lll-mathlib` closure (the executable cores and their Mathlib correspondence proofs) at a single coherent -pinned set. `import HexAll` re-exports all of them; or import an individual +pinned set. `import Hex` re-exports all of them; or import an individual library directly. To depend on just the executable LLL core without Mathlib, require `hex-lll` instead of `hex`. -/ diff --git a/README.md b/README.md index f77ee9c..f2a8b88 100644 --- a/README.md +++ b/README.md @@ -3,40 +3,57 @@ Verified computational algebra in Lean 4: an aggregator for the released `hex` libraries. -API documentation: - -Requiring this package pulls in the whole released `hex-lll-mathlib` closure -at a single coherent pinned set. The Mathlib-free computational libraries -(what used to be a single `HexMatrix` is now split into a matrix layer and -the row-reduction, determinant, and Bareiss libraries built on it): - -| Library | Repo | -|---|---| -| `HexBasic` | [hex-basic](https://github.com/kim-em/hex-basic) | -| `HexMatrix` | [hex-matrix](https://github.com/kim-em/hex-matrix) | -| `HexRowReduce` | [hex-row-reduce](https://github.com/kim-em/hex-row-reduce) | -| `HexDeterminant` | [hex-determinant](https://github.com/kim-em/hex-determinant) | -| `HexBareiss` | [hex-bareiss](https://github.com/kim-em/hex-bareiss) | -| `HexGramSchmidt` | [hex-gram-schmidt](https://github.com/kim-em/hex-gram-schmidt) | -| `HexLLL` | [hex-lll](https://github.com/kim-em/hex-lll) | - -and their Mathlib correspondence layers: - -| Library | Repo | -|---|---| -| `HexMatrixMathlib` | [hex-matrix-mathlib](https://github.com/kim-em/hex-matrix-mathlib) | -| `HexRowReduceMathlib` | [hex-row-reduce-mathlib](https://github.com/kim-em/hex-row-reduce-mathlib) | -| `HexDeterminantMathlib` | [hex-determinant-mathlib](https://github.com/kim-em/hex-determinant-mathlib) | -| `HexBareissMathlib` | [hex-bareiss-mathlib](https://github.com/kim-em/hex-bareiss-mathlib) | -| `HexGramSchmidtMathlib` | [hex-gram-schmidt-mathlib](https://github.com/kim-em/hex-gram-schmidt-mathlib) | -| `HexLLLMathlib` | [hex-lll-mathlib](https://github.com/kim-em/hex-lll-mathlib) | +- Manual: +- API documentation: +# Quickstart + +Add to your `lakefile.toml`: + +```toml +[[require]] +name = "hex" +git = "https://github.com/leanprover/hex.git" +rev = "main" ``` -require hex from git "https://github.com/kim-em/hex.git" @ "" + +Then `import Hex` re-exports every library in the table below at a single +coherent pinned set: + +```lean +import Hex + +open Hex + +-- Exact, fraction-free integer determinant. +def M : Matrix Int 3 3 := #m[2, 1, 1; 1, 2, 1; 1, 1, 2] +#eval M.det -- 4 + +-- LLL: reduce an integer lattice basis and read off a provably short vector. +-- The `by decide` arguments discharge the reduction-factor side conditions. +def L : Matrix Int 3 3 := #m[1, 1, 1; 1, 0, 2; 3, 5, 6] +#eval lllNative.firstShortVector L (3 / 4) (by decide +kernel) (by decide +kernel) (by decide) ``` -To depend on just the Mathlib-free LLL, require -[`hex-lll`](https://github.com/kim-em/hex-lll) directly. +To depend on just one piece, require that library directly (for example +[`hex-lll`](https://github.com/leanprover/hex-lll) for the Mathlib-free LLL +core) instead of the aggregator. + +# Libraries + +Each computational library is Mathlib-free; its Mathlib correspondence proofs +and Mathlib-facing API, where they exist, live in a separate `*-mathlib` +library. + +| Component | Computational | Mathlib layer | +|---|---|---| +| Foundations | [HexBasic](https://github.com/leanprover/hex-basic) | — | +| Matrices | [HexMatrix](https://github.com/leanprover/hex-matrix) | [HexMatrixMathlib](https://github.com/leanprover/hex-matrix-mathlib) | +| Row reduction | [HexRowReduce](https://github.com/leanprover/hex-row-reduce) | [HexRowReduceMathlib](https://github.com/leanprover/hex-row-reduce-mathlib) | +| Determinants | [HexDeterminant](https://github.com/leanprover/hex-determinant) | [HexDeterminantMathlib](https://github.com/leanprover/hex-determinant-mathlib) | +| Bareiss | [HexBareiss](https://github.com/leanprover/hex-bareiss) | [HexBareissMathlib](https://github.com/leanprover/hex-bareiss-mathlib) | +| Gram-Schmidt | [HexGramSchmidt](https://github.com/leanprover/hex-gram-schmidt) | [HexGramSchmidtMathlib](https://github.com/leanprover/hex-gram-schmidt-mathlib) | +| LLL | [HexLLL](https://github.com/leanprover/hex-lll) | [HexLLLMathlib](https://github.com/leanprover/hex-lll-mathlib) | Development of the full project (including unreleased libraries) happens in the [`hex-dev`](https://github.com/kim-em/hex-dev) monorepo. diff --git a/lakefile.toml b/lakefile.toml index a1a5ea0..f895a67 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,5 +1,5 @@ name = "hex" -defaultTargets = ["HexAll"] +defaultTargets = ["Hex"] # Aggregator: requires the full released hex-lll-mathlib closure at a single # coherent pinned SHA set. Require `hex` to depend on everything released; or @@ -36,4 +36,4 @@ git = "https://github.com/leanprover/hex-lll-mathlib.git" rev = "2f577e09690a6a45cf845a50ab59af060a296b74" [[lean_lib]] -name = "HexAll" +name = "Hex"