[Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1

[Matthew Daggitt]

Hi Sergei,


> Can you, please, explain: what is the difference between writing

...

open import Relation.Binary.PropositionalEquality using (foo)
> ...
> and

...

open import Relation.Binary.PropositionalEquality.Core using (foo)
> ...
>

The former will have dependencies on all the imports listed at the top of
`Relation.Binary.PropositionalEquality(.Algebra/Properties)` which includes
the entire `Algebra` and `Relation.Binary` hierarchies. This can make it
time consuming to load the module and increase the memory overhead.

The CHANGELOG wording perhaps needs updating for the full release, as
users should
not import `Core` modules directly
<https://github.com/agda/agda-stdlib/blob/1309c75160e3125e1ce35b0b3db748821c75e22a/README.agda#L247>,
and as we don't provide guarantees about their content.

Best,
Matthew

On Tue, Sep 1, 2020 at 3:27 AM <mechvel at scico.botik.ru> wrote:

> On 2020-08-31 16:32, Matthew Daggitt wrote:
> > Dear all,
> >
> > The Agda Team is pleased to announce the first release candidate of
> > version 1.4 of the standard library.
> > [..]
>
> It is written there in CHANGELOG.md
> "
>   The module `Relation.Binary.PropositionalEquality` has been growing in
> size and
>   now depends on a lot of other parts of the library, even though its
> basic
>   functionality does not. To fix this some of its parts have been
> factored out.
>    `Relation.Binary.PropositionalEquality.Core` already existed. Added
> are:
>    ```agda
>    Relation.Binary.PropositionalEquality.Properties
>    Relation.Binary.PropositionalEquality.Algebra
>    ```
> These new modules are re-exported by
> `Relation.Binary.PropositionalEquality`
> and so these changes should be invisble to current users, but can be
> useful
> to authors of large libraries.
> "
>
> Can you, please, explain: what is the difference between writing
> module Foo where
> open import Relation.Binary.PropositionalEquality using (foo)
> ...
> and
> module Foo Where
> open import Relation.Binary.PropositionalEquality.Core using (foo)
> ...
> (assuming that foo is in ...Core)
> ?
> Is the latter better for the authors of large libraries? Why?
> Do you mean that fewer modules of standard library will be type-checked?
> (because if PropositionalEquality is type-checked, then Agda needs to
> type-check
> at list once all the modules it imports).
> Does this make a difference to  Foo.agdai ?  its size?
>
> Thanks,
>
> ------
> Sergei
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200901/d9c057a0/attachment.html>