From 8ca6035b0b8909e081d31050ed0684d5689aa851 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Sat, 18 May 2024 00:33:00 +0100
Subject: [PATCH] import mathlib fork from url, rather than path

---
 lake-manifest.json | 7 +++++--
 lakefile.lean      | 5 ++---
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 7dcf97a..9552b6b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -55,11 +55,14 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"type": "path",
+  {"url": "https://github.com/monsterkrampe/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "d03f91a1e874fdbfaedbacc79d8421ce216aa12c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
+   "inputRev": "PFunctor-universe-refactoring",
    "inherited": false,
-   "dir": "./../mathlib4",
    "configFile": "lakefile.lean"}],
  "name": "qpf",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index e18a250..d9a3e4b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -9,6 +9,5 @@ lean_lib Qpf
 
 lean_lib Test
 
-require mathlib from "../mathlib4"
-  -- git
-  -- "https://github.com/leanprover-community/mathlib4.git"@"v4.7.0"
+require mathlib from git
+  "https://github.com/monsterkrampe/mathlib4.git"@"PFunctor-universe-refactoring"