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

[mechvel at scico.botik.ru]

On 2020-09-01 14:15, Matthew Daggitt wrote:
> [..]
>> Can you, please, explain: what is the difference between writing
>> ...
>> open import Relation.Binary.PropositionalEquality using (foo)
>> ...

Call it  Foo-I.agda.

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

Call it  Foo-II.agda.


> 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.


Sorry, I need to understand certain details about Agda.
Suppose that we do

   > agda $agdaLibOpt Foo-I.agda                 -- call it  TCommand

(1) Does "to load" mean to type-check?
     Or may be it means to take some ready  .agdai  modules into memory?

(2) What precisely makes TCommand more time consuming than for Foo-II ?
     Is it type-checking an additional large part of the standard 
library?
     (call it  LargeLibPart).

But this is only for the first call of TCommand.
When developing a project, after some implementation is edited in Foo-I,
the next TCommang for Foo-I.agda will not require type-checking 
LargeLibPart.
Right?
On the other hand, it needs for find where  foo  is defined. To do this, 
it takes
many ready .agdai  modules into memory and searches there for  foo,  and 
finds
its declaration in  ..Core.
Right?
So that it occurs that a large  memory and time  is still spent to get  
.agdai
of LargeLibPart into memory and to search in them.
Am I missing something?


> The CHANGELOG wording perhaps needs updating for the full release, as
> users should not import `Core` modules directly [1], and as we don't
> provide guarantees about their content.

I am totally confused.
You write that Foo-I (that imports `Core' in-directly is expensive to 
type-check,
because it
"will have dependencies on all the imports listed at the top
of `Relation.Binary.PropositionalEquality(.Algebra/Properties)` ...
".

The only way to avoid this is to import  foo  directly from `Core'.
Right?
And then, you write "users should not import `Core` modules directly 
[1]".

So, how does one import the above  foo ?

Regards,

--
SM



> 
> 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
> 
> 
> Links:
> ------
> [1]
> https://github.com/agda/agda-stdlib/blob/1309c75160e3125e1ce35b0b3db748821c75e22a/README.agda#L247
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda