[Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1

[Sergei Meshveliani]

On Sun, 2019-03-24 at 13:00 +0100, Nils Anders Danielsson wrote:
> On 22/03/2019 21.55, Sergei Meshveliani wrote:
> > I somehow hesitate whether to set the `module' header in M2.agda
> 
> I suggest that you always include the module header in files that are
> intended to be imported from other files.
> 

I always do so.
In this my example, M2.agda 
* defines `main' function,
* is not imported by any module,
* and I hesitate whether to set the `module' header in M2.agda.

(the effects are described below).
 
--
SM



*******************************************************
...
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.