gnu: idris: Update to 1.3.4.
* gnu/packages/patches/idris-build-with-haskeline-0.8.patch, gnu/packages/patches/idris-build-with-megaparsec-9.patch, gnu/packages/patches/idris-disable-test.patch: Delete patches. * gnu/local.mk (dist_patch_DATA): Unregister them. * gnu/packages/idris.scm (idris): Update to 1.3.4. [source]: Use git-fetch. Adjust patches. Co-authored-by: Attila Lendvai <attila@lendvai.name>master
parent
ae6cd99573
commit
0cf1178a65
|
@ -1283,9 +1283,6 @@ dist_patch_DATA = \
|
||||||
%D%/packages/patches/icedtea-7-hotspot-aarch64-use-c++98.patch\
|
%D%/packages/patches/icedtea-7-hotspot-aarch64-use-c++98.patch\
|
||||||
%D%/packages/patches/id3lib-CVE-2007-4460.patch \
|
%D%/packages/patches/id3lib-CVE-2007-4460.patch \
|
||||||
%D%/packages/patches/id3lib-UTF16-writing-bug.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/idris-test-ffi008.patch \
|
||||||
%D%/packages/patches/ilmbase-fix-tests.patch \
|
%D%/packages/patches/ilmbase-fix-tests.patch \
|
||||||
%D%/packages/patches/imagemagick-CVE-2020-27829.patch \
|
%D%/packages/patches/imagemagick-CVE-2020-27829.patch \
|
||||||
|
|
|
@ -3,6 +3,7 @@
|
||||||
;;; Copyright © 2016, 2017 David Craven <david@craven.ch>
|
;;; Copyright © 2016, 2017 David Craven <david@craven.ch>
|
||||||
;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
|
;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
|
||||||
;;; Copyright © 2019, 2021, 2022 Eric Bavier <bavier@posteo.net>
|
;;; Copyright © 2019, 2021, 2022 Eric Bavier <bavier@posteo.net>
|
||||||
|
;;; Copyright © 2022 Attila Lendvai <attila@lendvai.name>
|
||||||
;;;
|
;;;
|
||||||
;;; This file is part of GNU Guix.
|
;;; This file is part of GNU Guix.
|
||||||
;;;
|
;;;
|
||||||
|
@ -39,19 +40,17 @@
|
||||||
(define-public idris
|
(define-public idris
|
||||||
(package
|
(package
|
||||||
(name "idris")
|
(name "idris")
|
||||||
(version "1.3.3")
|
(version "1.3.4")
|
||||||
(source (origin
|
(source (origin
|
||||||
(method url-fetch)
|
(method git-fetch)
|
||||||
(uri (string-append
|
(uri (git-reference
|
||||||
"https://hackage.haskell.org/package/"
|
(url "https://github.com/idris-lang/Idris-dev.git")
|
||||||
"idris-" version "/idris-" version ".tar.gz"))
|
(commit (string-append "v" version))))
|
||||||
|
(file-name (git-file-name name version))
|
||||||
(sha256
|
(sha256
|
||||||
(base32
|
(base32
|
||||||
"1pachwc6msw3n1mz2z1r1w6h518w9gbhdvbaa5vi1qp3cn3wm6q4"))
|
"0cd2a92323hb9a6wy8sc0cqwnisf4pv8y9y2rxvxcbyv8cs1q8g2"))
|
||||||
(patches (search-patches "idris-disable-test.patch"
|
(patches (search-patches "idris-test-ffi008.patch"))))
|
||||||
"idris-build-with-haskeline-0.8.patch"
|
|
||||||
"idris-build-with-megaparsec-9.patch"
|
|
||||||
"idris-test-ffi008.patch"))))
|
|
||||||
(build-system haskell-build-system)
|
(build-system haskell-build-system)
|
||||||
(native-inputs ;For tests
|
(native-inputs ;For tests
|
||||||
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
|
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
|
||||||
|
|
|
@ -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: " ++
|
|
|
@ -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)
|
|
|
@ -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",
|
|
Reference in New Issue