diff --git a/.cruft.json b/.cruft.json index ae4c1a44b..738f2cc95 100644 --- a/.cruft.json +++ b/.cruft.json @@ -1,6 +1,6 @@ { "template": "https://github.com/runtimeverification/python-project-template", - "commit": "601d5e2a0e8a98c87dcb1ae694d22d76d0114e01", + "commit": "7a095b4dd0a51916da0a728b8fdd9adf7e469a68", "checkout": null, "context": { "cookiecutter": { @@ -11,7 +11,8 @@ "description": "", "author_name": "Runtime Verification, Inc.", "author_email": "contact@runtimeverification.com", - "_template": "https://github.com/runtimeverification/python-project-template" + "_template": "https://github.com/runtimeverification/python-project-template", + "_commit": "7a095b4dd0a51916da0a728b8fdd9adf7e469a68" } }, "directory": null diff --git a/Makefile b/Makefile index 6ebc62cc4..50ab2902e 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ UV := uv --directory kmir -UV_RUN := $(UV) run +UV_RUN := $(UV) run -- PARALLEL := 4 diff --git a/README.md b/README.md index e9380e91e..cd607e9d7 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@ Also included is the `kmir` tool, a python script that acts as a front-end to th ### KMIR Setup -Pre-requisites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`, `gcc >= 11.4.0`, `cargo == nightly-2024-11-29`, `k >= v7.1.205`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start). +Pre-requisites: `python >= 3.10`, [`uv`](https://docs.astral.sh/uv/), `pip >= 20.0.2`, `gcc >= 11.4.0`, `cargo == nightly-2024-11-29`, `k >= v7.1.205`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start). ```bash make build diff --git a/flake.lock b/flake.lock index 27cc37db1..68ff53cdd 100644 --- a/flake.lock +++ b/flake.lock @@ -34,6 +34,24 @@ "type": "github" } }, + "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, + "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" + } + }, "fmt-src": { "flake": false, "locked": { @@ -53,7 +71,7 @@ }, "haskell-backend": { "inputs": { - "flake-utils": "flake-utils", + "flake-utils": "flake-utils_2", "nixpkgs": [ "k-framework", "nixpkgs" @@ -100,15 +118,11 @@ "k-framework": { "inputs": { "flake-utils": [ - "k-framework", - "llvm-backend", - "utils" + "flake-utils" ], "haskell-backend": "haskell-backend", "llvm-backend": "llvm-backend", "nixpkgs": [ - "k-framework", - "rv-nix-tools", "nixpkgs" ], "pyproject-build-systems": "pyproject-build-systems", @@ -212,6 +226,53 @@ "type": "github" } }, + "nixpkgs_4": { + "locked": { + "lastModified": 1754292888, + "narHash": "sha256-1ziydHSiDuSnaiPzCQh1mRFBsM2d2yRX9I+5OPGEmIE=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "ce01daebf8489ba97bd1609d185ea276efdeb121", + "type": "github" + }, + "original": { + "id": "nixpkgs", + "ref": "nixos-25.05", + "type": "indirect" + } + }, + "nixpkgs_5": { + "locked": { + "lastModified": 1716457947, + "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "type": "github" + } + }, + "nixpkgs_6": { + "locked": { + "lastModified": 1744306051, + "narHash": "sha256-jWwqkmi8cplBu4CXUb4zdfpqKp3UJYVAs/b5m8M75sg=", + "owner": "runtimeverification", + "repo": "nixpkgs", + "rev": "e9a77bb24d408d3898f6a11fb065d350d6bc71f1", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "ref": "libmatch", + "repo": "nixpkgs", + "type": "github" + } + }, "pybind11-src": { "flake": false, "locked": { @@ -260,6 +321,35 @@ "type": "github" } }, + "pyproject-build-systems_2": { + "inputs": { + "nixpkgs": [ + "uv2nix", + "nixpkgs" + ], + "pyproject-nix": [ + "uv2nix", + "pyproject-nix" + ], + "uv2nix": [ + "uv2nix" + ] + }, + "locked": { + "lastModified": 1744599653, + "narHash": "sha256-nysSwVVjG4hKoOjhjvE6U5lIKA8sEr1d1QzEfZsannU=", + "owner": "pyproject-nix", + "repo": "build-system-pkgs", + "rev": "7dba6dbc73120e15b558754c26024f6c93015dd7", + "type": "github" + }, + "original": { + "owner": "pyproject-nix", + "repo": "build-system-pkgs", + "rev": "7dba6dbc73120e15b558754c26024f6c93015dd7", + "type": "github" + } + }, "pyproject-nix": { "inputs": { "nixpkgs": [ @@ -282,6 +372,27 @@ "type": "github" } }, + "pyproject-nix_2": { + "inputs": { + "nixpkgs": [ + "uv2nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1745782090, + "narHash": "sha256-c/mqxgOVDcwrdcY3FqG22MwLPGY5rCz5gte1sxISKnM=", + "owner": "pyproject-nix", + "repo": "pyproject.nix", + "rev": "2db2d95ddbc4ff5e29730cb82fdba6647be258a7", + "type": "github" + }, + "original": { + "owner": "pyproject-nix", + "repo": "pyproject.nix", + "type": "github" + } + }, "rapidjson-src": { "flake": false, "locked": { @@ -301,19 +412,41 @@ }, "root": { "inputs": { - "flake-utils": [ - "k-framework", - "flake-utils" - ], + "flake-utils": "flake-utils", "k-framework": "k-framework", - "nixpkgs": [ - "k-framework", - "nixpkgs" + "nixpkgs": "nixpkgs_4", + "pyproject-build-systems": "pyproject-build-systems_2", + "pyproject-nix": [ + "uv2nix", + "pyproject-nix" ], "rv-nix-tools": [ "k-framework", "rv-nix-tools" + ], + "stable-mir-json-flake": "stable-mir-json-flake", + "uv2nix": "uv2nix_2" + } + }, + "rust-overlay": { + "inputs": { + "nixpkgs": [ + "stable-mir-json-flake", + "nixpkgs" ] + }, + "locked": { + "lastModified": 1754276100, + "narHash": "sha256-VmYP9Jo0U234xtGTGtihqNHfGy1JZ1h9WaaJlIuzgCk=", + "owner": "oxalica", + "repo": "rust-overlay", + "rev": "dc2d2489572fa8a3b86c15ff9fd01f99b90cb90d", + "type": "github" + }, + "original": { + "owner": "oxalica", + "repo": "rust-overlay", + "type": "github" } }, "rv-nix-tools": { @@ -354,6 +487,25 @@ "type": "github" } }, + "rv-nix-tools_3": { + "inputs": { + "nixpkgs": "nixpkgs_5" + }, + "locked": { + "lastModified": 1726497185, + "narHash": "sha256-iN+5eLmDm/rLuIZezS5ZqiW1BtBpwrrM9CPPP7Z5Tog=", + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "rev": "854d4f05ea78547d46e807b414faad64cea10ae4", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "rev": "854d4f05ea78547d46e807b414faad64cea10ae4", + "type": "github" + } + }, "some-cabal-hashes-lib": { "flake": false, "locked": { @@ -370,6 +522,32 @@ "type": "github" } }, + "stable-mir-json-flake": { + "inputs": { + "flake-utils": [ + "flake-utils" + ], + "nixpkgs": [ + "nixpkgs" + ], + "rust-overlay": "rust-overlay", + "rv-nix-tools": "rv-nix-tools_3" + }, + "locked": { + "lastModified": 1754483429, + "narHash": "sha256-55JCOiB0rj65NkHxnh0UrGLlgni+c6KAAwkcQb2PgcU=", + "owner": "runtimeverification", + "repo": "stable-mir-json", + "rev": "8dcacda4d94f10ea102884887e56da335e4d161c", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "repo": "stable-mir-json", + "rev": "8dcacda4d94f10ea102884887e56da335e4d161c", + "type": "github" + } + }, "systems": { "locked": { "lastModified": 1681028828, @@ -400,9 +578,24 @@ "type": "github" } }, + "systems_3": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, "utils": { "inputs": { - "systems": "systems_2" + "systems": "systems_3" }, "locked": { "lastModified": 1705309234, @@ -438,6 +631,26 @@ "type": "github" } }, + "uv2nix_2": { + "inputs": { + "nixpkgs": "nixpkgs_6", + "pyproject-nix": "pyproject-nix_2" + }, + "locked": { + "lastModified": 1746048139, + "narHash": "sha256-LdCLyiihLg6P2/mjzP0+W7RtraDSIaJJPTy6SCtW5Ag=", + "owner": "pyproject-nix", + "repo": "uv2nix", + "rev": "680e2f8e637bc79b84268949d2f2b2f5e5f1d81c", + "type": "github" + }, + "original": { + "owner": "pyproject-nix", + "repo": "uv2nix", + "rev": "680e2f8e637bc79b84268949d2f2b2f5e5f1d81c", + "type": "github" + } + }, "z3": { "flake": false, "locked": { diff --git a/flake.nix b/flake.nix index 7f4c97611..8916ea9a1 100644 --- a/flake.nix +++ b/flake.nix @@ -1,50 +1,104 @@ { description = "kmir - "; inputs = { - k-framework.url = "github:runtimeverification/k/v7.1.280"; - nixpkgs.follows = "k-framework/nixpkgs"; - flake-utils.follows = "k-framework/flake-utils"; rv-nix-tools.follows = "k-framework/rv-nix-tools"; - # poetry2nix.follows = "k-framework/poetry2nix"; # FIXME: To stop crash with `nix flake update` + nixpkgs.url = "nixpkgs/nixos-25.05"; + + flake-utils.url = "github:numtide/flake-utils"; + + stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/8dcacda4d94f10ea102884887e56da335e4d161c"; + stable-mir-json-flake = { + inputs.nixpkgs.follows = "nixpkgs"; + inputs.flake-utils.follows = "flake-utils"; + }; + + k-framework.url = "github:runtimeverification/k/v7.1.280"; + k-framework = { + inputs.flake-utils.follows = "flake-utils"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + + uv2nix.url = "github:pyproject-nix/uv2nix/680e2f8e637bc79b84268949d2f2b2f5e5f1d81c"; + # stale nixpkgs is missing the alias `lib.match` -> `builtins.match` + # therefore point uv2nix to a patched nixpkgs, which introduces this alias + # this is a temporary solution until nixpkgs us up-to-date again + uv2nix.inputs.nixpkgs.url = "github:runtimeverification/nixpkgs/libmatch"; + # inputs.nixpkgs.follows = "nixpkgs"; + pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/7dba6dbc73120e15b558754c26024f6c93015dd7"; + pyproject-build-systems = { + inputs.nixpkgs.follows = "uv2nix/nixpkgs"; + inputs.uv2nix.follows = "uv2nix"; + inputs.pyproject-nix.follows = "uv2nix/pyproject-nix"; + }; + pyproject-nix.follows = "uv2nix/pyproject-nix"; }; - outputs = { self, nixpkgs, flake-utils, k-framework, ... }@inputs: + outputs = { + self, + nixpkgs, + rv-nix-tools, + flake-utils, + stable-mir-json-flake, + k-framework, + pyproject-nix, + pyproject-build-systems, + uv2nix + }: + let + pythonVer = "310"; + in flake-utils.lib.eachDefaultSystem (system: let - allOverlays = [ - k-framework.overlays.pyk - (final: prev: let - poetry2nix = - inputs.poetry2nix.lib.mkPoetry2Nix { pkgs = prev; }; - in { - kmir = poetry2nix.mkPoetryApplication { - python = prev.python310; - projectDir = ./kmir; - overrides = poetry2nix.overrides.withDefaults - (finalPython: prevPython: { - kframework = prev.pyk-python310; - }); - groups = []; - # We remove `dev` from `checkGroups`, so that poetry2nix does not try to resolve dev dependencies. - checkGroups = []; - }; - }) - ]; - in flake-utils.lib.eachSystem [ - "x86_64-linux" - "x86_64-darwin" - "aarch64-linux" - "aarch64-darwin" - ] (system: - let - pkgs = import nixpkgs { - inherit system; - overlays = allOverlays; + uvOverlay = final: prev: { + uv = uv2nix.packages.${final.system}.uv-bin; + }; + # create custom overlay for k, because the overlay in k-framework currently also includes a lot of other stuff instead of only k + kOverlay = final: prev: { + k = k-framework.packages.${final.system}.k; + }; + stable-mir-json-overlay = final: prev: { + stable-mir-json = stable-mir-json-flake.packages.${final.system}.stable-mir-json; + }; + mir-semantics-overlay = final: prev: { + mir-semantics = final.callPackage ./nix/mir-semantics { + inherit pyproject-nix pyproject-build-systems uv2nix; + python = final."python${pythonVer}"; }; - in { - packages = rec { - inherit (pkgs) kmir; - default = kmir; + }; + pkgs = import nixpkgs { + inherit system; + overlays = [ + uvOverlay + kOverlay + stable-mir-json-overlay + mir-semantics-overlay + ]; + }; + python = pkgs."python${pythonVer}"; + in { + devShells.default = + let + stable-mir-json-shell = stable-mir-json-flake.devShells.${system}.default; + in pkgs.mkShell { + name = "uv develop shell"; + buildInputs = (stable-mir-json-shell.buildInputs or []) ++ [ + python + pkgs.uv + ]; + env = (stable-mir-json-shell.env or { }) // { + # prevent uv from managing Python downloads and force use of specific + UV_PYTHON_DOWNLOADS = "never"; + UV_PYTHON = python.interpreter; }; - }) // { - overlay = nixpkgs.lib.composeManyExtensions allOverlays; + shellHook = (stable-mir-json-shell.shellHook or "") + '' + unset PYTHONPATH + ''; + }; + packages = rec { + inherit (pkgs) mir-semantics; + default = mir-semantics; + }; + }) // { + overlays.default = final: prev: { + inherit (self.packages.${final.system}) mir-semantics; }; + }; } diff --git a/nix/README.md b/nix/README.md new file mode 100644 index 000000000..d7ed7b0c4 --- /dev/null +++ b/nix/README.md @@ -0,0 +1,3 @@ +## Notes +#### git submodules +If you use git submodules that are not required for building the project with `nix`, then you should add these directories to the `gitignoreSourcePure` list in `nix/mir-semantics/default.nix`, see the respective left-over `TODO` in the nix file. Otherwise, the nix build that is uploaded to the nix binary cache by CI might not match the version that is requested by `kup`, in case this project is offered as a package by `kup`. This is due to weird behaviour in regards to git submodules by `git` and `nix`, where a submodule directory might exist and be empty or instead not exist, which impacts the resulting nix hash, which is of impartance when offering/downloading cached nix derivations. See [runtimeverification/k/pull/4804](https://github.com/runtimeverification/k/pull/4804) for more information. \ No newline at end of file diff --git a/nix/mir-semantics/build-systems-overlay.nix b/nix/mir-semantics/build-systems-overlay.nix new file mode 100644 index 000000000..d27c11519 --- /dev/null +++ b/nix/mir-semantics/build-systems-overlay.nix @@ -0,0 +1,22 @@ +final: prev: +let + inherit (final) resolveBuildSystem; + inherit (builtins) mapAttrs; + + # Build system dependencies specified in the shape expected by resolveBuildSystem + # The empty lists below are lists of optional dependencies. + # + # A package `foo` with specification written as: + # `setuptools-scm[toml]` in pyproject.toml would be written as + # `foo.setuptools-scm = [ "toml" ]` in Nix + buildSystemOverrides = { + # add dependencies here, e.g.: + # pyperclip.setuptools = [ ]; + }; +in +mapAttrs ( + name: spec: + prev.${name}.overrideAttrs (old: { + nativeBuildInputs = old.nativeBuildInputs ++ resolveBuildSystem spec; + }) +) buildSystemOverrides diff --git a/nix/mir-semantics/default.nix b/nix/mir-semantics/default.nix new file mode 100644 index 000000000..5977261d9 --- /dev/null +++ b/nix/mir-semantics/default.nix @@ -0,0 +1,55 @@ +{ + lib, + callPackage, + nix-gitignore, + + pyproject-nix, + pyproject-build-systems, + uv2nix, + + python +}: +let + pyproject-util = callPackage pyproject-nix.build.util {}; + pyproject-packages = callPackage pyproject-nix.build.packages { + inherit python; + }; + + # load a uv workspace from a workspace root + workspace = uv2nix.lib.workspace.loadWorkspace { + workspaceRoot = lib.cleanSource (nix-gitignore.gitignoreSourcePure [ + ../../.gitignore + ".github/" + "result*" + # do not include submodule directories that might be initilized empty or non-existent due to nix/git + # otherwise cachix build might not match the version that is requested by `kup` + # TODO: for new projects, add your submodule directories that are not required for nix builds here! + # e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory + # "/docs/external-computation" + ] ../.. + ); + }; + + # create overlay + lockFileOverlay = workspace.mkPyprojectOverlay { + # prefer "wheel" over "sdist" due to maintance overhead + # there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix + sourcePreference = "wheel"; + }; + + buildSystemsOverlay = import ./build-systems-overlay.nix; + + # construct package set + pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions [ + # make build tools available by default as these are not necessarily specified in python lock files + pyproject-build-systems.overlays.default + # include all packages from the python lock file + lockFileOverlay + # add build system overrides to certain python packages + buildSystemsOverlay + ]); +in pyproject-util.mkApplication { + # default dependancy group enables no optional dependencies and no dependency-groups + venv = pythonSet.mkVirtualEnv "mir-semantics-env" workspace.deps.default; + package = pythonSet.mir-semantics; +}