nix flake with dune and rocq development environment

4 files changed, 121 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..5059366
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,6 @@
+CLAUDE.md
+.claude
+_build/
+*.install
+.direnv/
+result
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..138c21c
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,22 @@
+(lang dune 3.7)
+
+(name sol)
+
+(generate_opam_files true)
+
+(license AGPL-3.0-only)
+
+(authors "Marcos Magueta")
+
+(maintainers "Marcos Magueta <maguetamarcos@gmail.com>")
+
+(package
+ (name sol)
+ (synopsis "Sol: a total relational language")
+ (description
+  "Sol is a total relational language where relations are the primary semantic objects, types are membership criteria, and execution is proof search, constraint propagation, and normalization.")
+ (depends
+  (ocaml
+   (>= 5.1))
+  zarith
+  (alcotest :with-test)))
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..77264eb
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,64 @@
+{
+  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;
+
+            propagatedBuildInputs = [
+              ocamlPackages.zarith
+            ];
+            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.alcotest
+              ocamlPackages.menhir
+              # Rocq, for the verified checkers and their extraction
+              pkgs.coq
+            ];
+          };
+        });
+    };
+}
diff --git a/sol.opam b/sol.opam
new file mode 100644
index 0000000..c2bde77
--- /dev/null
+++ b/sol.opam
@@ -0,0 +1,29 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Sol: a total relational language"
+description:
+  "Sol is a total relational language where relations are the primary semantic objects, types are membership criteria, and execution is proof search, constraint propagation, and normalization."
+maintainer: ["Marcos Magueta <maguetamarcos@gmail.com>"]
+authors: ["Marcos Magueta"]
+license: "AGPL-3.0-only"
+depends: [
+  "dune" {>= "3.7"}
+  "ocaml" {>= "5.1"}
+  "zarith"
+  "alcotest" {with-test}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]