import Lake
open Lake DSL

/-! # Telltale Lean Package

Lake build definition for the Telltale verification library.
Six libraries organized by subject: types, coinductive theory, choreography,
semantics, async protocol, and runtime.
-/

package telltale where
  -- Temporarily silence linter noise from iris-lean dependencies.
  moreLeanArgs := #[
    "-Dlinter.unusedSectionVars=false",
    "-Dlinter.unusedVariables=false"
  ]

-- Mathlib provides standard lemmas and automation for proofs.
-- Local checkout is pinned by revision in `lean/dependency_pins.json`
-- and validated by `scripts/check/lean-dependency-pins.sh`.
require mathlib from "/Users/hxrts/projects/lean_common/mathlib4"

-- Paco provides parametrized coinduction for EQ2 proofs.
require paco from git
  "https://github.com/hxrts/paco-lean" @ "v0.1.3"

-- Iris separation logic framework (local checkout, revision-pinned in
-- `lean/dependency_pins.json` for drift control).
require iris from "/Users/hxrts/projects/iris-lean"

-- Lean 4 code formatter.
require leanfmt from git
  "https://github.com/toku-sa-n/leanfmt" @ "main"

/-! ## Libraries -/

/-- Global and local session type definitions. -/
lean_lib SessionTypes where
  globs := #[`SessionTypes.*]

/-- Coinductive theory: EQ2, bisimulation, roundtrip bridge. -/
lean_lib SessionCoTypes where
  globs := #[`SessionCoTypes.*]

/-- Projection from global to local types and harmony correctness. -/
lean_lib Choreography where
  globs := #[`Choreography.*]

/-- Operational semantics, typing, determinism, deadlock freedom. -/
lean_lib Semantics where
  globs := #[`Semantics.*]

/-- Async buffered multiparty session types with coherence. -/
lean_lib Protocol where
  globs := #[`Protocol.*]

/-- VM, Iris separation logic backend, resource algebras, WP rules. -/
@[default_target]
lean_lib Runtime where
  globs := #[`Runtime.*]

/-- Classical transport layer: imported theorem interfaces and discharged kernels. -/
lean_lib ClassicalLayer where
  globs := #[`Classical.*]

/-- Distributed hypothesis validation and protocol-space classification. -/
lean_lib Distributed where
  globs := #[`Distributed.*]

/-- Analysis and extraction boundary layers. -/
lean_lib Entropy where
  globs := #[
    `ClassicalAnalysisAPI,
    `ClassicalAnalysisInstance,
    `ClassicalAnalysisInstance.*,
    `IrisExtractionAPI,
    `IrisExtractionInstance,
    `IrisExtractionInstance.*
  ]

/-- Linker args to silence macOS deployment target warnings for test executables. -/
def macosLinkArgs : Array String :=
  -- Match the toolchain's minimum macOS version for system libraries.
  if System.Platform.isOSX then
    #["-mmacosx-version-min=15.0"]
  else
    #[]

/-! ## Executables -/

/-- Executable runtime tests for the VM example. -/
lean_exe runtime_tests where
  root := `Runtime.Tests.Main
  moreLinkArgs := macosLinkArgs

/-- Executable simulator parity fixtures for material dynamics. -/
lean_exe simulator_parity_tests where
  root := `Runtime.Tests.SimulatorParity
  moreLinkArgs := macosLinkArgs

/-- VM runner: executes choreographies and emits observable traces. -/
lean_exe vm_runner where
  root := `Runtime.Tests.VMRunner
  moreLinkArgs := macosLinkArgs

/-- Projection validator (compares projected local types). -/
@[default_target]
lean_exe telltale_validator where
  root := `Choreography.Projection.Validator
  moreLinkArgs := macosLinkArgs
