import Lake
open Lake DSL
open System

package «SilverSight» where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- Add any additional package configuration options here

@[default_target]
lean_lib «SilverSightCore» where
  -- Add any library configuration options here
  srcDir := "Core"
  roots := #[`SilverSightCore, `SilverSight.FixedPoint, `SilverSight.Semantics.Schema, `SilverSight.Semantics.Layout, `SilverSight.Semantics.WireFormat, `SilverSight.Semantics.View, `SilverSight.Semantics.LayoutBridge, `SilverSight.Semantics.CanalLayout]

lean_lib «SilverSightFormal» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.FixedPoint,
    `SilverSight.PrimeLut,
    `SilverSight.FixedPointBridge,
    `CoreFormalism.Tactics,
    `CoreFormalism.Q16_16Numerics,
    `CoreFormalism.DynamicCanal,
    `CoreFormalism.Bind,
    `CoreFormalism.BraidBracket,
    `CoreFormalism.BraidStrand,
    `CoreFormalism.BraidCross,
    `CoreFormalism.BraidField,
    `CoreFormalism.BraidStateN,
    `CoreFormalism.SidonSets,
    `CoreFormalism.SieveLemmas,
    `CoreFormalism.InteractionGraphSidon,
    `CoreFormalism.BraidEigensolid,
    `CoreFormalism.BraidSpherionBridge,
    `CoreFormalism.E8Sidon,
    `CoreFormalism.EisensteinSeries,
    `CoreFormalism.ComplexProjectiveSpace,
    `CoreFormalism.GoormaghtighEnumeration,
    `CoreFormalism.HachimojiBase,
    `CoreFormalism.HachimojiCodec,
    `CoreFormalism.HachimojiLUT,
    `CoreFormalism.HachimojiBridging,
    `CoreFormalism.HachimojiManifoldAxiom,
    `CoreFormalism.ChentsovFinite,
    `CoreFormalism.HopfFibration,
    `CoreFormalism.StrandCapacityBound,
    `CoreFormalism.CRTSidon,
    -- `CoreFormalism.CRTSidonN,  -- TODO(lean-port): auto-generated, targets different mathlib API
    `SilverSight.AngrySphinx,
    `SilverSight.CollatzBraid,
    `SilverSight.GoldenSpiral,
    `SilverSight.GCCL,
    `SilverSight.WireFormat,
    `SilverSight.ProductSchema,
    `SilverSight.ProductWireFormat,
    `SilverSight.Receipt,
    `BindingSite.BindingSiteTypes,
    `BindingSite.BindingSiteHachimoji,
    `BindingSite.BindingSiteEntropy,
    `BindingSite.BindingSiteCodec
  ]

lean_lib «SilverSightRRC» where
  srcDir := "formal"
  roots := #[
    `SilverSight.HachimojiN8,
    `SilverSight.HachimojiN8Bridge,
    `SilverSight.HachimojiCharClass,
    `SilverSight.PhiDNALayout,
    `SilverSight.PhiConsistency,
    `SilverSight.PhiPipelineReceipt,
    `SilverSight.PIST.Spectral,
    `SilverSight.PIST.SpectralN,
    `SilverSight.PIST.MatrixN,
    `SilverSight.PIST.CharPoly,
    `SilverSight.PIST.FisherRigidity,
    `SilverSight.PIST.FisherRigidityN,
    `SilverSight.PIST.Classify,
    `SilverSight.PIST.ClassifyN,
    `SilverSight.PIST.Matrices250,
    `SilverSight.PIST.UnifiedCovariant,
    `SilverSight.PIST.CartanConnection,
    `SilverSight.PIST.YangBaxter,
    `SilverSight.PIST.SidonMirrorNotch,
    `SilverSight.PIST.Tdoku16D,
    `SilverSight.PIST.CrossDomainSynthesis,
    `SilverSight.PIST.MultiSurfacePacker,
    `SilverSight.PIST.ManifoldShortcut,
    `SilverSight.PIST.SidonAdapter,
    `SilverSight.PIST.WeightCandidateGen,
    `SilverSight.PIST.UnitDistCandidateGen,
    `SilverSight.PIST.CMYKColoringCore,
    `SilverSight.RRCLogogramProjection,
    `SilverSight.ReceiptCore,
    `SilverSight.RRC.Emit,
    `SilverSight.RRC.ReceiptDensity,
    `SilverSight.RRC.PolyFactorIdentity,
    `SilverSight.RRC.EntropyCandidates,
    `SilverSight.RRC.Q16_16Manifold,
    `SilverSight.AVMIsa.Types,
    `SilverSight.AVMIsa.Value,
    `SilverSight.AVMIsa.Instr,
    `SilverSight.AVMIsa.State,
    `SilverSight.AVMIsa.Step,
    `SilverSight.AVMIsa.TypeCheck,
    `SilverSight.AVMIsa.TypeSafety,
    `SilverSight.AVMIsa.Run,
    `SilverSight.AVMIsa.Emit,
    `SilverSight.AdjugateMatrix,
    `SilverSight.ColdReviewer,
    `SilverSight.Rollup,
    `SilverSight.FeasibleSet.Theorem,
    `SilverSight.FeasibleSet.QUBORelaxation,
    `SilverSight.CollectiveIntelligence.CostTransparency,
    `RRCLib.RRCEmit
  ]

/-! Dead code archived 2026-07-03. See archive/dead_code_2026-07-03/README.md
    - CoreFormalism/CharacterTransform.lean
    - PVGS_DQ_Bridge/ (8 .lean + 1 .py)
    - UniversalEncoding/ (2 .lean)
    - SilverSight/PIST/SpectralWitness.lean
    - SilverSight/Bind.lean
    - SilverSight/FeasibleSet/TestChain.lean
-/

lean_exe «rrc-emit-fixture» where
  root := `RrcEmitFixture
  srcDir := "exe"

lean_exe «q16-roundtrip» where
  root := `Q16_16Roundtrip
  srcDir := "exe"

-- Static C library for the Q16_16 roundtrip executable.
def cSrcDir : FilePath := FilePath.mk "c"

target q16_canonical.o pkg : FilePath := do
  let oFile := pkg.buildDir / cSrcDir / "q16_canonical.o"
  let srcJob ← inputFile (pkg.srcDir / cSrcDir / "q16_canonical.c") true
  let flags := #["-fPIC", "-O2"]
  buildO oFile srcJob flags

extern_lib q16_canonical pkg := do
  let name := nameToStaticLib "q16_canonical"
  let libFile := pkg.buildDir / cSrcDir / name
  let oJob ← fetch <| pkg.target ``q16_canonical.o
  buildStaticLib libFile #[oJob]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0-rc2"