feat: update to latest rocq -> fix "make all && make html"

Author: srghma

exercises/array_lock.v

@@ -1,4 +1,5 @@
 From iris.algebra Require Import auth excl gset numbers.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import lang proofmode notation par.
 
 Lemma lookup_array `{!heapGS_gen hlc Σ} l dq vs off v :

exercises/custom_ra.v

@@ -1,4 +1,5 @@
 From iris.algebra Require Import cmra.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang.lib Require Export par.
 From iris.heap_lang Require Import proofmode notation.
 

flake.nix

@@ -14,14 +14,29 @@
     {
       devShells.${system}.default = pkgs.mkShell {
         buildInputs = with pkgs; [
-          rocq-core
-          rocqPackages.stdlib
+          # OPAM tool and build dependencies
+          opam
+          gmp
+          pkg-config
+          rsync
+          unzip
+          patch
+
+          # Rocq & language server (Commented out because installed via opam)
+          # rocq-core
+          # rocqPackages.stdlib
           # rocqPackages.stdpp
           # rocqPackages.iris
-          rocqPackages.vsrocq-language-server
+          # rocqPackages.vsrocq-language-server
+
           gawk
           git
         ];
+
+        shellHook = ''
+          # Automatically load opam environment variables if an opam switch exists
+          eval $(opam env 2>/dev/null)
+        '';
       };
 
       checks.${system}.default = pkgs.stdenv.mkDerivation {

theories/array_lock.v

@@ -1,4 +1,5 @@
 From iris.algebra Require Import auth excl gset numbers.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import lang proofmode notation par.
 
 Lemma lookup_array `{!heapGS_gen hlc Σ} l dq vs off v :

theories/custom_ra.v

@@ -1,4 +1,5 @@
 From iris.algebra Require Import cmra.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang.lib Require Export par.
 From iris.heap_lang Require Import proofmode notation.