diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el
index 715e33658..e2cb6ad4a 100644
--- a/modules/lang/agda/config.el
+++ b/modules/lang/agda/config.el
@@ -1,41 +1,32 @@
 ;;; lang/agda/config.el -*- lexical-binding: t; -*-
 
-(defvar +agda-dir
-  (when (executable-find "agda-mode")
-    (file-name-directory (shell-command-to-string "agda-mode locate"))))
-
-(use-package! agda2
-  :when +agda-dir
-  :load-path +agda-dir)
-
-(use-package! agda2-mode
-  :defer t
-  :config
-  (map! :map agda2-mode-map
-        :localleader
-        "?"   #'agda2-show-goals
-        "."   #'agda2-goal-and-context-and-inferred
-        ","   #'agda2-goal-and-context
-        "="   #'agda2-show-constraints
-        "SPC" #'agda2-give
-        "a"   #'agda2-auto-maybe-all
-        "b"   #'agda2-previous-goal
-        "c"   #'agda2-make-case
-        "d"   #'agda2-infer-type-maybe-toplevel
-        "e"   #'agda2-show-context
-        "f"   #'agda2-next-goal
-        "gG"  #'agda2-go-back
-        "h"   #'agda2-helper-function-type
-        "l"   #'agda2-load
-        "n"   #'agda2-compute-normalised-maybe-toplevel
-        "p"   #'agda2-module-contents-maybe-toplevel
-        "r"   #'agda2-refine
-        "s"   #'agda2-solveAll
-        "t"   #'agda2-goal-type
-        "w"   #'agda2-why-in-scope-maybe-toplevel
-        (:prefix "x"
-          "c"   #'agda2-compile
-          "d"   #'agda2-remove-annotations
-          "h"   #'agda2-display-implicit-arguments
-          "q"   #'agda2-quit
-          "r"   #'agda2-restart)))
+(map!
+ :after agda2-mode
+ :map agda2-mode-map
+ :localleader
+ "?"   #'agda2-show-goals
+ "."   #'agda2-goal-and-context-and-inferred
+ ","   #'agda2-goal-and-context
+ "="   #'agda2-show-constraints
+ "SPC" #'agda2-give
+ "a"   #'agda2-auto-maybe-all
+ "b"   #'agda2-previous-goal
+ "c"   #'agda2-make-case
+ "d"   #'agda2-infer-type-maybe-toplevel
+ "e"   #'agda2-show-context
+ "f"   #'agda2-next-goal
+ "gG"  #'agda2-go-back
+ "h"   #'agda2-helper-function-type
+ "l"   #'agda2-load
+ "n"   #'agda2-compute-normalised-maybe-toplevel
+ "p"   #'agda2-module-contents-maybe-toplevel
+ "r"   #'agda2-refine
+ "s"   #'agda2-solveAll
+ "t"   #'agda2-goal-type
+ "w"   #'agda2-why-in-scope-maybe-toplevel
+ (:prefix "x"
+   "c"   #'agda2-compile
+   "d"   #'agda2-remove-annotations
+   "h"   #'agda2-display-implicit-arguments
+   "q"   #'agda2-quit
+   "r"   #'agda2-restart))
diff --git a/modules/lang/agda/doctor.el b/modules/lang/agda/doctor.el
deleted file mode 100644
index e38ccbc03..000000000
--- a/modules/lang/agda/doctor.el
+++ /dev/null
@@ -1,5 +0,0 @@
-;; -*- lexical-binding: t; no-byte-compile: t; -*-
-;;; lang/agda/doctor.el
-
-(unless (executable-find "agda-mode")
-  (warn! "Couldn't find agda-mode. Agda support won't work"))
diff --git a/modules/lang/agda/packages.el b/modules/lang/agda/packages.el
new file mode 100644
index 000000000..35bead2a1
--- /dev/null
+++ b/modules/lang/agda/packages.el
@@ -0,0 +1,15 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/agda/packages.el
+
+
+(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"))))