[Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1

[Sergei Meshveliani]

On Fri, 2019-03-15 at 12:41 +0000, Andres Sicard Ramirez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the first release candidate
> of Agda 2.6.0.
> [..]


I observe a certain effect related to folders and `-c' option (MAlonzo).

Consider the two modules: M1.agda residing in the $root, 
M2.agda residing in  $root/Foo/ : 

M1.agda 
Foo/M2.agda

-------------------- M2.agda ----------
-- module Foo.M2 where

open import M1

main : ...
main = ...
---------------------------------------


Case the header  "module Foo.M2 where"  is skipped
--------------------------------------------------
  If M2 is type-checked by 
                        > cd Foo
                        > emacs M2.agda 
                        > C-c C-l
  then M1 is not found.

  If M2 is `made' by
             > cd Foo
             > agda -c $libOptions M2.agda
  then
    M1 is found, and the executable is  Foo/M2


Case the header  "module Foo.M2 where"  is set
----------------------------------------------
Here
                > cd Foo
                > emacs M2.agda 
                > C-c C-l
type-checks it,
and
         > cd Foo
         > agda -c $libOptions M2.agda
  
puts executable to  root/M2

I somehow hesitate whether to set the `module' header in M2.agda and
from which folder to command "agda -c".
Users will `make' the executable, it will appear in different folders,
and users will often run the executable residing in an un-expected
folder.

I wonder, how to avoid a confusion.

Thanks,

------
Sergei