# SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.8
# SPDX-FileCopyrightText: 2026 Hyperpolymath
#
# Justfile - Oblíbený task runner
# All operations go through this file. See AUTHORITY_STACK.mustfile-nickel.scm.

set shell := ["bash", "-euo", "pipefail", "-c"]

# Default: show available recipes
default:
    @just --list

# ============================================================================
# BUILD
# ============================================================================

# Build the Oblíbený compiler
build:
    dune build

# Build with all warnings as errors
build-strict:
    dune build --force --error-reporting=short

# ============================================================================
# TEST
# ============================================================================

# Run all tests (conformance + unit)
test:
    dune test

# Run tests with verbose output
test-verbose:
    dune test --force --verbose

# ============================================================================
# PROOFS + FFI CHECKS (local mirrors of the ci.yml gate, PR #52/#56)
# ============================================================================

# Type-check (= prove) the Idris2 ABI proof layer — same gate as CI
proofs:
    idris2 --build src/abi/oblibeny-abi.ipkg

# Compile-check every Zig FFI source (no link; linking needs system liboqs)
zig-ffi-check:
    @if command -v zig >/dev/null 2>&1; then \
        for f in ffi/zig/src/*.zig ffi/zig/src/packages/*.zig; do \
            [ -f "$f" ] && echo "ast-check $f" && zig ast-check "$f"; \
        done; \
        echo "✓ Zig FFI sources compile-checked"; \
    else \
        echo "zig not installed — skipping (see ffi/zig/build.zig; Zig 0.13 verified in PR #56)"; \
    fi

# Fail if any soundness escape hatch appears in the ABI proofs — same gate as ci.yml
guard-escape-hatches:
    @if grep -rnE 'believe_me|assert_total|\bpostulate\b|\bpartial\b|idris_crash|\?[A-Za-z_][A-Za-z0-9_]*' \
         src/abi/Crypto.idr src/abi/Packages; then \
        echo "ERROR: soundness escape hatch found in ABI proofs"; \
        exit 1; \
    fi
    @echo "no escape hatches"

# ============================================================================
# RUN
# ============================================================================

# Run the golden path smoke test
demo:
    dune exec -- oblibeny examples/hello.obl --dump-trace

# Execute an Oblíbený program
run FILE:
    dune exec -- oblibeny {{FILE}}

# Check a file without executing (constrained form validation)
check FILE:
    dune exec -- oblibeny {{FILE}} --check

# ============================================================================
# DEVELOPMENT
# ============================================================================

# Format OCaml code
fmt:
    dune fmt 2>/dev/null || ocamlformat --inplace lib/*.ml bin/*.ml test/*.ml 2>/dev/null || echo "ocamlformat not available"

# Run lints and static checks
lint:
    @echo "Running constrained form validation..."
    dune build @check 2>/dev/null || dune build

# Clean build artifacts
clean:
    dune clean

# Rebuild from scratch
rebuild: clean build

# Watch for changes and rebuild
watch:
    dune build --watch

# ============================================================================
# DOCUMENTATION
# ============================================================================

# Generate documentation
doc:
    dune build @doc 2>/dev/null || echo "Documentation build not configured"

# ============================================================================
# RELEASE
# ============================================================================

# Run all checks (lint + test + FFI compile-check + escape-hatch guard)
ci: lint test zig-ffi-check guard-escape-hatches
    @echo "All checks passed."

# Prepare a release
release VERSION:
    @echo "Releasing {{VERSION}}..."
    @echo "1. Update dune-project version"
    @echo "2. Run: just ci"
    @echo "3. Tag: git tag v{{VERSION}}"
    @echo "4. Push: git push --tags"

# ============================================================================
# SPEC VALIDATION
# ============================================================================

# Verify ANCHOR and SPEC files are valid Scheme
validate-spec:
    @echo "Validating specification files..."
    @for f in ANCHOR*.scm SPEC*.scm AUTHORITY*.scm; do \
        if [ -f "$f" ]; then \
            echo "  ✓ $f exists"; \
        fi; \
    done

# Show the golden path command
golden-path:
    @echo "Golden path (from ANCHOR):"
    @echo "  dune test && dune exec -- oblibeny examples/hello.obl"

# ============================================================================
# DISTRIBUTION PROOF-OF-CONCEPT
# ============================================================================

# Verify Idris2 ABI proofs for hello package (ipkg-level; per-file --check is a fake gate)
abi-check-hello:
    @echo "Checking Idris2 ABI proofs (via oblibeny-abi.ipkg)..."
    cd src/abi && idris2 --build oblibeny-abi.ipkg

# Generate C code from the Idris2 ABI interface (module root = src/abi)
abi-gen-hello:
    @echo "Generating C from Idris2..."
    mkdir -p generated/abi/hello
    cd src/abi && idris2 --codegen c Packages/Hello/Interface.idr
    @echo "Generated under src/abi/build/ (C backend)"

# Build Zig FFI library for hello package
ffi-build-hello:
    @echo "Building Zig FFI for hello package..."
    mkdir -p dist/ffi
    cd ffi/zig && zig build-lib src/packages/hello.zig \
        -dynamic \
        -target x86_64-linux-musl \
        -O ReleaseSafe \
        -femit-bin=../../dist/ffi/libhello.so
    @echo "Built: dist/ffi/libhello.so"

# Build hello package for all architectures
pkg-build-hello:
    @echo "Cross-compiling hello for all architectures..."
    @mkdir -p examples/packages/hello.zpkg/binaries/x86_64 \
        examples/packages/hello.zpkg/binaries/aarch64 \
        examples/packages/hello.zpkg/binaries/riscv64
    @echo "  x86_64..."
    @cd examples/packages/hello.zpkg && \
        echo 'const std = @import("std"); pub fn main() !void { std.debug.print("Hello, Oblibeny Distribution!\\n", .{}); }' > hello.zig && \
        zig build-exe hello.zig -target x86_64-linux-musl -O ReleaseSafe && \
        mv hello binaries/x86_64/
    @echo "  aarch64..."
    @cd examples/packages/hello.zpkg && \
        zig build-exe hello.zig -target aarch64-linux-musl -O ReleaseSafe && \
        mv hello binaries/aarch64/
    @echo "  riscv64..."
    @cd examples/packages/hello.zpkg && \
        zig build-exe hello.zig -target riscv64-linux-musl -O ReleaseSafe && \
        mv hello binaries/riscv64/ && \
        rm -f hello.zig hello.o
    @echo "✓ Cross-compilation complete"

# Package hello.zpkg archive
pkg-archive-hello: pkg-build-hello
    @echo "Creating hello.zpkg archive..."
    cd examples/packages && tar -czf hello-1.0.0.zpkg hello.zpkg/
    @echo "✓ Created: examples/packages/hello-1.0.0.zpkg"

# Test hello package installation (requires root)
pkg-test-hello:
    @echo "Testing hello package installation..."
    @echo "WARNING: This requires root permissions"
    @echo "This is a placeholder - actual test not implemented yet"

# Build complete distribution stack
dist-build: abi-check-hello ffi-build-hello pkg-build-hello
    @echo "✓ Distribution stack built successfully"

# Show distribution architecture info
dist-info:
    @echo "Oblibeny Distribution Architecture"
    @echo "===================================="
    @echo ""
    @echo "Layer 1: Idris2 (ABI + Proofs)"
    @echo "  Location: src/abi/"
    @echo "  Purpose:  Formal verification of package interfaces"
    @echo ""
    @echo "Layer 2: Zig (FFI Implementation)"
    @echo "  Location: ffi/zig/"
    @echo "  Purpose:  System-level package operations"
    @echo ""
    @echo "Layer 3: Oblibeny (Coordination)"
    @echo "  Location: examples/packages/*.zpkg/install.obl"
    @echo "  Purpose:  Constrained-form package orchestration"
    @echo ""
    @echo "See: docs/DISTRIBUTION-ARCHITECTURE.adoc"

# ============================================================================
# DISTROLESS BOOTSTRAP (Bottom-Up Approach)
# ============================================================================

# Build bootstrap toolchain on Alpine
distroless-bootstrap:
    @echo "Building Oblibeny toolchain on Alpine..."
    podman build -f Containerfile.bootstrap -t oblibeny-bootstrap:latest .
    @echo "✓ Bootstrap environment ready"

# Export static binaries for distroless
distroless-export:
    @echo "Exporting static binaries for distroless..."
    mkdir -p dist/distroless/usr/bin
    @echo "Building static binaries with Zig..."
    cd ffi/zig && \
        zig build-exe src/packages/hello.zig \
            -target x86_64-linux-musl \
            -O ReleaseSafe \
            -static \
            -fstrip \
            -femit-bin=../../dist/distroless/usr/bin/hello
    @echo "✓ Static binaries ready in dist/distroless/"

# Build minimal distroless image (~11MB)
distroless-image:
    @echo "Building minimal distroless image..."
    podman build -f Containerfile.minimal -t oblibeny:minimal .
    @echo "✓ Image built: oblibeny:minimal"

# Run minimal image
distroless-run:
    @echo "Running minimal distroless image..."
    podman run --rm oblibeny:minimal

# Verify distroless image properties
distroless-verify:
    @echo "Verifying minimal distroless image..."
    @echo ""
    @echo "=== Image Size ==="
    @podman images oblibeny:minimal --format "Size: {{{{.Size}}}}"
    @echo ""
    @echo "=== File Count ==="
    @podman run --rm oblibeny:minimal sh -c 'find / -type f 2>/dev/null | wc -l' || \
        echo "(Cannot count - no shell in distroless, which is GOOD)"
    @echo ""
    @echo "=== Binaries ==="
    @podman run --rm --entrypoint=/usr/bin/obli-pkg oblibeny:minimal || echo "obli-pkg present"
    @podman run --rm oblibeny:minimal || echo "hello present"
    @echo ""
    @echo "✓ Verification complete"

# Clean distroless artifacts
distroless-clean:
    rm -rf dist/distroless
    podman rmi oblibeny:minimal oblibeny-bootstrap 2>/dev/null || true

# Full distroless build pipeline
distroless-build-all: distroless-export distroless-image distroless-verify
    @echo "✓ Complete distroless build finished"
