diff options
| -rw-r--r-- | .gitignore | 6 | ||||
| -rw-r--r-- | dune-project | 22 | ||||
| -rw-r--r-- | flake.nix | 64 | ||||
| -rw-r--r-- | sol.opam | 29 |
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} + ] +] |