|
| 1 | +# SPDX-License-Identifier: AGPL-3.0-or-later |
| 2 | +# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell |
| 3 | +# |
| 4 | +# Valence Shell - Nix Flake (Fallback Package Manager) |
| 5 | +# Primary: guix.scm | Fallback: flake.nix (per RSR guidelines) |
| 6 | +# |
| 7 | +# Usage: |
| 8 | +# nix develop # Enter development shell |
| 9 | +# nix build # Build the project |
| 10 | +# nix flake check # Verify the flake |
| 11 | + |
| 12 | +{ |
| 13 | + description = "Valence Shell - Formally verified shell implementing MAA framework"; |
| 14 | + |
| 15 | + inputs = { |
| 16 | + nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.05"; |
| 17 | + flake-utils.url = "github:numtide/flake-utils"; |
| 18 | + }; |
| 19 | + |
| 20 | + outputs = { self, nixpkgs, flake-utils }: |
| 21 | + flake-utils.lib.eachDefaultSystem (system: |
| 22 | + let |
| 23 | + pkgs = nixpkgs.legacyPackages.${system}; |
| 24 | + |
| 25 | + # Proof assistant versions |
| 26 | + proofTools = with pkgs; [ |
| 27 | + # Coq - Calculus of Inductive Constructions |
| 28 | + coq_8_18 |
| 29 | + coqPackages_8_18.coqide |
| 30 | + |
| 31 | + # OCaml - For extraction and FFI |
| 32 | + ocaml |
| 33 | + ocamlPackages.findlib |
| 34 | + ocamlPackages.dune_3 |
| 35 | + |
| 36 | + # Z3 SMT Solver |
| 37 | + z3 |
| 38 | + ]; |
| 39 | + |
| 40 | + # Build tools |
| 41 | + buildTools = with pkgs; [ |
| 42 | + just |
| 43 | + git |
| 44 | + gnumake |
| 45 | + ]; |
| 46 | + |
| 47 | + # Development tools |
| 48 | + devTools = with pkgs; [ |
| 49 | + # Shell utilities |
| 50 | + bash |
| 51 | + coreutils |
| 52 | + findutils |
| 53 | + |
| 54 | + # Container support |
| 55 | + podman |
| 56 | + ]; |
| 57 | + |
| 58 | + in { |
| 59 | + # Development shell |
| 60 | + devShells.default = pkgs.mkShell { |
| 61 | + name = "valence-shell-dev"; |
| 62 | + |
| 63 | + buildInputs = proofTools ++ buildTools ++ devTools; |
| 64 | + |
| 65 | + shellHook = '' |
| 66 | + echo "Valence Shell Development Environment" |
| 67 | + echo "======================================" |
| 68 | + echo "Version: 0.6.0" |
| 69 | + echo "" |
| 70 | + echo "Available proof systems:" |
| 71 | + echo " - Coq $(coqc --version 2>/dev/null | head -1 || echo 'not found')" |
| 72 | + echo " - Z3 $(z3 --version 2>/dev/null || echo 'not found')" |
| 73 | + echo "" |
| 74 | + echo "Build commands:" |
| 75 | + echo " just build-all - Build all proofs" |
| 76 | + echo " just verify-all - Verify all proofs" |
| 77 | + echo " just demo - Run demonstration" |
| 78 | + echo " just --list - Show all commands" |
| 79 | + echo "" |
| 80 | + echo "Note: Lean 4, Agda, Isabelle, and Mizar require separate installation." |
| 81 | + echo "See proofs/README.md for setup instructions." |
| 82 | + ''; |
| 83 | + }; |
| 84 | + |
| 85 | + # Packages |
| 86 | + packages.default = pkgs.stdenv.mkDerivation { |
| 87 | + pname = "valence-shell"; |
| 88 | + version = "0.6.0"; |
| 89 | + |
| 90 | + src = ./.; |
| 91 | + |
| 92 | + buildInputs = [ pkgs.coq_8_18 pkgs.ocaml ]; |
| 93 | + |
| 94 | + buildPhase = '' |
| 95 | + # Build Coq proofs |
| 96 | + cd proofs/coq |
| 97 | + for f in *.v; do |
| 98 | + if [ -f "$f" ]; then |
| 99 | + coqc "$f" || true |
| 100 | + fi |
| 101 | + done |
| 102 | + ''; |
| 103 | + |
| 104 | + installPhase = '' |
| 105 | + mkdir -p $out/share/valence-shell |
| 106 | + cp -r proofs $out/share/valence-shell/ |
| 107 | + cp -r impl $out/share/valence-shell/ 2>/dev/null || true |
| 108 | + cp -r docs $out/share/valence-shell/ 2>/dev/null || true |
| 109 | + cp README.md $out/share/valence-shell/ 2>/dev/null || true |
| 110 | + ''; |
| 111 | + |
| 112 | + meta = with pkgs.lib; { |
| 113 | + description = "Formally verified shell implementing MAA framework"; |
| 114 | + homepage = "https://github.com/hyperpolymath/valence-shell"; |
| 115 | + license = with licenses; [ mit agpl3Plus ]; |
| 116 | + maintainers = []; |
| 117 | + platforms = platforms.unix; |
| 118 | + }; |
| 119 | + }; |
| 120 | + |
| 121 | + # Checks |
| 122 | + checks = { |
| 123 | + # Verify flake builds |
| 124 | + build = self.packages.${system}.default; |
| 125 | + }; |
| 126 | + } |
| 127 | + ); |
| 128 | +} |
0 commit comments