|
| 1 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# valence-shell — Stapeln/Selur service definition. |
| 5 | +# |
| 6 | +# Formally verified shell with proven reversibility guarantees and MAA |
| 7 | +# framework. Reproducible verification container with Coq, Lean 4, Agda, |
| 8 | +# Z3, and OCaml/opam installed. Interactive container — runs /bin/bash |
| 9 | +# by default for proof verification workflows. |
| 10 | +# |
| 11 | +# Proof systems included: |
| 12 | +# - Coq — CIC foundation |
| 13 | +# - Lean 4 — Primary source of truth (via elan) |
| 14 | +# - Agda — Intensional type theory (if available) |
| 15 | +# - Z3 — SMT solver |
| 16 | +# - OCaml — Extraction target from Coq |
| 17 | +# |
| 18 | +# Usage: |
| 19 | +# podman-compose -f selur-compose.toml run --rm app |
| 20 | +# podman-compose -f selur-compose.toml run --rm app just verify-all |
| 21 | +# just stack-up |
| 22 | + |
| 23 | +[project] |
| 24 | +name = "valence-shell" |
| 25 | + |
| 26 | +# ============================================================================= |
| 27 | +# Valence Shell — Verification container (interactive) |
| 28 | +# ============================================================================= |
| 29 | +[services.app] |
| 30 | +build = { context = ".", dockerfile = "Containerfile" } |
| 31 | +restart = "no" |
| 32 | +networks = ["default"] |
| 33 | +volumes = [ |
| 34 | + "valence-workspace:/workspace/valence-shell", |
| 35 | +] |
| 36 | +# No healthcheck — this is an interactive container, not a long-running service. |
| 37 | +# Start with: podman-compose run --rm app just verify-all |
| 38 | + |
| 39 | +# ============================================================================= |
| 40 | +# Volumes |
| 41 | +# ============================================================================= |
| 42 | +[volumes.valence-workspace] |
| 43 | +driver = "local" |
0 commit comments