Standardize workspace: Justfile migration and A2ML directive cleanup

Author: hyperpolymath

impl/elixir/Justfile

@@ -0,0 +1,23 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Justfile for Valence Shell Elixir NIF
+
+set shell := ["bash", "-euo", "pipefail", "-c"]
+
+default:
+    @just --list --unsorted
+
+all:
+    @erlang_path="$$(erl -eval 'io:format("~s", [lists:concat([code:root_dir(), "/erts-", erlang:system_info(version), "/include"])])' -s init stop -noshell)"
+    @erl_interface_include="$$(erl -eval 'io:format("~s", [code:lib_dir(erl_interface, include)])' -s init stop -noshell)"
+    @erl_interface_lib="$$(erl -eval 'io:format("~s", [code:lib_dir(erl_interface, lib)])' -s init stop -noshell)"
+    @mkdir -p priv
+    cd ../zig && zig build -Doptimize=ReleaseFast
+    ${CC:-gcc} -fPIC -O2 -Wall -Wextra -I"$$erlang_path" -I"$$erl_interface_include" -I../zig/src -shared -fPIC \
+      -o priv/valence_ffi.so c_src/valence_nif.c ../zig/zig-out/lib/libvalence_ffi.a -L"$$erl_interface_lib" -lei -lpthread
+
+zig-lib:
+    cd ../zig && zig build -Doptimize=ReleaseFast
+
+clean:
+    rm -rf priv
+    rm -f c_src/*.o

impl/elixir/Makefile

@@ -0,0 +1,43 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Justfile for Lean4 -> C -> OCaml extraction pipeline
+
+set shell := ["bash", "-euo", "pipefail", "-c"]
+
+lean_src := "../../proofs/lean4"
+lean_extraction := "Extraction"
+target := "liblean_vsh.so"
+
+default:
+    @just --list --unsorted
+
+build-lean:
+    @echo "Building Lean 4 extraction..."
+    cd {{lean_src}} && lake build {{lean_extraction}}
+
+build-c: build-lean
+    @lean_prefix="$$(lean --print-prefix)"
+    @lean_include="$$lean_prefix/include"
+    @lean_lib="$$lean_prefix/lib/lean"
+    gcc -shared -fPIC -o {{target}} \
+      lean_wrapper.c \
+      {{lean_src}}/.lake/build/ir/{{lean_extraction}}.c \
+      -I"$$lean_include" -L"$$lean_lib" -lleanshared -Wl,-rpath,"$$lean_lib"
+
+all: build-c
+
+test: all
+    @if [ -f {{target}} ]; then \
+      echo "{{target}} exists"; \
+      ldd {{target}} | grep lean || echo "Warning: Lean library not linked"; \
+    else \
+      echo "{{target}} not found"; \
+      exit 1; \
+    fi
+
+clean:
+    rm -f {{target}}
+    cd {{lean_src}} && lake clean
+
+install: all
+    sudo cp {{target}} /usr/local/lib/
+    sudo ldconfig

impl/ocaml/Justfile

@@ -0,0 +1,20 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Justfile for Valence Shell Rocq proofs
+
+set shell := ["bash", "-euo", "pipefail", "-c"]
+
+default:
+    @just --list --unsorted
+
+build-mk:
+    coq_makefile -f _CoqProject -o build.mk
+
+all: build-mk
+    make -f build.mk
+
+clean:
+    @if [ -f build.mk ]; then make -f build.mk clean; fi
+    rm -f build.mk build.mk.conf
+
+install: build-mk
+    make -f build.mk install