name = "infoductor"
version = "0.1.0"
defaultTargets = ["Infoductor"]

# Generic Lean library + tooling for algebraic organization of code
# repositories: `restructure` macro layer, `Edit` monad, `Context`
# comonad, the `@[macroAlias]` / `@[methodology]` / `@[metaPath]`
# attribute registries, and reference dispatch tactics.
#
# Consumers (cubical-transport-hott-lean4, topolei, …) depend on
# `Infoductor.Foundation` (and, when wanted, the other lean_libs
# below) to organise their proofs without committing to a specific
# methodology — the methodology is the consumer's choice.
#
# Pairs naturally with the Pantograph project (the conductor of an
# electric train sits atop the pantograph hardware).

# ── Dependencies ────────────────────────────────────────────────────────────
# Mathlib is required by `Infoductor.Comonad` for its `Tactic.Explode`
# proof-decomposition primitive.  `Infoductor.Foundation` does NOT
# import Mathlib, so consumers depending only on Foundation pay no
# Mathlib build cost (Lake compiles only the imported subgraph).
# Pinned to the commit mm-lean was tracking at port time (2026-05-01).
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "master"

# ── Sub-libraries ───────────────────────────────────────────────────────────
# `Infoductor` is the umbrella name; sub-libraries below are cherry-
# pickable.  Downstream `import Infoductor.Foundation.Meta` (etc.)
# only pulls that sub-library's subgraph.

[[lean_lib]]
name = "Infoductor"
# Foundation lives directly under `Infoductor.Foundation.*`; this
# default lib root resolves the umbrella module + Foundation's
# sub-modules.  No Mathlib dependency through this lib.

# Comonad: comonadic proof-pattern detection.  Pulls Mathlib (for
# Tactic.Explode).  Optional — only built when imported by
# downstream code.
[[lean_lib]]
name = "Infoductor.Comonad"
roots = ["Infoductor.Comonad"]

# Future sub-libs (declared as each lands):
# Tactics:    reference dispatchers built on Foundation.
# Pantograph: plugin / live integration (when ready).
# Runner:     headless surface (when concrete need arises).