Skip to content

QUICKSTART-DEV.adoc

Latest commit

 

History

History
130 lines (102 loc) · 3.74 KB

QUICKSTART-DEV.adoc

File metadata and controls

130 lines (102 loc) · 3.74 KB
Raw

valence-shell — Quick Start for Developers

Table of Contents

Tech Stack

  • Rust — CLI implementation (impl/rust-cli/), Cargo crate vsh

  • Idris2 — ABI definitions with formal proofs (src/abi/, proofs/idris2/)

  • Zig — C-compatible FFI layer (ffi/zig/, exports valence_shell_*)

  • Coq / Lean4 / Agda / Isabelle / Mizar — 6-system polyglot proofs (proofs/)

  • Elixir — NIF daemon + MCP server (impl/elixir/)

  • OCaml — Lean-extraction FFI wrapper (impl/ocaml/)

Set Up Development Environment

Option A: Guix (preferred)

guix shell

Option B: Nix (fallback)

nix develop

Option C: Manual

git clone https://github.com/hyperpolymath/valence-shell.git
cd valence-shell
just setup-dev

Build

just build-everything    # Build proofs + FFI + CLI + Elixir + MCP
# or one layer at a time:
just build-coq           # Coq proofs
just build-lean4         # Lean4 proofs
just build-cli           # Rust CLI (vsh)
just build-ffi           # Zig + OCaml FFI

Test

just verify-all          # Verify all proof systems
just test-cli            # Cargo test for impl/rust-cli/
just test-ffi-zig        # Zig FFI integration tests
just test-ffi-ocaml      # OCaml FFI tests
just test-elixir         # Elixir NIF tests

Project Structure

valence-shell/
├── src/                  # Source code
├── src/abi/              # Idris2 ABI definitions (if applicable)
├── ffi/zig/              # Zig FFI bridge (if applicable)
├── tests/                # Test suite
├── docs/                 # Documentation
├── .machine_readable/    # Checkpoint files (STATE, META, ECOSYSTEM)
├── Justfile              # Task runner recipes
├── guix.scm              # Guix environment
├── flake.nix             # Nix environment (fallback)
└── 0-AI-MANIFEST.a2ml    # AI agent entry point

Key Recipes

just build          # Build the project
just test           # Run tests
just doctor         # Self-diagnostic
just lint           # Lint and format
just panic-scan     # Security scan via panic-attacker
just tour           # Guided tour of the codebase

Before Submitting a PR

just lint           # Format and lint
just test           # All tests pass
just panic-scan     # No new security issues

Contractile Invariants

Read .machine_readable/MUST.contractile before making changes. Key invariants that must never be violated:

  • No hardcoded absolute paths (/home/, /mnt/); use env vars, XDG dirs, or relative references

  • No new TypeScript / Python / Go files; no npm/bun/yarn/pnpm dependencies (Deno only)

  • No believe_me or assert_total (Idris2); no new Admitted. (Coq); no sorry (Lean); no unsafeCoerce (Haskell); no Obj.magic (OCaml)

  • No unsafe {} blocks without an inline safety comment (Rust)

  • No template placeholders ({{…​}}, <…​>) in shipped files — see .machine_readable/bot_directives/methodology.a2ml

  • All commits MUST be GPG-signed

  • Full machine-checked list lives at .machine_readable/MUST.contractile; K9 validators in contractiles/k9/ enforce it on every PR

LLM/AI Agent Development

If using an AI assistant, load the warmup context first:

just llm-context    # Outputs role-appropriate context

Or read 0-AI-MANIFEST.a2ml and .claude/CLAUDE.md directly.

Get Help