on master help sign in
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.
17c887astepcut
config.mk+3−1
@@ -1,6 +1,8 @@
1CC ?=cc
1CC ?=cc
2CABAL :=cabal
2CABAL :=cabal
3+# IDRIS_ENABLE_STATS should not be set in final release
3−CFLAGS :=-O2 -Wall -DHAS_PTHREAD $(CFLAGS)
4+CFLAGS :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS)
5+
4#CABALFLAGS :=
6#CABALFLAGS :=
5## Disable building of Effects
7## Disable building of Effects
6#CABALFLAGS :=-f NoEffects
8#CABALFLAGS :=-f NoEffects
rts/idris_stats.h+2−2
@@ -1,10 +1,10 @@
1#ifndef _IDRIS_STATS_H
1#ifndef _IDRIS_STATS_H
2#define _IDRIS_STATS_H
2#define _IDRIS_STATS_H
3
3
4+#ifdef IDRIS_ENABLE_STATS
4#include <time.h>
5#include <time.h>
6+#endif
5
7
6−// Should not be defined in release.
7−#define IDRIS_ENABLE_STATS
8
8
9// TODO: measure user time, exclusive/inclusive stats
9// TODO: measure user time, exclusive/inclusive stats
10typedef struct {
10typedef struct {