[Agda] lib for Development Agda

Discussion:

Sergei Meshveliani

2018-11-06 11:56:34 UTC

Dear Agda team,

Is is true that Development Agda of November 6 2018
(2.6.0-e7da0ce)
uses Standard library lib-0.17 ?

I try to upgrade the application from Development Agda of September 7 to
Development of November 6,
and it reports
Failed to find source of module
Data.List.Relation.Sublist.Extensional.Setoid in any of the
following locations:
...

It is desirable to understand what is the intended library for the
official Agda version to which Development Agda approaches.

Regards,

------
Sergei

Matthew Daggitt

2018-11-06 13:07:14 UTC

Permalink

Hi Sergei,
The development version of Agda will always use *at least* the most
recently released version of the standard library (i.e. v0.17). Sometimes,
when some language feature has changed, it may even use the development
version of the standard library.
Best,
Matthew

Post by Sergei Meshveliani
Dear Agda team,
Is is true that Development Agda of November 6 2018
(2.6.0-e7da0ce)
uses Standard library lib-0.17 ?
I try to upgrade the application from Development Agda of September 7 to
Development of November 6,
and it reports
Failed to find source of module
Data.List.Relation.Sublist.Extensional.Setoid in any of the
...
It is desirable to understand what is the intended library for the
official Agda version to which Development Agda approaches.
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Guillaume Allais

2018-11-06 17:46:37 UTC

Permalink

Hi Sergei,

`Data.List.Relation.Sublist.Extensional.Setoid` has been moved
to `Data.List.Relation.Subset.Setoid` because it was not define
a sublist relation but rather a subset one.

All of the breaking and non-breaking changes are documented in
the CHANGELOG for the standard library to make migration as
smooth as possible:
https://github.com/agda/agda-stdlib/blob/master/CHANGELOG/v0.17.md

Best,
--
gallais