tla-connect 0.0.4

TLA+/Apalache integration for model-based testing
Documentation 
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

{
  description = "tla-connect: TLA+/Apalache integration for model-based testing";

  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
    crane.url = "github:ipetkov/crane";
    flake-utils.url = "github:numtide/flake-utils";
    rust-overlay = {
      url = "github:oxalica/rust-overlay";
      inputs.nixpkgs.follows = "nixpkgs";
    };
  };

  outputs = { self, nixpkgs, crane, flake-utils, rust-overlay, ... }:
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = import nixpkgs {
          inherit system;
          overlays = [ (import rust-overlay) ];
        };

        rustToolchain = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml;
        craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;

        # Check if Cargo.lock exists to determine if we can build
        cargoLockExists = builtins.pathExists ./Cargo.lock;

        src = if cargoLockExists then craneLib.cleanCargoSource (craneLib.path ./.) else ./.;

        commonArgs = {
          inherit src;
          pname = "tla-connect";
          version = "0.1.0";
          strictDeps = true;

          buildInputs = [ ] ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
            pkgs.libiconv
          ];
        };

        # Only build if Cargo.lock exists
        cargoArtifacts = if cargoLockExists then craneLib.buildDepsOnly commonArgs else null;

        tla-connect = if cargoLockExists then craneLib.buildPackage (commonArgs // {
          inherit cargoArtifacts;
        }) else null;
      in
      {
        checks = pkgs.lib.optionalAttrs cargoLockExists {
          inherit tla-connect;

          tla-connect-clippy = craneLib.cargoClippy (commonArgs // {
            inherit cargoArtifacts;
            cargoClippyExtraArgs = "--all-targets -- --deny warnings";
          });

          tla-connect-doc = craneLib.cargoDoc (commonArgs // {
            inherit cargoArtifacts;
          });

          tla-connect-fmt = craneLib.cargoFmt {
            inherit src;
            pname = "tla-connect";
            version = "0.1.0";
          };

          tla-connect-nextest = craneLib.cargoNextest (commonArgs // {
            inherit cargoArtifacts;
            partitions = 1;
            partitionType = "count";
          });
        };

        packages = pkgs.lib.optionalAttrs cargoLockExists {
          default = tla-connect;
        };

        devShells.default = pkgs.mkShell {
          packages = with pkgs; [
            # Rust toolchain (from rust-overlay)
            rustToolchain
            rust-analyzer

            # Cargo tools
            cargo-watch
            cargo-edit
            cargo-outdated
            cargo-audit
            cargo-nextest

            # Development tools
            just
          ];
        };
      });
}