agda 2.5.1 #440

mietek · 2016-04-19T00:17:14Z

Updates Agda to 2.5.1 and the Agda standard library to 0.12.
Removes temporary maintenance patches.
Renames the without-malonzo option to without-ghc, following upstream change:
Replace 'MAlonzo' by 'GHC backend' in the --help option agda/agda#1859
Removes functionality relating to the removed FFI package:
agda/agda-stdlib@86b4fe4
Updates caveats for clarification following recent changes:
https://github.com/agda/agda/blob/master/CHANGELOG#L52-121
Updates and improves tests to test one feature at a time.

ilovezfs · 2016-04-19T06:19:02Z

Simplifies tests to avoid experimental features and better reflect
common usage.

Does that mean the old test is failing?

MikeMcQuaid · 2016-04-19T08:18:41Z

Formula/agda.rb

@@ -43,9 +32,9 @@ class Agda < Formula
  end

  option "without-stdlib", "Don't install the Agda standard library"
-  option "without-malonzo", "Disable the MAlonzo backend"
+  option "without-ghc", "Disable the GHC backend"


Need to add a deprecated_option to migrate people over.

mietek · 2016-04-19T10:01:05Z

@ilovezfs: Using -c generates Haskell code with import qualified Data.Text. Compiling this code requires having the text package installed and registered with GHC. We could create a Cabal sandbox as part of the test… I’ll try that.

mietek · 2016-04-19T10:37:11Z

Why would build.with? "ghc" be false if the package has been installed with the default options?

  option "without-ghc", "Disable the GHC backend"

  if build.with? "ghc"
    depends_on "ghc"
  else
    depends_on "ghc" => :build
  end

mietek · 2016-04-19T11:02:44Z

My /usr/local/Library/LinkedKegs/agda/INSTALL_RECEIPT.json contains the following:

{
  "used_options": [],
  "unused_options": ["--without-stdlib", "--without-malonzo", "--without-emacs"],
  "built_as_bottle": false,
  "poured_from_bottle": false,
  "time": 1461020063,
  "source_modified_time": 1460785695,
  "HEAD": "da34fba151ee33c1a2e14ab21ee0dc4ea451cc0f",
  "stdlib": null,
  "compiler": "clang",
  "source": {
    "path": "/usr/local/Library/Taps/homebrew/homebrew-core/Formula/agda.rb",
    "tap": "homebrew/core",
    "spec": "stable”
  }
}

I’m not sure why --without-malonzo is still there, as I’ve installed the package after having changed the option name in the formula.

MikeMcQuaid · 2016-04-19T11:23:38Z

@mietek Did you add deprecated_option?

mietek · 2016-04-19T11:53:36Z

@MikeMcQuaid: I have now.

mietek · 2016-04-19T12:00:53Z

@ilovezfs: I’ve rewritten the tests so that one feature is tested at a time.

We now test that:

typechecking a simple module works (SimpleTest);
typechecking a module that uses the standard library works, when the standard library is installed (StdlibTest);
compiling a simple module using the JavaScript backend works (SimpleTest);
compiling and running a simple program using the GHC backend works, when the GHC backend is enabled (IOTest);
compiling and running a program that uses the standard library using the GHC backend works, when the standard library is installed and the GHC backend is enabled (StdlibIOTest).

Both GHC backend tests run in a single Cabal sandbox that includes the text package.

mietek · 2016-04-19T14:41:06Z

The failure seems unrelated:

...
==> cabal sandbox init
Failed to execute: cabal
Error: agda: failed
Failed executing: cabal sandbox init
/usr/local/Library/Homebrew/formula.rb:1492:in `system'
/usr/local/Library/Homebrew/formula.rb:1429:in `open'
/usr/local/Library/Homebrew/formula.rb:1429:in `system'
/usr/local/Library/Homebrew/language/haskell.rb:19:in `cabal_sandbox'
/usr/local/Library/Taps/homebrew/homebrew-core/Formula/agda.rb:173:in `test'
/usr/local/Library/Homebrew/formula.rb:1334:in `run_test'
/usr/local/Library/Homebrew/extend/fileutils.rb:14:in `mktemp'
/usr/local/Library/Homebrew/extend/fileutils.rb:75:in `run'
/usr/local/Library/Homebrew/extend/fileutils.rb:75:in `chdir'
/usr/local/Library/Homebrew/extend/fileutils.rb:75:in `run'
/usr/local/Library/Homebrew/extend/fileutils.rb:13:in `mktemp'
/usr/local/Library/Homebrew/formula.rb:1328:in `run_test'
/usr/local/Library/Homebrew/test.rb:28
/Users/brewadmin/Homebrew/Cellar/ruby187/1.8.7-p374_1/lib/ruby/1.8/timeout.rb:67:in `timeout'
/usr/local/Library/Homebrew/test.rb:27

ilovezfs · 2016-04-19T17:27:50Z

Formula/agda.rb


-  if build.with? "malonzo"
+  if build.with? "ghc"


option "without-ghc", "Disable the GHC backend" if build.with? "ghc" depends_on "ghc" else depends_on "ghc" => :build end

I think can instead be

depends_on "ghc" => :recommended depends_on "ghc" => :build if build.without? "ghc"

which automatically gives you

--without-ghc Build without ghc support

If the other message is preferred for some reason, you can make it

option "without-ghc", "Disable the GHC backend" depends_on "ghc" => :recommended depends_on "ghc" => :build if build.without? "ghc"

It's 2 lines (or 3 if you don't like the default message) instead of 6.

Using :optional / :recommended is preferred and more idiomatic if the option name is also the name of the underlying formula. It used to be without-malonzo and malonzo isn't a formula. Since it's now ghc, the situation is different because ghc is a formula.

ilovezfs · 2016-04-19T17:35:38Z

@mietek That's probably because your cabal_install dependency is build-time only.

mietek · 2016-04-19T17:52:21Z

@ilovezfs: Oh, you’re right. Any ideas how to make cabal-install a build-time and test-time dependency? If this is not possible, we should just get rid of the two GHC backend tests.

ilovezfs · 2016-04-19T17:58:05Z

@mietek This is probably a stupid question, but why is the option not to have the ghc backend useful other than that the without-malonzo was a pre-existing option?

mietek · 2016-04-19T17:59:30Z

@ilovezfs: The only effect of the without-ghc option is that GHC is not pulled in as a run-time dependency, saving <1GB disk space.

ilovezfs · 2016-04-19T18:06:30Z

There's no distinction at this time between a test time and run time dependency. One option might be to drag in cabal-install unless it's a non-default --without ghc build.

ilovezfs · 2016-04-19T18:09:13Z

I can see that's probably a bad idea though since

Josephs-MacBook-Pro:Formula joe$ ag 'depends_on "cabal-install' | wc -l
      21
Josephs-MacBook-Pro:Formula joe$ ag 'depends_on "cabal-install' | grep -v build | wc -l
       0

mietek · 2016-04-19T18:14:18Z

One option might be to drag in "cabal-install" unless it's a non-default --without ghc build.

You’re right. Firstly, pulling in cabal-install is low-cost, as the package takes <20MB on disk. Secondly, almost anyone who wants to use GHC will want to use cabal-install, as well. Finally, anyone who wants to use the GHC backend for Agda will have to install the text package using cabal-install.

ilovezfs · 2016-04-19T18:18:51Z

I have no objection to dragging in cabal-install unless it's --without-ghc, but it's somewhat unorthodox so others may disagree. @zmwangx Thoughts?

zmwangx · 2016-04-19T18:48:25Z

Using -c generates Haskell code with import qualified Data.Text

If I'm interpreting this correctly, the GHC backend is basically unusable without text (not only for testing, but also at runtime), right? Then cabal-install should definitely be considered a dependency, because I'll assume that no one would want to manually install text and its dependencies.

Moreover, I concur with @mietek: adding the relatively lightweight cabal-install to the GHC monstrosity doesn't hurt. Cabal comes with GHC anyway, so cabal-install is pretty much a given.

ilovezfs · 2016-04-19T18:56:05Z

@zmwangx

to the GHC monstrosity

LOL.

So I think we can do

depends_on "ghc" => :recommended
if build.with? "ghc"
  depends_on "cabal-install"
else
  depends_on "ghc" => :build
  depends_on "cabal-install" => :build
end

mietek · 2016-04-20T02:41:57Z

To confirm — you are requesting that I change this:

if build.with? "ghc"
  depends_on "ghc"
  depends_on "cabal-install"
else
  depends_on "ghc" => :build
  depends_on "cabal-install" => :build
end

…to this:

depends_on "ghc" => :recommended
if build.with? "ghc"
  depends_on "cabal-install"
else
  depends_on "ghc" => :build
  depends_on "cabal-install" => :build
end

I don’t think this is an improvement, but — here goes.

zmwangx · 2016-04-20T02:47:53Z

I believe your latest commit correctly implemented the suggestion.

MikeMcQuaid · 2016-04-20T06:58:56Z

Any ideas how to make cabal-install a build-time and test-time dependency? If this is not possible, we should just get rid of the two GHC backend tests.

This is not possible. I personally think it's worth just avoiding using build dependencies at test time.

mietek · 2016-04-20T13:34:05Z

This is ready to merge.

ilovezfs · 2016-04-20T16:27:45Z

@mietek It seems that this doesn't build with ghc 8.0.1-rc3 unless I pass --without-emacs, so I'm wondering if we should either fix that now or make emacs optional instead of recommended since the ghc 8 release is imminent and we don't want this being broken at that point.

==> /usr/local/Cellar/agda/2.5.1/bin/agda-mode compile
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Symbol's function definition is void: byte-compile-disable-warning
Unable to compile the following Emacs Lisp files:
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/agda2-abbrevs.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/annotation.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/agda2-queue.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/eri.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/agda2.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/agda-input.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/agda2-highlight.el
  /usr/local/Cellar/agda/2.5.1/share/x86_64-osx-ghc-8.0.0.20160411/Agda-2.5.1/emacs-mode/agda2-mode.el
/usr/local/Library/Homebrew/debrew.rb:11:in `raise'
BuildError: Failed executing: /usr/local/Cellar/agda/2.5.1/bin/agda-mode compile

If you'd like to try it, here's the diff to get brew building ghc 8:
https://gist.github.com/ilovezfs/c4bc508827fc407957bd77e7f6e0d9a3

mietek · 2016-04-20T16:55:03Z

@ilovezfs: I don’t think Agda is currently expected to support GHC 8 (agda/agda#1799). The Agda Implementors’ Meeting XXIII is underway, so we can expect fixes shortly. I’d rather not delay this update.

ilovezfs · 2016-04-20T16:58:18Z

@mietek Thank you for reporting that so quickly, and in the right place. I'm 👍 merging this as is since we can always change it to optional later if necessary when ghc 8 ships.

zmwangx · 2016-04-20T17:04:43Z

Hmm that's weird, looking at the source code of agda-mode I don't see what could be broken by GHC 8, and byte-compile-disable-warning from bytecompile.el should be available (and definitely doesn't depend on GHC 8).

ilovezfs · 2016-04-21T07:02:58Z

@zmwangx Did you try it? I found it to be reproducible with 8.0.1-rc3 and not to occur with ghc-7.10.3b.

zmwangx · 2016-04-21T07:07:00Z

Did you try it?

Not I didn't, because I never enjoyed building GHC...

MikeMcQuaid · 2016-04-21T08:00:16Z

Formula/agda.rb

-      if build.with? "malonzo"
-        s += <<-EOS.undent
+      Agda 2.5.1 includes new library management features.
+      http://agda.readthedocs.org/en/stable/tools/package-system.html


Would still like this bit removed.

Disappointing.

Sorry, I thought I'd said that already and I've already explained that caveats are for Homebrew-specific information.

* Updates Agda to 2.5.1 and the Agda standard library to 0.12. * Removes temporary maintenance patches. * Renames the "without-malonzo" option to "without-ghc", following upstream change: agda/agda#1859 * Removes functionality relating to the removed FFI package: agda/agda-stdlib@86b4fe4 * Updates caveats for clarification following recent changes: https://github.com/agda/agda/blob/master/CHANGELOG#L52-121 * Updates and improves tests to test one feature at a time.

MikeMcQuaid · 2016-04-21T09:22:00Z

Thanks again @mietek and for your patience.

mietek force-pushed the agda-2.5.1 branch from cc5de17 to 553bb37 Compare April 19, 2016 00:34

MikeMcQuaid reviewed Apr 19, 2016
View reviewed changes

mietek force-pushed the agda-2.5.1 branch from 553bb37 to c3b31ce Compare April 19, 2016 11:40

mietek force-pushed the agda-2.5.1 branch from c3b31ce to 9e78a10 Compare April 19, 2016 12:07

mietek force-pushed the agda-2.5.1 branch from 9e78a10 to 77d06af Compare April 19, 2016 14:50

ilovezfs reviewed Apr 19, 2016
View reviewed changes

mietek force-pushed the agda-2.5.1 branch from 77d06af to 1f9ef58 Compare April 19, 2016 18:15

apjanke added the needs response Needs a response from the issue/PR author label Apr 20, 2016

ghost removed the needs response Needs a response from the issue/PR author label Apr 20, 2016

mietek force-pushed the agda-2.5.1 branch from 1f9ef58 to 81debdc Compare April 20, 2016 02:42

mietek mentioned this pull request Apr 20, 2016

Preparation for supporting GHC 8.0.1 agda/agda#1799

Closed

MikeMcQuaid reviewed Apr 21, 2016
View reviewed changes

mietek force-pushed the agda-2.5.1 branch from 81debdc to 36628f7 Compare April 21, 2016 08:08

MikeMcQuaid closed this in 366b932 Apr 21, 2016

asr mentioned this pull request Apr 21, 2016

agda-mode: Symbol's function definition is void: byte-compile-disable-warning agda/agda#1945

Closed

mietek mentioned this pull request Jun 21, 2016

Add installation instructions for OS X agda/agda#2060

Closed

Homebrew locked and limited conversation to collaborators May 4, 2018

agda 2.5.1 #440

agda 2.5.1 #440

Conversation

mietek commented Apr 19, 2016 • edited Loading

ilovezfs commented Apr 19, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mietek commented Apr 19, 2016

mietek commented Apr 19, 2016 • edited Loading

mietek commented Apr 19, 2016 • edited Loading

MikeMcQuaid commented Apr 19, 2016

mietek commented Apr 19, 2016 • edited Loading

mietek commented Apr 19, 2016 • edited Loading

mietek commented Apr 19, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ilovezfs commented Apr 19, 2016

mietek commented Apr 19, 2016 • edited Loading

ilovezfs commented Apr 19, 2016

mietek commented Apr 19, 2016

ilovezfs commented Apr 19, 2016 • edited Loading

ilovezfs commented Apr 19, 2016 • edited Loading

mietek commented Apr 19, 2016

ilovezfs commented Apr 19, 2016

zmwangx commented Apr 19, 2016

ilovezfs commented Apr 19, 2016

mietek commented Apr 20, 2016

zmwangx commented Apr 20, 2016

MikeMcQuaid commented Apr 20, 2016

mietek commented Apr 20, 2016

ilovezfs commented Apr 20, 2016

mietek commented Apr 20, 2016

ilovezfs commented Apr 20, 2016

zmwangx commented Apr 20, 2016

ilovezfs commented Apr 21, 2016

zmwangx commented Apr 21, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikeMcQuaid commented Apr 21, 2016

mietek commented Apr 19, 2016 •

edited

Loading

mietek commented Apr 19, 2016 •

edited

Loading

mietek commented Apr 19, 2016 •

edited

Loading

mietek commented Apr 19, 2016 •

edited

Loading

mietek commented Apr 19, 2016 •

edited

Loading

mietek commented Apr 19, 2016 •

edited

Loading

ilovezfs commented Apr 19, 2016 •

edited

Loading

ilovezfs commented Apr 19, 2016 •

edited

Loading