[Agda] Identifying experimental Agda features for Cabal support

[Nils Anders Danielsson]

On 2009-09-23 00:43, Darin Morrison wrote:
> On Tue, Sep 22, 2009 at 9:19 PM, Nils Anders Danielsson
> <nad at cs.nott.ac.uk> wrote:
>> * If a user does not trust a given feature, then I suppose (s)he would
>>  want to ensure that the feature is never used in a given development.
>>  In Haskell there is no easy way to enforce this. Do we want
>>  project-wide disabling of features to be easy? In that case I think it
>>  should also be easy to ensure that code does not use postulates, does
>>  not turn off the termination checker, etc.
> 
> Yes, this was also discussed.  It seems that people do want this
> functionality.  I don't think it would be hard to add this to the Agda
> cabal support.  All one needs to do is store a field for packages in
> the database specifying which extensions they used and then check this
> information during dependency analysis to determine whether
> undesirable features will be used.

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?

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.