diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el
index 0fa2bdbc7..876279f1d 100644
--- a/modules/lang/agda/config.el
+++ b/modules/lang/agda/config.el
@@ -1,5 +1,11 @@
 ;;; lang/agda/config.el -*- lexical-binding: t; -*-
 
+(when (and (featurep! +local)
+           (executable-find "agda-mode"))
+  (add-load-path!
+   (file-name-directory (shell-command-to-string "agda-mode locate"))))
+
+
 (map! :after agda2-mode
       :map agda2-mode-map
       :localleader
diff --git a/modules/lang/agda/packages.el b/modules/lang/agda/packages.el
index 35bead2a1..49278f745 100644
--- a/modules/lang/agda/packages.el
+++ b/modules/lang/agda/packages.el
@@ -1,15 +1,14 @@
 ;; -*- no-byte-compile: t; -*-
 ;;; lang/agda/packages.el
 
+(unless (featurep! +local)
+  (package! agda-input
+    :recipe (:host github :repo "agda/agda"
+             :files ("src/data/emacs-mode/agda-input.el")
+             :nonrecursive t))
 
-(package! agda-input
-  :recipe
-  (:host github :repo "agda/agda"
-         :files ("src/data/emacs-mode/agda-input.el")))
-
-(package! agda2-mode
-  :recipe
-  (:host github :repo "agda/agda"
-         :files
-         ("src/data/emacs-mode/*.el"
-          (:exclude "agda-input.el"))))
+  (package! agda2-mode
+    :recipe (:host github :repo "agda/agda"
+             :files ("src/data/emacs-mode/*.el"
+                     (:exclude "agda-input.el"))
+             :nonrecursive t)))