[Agda-dev] Why do we support cpp?

[Ulf Norell]

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