[Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate

Andreas Abel abela at chalmers.se
Mon Dec 6 20:55:38 CET 2021


You could try to limit to one CPU, to see the progress of compilation:

   $ cabal install -foptimise-heavily -j1

On 2021-12-06 20:53, Andreas Abel wrote:
> Compilation with -foptimize-heavily is slow and requires quite a bit of 
> RAM...
> 
> On 2021-12-06 20:52, mechvel at scico.botik.ru wrote:
>> On 2021-11-30 00:43, Andreas Abel wrote:
>>> The Agda Team is pleased to announce a release candidate for Agda 
>>> 2.6.2.1:
>>>
>>>     https://hackage.haskell.org/package/Agda-2.6.2.0.20211129/candidate
>>>
>>> 2.6.2.1 will be mostly a bugfix release, and will build in the latest
>>> Haskell ecosystem (GHC 9.2.1, aeson-2.0, hashable-1.4,
>>> hashtables-1.3).
>>> For detailed comparison with 2.6.2, consult the changelog published
>>> with the candidate above.
>>>
>>> Instructions how to test the candidate are available at:
>>>
>>>     https://github.com/agda/agda/pull/5678
>>>
>>> Please report any regressions over 2.6.2 at the Agda issue tracker.
>>> We plan to release Agda 2.6.2.1 next week, should not release-stopping
>>> regressions be reported.
>>>
>>
>>
>> I recall somebody wrote that
>>    $ cabal install -foptimise-heavily Agda
>>
>> produces a more efficient type checker (compiler?).
>>
>> I do now
>>
>>   $ cd 2.6.2.0.20211129
>> (where Agda.cabal resides) and run
>>
>>   $ cabal install -foptimise-heavily Agda
>>
>> It reports
>>
>> --------------------------------------
>> Wrote tarball sdist to
>> /home/mechvel/agda/2.6.2.0.20211129/dist-newstyle/sdist/Agda-2.6.2.0.20211129.tar.gz 
>>
>> Resolving dependencies...
>> Build profile: -w ghc-9.2.1 -O1
>> In order, the following will be built (use -v for more details):
>>   - Agda-2.6.2.0.20211129 (exe:agda, exe:agda-mode) (requires build)
>> Starting     Agda-2.6.2.0.20211129 (all, legacy fallback)
>> Building     Agda-2.6.2.0.20211129 (all, legacy fallback)
>> ---------------------------------------
>>
>> and hangs silently for 30 minutes already,  ghc  is detected as working.
>> Is this all right?
>>
>> ------
>> Sergei
>>
>>
> 

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/


More information about the Agda mailing list