From 22b13a6598e1c61d585396cfb711f3e4cda5c6be Mon Sep 17 00:00:00 2001
From: emeinhardt <ericmeinhardt@gmail.com>
Date: Fri, 15 Nov 2024 17:45:34 -0600
Subject: [PATCH] Add onix-based flake, associated make task, and .envrc
 template

---
 .envrc.tmpl        |  13 +
 Makefile           |   6 +
 flake.lock         |  97 +++++++
 flake.nix          |  56 ++++
 onix-lock-dev.json | 676 +++++++++++++++++++++++++++++++++++++++++++++
 onix-lock.json     | 217 +++++++++++++++
 6 files changed, 1065 insertions(+)
 create mode 100644 .envrc.tmpl
 create mode 100644 flake.lock
 create mode 100644 flake.nix
 create mode 100644 onix-lock-dev.json
 create mode 100644 onix-lock.json

diff --git a/.envrc.tmpl b/.envrc.tmpl
new file mode 100644
index 0000000..9db12dc
--- /dev/null
+++ b/.envrc.tmpl
@@ -0,0 +1,13 @@
+# rebuild the environment on `nix-direnv-reload` only
+nix_direnv_manual_reload
+
+# direnv will consider the environment changed if these files change, and
+# nix-direnv will then prompt for the manual reload
+watch_file flake.nix flake.lock onix-lock.json onix-lock-dev.json
+
+# use the flake with the `default` devShell:
+use flake
+
+# To use another devShell, you can use (e.g. for devShell.other:
+# use flake .#other
+
diff --git a/Makefile b/Makefile
index 69b74b5..78c19c5 100644
--- a/Makefile
+++ b/Makefile
@@ -6,3 +6,9 @@ clean:
 
 watch:
 	@dune build @all -w
+
+onix-lock:
+	onix lock ./imandra-document.opam --resolutions="ocaml-system=5.2.0" --lock-file ./onix-lock.json
+	onix lock ./imandra-document.opam --resolutions="ocaml-system=5.2.0,ocaml-lsp-server" --with-test=true --lock-file ./onix-lock-dev.json 
+	git add onix-lock.json onix-lock-dev.json
+
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..b750acc
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,97 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "flake-utils_2": {
+      "locked": {
+        "lastModified": 1652776076,
+        "narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1731531548,
+        "narHash": "sha256-sz8/v17enkYmfpgeeuyzniGJU0QQBfmAjlemAUYhfy8=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "24f0d4acd634792badd6470134c387a3b039dace",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "ref": "nixpkgs-unstable",
+        "type": "indirect"
+      }
+    },
+    "onix": {
+      "inputs": {
+        "flake-utils": "flake-utils_2",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1726775591,
+        "narHash": "sha256-AnNG7PrYN5Svhttfa1Cb31cNkHD+4ExgEGe/GPAecYs=",
+        "owner": "rizo",
+        "repo": "onix",
+        "rev": "3740a2beb84bc21860385f8bbb0d5f557842de03",
+        "type": "github"
+      },
+      "original": {
+        "owner": "rizo",
+        "repo": "onix",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs",
+        "onix": "onix"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..db2e006
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,56 @@
+{
+  inputs = {
+    nixpkgs.url = "nixpkgs/nixpkgs-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+
+    onix.url = "github:rizo/onix";
+    onix.inputs.nixpkgs.follows = "nixpkgs";
+  };
+
+  outputs = { self, nixpkgs, flake-utils, onix }@inputs:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = nixpkgs.legacyPackages.${system};
+        onix' = onix.packages.${system}.latest;
+        opamFiles = [ 
+          ./imandra-document.opam
+        ];
+        onixEnv = onix'.env {
+          path = ./.;
+          roots = opamFiles;
+          lock = ./onix-lock.json;
+          deps = { "ocaml-system" = "*"; };
+        };
+        onixEnvDev = onix'.env {
+          path = ./.;
+          roots = opamFiles;
+          lock = ./onix-lock-dev.json;
+          deps = {
+            "ocaml-system" = "*";
+            "ocaml-lsp-server" = "*";
+          };
+        };
+
+      in rec {
+        formatter = pkgs.nixfmt-rfc-style;
+
+        packages.imandra-document = onixEnv.pkgs.imandra-document;
+
+        devShells.onixLock = pkgs.mkShell { 
+          buildInputs = [
+            onix'
+          ]; 
+        };
+
+        devShells.default = onixEnvDev.shell.overrideAttrs (final: prev: {
+          buildInputs = prev.buildInputs ++ [ 
+            pkgs.ocamlformat_0_22_4 
+            pkgs.dune_3
+            pkgs.ocaml
+            onix' 
+          ];
+        });
+
+        packages.dev-shell = devShells.default.inputDerivation;
+      });
+}
diff --git a/onix-lock-dev.json b/onix-lock-dev.json
new file mode 100644
index 0000000..0760257
--- /dev/null
+++ b/onix-lock-dev.json
@@ -0,0 +1,676 @@
+{
+   "version": "0.0.5",
+   "repositories": [
+     {
+       "url": "https://github.com/ocaml/opam-repository.git",
+       "rev": "a6cd5e92975350b992cb58b4351df6fceefc8144"
+     }
+   ],
+   "packages" : {
+     "astring": {
+       "version": "0.8.5",
+       "src": {
+         "url": "https://erratique.ch/software/astring/releases/astring-0.8.5.tbz",
+         "sha256": "865692630c07c3ab87c66cdfc2734c0fdfc9c34a57f8e89ffec7c7d15e7a70fa"
+       },
+       "depends": [
+         "ocaml"
+       ],
+       "build-depends": [
+         "ocamlbuild",
+         "ocamlfind",
+         "topkg"
+       ]
+     },
+     "base": {
+       "version": "v0.17.1",
+       "src": {
+         "url": "https://github.com/janestreet/base/archive/refs/tags/v0.17.1.tar.gz",
+         "sha512": "ed5eb5e83d8085fc06f111862d609b393e394bbdcc6e25bab50030a250ffa2e540dbee02169b6f28ec220f10f61d189cd7b5646eece910c63620f5174fb5a655"
+       },
+       "depends": [
+         "dune",
+         "dune-configurator",
+         "ocaml",
+         "ocaml_intrinsics_kernel",
+         "sexplib0"
+       ],
+       "build-depends": [
+         "dune",
+         "dune-configurator"
+       ]
+     },
+     "base-bigarray": {
+       "version": "base"
+     },
+     "base-domains": {
+       "version": "base",
+       "depends": [
+         "ocaml"
+       ]
+     },
+     "base-nnp": {
+       "version": "base",
+       "depends": [
+         "base-domains"
+       ]
+     },
+     "base-threads": {
+       "version": "base"
+     },
+     "base-unix": {
+       "version": "base"
+     },
+     "camlp-streams": {
+       "version": "5.0.1",
+       "src": {
+         "url": "https://github.com/ocaml/camlp-streams/archive/v5.0.1.tar.gz",
+         "sha512": "2efa8dd4a636217c8d49bac1e4e7e5558fc2f45cfea66514140a59fd99dd08d61fb9f1e17804997ff648b71b13820a5d4a1eb70fed9d848aa2abd6e41f853c86"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "chrome-trace": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "conf-gmp": {
+       "version": "4",
+       "src-extra": {
+         "test.c": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/conf-gmp/test.c.4",
+           "sha256": "54a30735f1f271a2531526747e75716f4490dd7bc1546efd6498ccfe3cc4d6fb"
+         }
+       },
+       "depexts": [
+         "gmp"
+       ]
+     },
+     "conf-pkg-config": {
+       "version": "3",
+       "depexts": [
+         "pkg-config"
+       ]
+     },
+     "containers": {
+       "version": "3.14",
+       "src": {
+         "url": "https://github.com/c-cube/ocaml-containers/releases/download/v3.14/containers-3.14.tbz",
+         "sha256": "c94fba0c7c54349b7021c31f85120495197ddde438c574d48362ec669bf7e564"
+       },
+       "depends": [
+         "base-threads",
+         "base-unix",
+         "dune",
+         "dune-configurator",
+         "either",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune",
+         "dune-configurator"
+       ]
+     },
+     "csexp": {
+       "version": "1.5.2",
+       "src": {
+         "url": "https://github.com/ocaml-dune/csexp/releases/download/1.5.2/csexp-1.5.2.tbz",
+         "sha256": "1a14dd04bb4379a41990248550628c77913a9c07f3c35c1370b6960e697787ff"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "dune": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "base-threads",
+         "base-unix",
+         "ocaml"
+       ]
+     },
+     "dune-build-info": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "dune-configurator": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "base-unix",
+         "csexp",
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "dune-rpc": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "csexp",
+         "dune",
+         "dyn",
+         "ordering",
+         "pp",
+         "stdune",
+         "xdg"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "dyn": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "dune",
+         "ocaml",
+         "ordering",
+         "pp"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "either": {
+       "version": "1.0.0",
+       "src": {
+         "url": "https://github.com/mirage/either/releases/download/1.0.0/either-1.0.0.tbz",
+         "sha256": "bf674de3312dee7b7215f07df1e8a96eb3d679164b8a918cdd95b8d97e505884"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "fiber": {
+       "version": "3.7.0",
+       "src": {
+         "url": "https://github.com/ocaml-dune/fiber/releases/download/3.7.0/fiber-lwt-3.7.0.tbz",
+         "sha256": "8648a15ae93fe6942999ce36887429a3913b62829c4714e520cc0e7a1c3b9682"
+       },
+       "depends": [
+         "dune",
+         "dyn",
+         "ocaml",
+         "stdune"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "host-arch-unknown": {
+       "version": "1"
+     },
+     "imandra-document": {
+       "version": "dev",
+       "src": { "url": "file://." },
+       "depends": [
+         "containers",
+         "dune",
+         "ocaml",
+         "zarith"
+       ],
+       "build-depends": [
+         "dune"
+       ],
+       "vars": { "with-test": true }
+     },
+     "jsonrpc": {
+       "version": "1.19.0",
+       "src": {
+         "url": "https://github.com/ocaml/ocaml-lsp/releases/download/1.19.0/lsp-1.19.0.tbz",
+         "sha256": "e783d9f1a7f89ce1bf4c9148aa34a228368bd149bbcca43de80b459221dee5ec"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "lsp": {
+       "version": "1.19.0",
+       "src": {
+         "url": "https://github.com/ocaml/ocaml-lsp/releases/download/1.19.0/lsp-1.19.0.tbz",
+         "sha256": "e783d9f1a7f89ce1bf4c9148aa34a228368bd149bbcca43de80b459221dee5ec"
+       },
+       "depends": [
+         "dune",
+         "jsonrpc",
+         "ocaml",
+         "ppx_yojson_conv_lib",
+         "uutf",
+         "yojson"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "merlin-lib": {
+       "version": "5.2.1-502",
+       "src": {
+         "url": "https://github.com/ocaml/merlin/releases/download/v5.2.1-502/merlin-5.2.1-502.tbz",
+         "sha256": "5c02dc71b2d31b619851c14a965b91c650a4dbcd49bf56004eee61e0c58d584c"
+       },
+       "depends": [
+         "csexp",
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ocaml": {
+       "version": "5.2.0",
+       "depends": [
+         "ocaml-config",
+         "ocaml-system"
+       ],
+       "build-depends": [
+         "ocaml-system"
+       ]
+     },
+     "ocaml-config": {
+       "version": "3",
+       "src-extra": {
+         "gen_ocaml_config.ml.in": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocaml-config/gen_ocaml_config.ml.in.3",
+           "sha256": "a9ad8d84a08961159653a978db92d10f694510182b206cacb96d5c9f63b5121e"
+         },
+         "ocaml-config.install": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocaml-config/ocaml-config.install",
+           "sha256": "6e4fd93f4cce6bad0ed3c08afd0248dbe7d7817109281de6294e5b5ef5597051"
+         }
+       },
+       "depends": [
+         "ocaml-system"
+       ],
+       "build-depends": [
+         "ocaml-system"
+       ]
+     },
+     "ocaml-index": {
+       "version": "1.1",
+       "src": {
+         "url": "https://github.com/ocaml/merlin/releases/download/v5.2.1-502/merlin-5.2.1-502.tbz",
+         "sha256": "5c02dc71b2d31b619851c14a965b91c650a4dbcd49bf56004eee61e0c58d584c"
+       },
+       "depends": [
+         "dune",
+         "merlin-lib",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ocaml-lsp-server": {
+       "version": "1.19.0",
+       "src": {
+         "url": "https://github.com/ocaml/ocaml-lsp/releases/download/1.19.0/lsp-1.19.0.tbz",
+         "sha256": "e783d9f1a7f89ce1bf4c9148aa34a228368bd149bbcca43de80b459221dee5ec"
+       },
+       "depends": [
+         "astring",
+         "base",
+         "camlp-streams",
+         "chrome-trace",
+         "csexp",
+         "dune",
+         "dune-build-info",
+         "dune-rpc",
+         "dyn",
+         "fiber",
+         "jsonrpc",
+         "lsp",
+         "merlin-lib",
+         "ocaml",
+         "ocamlc-loc",
+         "ocamlformat-rpc-lib",
+         "ordering",
+         "pp",
+         "ppx_yojson_conv_lib",
+         "re",
+         "spawn",
+         "stdune",
+         "xdg",
+         "yojson"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ocaml-system": {
+       "version": "5.2.0",
+       "src-extra": {
+         "gen_ocaml_config.ml.in": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocaml-system/gen_ocaml_config.ml.in",
+           "sha256": "71bcd3d35e28cbf71eda81991c8741268f4b87ced71573b2e75f64f136cebfc1"
+         }
+       },
+       "depends": [
+         "host-arch-unknown"
+       ],
+       "depexts": [
+         "ocaml-ng.ocamlPackages_5_2.ocaml"
+       ]
+     },
+     "ocaml_intrinsics_kernel": {
+       "version": "v0.17.1",
+       "src": {
+         "url": "https://github.com/janestreet/ocaml_intrinsics_kernel/archive/refs/tags/v0.17.1.tar.gz",
+         "sha512": "21e596d6407a620866cee7cab47ef1a9446d6a733b4994e809ea5566d5fa956682a5c6a6190ffb0ed48458abd658301944ed10c4389d91ecb8df677a5f87f2ab"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ocamlbuild": {
+       "version": "0.15.0",
+       "src": {
+         "url": "https://github.com/ocaml/ocamlbuild/archive/refs/tags/0.15.0.tar.gz",
+         "sha512": "c8311a9a78491bf759eb27153d6ba4692d27cd935759a145f96a8ba8f3c2e97cef54e7d654ed1c2c07c74f60482a4fef5224e26d0f04450e69cdcb9418c762d3"
+       },
+       "depends": [
+         "ocaml"
+       ]
+     },
+     "ocamlc-loc": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "dune",
+         "dyn",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ocamlfind": {
+       "version": "1.9.6",
+       "src": {
+         "url": "http://download.camlcity.org/download/findlib-1.9.6.tar.gz",
+         "sha512": "cfaf1872d6ccda548f07d32cc6b90c3aafe136d2aa6539e03143702171ee0199add55269bba894c77115535dc46a5835901a5d7c75768999e72db503bfd83027"
+       },
+       "src-extra": {
+         "0001-Harden-test-for-OCaml-5.patch": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocamlfind/0001-Harden-test-for-OCaml-5.patch",
+           "sha256": "6fcca5f2f7abf8d6304da6c385348584013ffb8602722a87fb0bacbab5867fe8"
+         }
+       },
+       "depends": [
+         "ocaml"
+       ]
+     },
+     "ocamlformat-rpc-lib": {
+       "version": "0.26.2",
+       "src": {
+         "url": "https://github.com/ocaml-ppx/ocamlformat/releases/download/0.26.2/ocamlformat-0.26.2.tbz",
+         "sha256": "2e4f596bf7aa367a844fe83ba0f6b0bf14b2a65179ddc082363fe9793d0375c5"
+       },
+       "depends": [
+         "csexp",
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ordering": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "pp": {
+       "version": "1.2.0",
+       "src": {
+         "url": "https://github.com/ocaml-dune/pp/releases/download/1.2.0/pp-1.2.0.tbz",
+         "sha256": "a5e822573c55afb42db29ec56eacd1f2acd8f65cf2df2878e291de374ce6909c"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ppx_yojson_conv_lib": {
+       "version": "v0.17.0",
+       "src": {
+         "url": "https://github.com/janestreet/ppx_yojson_conv_lib/archive/refs/tags/v0.17.0.tar.gz",
+         "sha256": "f6e6ee92408c53c5ecd8bb5ae93811aa4cf71f8dc144d5943be8fc2c7697b199"
+       },
+       "depends": [
+         "dune",
+         "ocaml",
+         "yojson"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "re": {
+       "version": "1.12.0",
+       "src": {
+         "url": "https://github.com/ocaml/ocaml-re/releases/download/1.12.0/re-1.12.0.tbz",
+         "sha256": "a01f2bf22f72c2f4ababd8d3e7635e35c1bf6bc5a41ad6d5a007454ddabad1d4"
+       },
+       "depends": [
+         "dune",
+         "ocaml",
+         "seq"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "seq": {
+       "version": "base",
+       "src-extra": {
+         "META.seq": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/seq/META.seq",
+           "sha256": "e95062b4d0519ef8335c02f7d0f1952d11b814c7ab7e6d566a206116162fa2be"
+         },
+         "seq.install": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/seq/seq.install",
+           "sha256": "fff926c2c4d5a82b6c94c60c4c35eb06e3d39975893ebe6b1f0e6557cbe34904"
+         }
+       },
+       "depends": [
+         "ocaml"
+       ]
+     },
+     "sexplib0": {
+       "version": "v0.17.0",
+       "src": {
+         "url": "https://github.com/janestreet/sexplib0/archive/refs/tags/v0.17.0.tar.gz",
+         "sha512": "ad387e40789fe70a11473db7e85fe017b801592624414e9030730b2e92ea08f98095fb6e9236430f33c801605ebee0a2a6284e0f618a26a7da4599d4fd9d395d"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "spawn": {
+       "version": "v0.15.1",
+       "src": {
+         "url": "https://github.com/janestreet/spawn/archive/v0.15.1.tar.gz",
+         "sha256": "9afdee314fab6c3fcd689ab6eb5608d6b78078e6dede3953a47debde06c19d50"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "stdune": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "base-unix",
+         "csexp",
+         "dune",
+         "dyn",
+         "ocaml",
+         "ordering",
+         "pp"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "topkg": {
+       "version": "1.0.7",
+       "src": {
+         "url": "https://erratique.ch/software/topkg/releases/topkg-1.0.7.tbz",
+         "sha512": "09e59f1759bf4db8471f02d0aefd8db602b44932a291c05c312b1423796e7a15d1598d3c62a0cec7f083eff8e410fac09363533dc4bd2120914bb9664efea535"
+       },
+       "depends": [
+         "ocaml",
+         "ocamlbuild"
+       ],
+       "build-depends": [
+         "ocamlbuild",
+         "ocamlfind"
+       ]
+     },
+     "uutf": {
+       "version": "1.0.3",
+       "src": {
+         "url": "https://erratique.ch/software/uutf/releases/uutf-1.0.3.tbz",
+         "sha512": "50cc4486021da46fb08156e9daec0d57b4ca469b07309c508d5a9a41e9dbcf1f32dec2ed7be027326544453dcaf9c2534919395fd826dc7768efc6cc4bfcc9f8"
+       },
+       "depends": [
+         "ocaml"
+       ],
+       "build-depends": [
+         "ocamlbuild",
+         "ocamlfind",
+         "topkg"
+       ]
+     },
+     "xdg": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "yojson": {
+       "version": "2.2.2",
+       "src": {
+         "url": "https://github.com/ocaml-community/yojson/releases/download/2.2.2/yojson-2.2.2.tbz",
+         "sha256": "9abfad8c9a79d4723ad2f6448e669c1e68dbfc87cc54a1b7c064b0c90912c595"
+       },
+       "depends": [
+         "dune",
+         "ocaml",
+         "seq"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "zarith": {
+       "version": "1.14",
+       "src": {
+         "url": "https://github.com/ocaml/Zarith/archive/release-1.14.tar.gz",
+         "sha256": "5db9dcbd939153942a08581fabd846d0f3f2b8c67fe68b855127e0472d4d1859"
+       },
+       "depends": [
+         "conf-gmp",
+         "conf-pkg-config",
+         "ocaml",
+         "ocamlfind"
+       ],
+       "build-depends": [
+         "ocamlfind"
+       ]
+     }
+   }
+}
diff --git a/onix-lock.json b/onix-lock.json
new file mode 100644
index 0000000..c28519a
--- /dev/null
+++ b/onix-lock.json
@@ -0,0 +1,217 @@
+{
+   "version": "0.0.5",
+   "repositories": [
+     {
+       "url": "https://github.com/ocaml/opam-repository.git",
+       "rev": "a6cd5e92975350b992cb58b4351df6fceefc8144"
+     }
+   ],
+   "packages" : {
+     "base-bigarray": {
+       "version": "base"
+     },
+     "base-domains": {
+       "version": "base",
+       "depends": [
+         "ocaml"
+       ]
+     },
+     "base-nnp": {
+       "version": "base",
+       "depends": [
+         "base-domains"
+       ]
+     },
+     "base-threads": {
+       "version": "base"
+     },
+     "base-unix": {
+       "version": "base"
+     },
+     "conf-gmp": {
+       "version": "4",
+       "src-extra": {
+         "test.c": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/conf-gmp/test.c.4",
+           "sha256": "54a30735f1f271a2531526747e75716f4490dd7bc1546efd6498ccfe3cc4d6fb"
+         }
+       },
+       "depexts": [
+         "gmp"
+       ]
+     },
+     "conf-pkg-config": {
+       "version": "3",
+       "depexts": [
+         "pkg-config"
+       ]
+     },
+     "containers": {
+       "version": "3.14",
+       "src": {
+         "url": "https://github.com/c-cube/ocaml-containers/releases/download/v3.14/containers-3.14.tbz",
+         "sha256": "c94fba0c7c54349b7021c31f85120495197ddde438c574d48362ec669bf7e564"
+       },
+       "depends": [
+         "base-threads",
+         "base-unix",
+         "dune",
+         "dune-configurator",
+         "either",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune",
+         "dune-configurator"
+       ]
+     },
+     "csexp": {
+       "version": "1.5.2",
+       "src": {
+         "url": "https://github.com/ocaml-dune/csexp/releases/download/1.5.2/csexp-1.5.2.tbz",
+         "sha256": "1a14dd04bb4379a41990248550628c77913a9c07f3c35c1370b6960e697787ff"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "dune": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "base-threads",
+         "base-unix",
+         "ocaml"
+       ]
+     },
+     "dune-configurator": {
+       "version": "3.16.1",
+       "src": {
+         "url": "https://github.com/ocaml/dune/releases/download/3.16.1/dune-3.16.1.tbz",
+         "sha256": "b781ae20f87613c2a11bd0717809e00470c82d615e15264f9a64e033051ac3de"
+       },
+       "depends": [
+         "base-unix",
+         "csexp",
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "either": {
+       "version": "1.0.0",
+       "src": {
+         "url": "https://github.com/mirage/either/releases/download/1.0.0/either-1.0.0.tbz",
+         "sha256": "bf674de3312dee7b7215f07df1e8a96eb3d679164b8a918cdd95b8d97e505884"
+       },
+       "depends": [
+         "dune",
+         "ocaml"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "host-arch-unknown": {
+       "version": "1"
+     },
+     "imandra-document": {
+       "version": "dev",
+       "src": { "url": "file://." },
+       "depends": [
+         "containers",
+         "dune",
+         "ocaml",
+         "zarith"
+       ],
+       "build-depends": [
+         "dune"
+       ]
+     },
+     "ocaml": {
+       "version": "5.2.0",
+       "depends": [
+         "ocaml-config",
+         "ocaml-system"
+       ],
+       "build-depends": [
+         "ocaml-system"
+       ]
+     },
+     "ocaml-config": {
+       "version": "3",
+       "src-extra": {
+         "gen_ocaml_config.ml.in": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocaml-config/gen_ocaml_config.ml.in.3",
+           "sha256": "a9ad8d84a08961159653a978db92d10f694510182b206cacb96d5c9f63b5121e"
+         },
+         "ocaml-config.install": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocaml-config/ocaml-config.install",
+           "sha256": "6e4fd93f4cce6bad0ed3c08afd0248dbe7d7817109281de6294e5b5ef5597051"
+         }
+       },
+       "depends": [
+         "ocaml-system"
+       ],
+       "build-depends": [
+         "ocaml-system"
+       ]
+     },
+     "ocaml-system": {
+       "version": "5.2.0",
+       "src-extra": {
+         "gen_ocaml_config.ml.in": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocaml-system/gen_ocaml_config.ml.in",
+           "sha256": "71bcd3d35e28cbf71eda81991c8741268f4b87ced71573b2e75f64f136cebfc1"
+         }
+       },
+       "depends": [
+         "host-arch-unknown"
+       ],
+       "depexts": [
+         "ocaml-ng.ocamlPackages_5_2.ocaml"
+       ]
+     },
+     "ocamlfind": {
+       "version": "1.9.6",
+       "src": {
+         "url": "http://download.camlcity.org/download/findlib-1.9.6.tar.gz",
+         "sha512": "cfaf1872d6ccda548f07d32cc6b90c3aafe136d2aa6539e03143702171ee0199add55269bba894c77115535dc46a5835901a5d7c75768999e72db503bfd83027"
+       },
+       "src-extra": {
+         "0001-Harden-test-for-OCaml-5.patch": {
+           "url": "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/ocamlfind/0001-Harden-test-for-OCaml-5.patch",
+           "sha256": "6fcca5f2f7abf8d6304da6c385348584013ffb8602722a87fb0bacbab5867fe8"
+         }
+       },
+       "depends": [
+         "ocaml"
+       ]
+     },
+     "zarith": {
+       "version": "1.14",
+       "src": {
+         "url": "https://github.com/ocaml/Zarith/archive/release-1.14.tar.gz",
+         "sha256": "5db9dcbd939153942a08581fabd846d0f3f2b8c67fe68b855127e0472d4d1859"
+       },
+       "depends": [
+         "conf-gmp",
+         "conf-pkg-config",
+         "ocaml",
+         "ocamlfind"
+       ],
+       "build-depends": [
+         "ocamlfind"
+       ]
+     }
+   }
+}