Make Idris build with GHC8

[KaneTW]

Fixes #3193. Note that I used the git version of trifecta (stack.yaml has the respective commit) to build this (due to transformers bounds).

The GHC bug in question is https://ghc.haskell.org/trac/ghc/ticket/12201 and the actual workaround is a dummy DeltaParsing IdrisParser instance (which is identical to the (StateT s m) one)

[jfdm]

@KaneTW Thanks for the contribution, it is much appreciated. However, I think as the issue is an 'upstream' issue it might be best to wait until it is fixed before we start adding in fixes for Idris. Especially, if it means pulling in a development version of a dependency.

Currently, the released version of Idris works with GHC prior to version 8.0. Although user's might have trouble installing Idris using cabal and GHC 8.0, I think that an valid and better work-around is to ask users to build the released version of Idris from source using stack. The current Stack configuration for Idris, that is released through hackage, will pull in an earlier version of GHC and will work with 'known to be working' package sets.

By using LTS Haskell we can be presented with, and build using, stable releases of GHC and Hackage. My is opinion that stability is more important than being inline with upstream. Stack will migrate to GHC 8.0 at some point after the summer and will then bring known working packages with it [1,2]. With that, I am okay with waiting for upstream to fix itself, before we look to build Idris against GHC 8.0, and revisit supporting earlier versions of GHC.

Although, I am happy for someone to convince me otherwise.

1. https://www.fpcomplete.com/blog/2016/05/moving-stackage-nightly-ghc-8
2. https://unknownparallel.wordpress.com/2016/05/22/stackage-lts-and-ghc-8-0/

[KaneTW]

I completely agree. I mostly did this so there's an easily accessible way to build with GHC8 for people who are interested.

[ilovezfs]

For what it's worth, I'd like to point out that as a result of this policy, Idris is literally the only Haskell formula in Homebrew that cannot build with GHC 8. I think it would be much better to patch Idris for the time being than to abdicate responsibility and rely on Stack to keep you afloat.

[ilovezfs]

Also, FYI: I've just shipped 0.12.
Homebrew/homebrew-core@c685783
Homebrew/homebrew-core@19c729b

[ahmadsalim]

@ilovezfs I think the policy is just that we wait to trifecta is properly released and not rely on a git version. I hope you see that that is a sensible policy.

Thanks for shipping 0.12!

[ilovezfs]

@ahmadsalim You're welcome. I trust your judgment. Are you in contact with trifecta upstream about their situation? I'd just urge you guys to consider GHC 8 a high priority regardless of Stack's timetable. Also, this PR is failing for 0.12 and HEAD:

src/Idris/Parser.hs:1572:24: error:
    Not in scope: data constructor ‘ErrInfo’
    Perhaps you meant ‘EInfo’ (imported from Idris.AbsSyntax)

src/Idris/Parser.hs:1634:22: error:
    Not in scope: data constructor ‘ErrInfo’
    Perhaps you meant ‘EInfo’ (imported from Idris.AbsSyntax)
cabal: Leaving directory '.'
cabal: Error: some packages failed to install:
idris-0.12 failed during the building phase. The exception was:
ExitFailure 1

Note that I also had to throw in a cabal.config with allow-newer: True to get passed an initial Solver failure.

[ahmadsalim]

@ilovezfs I am unsure what the current status is on communication, but we agreed on IRC that contacting the Trifecta developers might be a good idea.

[LeifW]

Arch Linux packaged the released version of Trifecta, they just "patched" the .cabal bounds: https://git.archlinux.org/svntogit/community.git/tree/trunk/PKGBUILD?h=packages/haskell-trifecta#n22
However, they can't build a new Idris package (since it doesn't build on GHC 8). Maybe similarly applying this patch would be a solution?

[ilovezfs]

I'm wondering if the failure is due to the fact that I used vanilla cabal and not stack. I guess to get this PR to work with cabal, I'd need to handle the trifecta part manually, if that's the problem.

[ilovezfs]

@LeifW well Arch Linux could "just" use Stack as a workaround to package their binaries like I did: https://github.com/Homebrew/homebrew-core/blob/master/Formula/idris.rb#L23-L43

[LeifW]

@ilovezfs Are you using the git version of Idris, or just patching the .cabal bounds on the released version? The ErrInfo type was introduced on git after the last release: ekmett/trifecta#54 (comment)

[LeifW]

I don't believe this patch relies on the git version of Trifecta; you could undo the changes that introduce ErrInfo if you wish to use it w/ release version of Trifecta (w/ appropriately adjusted cabal bounds to build on GHC 8).

[KaneTW]

Correct. The important part is the instance DeltaParsing IdrisParser and adjusted bounds. ErrInfo isn't really necessary.

[ilovezfs]

@LeifW I think I can just grab trifecta as a resource at that revision and it should work. Will take a few minutes to find out :)

[ilovezfs]

@KaneTW BTW now looks like this PR applies to the release but no longer applies to HEAD.

[KaneTW]

@ilovezfs I merged current master onto it.

[ilovezfs]

@KaneTW Hehe...I assume that will now cause it to fail against the release tarball?

[ilovezfs]

Voilà: Idris 0.12.0 built with GHC 8

==> Summary
🍺  /usr/local/Cellar/idris/0.12: 174 files, 206.1M, built in 10 minutes 13 seconds

[ilovezfs]

@KaneTW Yeah, this still fails against HEAD (though it still applies to the release tarball right now):

==> Applying 3226.patch
/usr/bin/patch -g 0 -f -p1 -i /private/tmp/idris--patch-20160621-54553-1qfzofg/3226.patch
patching file idris.cabal
Hunk #1 succeeded at 1027 (offset 3 lines).
Hunk #2 succeeded at 1044 (offset 3 lines).
patching file src/Idris/Parser.hs
Hunk #1 succeeded at 1569 (offset 2 lines).
Hunk #2 succeeded at 1631 (offset 2 lines).
patching file src/Idris/Prover.hs
patching file src/Idris/REPL.hs
Hunk #5 succeeded at 1787 with fuzz 1.
patching file src/Pkg/PParser.hs
patching file stack.yaml
Hunk #1 FAILED at 1.
1 out of 1 hunk FAILED -- saving rejects to file stack.yaml.rej
patching file src/Idris/Parser/Helpers.hs
patching file src/Pkg/PParser.hs
/usr/local/Library/Homebrew/debrew.rb:11:in `raise'
ErrorDuringExecution: Failure while executing: /usr/bin/patch -g 0 -f -p1 -i /private/tmp/idris--patch-20160621-54553-1qfzofg/3226.patch
1. raise
2. ignore
3. backtrace
4. irb
5. shell
Choose an action: 

[KaneTW]

Weird. It should apply, so I have no idea what's happening with stack.yaml there. I guess I could make a stack-ghc8.yaml?

This is what my stack.yaml diff looks like

% git diff main/master -- stack.yaml
diff --git a/stack.yaml b/stack.yaml
index 55870c6..ce644ed 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,7 +1,11 @@
-resolver: lts-6.4
+resolver: nightly-2016-06-16

 packages:
-  - '.'
+  - location: .
+  - location:
+      git: https://github.com/ekmett/trifecta
+      commit: 53f76115ceba688fb0f5aef2fea5d085a1f813ec
+    extra-dep: true

 flags:
   idris:

[ilovezfs]

@LeifW I think Arch Linux can use this:
https://gist.githubusercontent.com/ilovezfs/2d58cce25c8382523b55f13ba379096d/raw/d1b68428ed46447978dd688f7f7335923fa4f08e/gistfile1.txt

[KaneTW]

Yeah, that should work for a bound-adjusted trifecta version.

[ilovezfs]

@KaneTW @ahmadsalim I'm rather tempted to dump Stack and do this with the Homebrew formula:

require "language/haskell"

class Idris < Formula
  include Language::Haskell::Cabal

  desc "Pure functional programming language with dependent types"
  homepage "http://www.idris-lang.org"
  url "https://github.com/idris-lang/Idris-dev/archive/v0.12.tar.gz"
  sha256 "dfc31dffd1bafd996a951cbcc551a69337f16a3fa5c2974ec872d62a38bd7c75"
  head "https://github.com/idris-lang/Idris-dev.git"

  bottle do
    sha256 "ef4de83fa2e754bc7730a6e79e4e7be548e47713790573804465ec84ef6b96de" => :el_capitan
    sha256 "233838359600772f282b90030147b6cdb78ebceb95a7c7c85e9a0b81d8413ac5" => :yosemite
    sha256 "0f949e2fd727d9c73575c6ea002048057440472fc916435ee542232461ea2485" => :mavericks
  end

  patch :DATA

  depends_on "pkg-config" => :build
  depends_on "gmp"
  depends_on "libffi"

  depends_on "ghc" => :build
  depends_on "cabal-install" => :build

  def install
    cabal_sandbox do
      system "cabal", "get", "trifecta"
      cd "trifecta-1.5.2" do
        inreplace "trifecta.cabal" do |s|
          s.gsub! "comonad              >= 4       && < 5,",
                  "comonad              >= 4       && < 6,"
          s.gsub! "transformers         >= 0.2     && < 0.5,",
                  "transformers         >= 0.2     && < 0.6,"
        end
      end
      cabal_sandbox_add_source "trifecta-1.5.2"
      args = []
      args << "-f FFI" if build.with? "libffi"
      args << "-f release" if build.stable?
      install_cabal_package *args
    end
  end

  test do
    (testpath/"hello.idr").write <<-EOS.undent
      module Main
      main : IO ()
      main = putStrLn "Hello, Homebrew!"
    EOS

    (testpath/"ffi.idr").write <<-EOS.undent
      module Main
      puts: String -> IO ()
      puts x = foreign FFI_C "puts" (String -> IO ()) x

      main : IO ()
      main = puts "Hello, interpreter!"
    EOS
    system bin/"idris", testpath/"hello.idr", "-o", testpath/"hello"
    assert_match /Hello, Homebrew!/, shell_output(testpath/"hello")

    system bin/"idris", testpath/"ffi.idr", "-o", testpath/"ffi"
    assert_match /Hello, interpreter!/, shell_output(testpath/"ffi")
  end
end

__END__
From e9d052adb828fa9dd11dd711ce9ea773f9235f94 Mon Sep 17 00:00:00 2001
From: joe <joe@iMac-TMP.local>
Date: Tue, 21 Jun 2016 09:46:58 -0700
Subject: [PATCH] ghc8

---
 idris.cabal                 |  8 ++++----
 src/Idris/Parser/Helpers.hs | 15 +++++++++++++++
 src/Pkg/PParser.hs          | 14 ++++++++++++++
 3 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/idris.cabal b/idris.cabal
index 3464817..945be8b 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -1027,7 +1027,7 @@ Library
                 , ansi-terminal < 0.7
                 , ansi-wl-pprint < 0.7
                 , base64-bytestring < 1.1
-                , binary >= 0.7 && < 0.8
+                , binary >= 0.7 && < 0.9
                 , blaze-html >= 0.6.1.3 && < 0.9
                 , blaze-markup >= 0.5.2.1 && < 0.8
                 , bytestring < 0.11
@@ -1044,12 +1044,12 @@ Library
                 , optparse-applicative >= 0.11 && < 0.13
                 , parsers >= 0.9 && < 0.13
                 , pretty < 1.2
-                , process < 1.3
+                , process < 1.5
                 , split < 0.3
                 , terminal-size < 0.4
                 , text >=1.2.1.0 && < 1.3
-                , time >= 1.4 && < 1.6
-                , transformers < 0.5
+                , time >= 1.4 && < 1.7
+                , transformers < 0.6
                 , transformers-compat >= 0.3
                 , trifecta >= 1.1 && < 1.6
                 , uniplate >=1.6 && < 1.7
diff --git a/src/Idris/Parser/Helpers.hs b/src/Idris/Parser/Helpers.hs
index 80e66cd..13a7d17 100644
--- a/src/Idris/Parser/Helpers.hs
+++ b/src/Idris/Parser/Helpers.hs
@@ -58,6 +58,21 @@ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

 deriving instance Parsing IdrisInnerParser

+#if MIN_VERSION_base(4,9,0)
+instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where
+  line = lift line
+  {-# INLINE line #-}
+  position = lift position
+  {-# INLINE position #-}
+  slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s
+  {-# INLINE slicedWith #-}
+  rend = lift rend
+  {-# INLINE rend #-}
+  restOfLine = lift restOfLine
+  {-# INLINE restOfLine #-}
+
+#endif
+
 #if MIN_VERSION_base(4,8,0)
 instance {-# OVERLAPPING #-} TokenParsing IdrisParser where
 #else
diff --git a/src/Pkg/PParser.hs b/src/Pkg/PParser.hs
index 26e60dc..f68db14 100644
--- a/src/Pkg/PParser.hs
+++ b/src/Pkg/PParser.hs
@@ -59,6 +59,20 @@ defaultPkg = PkgDesc "" Nothing Nothing Nothing Nothing
 instance HasLastTokenSpan PParser where
   getLastTokenSpan = return Nothing

+#if MIN_VERSION_base(4,9,0)
+instance {-# OVERLAPPING #-} DeltaParsing PParser where
+  line = lift line
+  {-# INLINE line #-}
+  position = lift position
+  {-# INLINE position #-}
+  slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s
+  {-# INLINE slicedWith #-}
+  rend = lift rend
+  {-# INLINE rend #-}
+  restOfLine = lift restOfLine
+  {-# INLINE restOfLine #-}
+#endif
+
 #if MIN_VERSION_base(4,8,0)
 instance {-# OVERLAPPING #-} TokenParsing PParser where
 #else
-- 
2.9.0

[KaneTW]

That should work fine.

[ilovezfs]

@KaneTW Indeed it built and the test passes:

==> Summary
🍺  /usr/local/Cellar/idris/0.12: 174 files, 205.2M, built in 10 minutes 17 seconds
iMac-TMP:~ joe$ brew test -v idris
Testing idris
==> Using the sandbox
/usr/bin/sandbox-exec -f /tmp/homebrew20160621-98843-vcbs9m.sb /System/Library/Frameworks/Ruby.framework/Versions/2.0/usr/bin/ruby -W0 -I /usr/local/Library/Homebrew -- /usr/local/Library/Homebrew/test.rb /usr/local/Library/Taps/homebrew/homebrew-core/Formula/idris.rb -v
==> /usr/local/Cellar/idris/0.12/bin/idris /tmp/idris-test-20160621-98844-15q7li1/hello.idr -o /tmp/idris-test-20160621-98844-15q7li1/hello
==> /tmp/idris-test-20160621-98844-15q7li1/hello
==> /usr/local/Cellar/idris/0.12/bin/idris /tmp/idris-test-20160621-98844-15q7li1/ffi.idr -o /tmp/idris-test-20160621-98844-15q7li1/ffi
==> /tmp/idris-test-20160621-98844-15q7li1/ffi
iMac-TMP:~ joe$ 

[ilovezfs]

That patch also applies cleanly to HEAD

==> Checking out branch master
git checkout -f master --
Already on 'master'
Your branch is up-to-date with 'origin/master'.
git reset --hard origin/master
HEAD is now at d13a720 Merge pull request #3237 from jfdm/bump-stack-resolver
==> Patching
patching file idris.cabal
patching file src/Idris/Parser/Helpers.hs
patching file src/Pkg/PParser.hs

[ilovezfs]

@KaneTW Doesn't Stack have an equivalent of cabal allow-newer?

[KaneTW]

Huh. So it does. That makes this easier.

Give me a moment.

[ilovezfs]

At least for cabal sandbox, technically there's no need to even patch trifecta surgically as above. Just need to add a "cabal.config" (and stack equivalent) at the root of the repository containing the single line

allow-newer: comonad,transformers

and the released trifecta can be used without modification. Not sure if that works for the regular runhaskell side of things too or if that needs its own version of the same?

[ilovezfs]

@ahmadsalim By the way you might also want to thank trifecta upstream for jumping on this: ekmett/trifecta#61

[KaneTW]

GHC8 travis config seems to work.

[KaneTW]

There's an issue with Travis builds and a warning:

/home/kane/Idris-dev-ghc8/src/Idris/Elab/Term.hs:2013:5: warning:
    Pattern match checker exceeded (2000000) iterations in
    an equation for ‘runTacTm’. (Use -fmax-pmcheck-iterations=n
    to set the maximun number of iterations to n)

This fails due to -Werror on Travis.

Setting iterations to 4m didn't work, and I couldn't go much higher due to memory constraints (tried 10m and it used ~8gb after a while)

[ahmadsalim]

@KaneTW Interesting, it seems to relate to the following bug: https://ghc.haskell.org/trac/ghc/ticket/11822 . Apparently the new pattern matching checker, checks more than the old one (and is slower) and due to memory consumption they had to put a limit.
I am unsure how we can get this reduced without rewriting said function (but may be that is a good idea anyway). I will take a look today and see if I can make another PR for making that function simpler.

[ahmadsalim]

@KaneTW I have opened PR #3250 to mitigate the issue, hopefully everything else runs smoothly. When the PR is merged, could you please try to see if it helps?

[ahmadsalim]

OK, PR #3250 is now merged.

[KaneTW]

Works on my machine.

[melted]

Travis jumps off the rails on GHC 7.6 and 7.8, already at cabal configure.

There's nothing obvious in the PR that could cause that.

[ahmadsalim]

@melted I have tried to restart the build, let us see if it is a Travis issue.

[ahmadsalim]

It seems like it still fails.

[ahmadsalim]

@KaneTW Sorry to bother again, would it be possible for you to add the -v3 flag to cabal configure so we can get a sense on why it fails?

Thanks for the patience

[ahmadsalim]

I meant in the travis.yml file under script

[ilovezfs]

@ahmadsalim stupid question: have you checked if this affects master too?

[ahmadsalim]

@ilovezfs As far as I can see from my PR from yesterday, it does not.

[melted]

The builds on master looks good

I have built this branch locally with 7.8 and an old cabal so it likely isn't anything to do with the new dependency versions and old compilers.

[melted]

I have cloned this branch, activated travis on my idris-dev and pushed one with more logging to github.

[melted]

Found it, it's the new process bound that causes it.

[melted]

I'm going to merge this, failures and all, and put in my fix in a separate PR.

[ilovezfs]

@KaneTW @ahmadsalim @melted awesome work guys! 💯

[ilovezfs]

@ahmadsalim @edwinb any outstanding blockers for a new tag? 😇

[ahmadsalim]

@ilovezfs As far as I understand the release will come very soon 😄

[ilovezfs]

@ahmadsalim @edwinb any update on when the new release might be out?

ilovezfs does his annoying child "Are we there yet?" thing again

[ahmadsalim]

@ilovezfs Unfortunately, it is beyond my control so I can't say when.

[jfdm]

Just to reiterate the comments of @ahmadsalim

@edwinb is responsible for cutting a release as they are currently tied in with development of the book.

[ilovezfs]

@ahmadsalim @edwinb @jfdm FYI: Homebrew/homebrew-core#3334

Thanks for the new release!