1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120

{ depot, pkgs, lib, ... }:

# alloy-viz — headless Alloy analyzer with a browser frontend.
#
# Two binaries from one project:
#
#   alloy-viz         (Go)   the thing you run: web UI and supervisor of the
#                            solver process.
#   alloy-viz-solver  (Java) a dumb worker speaking NUL-framed JSON on stdin/
#                            stdout, holding a warm JVM and a parsed model.
#
# The Java half is built with plain javac against the release jar from nixpkgs.
# Alloy upstream builds with Gradle+bnd, but we compile a single file against a
# handful of public classes (CompUtil, TranslateAlloyToKodkod, A4Solution,
# A4SolutionWriter, A4Reporter), so none of that is needed.
#
# We do not build Alloy itself: pkgs.alloy6 ships the jar, and the jar also
# bundles an unshaded gson, which the worker uses for its JSON framing rather
# than pulling in a dependency of its own.

let
  goDeps = import ./go-deps.nix { inherit depot pkgs; };

  jdk = pkgs.openjdk21;
  alloyJar = "${pkgs.alloy6}/share/alloy/alloy6.jar";

  solver = pkgs.stdenv.mkDerivation {
    pname = "alloy-viz-solver";
    version = "0.1";

    src = ./java;

    nativeBuildInputs = [ jdk pkgs.makeWrapper ];

    buildPhase = ''
      runHook preBuild
      mkdir -p classes
      javac -cp ${alloyJar} -d classes $(find src -name '*.java')
      jar cf alloy-viz-solver.jar -C classes .
      runHook postBuild
    '';

    installPhase = ''
      runHook preInstall
      mkdir -p $out/share/java $out/bin
      cp alloy-viz-solver.jar $out/share/java/

      makeWrapper ${jdk}/bin/java $out/bin/alloy-viz-solver \
        --add-flags "-Djava.awt.headless=true" \
        --add-flags "-Dorg.slf4j.simpleLogger.logFile=/dev/null" \
        --add-flags "-cp ${alloyJar}:$out/share/java/alloy-viz-solver.jar" \
        --add-flags "de.profpatsch.alloy.Worker"
      runHook postInstall
    '';

    meta = {
      description = "Headless Alloy solver worker for alloy-viz";
      mainProgram = "alloy-viz-solver";
    };
  };

  # -Djava.awt.headless=true keeps Swing out of the picture. The parser,
  # translator and solver packages have no AWT imports at all, so this only
  # guards against incidental initialisation.
  #
  # -Dorg.slf4j.simpleLogger.logFile=/dev/null is the *only* way to silence
  # kodkod's progress chatter: it logs through slf4j-simple, and neither
  # defaultLogLevel=off nor per-logger levels suppress it. Left unsilenced it
  # would interleave with the frame stream on stderr.

  ui = depot.nix.buildGo.program {
    name = "alloy-viz";
    srcs = [
      ./main.go
      ./worker.go
      ./jobs.go
      ./instance.go
      ./theme.go
      ./dot.go
      ./serve.go
      ./templates.go
      ./watch.go
    ];
    deps = [
      goDeps.fsnotify-fsnotify
    ];
  };
in
pkgs.symlinkJoin {
  name = "alloy-viz";
  outputs = [ "out" "man" ];
  paths = [ ui solver ];
  buildInputs = [ pkgs.makeWrapper ];

  postBuild = ''
    # graphviz lays out the instance graphs; ALLOY_VIZ_SOLVER lets the Go half
    # find its worker, so `nix run` works with no further setup.
    wrapProgram $out/bin/alloy-viz \
      --prefix PATH : ${lib.makeBinPath [ pkgs.graphviz ]} \
      --set-default ALLOY_VIZ_SOLVER ${solver}/bin/alloy-viz-solver

    mkdir -p $man/share/man/man1
    cp ${./alloy-viz.1} $man/share/man/man1/alloy-viz.1
  '';

  meta = {
    description = "View Alloy instances in a browser, without the Alloy GUI";
    longDescription = ''
      Replaces driving the Alloy Analyzer's Swing GUI by hand. Point alloy-viz
      at a .als file and it solves the selected command, renders the instance
      as a graph via graphviz, and re-solves whenever the file is saved.

      The JVM is kept warm between runs, so repeated runs skip the JVM start
      and parse that `alloy exec` pays every time. Solving happens in a
      separate process because a running SAT4J solve cannot be interrupted
      in-process; cancelling kills it.
    '';
    mainProgram = "alloy-viz";
  };
}