Add nix package management (#772)

This patch adds support for developing and building alt-ergo using nix.

Usage:
 - `nix-shell` creates a new development shell that can be used to
   develop alt-ergo in a standard way using `dune`

 - `nix run -f . alt-ergo` to build and run alt-ergo using nix

Dependencies are managed using [niv](nmattia/niv).

.gitignore

@@ -43,3 +43,6 @@ www/
 
 # Generated dune files by gentest
 tests/*/**/dune
+
+# Generated nix files
+/result*

CONTRIBUTING.md

@@ -29,6 +29,27 @@ In addition to agreeing to the terms of the Alt-Ergo's [License], we ask our con
 [License]: ../About/licenses/index
 [Contributor License Agreement (CLA)]: https://www.ocamlpro.com/files/CLA-OCamlPro-corporate.txt
 
+## Develop with Nix
+
+If you are using nix, you can get a development shell for Alt-Ergo using:
+
+```shell
+$ nix-shell
+```
+
+To build and run a development version of alt-ergo you can use (this requires
+the [experimental `nix` command](https://nixos.wiki/wiki/Nix_command)):
+
+```shell
+$ nix run -f . alt-ergo
+```
+
+Or directly from GitHub:
+
+```shell
+$ nix run -f https://github.com/OCamlPro/alt-ergo/archive/master.tar.gz#alt-ergo alt-ergo
+```
+
 ## Release Process
 
 Alt-Ergo releases do not have a fixed schedule and are made based on features. We try to maintain the main branch (`next`) of the repository as stable as possible, and cut a release from there when an important feature is complete. We also make point release to fix important bugs.

default.nix

@@ -0,0 +1,59 @@
+{ sources ? import ./nix/sources.nix
+, pkgs ? import ./nix { inherit sources; }
+}:
+
+let
+  inherit (pkgs) lib ocamlPackages;
+  version = "dev";
+  src = lib.cleanSource ./.;
+  alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+    pname = "alt-ergo-lib";
+    inherit version src;
+
+    minimalOCamlVersion = "4.08";
+    duneVersion = "3";
+
+    propagatedBuildInputs = with ocamlPackages; [
+      dune-build-info
+      zarith
+      ocplib-simplex
+      seq
+      stdlib-shims
+      fmt
+      ppx_blob
+      dolmen_loop
+      camlzip
+    ];
+  };
+
+  alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+    pname = "alt-ergo-parsers";
+    inherit version src;
+
+    minimalOCamlVersion = "4.08";
+    duneVersion = "3";
+
+    nativeBuildInputs = [ ocamlPackages.menhir ];
+    propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [
+      psmt2-frontend
+    ]);
+  };
+
+  alt-ergo = ocamlPackages.buildDunePackage {
+    pname = "alt-ergo";
+    inherit version src;
+
+    minimalOCamlVersion = "4.08";
+    duneVersion = "3";
+
+    buildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [
+      cmdliner
+      dune-site
+    ]);
+  };
+
+in
+
+{
+  alt-ergo = alt-ergo;
+}

nix/default.nix

@@ -0,0 +1,16 @@
+{ sources ? import ./sources.nix }:
+
+import sources.nixpkgs {
+  overlays = [
+    (_: pkgs: { inherit sources; })
+    (_: pkgs: {
+      ocamlPackages = pkgs.ocamlPackages.overrideScope' (self: super: {
+        pp_loc = pkgs.callPackage ./pp_loc.nix { };
+        ocplib-simplex = pkgs.callPackage ./ocplib-simplex.nix { };
+        dolmen = pkgs.callPackage ./dolmen.nix { };
+        dolmen_type = pkgs.callPackage ./dolmen_type.nix { };
+        dolmen_loop = pkgs.callPackage ./dolmen_loop.nix { };
+      });
+    })
+  ];
+}

nix/dolmen.nix

@@ -0,0 +1,23 @@
+{ sources, lib, ocamlPackages }:
+
+let
+  dolmen = sources.dolmen;
+in
+
+ocamlPackages.buildDunePackage {
+  strictDeps = true;
+  pname = "dolmen";
+  inherit (dolmen) version;
+
+  minimalOCamlVersion = "4.08";
+  duneVersion = "3";
+
+  src = dolmen;
+
+  nativeBuildInputs = [ ocamlPackages.menhir ];
+  propagatedBuildInputs = [ ocamlPackages.menhirLib ocamlPackages.fmt ];
+
+  meta = with lib; {
+    inherit (dolmen) homepage description;
+  };
+}

nix/dolmen_loop.nix

@@ -0,0 +1,13 @@
+{ sources, lib, ocamlPackages }:
+
+ocamlPackages.buildDunePackage {
+  pname = "dolmen_loop";
+  inherit (ocamlPackages.dolmen) version src strictDeps;
+
+  minimalOCamlVersion = "4.08";
+  duneVersion = "3";
+
+  propagatedBuildInputs = [ ocamlPackages.gen ocamlPackages.dolmen_type ];
+
+  meta = ocamlPackages.dolmen.meta;
+}

nix/dolmen_type.nix

@@ -0,0 +1,18 @@
+{ sources, lib, ocamlPackages }:
+
+ocamlPackages.buildDunePackage {
+  pname = "dolmen_type";
+  inherit (ocamlPackages.dolmen) version src strictDeps;
+
+  minimalOCamlVersion = "4.08";
+  duneVersion = "3";
+
+  propagatedBuildInputs = [
+    ocamlPackages.dolmen
+    ocamlPackages.pp_loc
+    ocamlPackages.spelll
+    ocamlPackages.uutf
+  ];
+
+  meta = ocamlPackages.dolmen.meta;
+}

nix/ocplib-simplex.nix

@@ -0,0 +1,18 @@
+{ sources, lib, ocamlPackages }:
+
+ocamlPackages.buildDunePackage {
+  strictDeps = true;
+  pname = "ocplib-simplex";
+  inherit (sources.ocplib-simplex) version;
+
+  minimalOCamlVersion = "4.02";
+  duneVersion = "3";
+
+  src = sources.ocplib-simplex;
+
+  propagatedBuildInputs = [ ocamlPackages.num ocamlPackages.logs ];
+
+  meta = with lib; {
+    inherit (sources.ocplib-simplex) homepage description;
+  };
+}

nix/pp_loc.nix

@@ -0,0 +1,13 @@
+{ sources, lib, ocamlPackages }:
+
+ocamlPackages.buildDunePackage {
+  strictDeps = true;
+  pname = "pp_loc";
+  inherit (sources.pp_loc) version;
+
+  src = sources.pp_loc;
+
+  meta = with lib; {
+    inherit (sources.pp_loc) homepage description;
+  };
+}

nix/sources.json

@@ -0,0 +1,53 @@
+{
+    "dolmen": {
+        "branch": "v0.9",
+        "description": "Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction",
+        "homepage": "",
+        "owner": "Gbury",
+        "repo": "dolmen",
+        "rev": "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a",
+        "sha256": "1lbygac7pmq8d5pps4idc36ga69vx2fwz9pdpv7j2xiqxgava46y",
+        "type": "tarball",
+        "url": "https://github.com/Gbury/dolmen/archive/d9f5abbaffe6e5daa4b06758db66134fe85c8c6a.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
+        "version": "0.9"
+    },
+    "nixpkgs": {
+        "branch": "release-23.05",
+        "description": "Nix Packages collection",
+        "homepage": null,
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "b4ddd645e94706759d443755dbec35901553f35d",
+        "sha256": "1bbg07zmjv5b60v3ar18jpx2fhla2575kcrami53gn2xzm7g9py6",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/b4ddd645e94706759d443755dbec35901553f35d.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+    },
+    "ocplib-simplex": {
+        "branch": "v0.5",
+        "description": "A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities",
+        "homepage": "",
+        "owner": "OCamlPro",
+        "repo": "ocplib-simplex",
+        "rev": "9b0944c81088b9039775e48cdbc3499128ca3692",
+        "sha256": "1dxx68k2smnxrp9b8snpvi74d41yfxn2j6swbqnny6r1d1950bmk",
+        "type": "tarball",
+        "url": "https://github.com/OCamlPro/ocplib-simplex/archive/9b0944c81088b9039775e48cdbc3499128ca3692.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
+        "version": "0.5"
+    },
+    "pp_loc": {
+        "branch": "v2.1.0",
+        "description": "Pretty-printing for error source locations",
+        "homepage": "https://armael.github.io/pp_loc/pp_loc/",
+        "owner": "Armael",
+        "repo": "pp_loc",
+        "rev": "d8162fd289849ea2f4125054ab88540416bdaa25",
+        "sha256": "1wf5pqfxbfbjlwg24n3w99xm29qn1xjjjqn2z01vr5wgxcj9nfvd",
+        "type": "tarball",
+        "url": "https://github.com/Armael/pp_loc/archive/d8162fd289849ea2f4125054ab88540416bdaa25.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
+        "version": "2.1.0"
+    }
+}