From e607b6da3e82390eb8f7bc042de10de72f7312c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Fri, 9 Aug 2024 12:07:01 +0200
Subject: [PATCH] pin RefinedRust version
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>
---
 .github/workflows/verify.yml | 4 ----
 .gitmodules                  | 3 +++
 verification/.gitignore      | 1 -
 verification/refinedrust     | 1 +
 verification/setup.md        | 5 +----
 5 files changed, 5 insertions(+), 9 deletions(-)
 create mode 160000 verification/refinedrust

diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml
index 5db1a1c9..dd09b010 100644
--- a/.github/workflows/verify.yml
+++ b/.github/workflows/verify.yml
@@ -24,14 +24,10 @@ jobs:
       run: opam switch create refinedrust-ace --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
     - name: Install coq
       run: eval $(opam env) && opam update && opam pin add coq 8.17.1 -y
-    #- name: Fix permissions
-      #run: chown -R 1000 .
     - name: ls
       run: ls -la .
     - name: Install openssl dependency
       run: sudo apt update && sudo apt install libssl-dev -y
-    - name: Pull RefinedRust
-      run: git clone https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev.git verification/refinedrust
     - name: Install rustup
       run: curl --proto "=https" --tlsv1.2 -sSf https://sh.rustup.rs | bash /dev/stdin "-y"
     - name: Setup Rust toolchain
diff --git a/.gitmodules b/.gitmodules
index 922dd6a4..64577a8f 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -7,3 +7,6 @@
 [submodule "security-monitor/opensbi"]
 	path = security-monitor/opensbi
 	url = https://github.com/riscv-software-src/opensbi.git
+[submodule "verification/refinedrust"]
+	path = verification/refinedrust
+	url = https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev.git
diff --git a/verification/.gitignore b/verification/.gitignore
index 4ee74ed8..a8276b4e 100644
--- a/verification/.gitignore
+++ b/verification/.gitignore
@@ -2,6 +2,5 @@ _opam
 _build
 log 
 rustc-ice-*
-refinedrust
 generated_code.bak
 _CoqProject
diff --git a/verification/refinedrust b/verification/refinedrust
new file mode 160000
index 00000000..00723737
--- /dev/null
+++ b/verification/refinedrust
@@ -0,0 +1 @@
+Subproject commit 00723737488d913a2e510b1a1698dbe975ad118e
diff --git a/verification/setup.md b/verification/setup.md
index 5442f9b6..fcdd39b8 100644
--- a/verification/setup.md
+++ b/verification/setup.md
@@ -11,10 +11,7 @@ This file documents the basic verification setup.
 For using the RefinedRust toolchain and checking the verified parts of the code, you need to install both the Coq proof assistant and RefinedRust Coq libraries as well as the RefinedRust frontend.
 
 First of all, open a terminal and navigate to the directory containing this file.
-Then, clone the RefinedRust repository into a subdirectory:
-```
-git clone https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev.git refinedrust
-```
+Make sure that there is a subdirectory called `refinedrust` that is up-to-date.
 
 ### Installing Coq and the RefinedRust Coq libraries