[Agda-dev] Why do we support cpp?

[Ulf Norell]

make CABAL_OPTS=--flags=-cpphs

/ Ulf


On Fri, May 18, 2018 at 11:42 AM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/59d19e7e/attachment.html>