[Agda] Identifying experimental Agda features for Cabal support

[Darin Morrison]

On Wed, Sep 23, 2009 at 11:03 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:

> I assume that this would be coupled with a new semantics for the
> extensions field. In Haskell the extensions field can be used to enable
> a feature for an entire project, and LANGUAGE pragmas can be used to
> enable features in individual files. In Agda extensions which were not
> listed in the extensions field would not be allowed to be used at all in
> the project, nor in any dependencies. (And LANGUAGE pragmas would be
> pointless.) Is this what you had in mind?

That would be one way to do it.  What I had in mind though was more
along the lines of having the user specify an additional option
elsewhere if they didn't want to allow certain features to be used in
any dependencies.  Something like --no-universe-polymorphism.  This
could just be added to a custom command line options field in the
.cabal file.

-- 
Darin