[Agda-dev] Why do we support cpp?

[Andrés Sicard-Ramírez]

Hi Jesper,

On 18 May 2018 at 03:53, Jesper Cockx <Jesper at sikanda.be> wrote:
> 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.

We switched from cpp to cpphs due to some issues on OS X, but
since cpphs didn't work in all the configurations (see
https://github.com/agda/agda/issues/1285 ) we need to support both.

Best,


-- 
Andrés