initial

.envrc

@@ -0,0 +1 @@
+use flake

.gitignore

@@ -0,0 +1,2 @@
+.direnv
+.*.aux

.vscode/settings.json

@@ -0,0 +1,19 @@
+{
+	"coq.format.indentAfterBullet": "indent",
+	"coq.format.unindentOnCloseProof": true,
+	"coq.format.indentAfterOpenProof": true,
+	"editor.formatOnType": true,
+	"editor.unicodeHighlight.ambiguousCharacters": false,
+	"editor.tabSize": 2,
+	"vscoq.path": "/nix/store/3bhqs93fw89kx339mirf4jgg52dw4fcs-ocaml4.14.2-vscoq-language-server-2.1.4/bin/vscoqtop",
+	"vscoq.args": [
+		"-noinit",
+		"-indices-matter",
+		"-type-in-type",
+		"-w",
+		"-notation-overridden",
+		"-Q",
+		"/Applications/Coq-Platform~8.15~2022.04.app/Contents/Resources/lib/coq/user-contrib/UniMath",
+		"UniMath"
+	]
+}

Test.v

@@ -0,0 +1,6 @@
+Require Export UniMath.Foundations.All.
+
+Lemma myfirstlemma : 2 + 2 = 4.
+Proof.
+  apply idpath.
+Defined.

flake.lock

@@ -0,0 +1,58 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
+      },
+      "original": {
+        "id": "flake-utils",
+        "type": "indirect"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1722141560,
+        "narHash": "sha256-Ul3rIdesWaiW56PS/Ak3UlJdkwBrD4UcagCmXZR9Z7Y=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "038fb464fcfa79b4f08131b07f2d8c9a6bcc4160",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "type": "indirect"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "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

@@ -0,0 +1,42 @@
+{
+  outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      pkgs = import nixpkgs { inherit system; };
+
+      coq = pkgs.coq;
+
+      coqPackages = pkgs.mkCoqPackages coq;
+
+      unimath = pkgs.stdenv.mkDerivation {
+        name = "unimath";
+        src = pkgs.fetchFromGitHub {
+          owner = "unimath";
+          repo = "unimath";
+          rev = "v20240331";
+          sha256 = "sha256-HqAft5pFQbBHQfmvUZEqozVZjnGBlJ5Y8A983JQxQSs=";
+        };
+        buildInputs = with pkgs;[
+          coq
+          git
+          gnumake
+          ocamlPackages.camlp5
+          ocamlPackages.findlib
+          ocamlPackages.num
+        ];
+        buildPhase = ''
+          echo $NIX_BUILD_CORES
+          make -j $NIX_BUILD_CORES
+        '';
+      };
+    in
+    {
+      packages = { inherit unimath; };
+
+      devShell = pkgs.mkShell {
+        packages = [
+          coq
+          coqPackages.vscoq-language-server
+        ];
+      };
+    });
+}