[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Sergei Meshveliani]

I am sorry, please, withdraw this report.

When porting to Standard library, I have confused the parametric module
import. It needs to be 

  open Sublist-Setoid A' using () renaming (_⊆_ to _⊆'_) 

instead of 
  open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_) 

------
Sergei



On Fri, 2018-05-25 at 15:37 +0300, Sergei Meshveliani wrote:
> On Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:
> > Dear all,
> > 
> > The Agda Team is very pleased to announce the first release candidate
> > of Agda 2.5.4. We plan to release 2.5.4 in one week.
> > 
> > [..]
> > 
> > Enjoy the RC and please test as much as possible.
> 
> 
> Please, consider a small code attached.
> This is a lemma about mapping the _⊆_ relation for lists over setoids:
> 
>   map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
>                                          (map f) Preserves _⊆_ ⟶ _⊆'_
>  
> In DoCon-A-2.02  (see there List.L0.agda)  a similar code works under
> Agda-2.5.3.
> 
> To port to Agda 2.5.3.20180519, I change the import for the experimental
> Standard library: 
> 
>  import Data.List.Membership.Setoid as Membership
>  import Data.List.Relation.Sublist.Setoid as Sublist-Setoid
>  import Data.List.Relation.Sublist.Propositional as Sublist-≡
> 
> And change the local import in  module CongMap0  to
> 
>   open Membership A       using (_∈_)
>   open Sublist-Setoid A   using (_⊆_)
>   open Membership A'      using () renaming (_∈_ to _∈'_)
>   open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_)   -- * 
> 
> 
> Now, everything is type-checked there -- except this last function
> 
>   map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
>                                            (map f) Preserves _⊆_ ⟶ _⊆'_
>   map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
>        let
>          (x , x∈≡xs , fx≈z) = counter-map {A = C} {sd = A'} f z∈f-xs
>          x∈xs    = ∈≡→∈ x∈≡xs
>          x∈ys    = xs⊆ys x∈xs
>          fx∈f-ys = map∈ f fCong x∈ys
>        in
>        cong₁∈' fx≈z fx∈f-ys
> 
> The report is
>   β != β= of type Level
>   when checking that the expression z∈f-xs has type
>   _y_249 A A' f fCong xs⊆ys z∈f-xs ∈'
>   map f (_xs_248 A A' f fCong xs⊆ys z∈f-xs)
> 
> I wonder whether
> * this is a bug in the candidate Agda
> * or an error in  List.L0.agda  (missed by Agda 2.5.3)
> * or a wrong port.
> 
> Can you, please, help?
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda