edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Revert "Refactor makefiles" #380

Closed edwinb closed 4 years ago

edwinb commented 4 years ago

Reverts edwinb/Idris2#370

This turned out to cause a few problems, and I can't immediately see how to fix them so I'll need to revert for now. They are:

edwinb commented 4 years ago

So much for reverting being simple. I guess I'll leave it for now.

ska80 commented 4 years ago
  • Even if OPT isn't set, it builds idris2.c with -O2 due to a setting in dist/Makefile. Ideally, by default, the code in dist/rts should be built with -O2 since its stable rts code, but during development we don't want -O2 for the generated idris2.c
  • Most worryingly, when I do make -C dist/rts clean I get an error:
    make: Entering directory '/home/edwin/Research/Yaffle/dist/rts'
    ../config.mk:1: /config.mk: No such file or directory
    make: *** No rule to make target '/config.mk'. Stop.

@edwinb I have fixed those issues in PR #383

Now make -C dist/rts clean works as expected.