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

[Andreas Abel]

What is the problem with Primitive.agda?

$ agda --safe Safe.agda
Checking Safe (/home/abel/agda/test/bugs/Safe.agda).
Finished Safe.

What other output would you expect?

Primitive.agda was necessary since the internal machinery used levels by 
default (--universe-polymorphism) and would trip over undefined BUILTINs 
in error messages etc. all the time.

On 15.02.2016 13:22, Andrés Sicard-Ramírez wrote:
> 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
>
> ?
>
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/