[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