Primitive.agda [was [Agda-dev] Agda and Packages/Libraries]

[Andrés Sicard-Ramírez]

2016-02-04 16:47 GMT-05:00 Philipp Hausmann <philipp.hausmann at 314.ch>:
> ---------- Forwarded message ----------
> From: Philipp Hausmann <philipp.hausmann at 314.ch>
> To: "Andrés Sicard-Ramírez" <asr at eafit.edu.co>
> Cc: Agda-dev mailing list <agda-dev at lists.chalmers.se>
> Date: Thu, 4 Feb 2016 22:47:55 +0100
> Subject: Re: [Agda-dev] Agda and Packages/Libraries

>> I suggest to remove the `fauchi` bits from Agda.cabal.

> The main reason why it's part of Agda.cabal is that Agda's Setup.hs needs it
> to install the Primitive.agda file. If I split off `fauchi` into a separate
> cabal file or repository, I would have to duplicate some of the
> package build code inside Setup.hs.
>
> Treating Primitive.agda like a "normal" package is necessary to avoid
> having to special-case it everywhere, which I think would be
> hard to maintain.

I'm not a big fan of Primitive.agda (I didn't understand the
motivation for adding this module). For example, given

  moduleSafe where

  open import Agda.Primitive

  Foo : Set
  Foo = Level

Which should be the output of

  $ agda --safe Safe.agda

?



-- 
Andrés