From 89d5ac8a17d4ccba5913fbb046a1ea198def4234 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= <tomas.riveral@icloud.com>
Date: Tue, 9 Jun 2026 16:26:34 +0200
Subject: [PATCH 1/4] micro-vivify: comment out from flake.nix

---
 flake.nix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/flake.nix b/flake.nix
index a95a4ee..363ea8a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -45,10 +45,10 @@
       url = "github:nix-community/disko";
       inputs.nixpkgs.follows = "nixpkgs";
     };
-    microPlugins-vivify = {
+    /*microPlugins-vivify = {
       url = "git+https://codeberg.org/gibbert/micro-vivify";
       flake = false;
-    };
+    };*/
     flake-parts = {
       url = "github:hercules-ci/flake-parts";
     };

From 259ee7e5541402550e4b141ce2b0553124c3d2ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= <tomas.riveral@icloud.com>
Date: Tue, 9 Jun 2026 20:11:13 +0200
Subject: [PATCH 2/4] mathematics: init module with lean4

---
 modules/applications/mathematics.nix | 7 +++++++
 modules/hosts/desktop.nix            | 1 +
 modules/hosts/laptop.nix             | 1 +
 3 files changed, 9 insertions(+)
 create mode 100644 modules/applications/mathematics.nix

diff --git a/modules/applications/mathematics.nix b/modules/applications/mathematics.nix
new file mode 100644
index 0000000..943a2f0
--- /dev/null
+++ b/modules/applications/mathematics.nix
@@ -0,0 +1,7 @@
+_: {
+  flake.nixosModules.mathematics = {pkgs, ...}: {
+    environment.systemPackages = with pkgs; [
+      lean4
+    ];
+  }; 
+}
diff --git a/modules/hosts/desktop.nix b/modules/hosts/desktop.nix
index b46a235..fa83317 100644
--- a/modules/hosts/desktop.nix
+++ b/modules/hosts/desktop.nix
@@ -35,6 +35,7 @@
       kdrive-desktop # we will setup this later
       latex
       ly
+      mathematics
       mullvad
       networking
       notifications
diff --git a/modules/hosts/laptop.nix b/modules/hosts/laptop.nix
index f6b1400..85fe064 100644
--- a/modules/hosts/laptop.nix
+++ b/modules/hosts/laptop.nix
@@ -36,6 +36,7 @@
       kdrive-laptop
       latex
       ly
+      mathematics
       mullvad
       networking
       notifications

From d9969cbd715bba108e10a4f2ad297262ef2e2101 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= <tomas.riveral@icloud.com>
Date: Tue, 9 Jun 2026 20:11:13 +0200
Subject: [PATCH 3/4] mathematics: init module with lean4

---
 modules/applications/mathematics.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/modules/applications/mathematics.nix b/modules/applications/mathematics.nix
index 943a2f0..2d8ce6e 100644
--- a/modules/applications/mathematics.nix
+++ b/modules/applications/mathematics.nix
@@ -1,7 +1,7 @@
 _: {
   flake.nixosModules.mathematics = {pkgs, ...}: {
     environment.systemPackages = with pkgs; [
-      lean4
+      elan
     ];
   }; 
 }

From a063b505c6c7cbd771e7b0218da0df6ac80b5d46 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= <tomas.riveral@icloud.com>
Date: Wed, 10 Jun 2026 10:26:16 +0200
Subject: [PATCH 4/4] CI: weekly PR merge to main from desktop and laptop

---
 .github/workflows/sync-main.yml | 58 +++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 .github/workflows/sync-main.yml

diff --git a/.github/workflows/sync-main.yml b/.github/workflows/sync-main.yml
new file mode 100644
index 0000000..d92f97f
--- /dev/null
+++ b/.github/workflows/sync-main.yml
@@ -0,0 +1,58 @@
+name: Sync branches into main
+
+on:
+  schedule:
+    - cron: "0 14 * * 1"
+
+    - cron: "0 14 * * 3"
+
+  workflow_dispatch:
+
+permissions:
+  contents: write
+  pull-requests: write
+
+jobs:
+  sync:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Determine source branch
+        id: branch
+        run: |
+          DOW=$(date -u +%u)
+
+          if [ "$DOW" = "1" ]; then
+            echo "source=laptop" >> "$GITHUB_OUTPUT"
+          elif [ "$DOW" = "3" ]; then
+            echo "source=desktop" >> "$GITHUB_OUTPUT"
+          else
+            echo "Not a scheduled sync day"
+            exit 1
+          fi
+
+      - name: Create pull request
+        id: cpr
+        uses: peter-evans/create-pull-request@v7
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          base: main
+          branch: ${{ steps.branch.outputs.source }}
+          title: "Weekly sync: ${{ steps.branch.outputs.source }} → main"
+          body: |
+            This pull request was created automatically by GitHub Actions.
+
+            If the branch can be merged cleanly, auto-merge will merge it automatically.
+
+            If there are merge conflicts, this PR will remain open until they are resolved.
+          draft: false
+
+      - name: Enable auto-merge
+        if: steps.cpr.outputs.pull-request-number
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          gh pr merge \
+            ${{ steps.cpr.outputs.pull-request-number }} \
+            --auto \
+            --merge