fix: nix

default.nix

@@ -1,35 +1,37 @@
-{ withProvers ? false, devDeps ? [] }:
+{ withProvers ? false, devDeps ? [ ], nixpkgs }:
+with nixpkgs;
 
-with import <nixpkgs> {};
-
-let alt-ergo-pin = callPackage scripts/nix/alt-ergo/default.nix { nixpkgs = <nixpkgs>; };
+let alt-ergo-pin = callPackage scripts/nix/alt-ergo/default.nix { nixpkgs = nixpkgs; };
 in
 
-let cvc4-pin = callPackage scripts/nix/cvc4/default.nix { nixpkgs = <nixpkgs>; };
+let cvc4-pin = callPackage scripts/nix/cvc4/default.nix { nixpkgs = nixpkgs; };
 in
 
-let cvc5-pin = callPackage scripts/nix/cvc5/default.nix { nixpkgs = <nixpkgs>; };
+let cvc5-pin = callPackage scripts/nix/cvc5/default.nix { nixpkgs = nixpkgs; };
 in
 
-let z3-pin = callPackage scripts/nix/z3/default.nix { nixpkgs = <nixpkgs>; };
+let z3-pin = callPackage scripts/nix/z3/default.nix { nixpkgs = nixpkgs; };
 in
 
-let provers =
-  if withProvers then [
-    alt-ergo-pin
-    cvc4-pin
-    cvc5-pin
-    z3-pin
-  ] else []; in
+let
+  provers =
+    if withProvers then [
+      alt-ergo-pin
+      cvc4-pin
+      cvc5-pin
+      z3-pin
+    ] else [ ];
+in
 
-let why3-pin =
-  why3.overrideAttrs (o : rec {
-    version = "1.6.0";
-    src = fetchurl {
-      url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
-      sha256 = "sha256-hFvM6kHScaCtcHCc6Vezl9CR7BFbiKPoTEh7kj0ZJxw=";
-    };
-  });
+let
+  why3-pin =
+    why3.overrideAttrs (o: rec {
+      version = "1.6.0";
+      src = fetchurl {
+        url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
+        sha256 = "sha256-hFvM6kHScaCtcHCc6Vezl9CR7BFbiKPoTEh7kj0ZJxw=";
+      };
+    });
 in
 
 stdenv.mkDerivation {

flake.nix

@@ -0,0 +1,23 @@
+{
+  description = "my project description";
+
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem
+      (system:
+        let pkgs = nixpkgs.legacyPackages.${system}; in
+        let ec = pkgs.callPackage ./default.nix { nixpkgs = pkgs;};
+        in {
+          devShells.default = pkgs.mkShell {
+            buildInputs = ec.buildInputs
+              ++ ec.propagatedBuildInputs
+              ++ (with pkgs.python3Packages; [
+              pyyaml
+            ]);
+          };
+        }
+
+      );
+}
+

scripts/nix/alt-ergo/default.nix

@@ -16,25 +16,29 @@ let
   };
 in
 
-let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
-  pname = "alt-ergo-lib";
-  inherit version src configureScript;
-  configureFlags = [ pname ];
-  nativeBuildInputs = [ which ];
-  buildInputs = with ocamlPackages; [ dune-configurator ];
-  propagatedBuildInputs = with ocamlPackages; [ dune-build-info num ocplib-simplex seq stdlib-shims zarith ];
-  preBuild = ''
-    substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"'
-  '';
-}; in
-
-let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
-  pname = "alt-ergo-parsers";
-  inherit version src configureScript;
-  configureFlags = [ pname ];
-  nativeBuildInputs = [ which ocamlPackages.menhir ];
-  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
-}; in
+let
+  alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+    pname = "alt-ergo-lib";
+    inherit version src configureScript;
+    configureFlags = [ pname ];
+    nativeBuildInputs = [ which ];
+    buildInputs = with ocamlPackages; [ dune-configurator ];
+    propagatedBuildInputs = with ocamlPackages; [ dune-build-info num ocplib-simplex seq stdlib-shims zarith ];
+    preBuild = ''
+      substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"'
+    '';
+  };
+in
+
+let
+  alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+    pname = "alt-ergo-parsers";
+    inherit version src configureScript;
+    configureFlags = [ pname ];
+    nativeBuildInputs = [ which ocamlPackages.menhir ];
+    propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+  };
+in
 
 ocamlPackages.buildDunePackage {
 
@@ -47,8 +51,8 @@ ocamlPackages.buildDunePackage {
 
   meta = {
     description = "High-performance theorem prover and SMT solver";
-    homepage    = "https://alt-ergo.ocamlpro.com/";
-    license     = lib.licenses.ocamlpro_nc;
+    homepage = "https://alt-ergo.ocamlpro.com/";
+    license = lib.licenses.ocamlpro_nc;
     maintainers = [ lib.maintainers.thoughtpolice ];
   };
 }

scripts/nix/cvc4/default.nix

@@ -7,9 +7,9 @@ stdenv.mkDerivation rec {
   version = "1.8";
 
   src = fetchFromGitHub {
-    owner  = "cvc4";
-    repo   = "cvc4";
-    rev    = version;
+    owner = "cvc4";
+    repo = "cvc4";
+    rev = version;
     sha256 = "1rhs4pvzaa1wk00czrczp58b2cxfghpsnq534m0l3snnya2958jp";
   };
 
@@ -41,9 +41,9 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
-    homepage    = "http://cvc4.cs.stanford.edu/web/";
-    license     = licenses.gpl3;
-    platforms   = platforms.unix;
+    homepage = "http://cvc4.cs.stanford.edu/web/";
+    license = licenses.gpl3;
+    platforms = platforms.unix;
     maintainers = with maintainers; [ vbgl thoughtpolice gebner ];
   };
 }

scripts/nix/cvc5/default.nix

@@ -7,15 +7,22 @@ stdenv.mkDerivation rec {
   version = "1.0.6";
 
   src = fetchFromGitHub {
-    owner  = "cvc5";
-    repo   = "cvc5";
-    rev    = "cvc5-${version}";
-    hash  = "sha256-pZiXAO92cwnYtaVMDFBEmk+NzDf4eKdc0eY0RltofPA=";
+    owner = "cvc5";
+    repo = "cvc5";
+    rev = "cvc5-${version}";
+    hash = "sha256-pZiXAO92cwnYtaVMDFBEmk+NzDf4eKdc0eY0RltofPA=";
   };
 
   nativeBuildInputs = [ pkg-config cmake flex ];
   buildInputs = [
-    cadical.dev symfpu gmp gtest libantlr3c antlr3_4 boost jdk
+    cadical.dev
+    symfpu
+    gmp
+    gtest
+    libantlr3c
+    antlr3_4
+    boost
+    jdk
     (python3.withPackages (ps: with ps; [ pyparsing tomli ]))
   ];
 
@@ -31,9 +38,9 @@ stdenv.mkDerivation rec {
 
   meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
-    homepage    = "https://cvc5.github.io";
-    license     = licenses.gpl3Only;
-    platforms   = platforms.unix;
+    homepage = "https://cvc5.github.io";
+    license = licenses.gpl3Only;
+    platforms = platforms.unix;
     maintainers = with maintainers; [ shadaj ];
   };
 }

scripts/nix/z3/default.nix

@@ -5,9 +5,9 @@ with import nixpkgs { };
 let python = python3; in
 
 stdenv.mkDerivation rec {
-  pname   = "z3";
+  pname = "z3";
   version = "4.12.2";
-  sha256  = "sha256-DTgpKEG/LtCGZDnicYvbxG//JMLv25VHn/NaF307JYA=";
+  sha256 = "sha256-DTgpKEG/LtCGZDnicYvbxG//JMLv25VHn/NaF307JYA=";
 
   src = fetchFromGitHub {
     owner = "Z3Prover";

shell.nix

@@ -1,14 +1,14 @@
-{ withProvers ? true, devDeps ? [] }:
+{ withProvers ? true, devDeps ? [ ] }:
 
-with import <nixpkgs> {};
+with import <nixpkgs> { };
 
 let ec = callPackage ./default.nix { inherit withProvers devDeps; };
 in
 
 pkgs.mkShell {
   buildInputs = ec.buildInputs
-  ++ ec.propagatedBuildInputs
-  ++ (with python3Packages; [
+    ++ ec.propagatedBuildInputs
+    ++ (with python3Packages; [
     pyyaml
   ]);
 }