diff --git a/gnu/local.mk b/gnu/local.mk
index 70133e6502..4e46b47ad9 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1283,9 +1283,6 @@ dist_patch_DATA =						\
   %D%/packages/patches/icedtea-7-hotspot-aarch64-use-c++98.patch\
   %D%/packages/patches/id3lib-CVE-2007-4460.patch			\
   %D%/packages/patches/id3lib-UTF16-writing-bug.patch			\
-  %D%/packages/patches/idris-disable-test.patch			\
-  %D%/packages/patches/idris-build-with-haskeline-0.8.patch	\
-  %D%/packages/patches/idris-build-with-megaparsec-9.patch	\
   %D%/packages/patches/idris-test-ffi008.patch			\
   %D%/packages/patches/ilmbase-fix-tests.patch			\
   %D%/packages/patches/imagemagick-CVE-2020-27829.patch		\
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index f84431cab9..28e918a486 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -19,9 +19,28 @@
 ;;; You should have received a copy of the GNU General Public License
 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
 
+;;; TODO:
+;;;
+;;;  - Idris has multiple backends, but we only register Chez as an
+;;;  input.  Decide how to make backends optional, and/or which ones to package
+;;;  by default.
+;;;
+;;;  - Set RUNPATH instead of using LD_LIBRARY_PATH.  See
+;;;  http://blog.tremily.us/posts/rpath/  This probably needs patching Idris
+;;;  because it uses its FFI infrastrucutre to open libidris_support.so, which
+;;;  is based on dlopen.
+;;;
+;;;  - The reason some of the historical packages point to
+;;;  github.com/attila-lendvai-patches is that these versions need some
+;;;  patches to make them buildable today, and these branches haven't been
+;;;  incorporated into the official repo yet.  Once/if that happens, these
+;;;  URL's can be changed to point to the official repo.
+
 (define-module (gnu packages idris)
   #:use-module (gnu packages)
+  #:use-module (gnu packages base)
   #:use-module (gnu packages bash)
+  #:use-module (gnu packages chez)
   #:use-module (gnu packages haskell-check)
   #:use-module (gnu packages haskell-web)
   #:use-module (gnu packages haskell-xyz)
@@ -29,31 +48,40 @@ (define-module (gnu packages idris)
   #:use-module (gnu packages llvm)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ncurses)
+  #:use-module (gnu packages node)
   #:use-module (gnu packages perl)
+  #:use-module (gnu packages racket)
+  #:use-module (gnu packages version-control)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system haskell)
   #:use-module (guix download)
+  #:use-module (guix git)
   #:use-module (guix git-download)
   #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (guix gexp)
   #:use-module (guix packages)
-  #:use-module (guix utils))
+  #:use-module (guix utils)
+  #:use-module (ice-9 match)
+  #:use-module (ice-9 regex)
+  #:export (make-idris-package))
 
-(define-public idris-1.3.3
+;;;
+;;; Idris 1
+;;;
+(define-public idris-1.3.4
   (package
     (name "idris")
-    (version "1.3.3")
+    (version "1.3.4")
     (source (origin
-              (method url-fetch)
-              (uri (string-append
-                    "https://hackage.haskell.org/package/"
-                    "idris-" version "/idris-" version ".tar.gz"))
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/idris-lang/Idris-dev.git")
+                    (commit (string-append "v" version))))
               (sha256
                (base32
-                "1pachwc6msw3n1mz2z1r1w6h518w9gbhdvbaa5vi1qp3cn3wm6q4"))
-              (patches (search-patches "idris-disable-test.patch"
-                                       "idris-build-with-haskeline-0.8.patch"
-                                       "idris-build-with-megaparsec-9.patch"
-                                       "idris-test-ffi008.patch"))))
+                "0cd2a92323hb9a6wy8sc0cqwnisf4pv8y9y2rxvxcbyv8cs1q8g2"))
+              (patches (search-patches "idris-test-ffi008.patch"))
+              (file-name (git-file-name "idris" version))))
     (build-system haskell-build-system)
     (native-inputs                      ;For tests
      (list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
@@ -141,7 +169,11 @@ (define-public idris-1.3.3
              (let* ((out (assoc-ref outputs "out"))
                     (exe (string-append out "/bin/idris")))
                (wrap-program exe
-                 `("IDRIS_CC" = (,',(cc-for-target))))))))))
+                 `("IDRIS_CC" = (,',(cc-for-target))))
+               (with-directory-excursion (string-append out "/bin/")
+                 (let ((versioned-name ,(string-append name "-" version)))
+                   (rename-file ,name versioned-name)
+                   (symlink versioned-name ,name)))))))))
     (native-search-paths
      (list (search-path-specification
             (variable "IDRIS_LIBRARY_PATH")
@@ -155,7 +187,254 @@ (define-public idris-1.3.3
 Epigram and Agda.")
     (license license:bsd-3)))
 
-(define-public idris idris-1.3.3)
+(define-public idris idris-1.3.4)
+
+;;;
+;;; Idris 2
+;;;
+(define* (make-idris-package source idris-version
+                             #:key bootstrap-idris
+                             (idris-version-tag #false)
+                             (guix-version (string-append
+                                            idris-version
+                                            (if idris-version-tag
+                                                (string-append
+                                                 "-" idris-version-tag)
+                                                "")))
+                             (ignore-test-failures? #false)
+                             (unwrap? #true)
+                             (tests? #true)
+                             (historical? #false)
+                             (hidden? #false) ; or (hidden? historical?)
+                             (substitutable? (not historical?))
+                             (files-to-patch-for-shell
+                              '("src/Compiler/Scheme/Chez.idr"
+                                "src/Compiler/Scheme/Racket.idr"
+                                "src/Compiler/Scheme/Gambit.idr"
+                                "src/Compiler/ES/Node.idr"
+                                "bootstrap/idris2_app/idris2.rkt"
+                                "bootstrap/idris2_app/idris2.ss"
+                                "build/stage1/idris2_app/idris2.ss"
+                                "build/stage1/idris2_app/idris2.rkt"
+                                ))
+                             (with-bootstrap-shortcut? (not historical?)))
+  "HISTORICAL? means that it's only interesting for historical reasons, e.g. to be
+used as a bootsrapping stage.
+
+WITH-BOOTSTRAP-SHORTCUT? controls whether to use a previous version of Idris to
+build us (which is potentially recursive), or use the captured compiler output
+(Scheme code)."
+  (package
+    (name "idris2")
+    (version guix-version)
+    (source (match source
+              ((commit hash . url)
+               (origin
+                 (method git-fetch)
+                 (uri (git-reference
+                       (url (if (null? url)
+                                "https://github.com/idris-lang/Idris2.git"
+                                (car url)))
+                       (commit commit)))
+                 (sha256 (base32 hash))
+                 (file-name (git-file-name name version))))
+              ((or (? git-checkout?)
+                   (? local-file?))
+               source)))
+    (build-system gnu-build-system)
+    (native-inputs
+     (list (if with-bootstrap-shortcut?
+               chez-scheme
+               bootstrap-idris)
+           clang-toolchain-12 ; older clang-toolchain versions don't have a bin/cc
+           coreutils which git
+           node                         ; only for the tests
+           racket                       ; only for the tests
+           sed))
+    (inputs
+     (list bash-minimal chez-scheme gmp))
+    (arguments
+     (list
+      #:tests? tests?
+      #:substitutable? substitutable?
+      #:make-flags
+      #~(list (string-append "CC=" #$(cc-for-target))
+              #$(string-append "IDRIS_VERSION=" idris-version)
+              #$(string-append "IDRIS_VERSION_TAG=" (or idris-version-tag ""))
+              #$(if with-bootstrap-shortcut?
+                    #~(string-append "SCHEME="
+                                     #$(this-package-input "chez-scheme")
+                                     "/bin/scheme")
+                    #~(string-append "BOOTSTRAP_IDRIS="
+                                     #$bootstrap-idris
+                                     "/bin/" #$(package-name bootstrap-idris)))
+              (string-append "PREFIX=" (assoc-ref %outputs "out"))
+              "-j1")
+      #:phases
+      `(modify-phases %standard-phases
+         (delete 'bootstrap)
+         (delete 'configure)
+         (delete 'check)    ; check must happen after install and wrap-program
+         (add-after 'unpack 'patch-paths
+           (lambda* (#:key inputs #:allow-other-keys)
+             (let ((files-to-patch (filter file-exists?
+                                           ',files-to-patch-for-shell)))
+               (substitute* files-to-patch
+                 ((,(regexp-quote "#!/bin/sh"))
+                  (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+                 (("/usr/bin/env")
+                  (string-append (assoc-ref inputs "coreutils") "/bin/env"))))))
+         ,@(if unwrap?
+               `((add-after 'install 'unwrap
+                   (lambda* (#:key outputs #:allow-other-keys)
+                     ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+                     ;; the real executable, but it sets LD_LIBRARY_PATH
+                     ;; incorrectly.  Remove bin/idris2 and replace it with
+                     ;; bin/idris2_app/idris2.so instead.
+                     (let* ((out (assoc-ref outputs "out"))
+                            (image-base (string-append
+                                         out "/bin/idris2_app/idris2"))
+                            (image (if (file-exists? image-base)
+                                       image-base
+                                       ;; For v0.5.1 and older.
+                                       (string-append image-base ".so"))))
+                       (delete-file (string-append out "/bin/idris2"))
+                       (rename-file image (string-append out "/bin/idris2"))
+                       (delete-file-recursively (string-append out "/bin/idris2_app"))
+                       (delete-file-recursively (string-append out "/lib"))))))
+               '())
+         ,@(if with-bootstrap-shortcut?
+               `((replace 'build
+                   (lambda* (#:key make-flags #:allow-other-keys)
+                     ;; i.e. do not build it using the previous version of
+                     ;; Idris, but rather compile the comitted compiler
+                     ;; output.
+                     (apply invoke "make" "bootstrap" make-flags))))
+               '())
+         (add-after 'unwrap 'wrap-program
+           (lambda* (#:key outputs inputs #:allow-other-keys)
+             (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+                                         "/bin/scheme"))
+                    (out (assoc-ref outputs "out"))
+                    (exe (string-append out "/bin/" ,name))
+                    (version ,idris-version))
+               (wrap-program exe
+                 `("IDRIS2_PREFIX" = (,out))
+                 `("LD_LIBRARY_PATH" prefix (,(string-append
+                                               out "/idris2-" version "/lib")))
+                 `("CC" = (,',(cc-for-target)))
+                 `("CHEZ" = (,chez)))
+               (with-directory-excursion (string-append out "/bin/")
+                 (let ((versioned-name ,(string-append name "-" version)))
+                   (rename-file ,name versioned-name)
+                   (symlink versioned-name ,name))))))
+         (add-after 'wrap-program 'check
+           (lambda* (#:key outputs make-flags #:allow-other-keys)
+             (let ((invoke-make
+                    (lambda (target)
+                      (apply invoke "make"
+                             "INTERACTIVE="
+                             ;; "THREADS=1" ; for reproducible test output
+                             (string-append "IDRIS2="
+                                            (assoc-ref outputs "out")
+                                            "/bin/" ,name)
+                             target make-flags))))
+               ;; TODO This is something like how it should be handled, but
+               ;; the Makefile unconditionally invokes the `testenv` target,
+               ;; and thus overwrites the `runtest` script when `make test` is
+               ;; invoked.  For now this situation is resolved in the Idris
+               ;; Makefile, by explicitly invoking the Idris `runtest` wrapper
+               ;; script with an sh prefix.
+               ;;
+               ;;(invoke-make "testenv")
+               ;;(patch-shebang "build/stage2/runtests")
+               (,(if ignore-test-failures?
+                     'false-if-exception
+                     'begin)
+                (invoke-make "test"))))))))
+    (properties `((hidden? . ,hidden?)))
+    (home-page "https://www.idris-lang.org")
+    (synopsis "General purpose language with full dependent types")
+    (description "Idris is a general purpose language with full dependent
+types.  It is compiled, with eager evaluation.  Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type.  The language is closely related to
+Epigram and Agda.")
+    (license license:bsd-3)))
+
+(define-public idris2-0.1.1
+  ;; branch idris.2
+  ;; This is the first (untagged) Idris2 version that bootstraps off of the
+  ;; Idris1 line.  Originally it was in the repo called Idris2-boot.
+  (make-idris-package '("3c2335ee6bc00b7f417ac672a4ab7b73599abeb3"
+                        "10w10ggyvlw7m1pazbfxr4sj3wpb6z1ap6rg3lxc0z6f2s3x53cb")
+                      "0.1.1"
+                      #:bootstrap-idris idris-1.3.4
+                      #:historical? #true
+                      #:unwrap? #false
+                      ;; TODO `make bootstrap` needs to be backported into the
+                      ;; Makefile in this branch.  Force the bootstrap
+                      ;; shortcut to be turned off.
+                      #:with-bootstrap-shortcut? #false))
+
+(define-public idris2-0.2.1
+  ;; branch idris.3
+  (make-idris-package '("257bbc27498808e8cd4155cc06ea3f6a07541537"
+                        "0idxplcmd6p13i2n0g49bc2snddny4kdr4wvd8854snzsiwqn7p1"
+                        "https://github.com/attila-lendvai-patches/Idris2")
+                      "0.2.1"
+                      #:bootstrap-idris idris2-0.1.1
+                      #:historical? #true))
+
+(define-public idris2-0.2.2
+  ;; branch idris.4
+  (make-idris-package '("9bc8e6e9834cbc7b52dc6ca2d80d7e96afeb47d1"
+                        "0xzl1mb5yxgp6v36rngy00i59cfy67niyiblcpaksllrgmg639p4"
+                        "https://github.com/attila-lendvai-patches/Idris2")
+                      "0.2.2"
+                      #:bootstrap-idris idris2-0.2.1
+                      #:historical? #true))
+
+(define-public idris2-0.3.0
+  ;; branch idris.5
+  (make-idris-package '("025b5cd25b76eae28283a10bd155c384e46fbd82"
+                        "00a83paib571ahknipmgw7g9pbym105isk3bz0c1ng41s4kjpsxh"
+                        "https://github.com/attila-lendvai-patches/Idris2")
+                      "0.3.0"
+                      #:bootstrap-idris idris2-0.2.2
+                      #:historical? #true))
+
+(define-public idris2-0.4.0
+  ;; branch idris.6
+  (make-idris-package '("v0.4.0"
+                        "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g")
+                      "0.4.0"
+                      #:bootstrap-idris idris2-0.3.0
+                      #:ignore-test-failures? #true ; TODO investigate
+                      #:historical? #true))
+
+(define-public idris2-0.5.1
+  (make-idris-package '("v0.5.1"
+                        "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+                      "0.5.1"))
+
+;; TODO re build failure: in the build sandbox some parts of the test output
+;; is missing.  I cannot reproduce it in a guix shell.  My assumption is that
+;; it's an Idris bug that only manifests in certain circumstances.  There are
+;; some other issues left with the use of #!/bin/sh, too.
+(define-public idris2-dev
+  (make-idris-package '("4bb12225424d76c7874b176e2bfb8b5550c112eb"
+                        "0kb800cgfm0afa83pbyi3x9bpswcl8jz4pr68zy092fs50km3bj7"
+                        "https://github.com/attila-lendvai-patches/Idris2")
+                      "0.5.1"
+                      #:ignore-test-failures? #true
+                      #:idris-version-tag "dev"))
+
+(define-public idris2 idris2-0.5.1)
+
+;;;
+;;; Idris apps
+;;;
 
 ;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
 (define (idris-default-arguments name)
diff --git a/gnu/packages/patches/idris-build-with-haskeline-0.8.patch b/gnu/packages/patches/idris-build-with-haskeline-0.8.patch
deleted file mode 100644
index 5d1fec2409..0000000000
--- a/gnu/packages/patches/idris-build-with-haskeline-0.8.patch
+++ /dev/null
@@ -1,85 +0,0 @@
-From 89a87cf666eb8b27190c779e72d0d76eadc1bc14 Mon Sep 17 00:00:00 2001
-From: Niklas Larsson <niklas@mm.st>
-Date: Sat, 6 Jun 2020 15:29:45 +0200
-Subject: [PATCH] Fix to unblock haskeline-0.8
-
----
-Taken from <https://github.com/idris-lang/Idris-dev/pull/4871>
-
- idris.cabal         |  2 +-
- src/Idris/Output.hs |  8 --------
- src/Idris/REPL.hs   | 12 +++++-------
- 3 files changed, 6 insertions(+), 16 deletions(-)
-
-diff --git a/idris.cabal b/idris.cabal
-index 38359019a9..bc9e265023 100644
---- a/idris.cabal
-+++ b/idris.cabal
-@@ -336,7 +336,7 @@ Library
-                 , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0
-                 , filepath < 1.5
-                 , fingertree >= 0.1.4.1 && < 0.2
--                , haskeline >= 0.7 && < 0.8
-+                , haskeline >= 0.8 && < 0.9
-                 , ieee754 >= 0.7 && < 0.9
-                 , megaparsec >= 7.0.4 && < 9
-                 , mtl >= 2.1 && < 2.3
-diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs
-index 70b4d48a30..6b5d59948c 100644
---- a/src/Idris/Output.hs
-+++ b/src/Idris/Output.hs
-@@ -37,21 +37,13 @@ import Prelude hiding ((<$>))
- #endif
- 
- import Control.Arrow (first)
--import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
- import Data.List (intersperse, nub)
- import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
- import qualified Data.Set as S
--import System.Console.Haskeline.MonadException (MonadException(controlIO),
--                                                RunIO(RunIO))
- import System.FilePath (replaceExtension)
- import System.IO (Handle, hPutStr, hPutStrLn)
- import System.IO.Error (tryIOError)
- 
--instance MonadException m => MonadException (ExceptT Err m) where
--    controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
--                    run' = RunIO (fmap ExceptT . run . runExceptT)
--                    in fmap runExceptT $ f run'
--
- pshow :: IState -> Err -> String
- pshow ist err = displayDecorated (consoleDecorate ist) .
-                 renderPretty 1.0 80 .
-diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
-index 05587d9672..5e0dc21089 100644
---- a/src/Idris/REPL.hs
-+++ b/src/Idris/REPL.hs
-@@ -122,23 +122,21 @@ repl orig mods efile
-                              (if colour && not isWindows
-                                 then colourisePrompt theme str
-                                 else str) ++ " "
--        x <- H.catch (H.withInterrupt $ getInputLine prompt)
--                     (ctrlC (return $ Just ""))
-+        x <- H.handleInterrupt (ctrlC (return $ Just "")) (H.withInterrupt $ getInputLine prompt)
-         case x of
-             Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
-                           return ()
-             Just input -> -- H.catch
--                do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile)
--                                 (ctrlC (return (Just mods)))
-+                do ms <- H.handleInterrupt (ctrlC (return (Just mods))) (H.withInterrupt $ lift $ processInput input orig mods efile)
-                    case ms of
-                         Just mods -> let efile' = fromMaybe efile (listToMaybe mods)
-                                      in repl orig mods efile'
-                         Nothing -> return ()
- --                             ctrlC)
- --       ctrlC
--   where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
--         ctrlC act e = do lift $ iputStrLn (show e)
--                          act -- repl orig mods
-+   where ctrlC :: InputT Idris a -> InputT Idris a
-+         ctrlC act = do lift $ iputStrLn "Interrupted"
-+                        act -- repl orig mods
- 
-          showMVs c thm [] = ""
-          showMVs c thm ms = "Holes: " ++
diff --git a/gnu/packages/patches/idris-build-with-megaparsec-9.patch b/gnu/packages/patches/idris-build-with-megaparsec-9.patch
deleted file mode 100644
index 6d7ff1d713..0000000000
--- a/gnu/packages/patches/idris-build-with-megaparsec-9.patch
+++ /dev/null
@@ -1,27 +0,0 @@
-From 6ea9bc913877d765048d7cdb7fc5aec60b196fac Mon Sep 17 00:00:00 2001
-From: Felix Yan <felixonmars@archlinux.org>
-Date: Wed, 16 Dec 2020 21:48:32 +0800
-Subject: [PATCH] Fix compatibility with megaparsec 9
-
----
-Taken from <https://github.com/idris-lang/Idris-dev/pull/4892>
-
- src/Idris/Parser/Stack.hs | 4 ++++
- 1 file changed, 4 insertions(+)
-
-diff --git a/src/Idris/Parser/Stack.hs b/src/Idris/Parser/Stack.hs
-index fb7b611440..879786f4d2 100644
---- a/src/Idris/Parser/Stack.hs
-+++ b/src/Idris/Parser/Stack.hs
-@@ -84,7 +84,11 @@ instance Message ParseError where
-       (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
- #endif
-   messageText = PP.text . init . P.parseErrorTextPretty . parseError
-+#if MIN_VERSION_megaparsec(9,0,0)
-+  messageSource err = sline
-+#else
-   messageSource err = Just sline
-+#endif
-     where
- #if MIN_VERSION_megaparsec(8,0,0)
-       (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
diff --git a/gnu/packages/patches/idris-disable-test.patch b/gnu/packages/patches/idris-disable-test.patch
deleted file mode 100644
index ec8c7c8451..0000000000
--- a/gnu/packages/patches/idris-disable-test.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-The "pkg010" test output depends on the version of optparse-applicative being
-used.  The expected output requires optparse-applicative >= 0.15.1.0.  Skip
-the test for now.
-
---- idris-1.3.3/test/TestData.hs	2021-01-19 23:05:24.238958262 -0600
-+++ idris-1.3.3/test/TestData.hs	2021-01-19 23:10:33.314390997 -0600
-@@ -212,8 +212,10 @@
-       (  5, ANY  ),
-       (  6, ANY  ),
-       (  7, ANY  ),
--      (  8, ANY  ),
--      ( 10, ANY  )]),
-+      (  8, ANY  )]),
-+--      FIXME: Expected output depends on optparse-applicative version.
-+--      See https://github.com/idris-lang/Idris-dev/issues/4896
-+--      ( 10, ANY  )]),
-   ("prelude",         "Prelude",
-     [ (  1, ANY  )]),
-   ("primitives",      "Primitive types",
