Merge branch 'ci/lafeychine/nix' into 'main'

Add nix support

See merge request !15

DEVELOPERS.md

+# Information for RefinedRust developers
+
+## Setup
+You will need to install some specific dependencies in order to have a development setup of this project.
+
+There are two maintained ways to do this, using `nix` or (`opam` and `rustup`).
+
+Both methods require you to have a local copy of this project.
+
+### Setup using `nix` flakes
+We assume that you have `nix` installed on your system. Setup instructions can be found here: https://nixos.org/download
+
+To setup the project for development purposes, you can use `nix develop` to enter an interactive subshell containing the tools you will need:
+```bash
+cd <refinedrust-root-project>
+nix develop
+```
+
+The tools lives in this subshell and will disappear as soon as you leave the subshell.
+
+If you do not have flakes enabled, you may get this error:
+```
+error: experimental Nix feature 'nix-command' is disabled; use ''–extra-experimental-features nix-command' to override
+```
+
+All you have to do is enable flakes, see this [NixOS wiki page](https://nixos.wiki/wiki/Flakes) for more details on how to enable flakes permanently.
+
+### Setup using `opam` and `rustup`
+By following the procedure in the `README.md`, you should have the required setup for development.
 
 ## Editor configuration for working on the frontend
-To work on the frontend and get nice autocompletion for rustc internal things, etc., you can use `rust-analyzer`.
-The `Cargo.toml` for `rr_frontend` sets the right flags to make `rust-analyzer` use rustc-internal things.
+To work comfortably on the frontend, it is recommended to use `rust-analyzer`, which provides nice features to your editor like code completion.
+
+If you are using `nix develop`, the following command must be run each time the toolchain is updated due [to a bug inside `cargo`](https://github.com/rust-lang/cargo/issues/10096):
+```bash
+sudo unshare -m bash -c "mount -o remount,rw /nix/store; cargo metadata --format-version 1 --manifest-path ${RUST_SRC_PATH}"
+```
+
+Furthermore, it is required that `rust-analyzer.rustc.source` points to the value of `${RUST_SRC_PATH}`:
+```bash
+echo ${RUST_SRC_PATH}  # Keep this path, you will need it.
+```
 
-The remaining config depends on your editor.
+The remaining configuration depends on your editor.
+
+### Emacs
+For Emacs, you need to install the [LSP Mode plugin](https://emacs-lsp.github.io/lsp-mode/page/installation/).
+
+After installation, you need to configure the property `rust-analyzer.rust.source` to point out the location of the source of `rust-analyzer` (`RUST_SRC_PATH`).
+
+This property has to be set in your configuration, and can be temporarily set by using:
+```
+<M-x> set-variable, choose `lsp-rust-analyzer-rustc-source` and replace by "<the path given by ${RUST_SRC_PATH}>"
+<M-x> lsp-restart-workspace
+```
+
+Please remember to update this value each time the rust toolchain is updated.
 
 ### Vim
 For Vim, [`YouCompleteMe`](https://github.com/ycm-core/YouCompleteMe) has good support for Rust using `rust-analyzer`.
@@ -36,11 +87,47 @@ def Settings(**kwargs):
 ```
 (if you already set other options, add just the `rustcSource` config).
 
-TODO: can we also point directly to the `rust-src` in the `refinedrust` toolchain? Problem: it does not have `Cargo.toml`.
+### Visual Studio Code
+For Visual Studio Code, you need to install the [rust-analyzer extension](https://marketplace.visualstudio.com/items?itemName=rust-lang.rust-analyzer).
 
+After installation, you need to configure the property `rust-analyzer.rust.source` to point out the location of the source of `rust-analyzer` (`RUST_SRC_PATH`).
+
+This property has to be set inside the `settings.json` file of your user (not the workspace):
+```json
+{
+    "rust-analyzer.rustc.source": "<the path given by ${RUST_SRC_PATH}>"
+}
+```
 
-## Updating the frontend's rustc version
+Please remember to update this value each time the rust toolchain is updated, by repeating the same steps.
+
+## Updating dependencies
+
+### Updating the frontend's rustc version
 1. Update the file `rust-toolchain.toml` in `rr_frontend` to the new desired nightly version.
-2. Try to get the frontend building again.
+2. Make the required changes for `nix` (see below).
+3. Try to get the frontend building again.
+
+### Updating `nix` dependencies
+The project is described with `nix` using the file `flake.nix`, containing a list of `inputs` and `outputs`.
+
+#### Updating `nix` inputs
+The `inputs` set contains some repositories (`fenix`, `nixpkgs`, ...) that describe how to build dependencies.
+
+In order to be reproducible, this `inputs` set is locked to a specific version
+using the file `flake.lock`.
+
+To update this set, you can use `nix flake update` and commit the modified `flake.lock` file.
+
+#### Updating `nix` outputs
+The `outputs` set describe the project, including how to build some external dependencies.
 
+Those dependencies are described using a couple:
+ - `version`/`sha256` for `coq`, such as `stdpp`, `iris` or `lambda-rust`, and;
+ - `dir`/`sha256` for specifying the `rust` toolchain.
 
+To update a dependency:
+1. Replace the `sha256` string with the empty string `""`.
+2. For a `coq` dependency, replace the `version` string with the desired `git` commit hash.
+3. Run `nix build` and wait for the error that throws the hash mismatch.
+4. Replace the `sha256` empty string with the hash from the received error. 

README.md

@@ -14,7 +14,34 @@ Stdlib interfaces (without proofs) can be found in the `stdlib` subfolder.
 * the `rust_typing` subfolder contains the implementation of the RefinedRust type system and proof automation.
 
 ## Setup
-### Setup instructions for the Coq code:
+To use this project, you will need to install some specific dependencies.
+
+There are two maintained ways to do this, using `nix` or (`opam` and `rustup`).
+
+If you are using `nix`, you do not need to have a copy of this repository.
+
+### Setup using `nix` flakes
+We assume that you have `nix` installed on your system. Setup instructions can be found here: https://nixos.org/download
+
+You can use `nix shell` to enter an interactive subshell containing the project:
+```bash
+nix shell "gitlab:lgaeher/refinedrust-dev?host=gitlab.mpi-sws.org"
+```
+
+The project lives in this subshell and will disappear as soon as you leave the subshell.
+
+If you do not have flakes enabled, you may get this error:
+```
+error: experimental Nix feature 'nix-command' is disabled; use ''–extra-experimental-features nix-command' to override
+```
+
+All you have to do is activate flakes temporarily by using `--extra-experimental-features 'nix-command flakes'`:
+```bash
+nix --extra-experimental-features 'nix-command flakes' shell "gitlab:lgaeher/refinedrust-dev?host=gitlab.mpi-sws.org"
+```
+
+### Setup using `opam` and `rustup`
+#### Setup instructions for the Coq code:
 We assume that you have `opam` installed on your system. Setup instructions can be found here: https://opam.ocaml.org/doc/Install.html
 
 0. `cd` into the directory containing this README.
@@ -38,8 +65,7 @@ make builddep
 dune build theories
 ```
 
-
-### Setup instructions for the frontend:
+#### Setup instructions for the frontend:
 1. Make sure that you have a working `rustup`/Rust install. Instructions for setting up Rust can be found on https://rustup.rs/.
 2. Run `./refinedrust build` in `rr_frontend` to build the frontend.
 3. Run `./refinedrust install` in `rr_frontend` to install the frontend.

case_studies/extra_proofs/tests/enums/dune

 (coq.theory
 (flags -w -notation-overridden -w -redundant-canonical-projection)
 (name refinedrust.extra_proofs.tests.enums)
-(theories caesium lithium refinedrust))
+(theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust))

flake.lock

+{
+  "nodes": {
+    "fenix": {
+      "inputs": {
+        "nixpkgs": [
+          "nixpkgs"
+        ],
+        "rust-analyzer-src": "rust-analyzer-src"
+      },
+      "locked": {
+        "lastModified": 1704435752,
+        "narHash": "sha256-7ZDpuqGS6aWfT3E8y4TEVSvCUoT7gOH2Cc0NvvDx/1g=",
+        "owner": "nix-community",
+        "repo": "fenix",
+        "rev": "15c95e2adbe285c82ce347a31110b83d13aad586",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "fenix",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1701680307,
+        "narHash": "sha256-kAuep2h5ajznlPMD9rnQyffWG8EM/C73lejGofXvdM8=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "4022d587cbbfd70fe950c1e2083a02621806a725",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "naersk": {
+      "inputs": {
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1698420672,
+        "narHash": "sha256-/TdeHMPRjjdJub7p7+w55vyABrsJlt5QkznPYy55vKA=",
+        "owner": "nix-community",
+        "repo": "naersk",
+        "rev": "aeb58d5e8faead8980a807c840232697982d47b9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "naersk",
+        "type": "github"
+      }
+    },
+    "nix-filter": {
+      "locked": {
+        "lastModified": 1705332318,
+        "narHash": "sha256-kcw1yFeJe9N4PjQji9ZeX47jg0p9A0DuU4djKvg1a7I=",
+        "owner": "numtide",
+        "repo": "nix-filter",
+        "rev": "3449dc925982ad46246cfc36469baf66e1b64f17",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "nix-filter",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1704194953,
+        "narHash": "sha256-RtDKd8Mynhe5CFnVT8s0/0yqtWFMM9LmCzXv/YKxnq4=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "bd645e8668ec6612439a9ee7e71f7eac4099d4f6",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "ref": "nixos-unstable",
+        "type": "indirect"
+      }
+    },
+    "root": {
+      "inputs": {
+        "fenix": "fenix",
+        "flake-utils": "flake-utils",
+        "naersk": "naersk",
+        "nix-filter": "nix-filter",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "rust-analyzer-src": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1704392858,
+        "narHash": "sha256-66IArofsKG0bxghUClvuzqDekXf/cTcsV81YtZYhZVE=",
+        "owner": "rust-lang",
+        "repo": "rust-analyzer",
+        "rev": "c84352a3467c7856e5c65b8e1a4c7710c2d5a756",
+        "type": "github"
+      },
+      "original": {
+        "owner": "rust-lang",
+        "ref": "nightly",
+        "repo": "rust-analyzer",
+        "type": "github"
+      }
+    },
+    "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
+}

flake.nix

+{
+  inputs = {
+    nixpkgs.url = "nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+    nix-filter.url = "github:numtide/nix-filter";
+
+    fenix = {
+      url = "github:nix-community/fenix";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+
+    naersk = {
+      url = "github:nix-community/naersk";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+  };
+
+  outputs = {
+    self,
+    fenix,
+    flake-utils,
+    naersk,
+    nix-filter,
+    nixpkgs,
+  }:
+    flake-utils.lib.eachDefaultSystem (system: let
+      overlays = [fenix.overlays.default];
+      pkgs = import nixpkgs {inherit overlays system;};
+
+      name = "refinedrust";
+      version = "0.1.0";
+
+      coq = {
+        pkgs = pkgs.coqPackages_8_17;
+        toolchain = [coq.pkgs.coq] ++ coq.pkgs.coq.nativeBuildInputs;
+        version = coq.pkgs.coq.coq-version;
+
+        stdpp = {
+          version = "4be5fd62ddbd5359f912e2cebb415b015c37e565";
+          sha256 = "sha256-9pNWjPy1l1EovcKZchC/23FwlllD/Oa3jEOtN5tDzik=";
+        };
+
+        iris = {
+          version = "1de1b3112754e14a4968534572e118a23344eafe";
+          sha256 = "sha256-Cimb3XxnchPSWVGMSyWmJdLQqHMilw11o2hq/4h8dVQ=";
+        };
+
+        lambda-rust = {
+          version = "4ec2733cce240e3595c37cb926eb000455be77a4";
+          sha256 = "sha256-kX9NIPPOoajuJDVly9qGUCCd3lt8Da2k0dZnDY2zKbY=";
+        };
+      };
+
+      meta = with pkgs.lib; {
+        homepage = "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev";
+        license = licenses.bsd3;
+      };
+
+      rust = {
+        toolchain = pkgs.fenix.fromToolchainFile {
+          dir = ./rr_frontend;
+          sha256 = "sha256-0NR5RJ4nNCMl9ZQDA6eGAyrDWS8fB28xIIS1QGLlOxw=";
+        };
+
+        env = naersk.lib.${system}.override {
+          cargo = rust.toolchain;
+          rustc = rust.toolchain;
+        };
+        lib = "${rust.toolchain}/lib/rustlib/$(rustc -Vv | grep '^host:' | cut -d' ' -f2)/lib";
+        src = "${rust.toolchain}/lib/rustlib/rustc-src/rust/compiler";
+      };
+    in rec {
+      packages = let
+        fetchCoqDeps = with pkgs.lib;
+          drv: [drv] ++ flatten (map fetchCoqDeps drv.propagatedBuildInputs);
+
+        mkDepCoqDerivation = pin: {
+          pname,
+          propagatedBuildInputs ? [],
+          owner ? "iris",
+        }:
+          coq.pkgs.mkCoqDerivation {
+            inherit pname propagatedBuildInputs owner;
+
+            domain = "gitlab.mpi-sws.org";
+            preBuild = "patchShebangs coq-lint.sh";
+
+            release.${pin.version}.sha256 = "${pin.sha256}";
+            version = pin.version;
+          };
+      in {
+        theories = let
+          stdpp = mkDepCoqDerivation coq.stdpp {
+            pname = "stdpp";
+          };
+
+          iris = mkDepCoqDerivation coq.iris {
+            pname = "iris";
+
+            propagatedBuildInputs = [stdpp];
+          };
+
+          lambda-rust = mkDepCoqDerivation coq.lambda-rust {
+            pname = "lambda-rust";
+            owner = "lgaeher";
+
+            propagatedBuildInputs = [iris];
+          };
+        in
+          coq.pkgs.mkCoqDerivation {
+            inherit meta version;
+
+            pname = name;
+            opam-name = name;
+
+            src = with nix-filter.lib;
+              nix-filter {
+                root = ./.;
+                include = ["dune-project" (inDirectory "theories")];
+              };
+
+            propagatedBuildInputs = with coq.pkgs; [coq-record-update equations lambda-rust];
+            useDune = true;
+          };
+
+        frontend = rust.env.buildPackage rec {
+          inherit meta version;
+
+          pname = "cargo-${name}";
+          src = ./rr_frontend;
+
+          buildInputs = [rust.toolchain];
+          nativeBuildInputs = with pkgs;
+            [makeWrapper]
+            ++ lib.optionals stdenv.isDarwin [libzip];
+
+          postInstall = with pkgs.lib.strings; ''
+            wrapProgram $out/bin/refinedrust-rustc \
+              --set LD_LIBRARY_PATH "${rust.lib}"
+
+            wrapProgram $out/bin/${pname} \
+              --set PATH "${makeSearchPath "bin" buildInputs}"
+          '';
+        };
+
+        default = pkgs.buildEnv {
+          inherit meta;
+
+          name = "cargo-${name}";
+          paths = coq.toolchain ++ [packages.frontend rust.toolchain];
+
+          pathsToLink = ["/bin"];
+          nativeBuildInputs = [pkgs.makeWrapper];
+          postBuild = with pkgs.lib.strings; ''
+            wrapProgram $out/bin/dune \
+              --set COQPATH "${makeSearchPath "lib/coq/${coq.version}/user-contrib" (fetchCoqDeps packages.theories)}"
+          '';
+        };
+      };
+
+      devShells.default = pkgs.mkShell {
+        inputsFrom = with packages; [frontend theories];
+
+        shellHook = ''
+          export LD_LIBRARY_PATH=''${LD_LIBRARY_PATH}:${rust.lib}
+          export RUST_SRC_PATH=${rust.src}/rustc_driver/Cargo.toml
+        '';
+      };
+
+      formatter = pkgs.alejandra;
+    });
+}

rr_frontend/rust-toolchain.toml

 [toolchain]
 channel = "nightly-2023-09-15"
-components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ]
+components = ["clippy", "llvm-tools-preview", "rust-analyzer", "rustc-dev", "rustfmt"]
 profile = "minimal"

theories/lithium/dune

 (coq.theory
  (name lithium)
- (package coq-lithium)
+ (package refinedrust)
  (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "Lithium")
  (theories stdpp iris RecordUpdate Ltac2))