search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

Make benchmarks compile with the whole basis builtin #173

Closed tanyongkiam closed 7 years ago

tanyongkiam commented 8 years ago

The benchmarks currently make direct use of CakeML AST for things like Array.sub -> Op Asub.

When "Array.sub" is parsed, this instead turns into a long Opapp ... ( ... ), where Array.sub is assumed to already be in the basis.

This makes it annoying to write new benchmarks in concrete syntax, because using

EVAL``(parse_prog o lexer_fun) "... insert benchmark here ..." ``

This shouldn't affect the speed of the benchmarks because all (or most of) the basis stubs can be inlined.

However, it will make some bits of the in-logic compilation slower. It might be useful to use Ramana's parallel evaluation machinery in bootstrap/

xrchz commented 7 years ago

@tanyongkiam is this done now?

tanyongkiam commented 7 years ago

I've been thinking of actually undoing this change or recovering the old benchmarks at some point.

Reason: it is hard to hand-trace the compiler when the entire basis is included.

xrchz commented 7 years ago

Why would you need to hand-trace the compiler? I suggest having a single benchmark/example used for such debugging, but the real benchmarks use the basis and are in concrete syntax. Also, I think this issue can probably be closed either way, right?

tanyongkiam commented 7 years ago

Sure, this one can be closed.

Hand-tracing is fairly useful, I've found several performance bugs by doing that in the past.