From 79736e578fb3548d18e9e355cf960f8e9e52966f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Tue, 14 May 2024 13:47:26 +0200
Subject: [PATCH] feat(nix): Add nix support in the 2.5.x branch (#1121)

With the right Dolmen version.
---
 default.nix            |  61 +++++++++++++
 nix/default.nix        |  16 ++++
 nix/dolmen.nix         |  23 +++++
 nix/dolmen_loop.nix    |  13 +++
 nix/dolmen_type.nix    |  18 ++++
 nix/ocplib-simplex.nix |  18 ++++
 nix/pp_loc.nix         |  13 +++
 nix/sources.json       |  53 +++++++++++
 nix/sources.nix        | 198 +++++++++++++++++++++++++++++++++++++++++
 shell.nix              |  42 +++++++++
 10 files changed, 455 insertions(+)
 create mode 100644 default.nix
 create mode 100644 nix/default.nix
 create mode 100644 nix/dolmen.nix
 create mode 100644 nix/dolmen_loop.nix
 create mode 100644 nix/dolmen_type.nix
 create mode 100644 nix/ocplib-simplex.nix
 create mode 100644 nix/pp_loc.nix
 create mode 100644 nix/sources.json
 create mode 100644 nix/sources.nix
 create mode 100644 shell.nix

diff --git a/default.nix b/default.nix
new file mode 100644
index 000000000..b0d4b045e
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,61 @@
+{ 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
+      ppx_deriving
+      stdcompat
+    ];
+  };
+
+  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;
+}
diff --git a/nix/default.nix b/nix/default.nix
new file mode 100644
index 000000000..eef884edd
--- /dev/null
+++ b/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 { };
+      });
+    })
+  ];
+}
diff --git a/nix/dolmen.nix b/nix/dolmen.nix
new file mode 100644
index 000000000..d1f4cbe3e
--- /dev/null
+++ b/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 = with ocamlPackages; [ hmap menhirLib fmt ];
+
+  meta = with lib; {
+    inherit (dolmen) homepage description;
+  };
+}
diff --git a/nix/dolmen_loop.nix b/nix/dolmen_loop.nix
new file mode 100644
index 000000000..08a03c965
--- /dev/null
+++ b/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;
+}
diff --git a/nix/dolmen_type.nix b/nix/dolmen_type.nix
new file mode 100644
index 000000000..46f1c64b5
--- /dev/null
+++ b/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;
+}
diff --git a/nix/ocplib-simplex.nix b/nix/ocplib-simplex.nix
new file mode 100644
index 000000000..1e01afc95
--- /dev/null
+++ b/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;
+  };
+}
diff --git a/nix/pp_loc.nix b/nix/pp_loc.nix
new file mode 100644
index 000000000..95ca16eff
--- /dev/null
+++ b/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;
+  };
+}
diff --git a/nix/sources.json b/nix/sources.json
new file mode 100644
index 000000000..ece4969f8
--- /dev/null
+++ b/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.11",
+        "description": "Nix Packages collection",
+        "homepage": null,
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "544b36d1b4815fd5f187ed00ff7a59fd0323317c",
+        "sha256": "0jh67yjfkv9sj4xldlv9p6whljg0rh96hy7x082061ghsb3kg6q4",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/544b36d1b4815fd5f187ed00ff7a59fd0323317c.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+    },
+    "ocplib-simplex": {
+        "branch": "v0.5.1",
+        "description": "A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities",
+        "homepage": "",
+        "owner": "OCamlPro",
+        "repo": "ocplib-simplex",
+        "rev": "12e7c1fd994d4c40cf7159008a67579f470df616",
+        "sha256": "0jkyqvcia4950cr1ip4n4xnjgaqlliljw48b40n95j75wjvy3d3w",
+        "type": "tarball",
+        "url": "https://github.com/OCamlPro/ocplib-simplex/archive/12e7c1fd994d4c40cf7159008a67579f470df616.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
+        "version": "0.5.1"
+    },
+    "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"
+    }
+}
diff --git a/nix/sources.nix b/nix/sources.nix
new file mode 100644
index 000000000..fe3dadf7e
--- /dev/null
+++ b/nix/sources.nix
@@ -0,0 +1,198 @@
+# This file has been generated by Niv.
+
+let
+
+  #
+  # The fetchers. fetch_<type> fetches specs of type <type>.
+  #
+
+  fetch_file = pkgs: name: spec:
+    let
+      name' = sanitizeName name + "-src";
+    in
+    if spec.builtin or true then
+      builtins_fetchurl { inherit (spec) url sha256; name = name'; }
+    else
+      pkgs.fetchurl { inherit (spec) url sha256; name = name'; };
+
+  fetch_tarball = pkgs: name: spec:
+    let
+      name' = sanitizeName name + "-src";
+    in
+    if spec.builtin or true then
+      builtins_fetchTarball { name = name'; inherit (spec) url sha256; }
+    else
+      pkgs.fetchzip { name = name'; inherit (spec) url sha256; };
+
+  fetch_git = name: spec:
+    let
+      ref =
+        spec.ref or (
+          if spec ? branch then "refs/heads/${spec.branch}" else
+          if spec ? tag then "refs/tags/${spec.tag}" else
+          abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!"
+        );
+      submodules = spec.submodules or false;
+      submoduleArg =
+        let
+          nixSupportsSubmodules = builtins.compareVersions builtins.nixVersion "2.4" >= 0;
+          emptyArgWithWarning =
+            if submodules
+            then
+              builtins.trace
+                (
+                  "The niv input \"${name}\" uses submodules "
+                  + "but your nix's (${builtins.nixVersion}) builtins.fetchGit "
+                  + "does not support them"
+                )
+                { }
+            else { };
+        in
+        if nixSupportsSubmodules
+        then { inherit submodules; }
+        else emptyArgWithWarning;
+    in
+    builtins.fetchGit
+      ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg);
+
+  fetch_local = spec: spec.path;
+
+  fetch_builtin-tarball = name: throw
+    ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`.
+        $ niv modify ${name} -a type=tarball -a builtin=true'';
+
+  fetch_builtin-url = name: throw
+    ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`.
+        $ niv modify ${name} -a type=file -a builtin=true'';
+
+  #
+  # Various helpers
+  #
+
+  # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695
+  sanitizeName = name:
+    (
+      concatMapStrings (s: if builtins.isList s then "-" else s)
+        (
+          builtins.split "[^[:alnum:]+._?=-]+"
+            ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name)
+        )
+    );
+
+  # The set of packages used when specs are fetched using non-builtins.
+  mkPkgs = sources: system:
+    let
+      sourcesNixpkgs =
+        import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; };
+      hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath;
+      hasThisAsNixpkgsPath = <nixpkgs> == ./.;
+    in
+    if builtins.hasAttr "nixpkgs" sources
+    then sourcesNixpkgs
+    else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then
+      import <nixpkgs> { }
+    else
+      abort
+        ''
+          Please specify either <nixpkgs> (through -I or NIX_PATH=nixpkgs=...) or
+          add a package called "nixpkgs" to your sources.json.
+        '';
+
+  # The actual fetching function.
+  fetch = pkgs: name: spec:
+
+    if ! builtins.hasAttr "type" spec then
+      abort "ERROR: niv spec ${name} does not have a 'type' attribute"
+    else if spec.type == "file" then fetch_file pkgs name spec
+    else if spec.type == "tarball" then fetch_tarball pkgs name spec
+    else if spec.type == "git" then fetch_git name spec
+    else if spec.type == "local" then fetch_local spec
+    else if spec.type == "builtin-tarball" then fetch_builtin-tarball name
+    else if spec.type == "builtin-url" then fetch_builtin-url name
+    else
+      abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}";
+
+  # If the environment variable NIV_OVERRIDE_${name} is set, then use
+  # the path directly as opposed to the fetched source.
+  replace = name: drv:
+    let
+      saneName = stringAsChars (c: if (builtins.match "[a-zA-Z0-9]" c) == null then "_" else c) name;
+      ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}";
+    in
+    if ersatz == "" then drv else
+      # this turns the string into an actual Nix path (for both absolute and
+      # relative paths)
+    if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}";
+
+  # Ports of functions for older nix versions
+
+  # a Nix version of mapAttrs if the built-in doesn't exist
+  mapAttrs = builtins.mapAttrs or (
+    f: set: with builtins;
+    listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set))
+  );
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295
+  range = first: last: if first > last then [ ] else builtins.genList (n: first + n) (last - first + 1);
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257
+  stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1));
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269
+  stringAsChars = f: s: concatStrings (map f (stringToCharacters s));
+  concatMapStrings = f: list: concatStrings (map f list);
+  concatStrings = builtins.concatStringsSep "";
+
+  # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331
+  optionalAttrs = cond: as: if cond then as else { };
+
+  # fetchTarball version that is compatible between all the versions of Nix
+  builtins_fetchTarball = { url, name ? null, sha256 }@attrs:
+    let
+      inherit (builtins) lessThan nixVersion fetchTarball;
+    in
+    if lessThan nixVersion "1.12" then
+      fetchTarball ({ inherit url; } // (optionalAttrs (name != null) { inherit name; }))
+    else
+      fetchTarball attrs;
+
+  # fetchurl version that is compatible between all the versions of Nix
+  builtins_fetchurl = { url, name ? null, sha256 }@attrs:
+    let
+      inherit (builtins) lessThan nixVersion fetchurl;
+    in
+    if lessThan nixVersion "1.12" then
+      fetchurl ({ inherit url; } // (optionalAttrs (name != null) { inherit name; }))
+    else
+      fetchurl attrs;
+
+  # Create the final "sources" from the config
+  mkSources = config:
+    mapAttrs
+      (
+        name: spec:
+          if builtins.hasAttr "outPath" spec
+          then
+            abort
+              "The values in sources.json should not have an 'outPath' attribute"
+          else
+            spec // { outPath = replace name (fetch config.pkgs name spec); }
+      )
+      config.sources;
+
+  # The "config" used by the fetchers
+  mkConfig =
+    { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null
+    , sources ? if sourcesFile == null then { } else builtins.fromJSON (builtins.readFile sourcesFile)
+    , system ? builtins.currentSystem
+    , pkgs ? mkPkgs sources system
+    }: rec {
+      # The sources, i.e. the attribute set of spec name to spec
+      inherit sources;
+
+      # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers
+      inherit pkgs;
+    };
+
+in
+mkSources (mkConfig { }) // { __functor = _: settings: mkSources (mkConfig settings); }
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 000000000..4de6bc7c4
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,42 @@
+{ pkgs ? import ./nix { } }:
+
+let
+  inherit (pkgs) lib python3Packages ocamlPackages;
+in
+
+pkgs.mkShell {
+  nativeBuildInputs = with ocamlPackages; [
+    pkgs.ocamlformat
+    pkgs.sphinx
+    python3Packages.myst-parser
+    python3Packages.sphinx-markdown-tables
+    python3Packages.sphinx-rtd-theme
+    ocaml
+    dune_3
+    ocaml-lsp
+    ocp-indent
+    dune-release
+    dune-site
+  ];
+
+  buildInputs = with ocamlPackages; [
+    ocplib-simplex
+    bos
+    dolmen_loop
+    camlzip
+    psmt2-frontend
+    stdlib-shims
+    menhir
+    dune-build-info
+    js_of_ocaml-ppx
+    js_of_ocaml-lwt
+    lwt_ppx
+    data-encoding
+    zarith_stubs_js
+    cmdliner
+    ppx_blob
+    odoc
+    ppx_deriving
+    stdcompat
+  ];
+}