[Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2
Sergei Meshveliani
mechvel at botik.ru
Thu Apr 14 13:38:49 CEST 2016
I have the following questions/notes.
1. I have tested it on DoCon-A. It looks all right.
2. In Standard library, I do not find the installation instruction
(I tried `cabal install', and this has occurred lucky).
3. I try
agda -c $agdaLibOpt +RTS -M9G -RTS Foo.agda
./Foo +RTS -M2G -RTS
, and it reports "link with the -rtsopts".
I try to insert -rtsopts to various places in the line of
agda -c $agdaLibOpt +RTS -M9G -RTS
, and Agda does not accept it.
Please, how precisely needs one to use -rtsopts ?
Thanks,
------
Sergei
On Wed, 2016-04-13 at 10:34 -0500, Andrés Sicard-Ramírez wrote:
> Dear all,
>
> The Agda Team is very pleased to announce the second release candidate
> (RC 2) of Agda 2.5.1 available at
>
> http://www1.eafit.edu.co/asr/tmp/Agda-2.5.0.20160412.tar.gz
>
>
> GHC supported versions
> ======================
>
> The RC 2 has been tested with GHC 7.6.3, 7.8.4 and 7.10.3.
>
>
> Installation
> ============
>
> The RC 2 can be installed using the following instructions:
>
> $ tar xzf Agda-2.5.0.20160214.tar.gz
> $ cd Agda-2.5.0.20160214.tar.gz
> $ cabal install
>
>
> Standard library
> ================
>
> The version of the standard library compatible with the RC 2 is
> available at
>
> https://github.com/agda/agda-stdlib/releases/tag/2.5.0.20160412
>
>
> What is new?
> ============
>
> The RC 2 includes various new features and changes:
>
> * Allow version suffix on libraries file. [Issue 1693]
>
> * Emacs mode. Module contents (C-c C-o) now also works for
> records. [Issue 1926]
>
> * New pragma HASKELL for adding inline Haskell code (GHC backend only)
>
> More information about the changes included in the RC 2 can be found
> in
>
> https://raw.githubusercontent.com/agda/agda/2.5.0.20160412/CHANGELOG
>
>
> Incompatibilities
> =================
>
> The RC 2 is not full compatible with the Agda 2.5.1 RC 1 nor Agda
> 2.4.2.5. The main incompatibilities are:
>
> * Builtins and primitives are now defined in a new set of modules
> available to all users, independent of any particular library. The
> standard library reexports the primitives from the new modules.
>
> The Agda.Builtin modules are installed in the same way as Agda.Primitive,
> but unlike Agda.Primitive they are not loaded automatically.
>
> * The aggressive behaviour of `with` introduced in 2.4.2.5 has been
> rolled back [Issue 1692]. With no longer abstracts in the types of
> variables appearing in the with-expressions. [Issue 745]
>
> * Record modules now properly hide all their parameters. [Issue 1759]
>
> * Removed --no-coverage-check option. [Issue 1918]
>
> More information about the incompatibilities included in the RC 2 can
> be found in the above CHANGELOG.
>
>
> Fixed issues after Agda 2.5.1 RC 1
> ==================================
>
> Approximately 40 bugs/regressions were fixed, some of them
> long-standing ones:
>
> * https://github.com/agda/agda/issues/140
>
> * https://github.com/agda/agda/issues/610
>
> * https://github.com/agda/agda/issues/745
>
> * https://github.com/agda/agda/issues/994
>
>
> Know regressions
> ================
>
> * https://github.com/agda/agda/issues/1775
>
> * https://github.com/agda/agda/issues/1821
>
>
> Enjoy Agda 2.5.1 release candidate 2 and please test as much as
> possible.
>
>
More information about the Agda
mailing list