[Agda-dev] Why do we support cpp?

[Jesper Cockx]

I would argue that we *also* have a lot of problems with cpp, and the
current approach gives us the worst of both worlds.

BTW, how can I tell ghc to use cpp instead of cpphs just for one build? It
seems I always get cpphs by default unless I uninstall it.

-- Jesper

On Fri, May 18, 2018 at 11:07 AM, Ulf Norell <ulfn at chalmers.se> wrote:

> FWIW I'm always building without cpphs, so I get the error before pushing.
> A reason not to switch to cpphs only is that we've been having lots of
> problems with it. A quick search on the issue tracker finds 40 issues
> mentioning cpphs.
>
> / Ulf
>
> On Fri, May 18, 2018 at 10:53 AM, Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> Hi all,
>>
>> Maybe I'm beating a dead horse here, but why do we still also support cpp
>> instead of only cpphs if cpp can't even properly handle primes (')? This is
>> extremely annoying and hits me in >50% of the cases when I push something.
>> I know about the issue where 'build-depends' in the cabal file doesn't
>> automatically install the dependencies, but couldn't we just add 'cabal
>> install cpphs' to the makefile and drop support for cpp? This seems like a
>> much better solution than polluting our code with {-'-} or additional line
>> breaks.
>>
>> -- Jesper
>>
>> ps: sorry for the rant.
>>
>> _______________________________________________
>> Agda-dev mailing list
>> Agda-dev at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda-dev
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180518/777eb506/attachment.html>