diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000000000000000000000000000000000000..443208743d53361f19c25b4f96d9d1fc70ee9f06
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,50 @@
+{
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
+    flake-utils.url = "github:numtide/flake-utils";
+
+#     compcert-capla.url =
+# "git+ssh://git@gitlab.inria.fr/fresco/capla/compiler?submodules=1&ref=master-merge-test";
+#     compcert-capla.flake = false;
+  };
+
+  outputs = { self, nixpkgs, flake-utils }:
+    with flake-utils.lib;
+    eachSystem defaultSystems (system:
+      let
+        pkgs = import nixpkgs { system = "x86_64-linux"; config.allowUnfree = true; };
+        # compcert-mod = pkgs.compcert.overrideAttrs (oA: {
+        #   src = compcert-capla;
+        # });
+      in rec {
+        # devShell = pkgs.mkShell {
+        #   nativeBuildInputs = with pkgs; [
+        #     compcert-mod
+        #     coq ocaml
+        #     ocamlPackages.findlib
+        #     ocamlPackages.menhir
+        #     ocamlPackages.menhirLib
+        #     coqPackages.MenhirLib
+        #     coqPackages.flocq
+        #     lapack
+        #     clang
+        #     bash
+        #     gcc
+        #   ];
+        # };
+        devShell = pkgs.coqPackages.mkCoqDerivation {
+          pname = "compcert";
+          owner = "compcert";
+          version = "1.0.0"; 
+          src = ./.;
+          propagatedBuildInputs = (with pkgs; [
+          ]) ++ (with pkgs.coqPackages.coq.ocamlPackages; [
+            ocaml
+            menhir menhirLib findlib
+          ]) ++ (with pkgs.coqPackages; [
+            coq
+            MenhirLib flocq mathcomp-ssreflect mathcomp-algebra mathcomp-zify
+          ]);
+        };
+      });
+}