[Agda] installing/using 2.6.0-207bde6

[Sergei Meshveliani]

On Tue, 2017-08-15 at 13:20 +0200, G. Allais wrote:
> Hi Sergey,
> 
> The problem does not lie with Ulf's Prelude or Agda's standard
> library but rather with Agda itself. You need to upgrade to
> (at least) the commit Ulf is pointing at.

I understood this from Ulf's reply. Thank you, and Ulf.

I have installed the current Development Agda (2.6.0-c9e11c1).
And it dos not type-check a certain module which is type-checked by 
Agda of April 13, 2017.
Now I am reducing the example, it may occur a bug. 



> Alternatively you could wait a bit and port your library to the
> next stable version which is about to be released. The installation
> instructions for your users will then be a lot simpler (basically:
> cabal install Agda-2.5.3).

I need to submit a certain paper before August 20, and it is desirable
to set there a reference to an working program.
The paper is so, that it is much better to refer to an working program.

I think of doing so:
to release DoCon-A-2.00 for this purpose, so far,
and then, to release DoCon-A-2.01 after the stable Agda appears. 

If I am not in time with 2.00, then I would refer to the program as
somewhat 
"to hopefully appear at this <address> within several days".

The subtle point is that it _did work_ under Agda of April 13, 2017,
but I cannot instruct in  install.txt  of how the used can reproduce
my situation in which it worked. This was a surprise for me. 

Regards,

------
Sergei




> Cheers,
> --
> gallais
> 
> On 14/08/17 17:32, Sergei Meshveliani wrote:
> > On Mon, 2017-08-14 at 16:41 +0200, Ulf Norell wrote:
> >>
> >>
> >> On Mon, Aug 14, 2017 at 2:46 PM, Sergei Meshveliani <mechvel at botik.ru>
> >> wrote:
> >>         
> >>            and added there import of `compare' and DivMod of Agda
> >>         Prelude.
> >>         
> >>         This caused the necessity to add
> >>              import Prelude.String
> >>              import Prelude.Nat
> >>         
> >>         to many files in the application.
> >>
> >>
> >> This problem was fixed in issue #2641 [1] (commit 64cc2b3). You should
> >> no longer need the imports of the Prelude modules.
> >>
> >>
> >> / Ulf
> >>
> >>
> >> [1] https://github.com/agda/agda/issues/2641 
> > 
> > 
> > My  install.txt  needs to explain plainly:  
> > where to take this needed (improved) Agda Prelude version 
> > (for Agda 2.6.0-207bde6).
> > 
> > Is it by 
> >       git clone https://github.com/UlfNorell/agda-prelude
> > ?
> > 
> > Thanks,
> > 
> > ------
> > Sergei
> > 
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> > 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda