Set IDRIS_ENABLE_STATS in config.mk instead of in idris_stats.h. stats are not supported on Arduino. Also make sure that when IDRIS_ENABLE_STATS is not set, the idris_stats.h does not pull in time.h as this header is not available on the Arduino platform.
commit17c887ad8a66ce94aa305b97da3019dd78d80153
authorstepcut <jeremy@n-heptane.com>
dateWed 16 Jul 2014, 15:22 (12 years ago)
parentf0ba64c
config.mk+3−1
@@ -1,6 +1,8 @@
11CC ?=cc
22CABAL :=cabal
3−CFLAGS :=-O2 -Wall -DHAS_PTHREAD $(CFLAGS)
3+# IDRIS_ENABLE_STATS should not be set in final release
4+CFLAGS :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS)
5+
46#CABALFLAGS :=
57## Disable building of Effects
68#CABALFLAGS :=-f NoEffects
rts/idris_stats.h+2−2
@@ -1,10 +1,10 @@
11#ifndef _IDRIS_STATS_H
22#define _IDRIS_STATS_H
33
4+#ifdef IDRIS_ENABLE_STATS
45#include <time.h>
6+#endif
57
6−// Should not be defined in release.
7−#define IDRIS_ENABLE_STATS
88
99// TODO: measure user time, exclusive/inclusive stats
1010typedef struct {