path: root/flake.nix

{
  description = "Sol: a total relational language and its virtual machine";

  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";

  outputs = { self, nixpkgs }:
    let
      systems = [
        "x86_64-linux"
        "aarch64-linux"
        "x86_64-darwin"
        "aarch64-darwin"
      ];

      forAllSystems = f:
        nixpkgs.lib.genAttrs systems (system:
          f (import nixpkgs { inherit system; }));
    in
    {
      packages = forAllSystems (pkgs:
        let ocamlPackages = pkgs.ocamlPackages; in
        {
          default = ocamlPackages.buildDunePackage {
            pname = "sol";
            version = "0.1.0";
            duneVersion = "3";
            src = self;

            # The parser is menhir-generated, and the proven
            # containment/lexicographic checkers are extracted from
            # Rocq during the build.
            nativeBuildInputs = [
              ocamlPackages.menhir
              pkgs.coq
            ];
            buildInputs = [
              pkgs.coqPackages.stdlib
            ];
            propagatedBuildInputs = [
              ocamlPackages.zarith
              ocamlPackages.yojson
            ];
            checkInputs = [ ocamlPackages.alcotest ];
            doCheck = true;

            meta = {
              description = "Sol: a total relational language";
              license = pkgs.lib.licenses.agpl3Only;
              maintainers = [ { name = "Marcos Magueta"; } ];
            };
          };
        });

      devShells = forAllSystems (pkgs:
        let ocamlPackages = pkgs.ocamlPackages; in
        {
          default = pkgs.mkShell {
            inputsFrom = [ self.packages.${pkgs.system}.default ];
            packages = [
              pkgs.dune_3
              ocamlPackages.ocaml
              ocamlPackages.ocaml-lsp
              ocamlPackages.ocamlformat
              ocamlPackages.utop
              ocamlPackages.odoc
              ocamlPackages.zarith
              ocamlPackages.yojson
              ocamlPackages.alcotest
              ocamlPackages.menhir
              # Rocq, for the verified checkers and their extraction
              pkgs.coq
              pkgs.coqPackages.stdlib
            ];
          };
        });
    };
}