max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/playground/Makefile): actually compile Lean code with optimizations

Browse source
This commit is contained in:
Sebastian Ullrich 2019-05-22 19:10:10 +02:00
parent 29623cd2c5
commit e5ed96798b
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/playground/Makefile
View file

@ -6,6 +6,7 @@ CROSS_CATS = .lean .lean.perf .hs .gc.hs .hs.perf .llvm.hs .ml .gc.ml .ml.perf
TIME_CATS = .lean .hs .llvm.hs .ml
RETIRED_CATS = .gcc.lean .flambda.ml
LEANC_FLAGS = -O3
GHC_FLAGS = -O3
OCAML_FLAGS = -O3
@ -30,7 +31,7 @@ all: reports report_cross.csv
%.lean.cpp: %.lean
$(LEAN_BIN)/lean --cpp=$@ $<
%.lean.out: %.lean.cpp
$(LEAN_BIN)/leanc -o $@ $<
$(LEAN_BIN)/leanc $(LEANC_FLAGS) -o $@ $<
# Binaries x.lean.out and x.gcc.lean.out etc. are produced by the
# same rules and x.lean source file by copying the latter to
# x.gcc.lean. This also avoids conflicts between intermediate