[Agda] installing/using 2.6.0-207bde6

[Sergei Meshveliani]

Dear Agda developers,

please, help me with installing/using Agda 2.6.0-207bde6.

The story is as follows.

1. I used the Development Agda of April 2017, which says that it is
2.6.0-207bde6.
And it worked with the Development Standard library downloaded in the
same day as the above Agda.
And my DoCon-A library worked there.

2. Then I added some functions, it has become DoCon-A-2.00-pre 
   (a candidate),
   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.
Anyway it worked.

3. Now I try to release DoCon-A-2.00.

I write in  install.txt 


Installation for  Agda 2.6.0-207bde6, MAlonzo, Linux
====================================================

1. Download this Agda version by running the commands

  > git clone https://github.com/agda/agda.git
  > cd agda
  > git checkout 207bde6

Install Agda following its instruction README.md.

2. Download and install the corresponding Standard library version
   by running the commands
  > cd agda
  > git submodule init

  Submodule 'std-lib' (https://github.com/agda/agda-stdlib)
  registered for path ...

  > git submodule update
  Cloning into std-lib...
  ...
  Submodule path 'std-lib': checked out ...

3. Download and install Agda Prelude
   (non-standard, 2-3 items used from it).

4. Then, installing DoCon-A is by
...
...
* Command
  > cd docon-A/source
  > agda -c $agdaLibOpt +RTS -K90m -M7300m -RTS $agdaGHC_opt 
                                        TypeCheckAll.agda
================================================================

Now I follow this instructions (install Agda and Standard library by
new). 
And give an easier command of

    agda $agdaLibOpt +RTS -K90m -M7G -RTS Structures2.agda

(type check a certain module in a certain initial part of application).
And it fails with

/home/mechvel/agda/agda/std-lib/src/Data/Integer/Addition/Properties.agda:30,29-30
No instance of type .Agda.Builtin.FromNat.Number Data.Nat.Base.ℕ
was found in scope.
when checking that 0 is a valid argument to a function of type
({a : .Agda.Primitive.Level} {A : Set a}
 {{r : .Agda.Builtin.FromNat.Number A}} (n : Data.Nat.Base.ℕ)
 {{_ : .Agda.Builtin.FromNat.Number.Constraint r n}} → A)
     
Probably this means that "import Prelude.Nat" 
needs to be added to the corresponding module.
But this time the corresponding module is not in the application, but it
is in the source of Standard library
(?) 

Please, what may this mean? 
How does this occur that the application worked earlier, and now does
not?
How to fix?

DoCon-A-2.00-pre  is on 

http://www.botik.ru/pub/local/Mechveliani/docon-A/2.00-pre/

The Agda version is of development, and Agda Prelude is used. 
This makes the installation instruction so complex, that I fail to make
it work for myself.
Can you look into this  install.txt  and try to install, and advise?

Thanks,

------
Sergei