Measure the startup overhead of different programming languages
Add lean impl
+103
-13
+88
True.c
+88
True.c
···
1
+
// Lean compiler output
2
+
// Module: True
3
+
// Imports: Init
4
+
#include <lean/lean.h>
5
+
#if defined(__clang__)
6
+
#pragma clang diagnostic ignored "-Wunused-parameter"
7
+
#pragma clang diagnostic ignored "-Wunused-label"
8
+
#elif defined(__GNUC__) && !defined(__CLANG__)
9
+
#pragma GCC diagnostic ignored "-Wunused-parameter"
10
+
#pragma GCC diagnostic ignored "-Wunused-label"
11
+
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
12
+
#endif
13
+
#ifdef __cplusplus
14
+
extern "C" {
15
+
#endif
16
+
LEAN_EXPORT lean_object* _lean_main(lean_object*);
17
+
LEAN_EXPORT lean_object* l_main___boxed__const__1;
18
+
static lean_object* _init_l_main___boxed__const__1() {
19
+
_start:
20
+
{
21
+
uint32_t x_1; lean_object* x_2;
22
+
x_1 = 0;
23
+
x_2 = lean_box_uint32(x_1);
24
+
return x_2;
25
+
}
26
+
}
27
+
LEAN_EXPORT lean_object* _lean_main(lean_object* x_1) {
28
+
_start:
29
+
{
30
+
lean_object* x_2; lean_object* x_3;
31
+
x_2 = l_main___boxed__const__1;
32
+
x_3 = lean_alloc_ctor(0, 2, 0);
33
+
lean_ctor_set(x_3, 0, x_2);
34
+
lean_ctor_set(x_3, 1, x_1);
35
+
return x_3;
36
+
}
37
+
}
38
+
lean_object* initialize_Init(uint8_t builtin, lean_object*);
39
+
static bool _G_initialized = false;
40
+
LEAN_EXPORT lean_object* initialize_True(uint8_t builtin, lean_object* w) {
41
+
lean_object * res;
42
+
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
43
+
_G_initialized = true;
44
+
res = initialize_Init(builtin, lean_io_mk_world());
45
+
if (lean_io_result_is_error(res)) return res;
46
+
lean_dec_ref(res);
47
+
l_main___boxed__const__1 = _init_l_main___boxed__const__1();
48
+
lean_mark_persistent(l_main___boxed__const__1);
49
+
return lean_io_result_mk_ok(lean_box(0));
50
+
}
51
+
char ** lean_setup_args(int argc, char ** argv);
52
+
void lean_initialize_runtime_module();
53
+
54
+
#if defined(WIN32) || defined(_WIN32)
55
+
#include <windows.h>
56
+
#endif
57
+
58
+
int main(int argc, char ** argv) {
59
+
#if defined(WIN32) || defined(_WIN32)
60
+
SetErrorMode(SEM_FAILCRITICALERRORS);
61
+
SetConsoleOutputCP(CP_UTF8);
62
+
#endif
63
+
lean_object* in; lean_object* res;
64
+
argv = lean_setup_args(argc, argv);
65
+
lean_initialize_runtime_module();
66
+
lean_set_panic_messages(false);
67
+
res = initialize_True(1 /* builtin */, lean_io_mk_world());
68
+
lean_set_panic_messages(true);
69
+
lean_io_mark_end_initialization();
70
+
if (lean_io_result_is_ok(res)) {
71
+
lean_dec_ref(res);
72
+
lean_init_task_manager();
73
+
res = _lean_main(lean_io_mk_world());
74
+
}
75
+
lean_finalize_task_manager();
76
+
if (lean_io_result_is_ok(res)) {
77
+
int ret = lean_unbox_uint32(lean_io_result_get_value(res));
78
+
lean_dec_ref(res);
79
+
return ret;
80
+
} else {
81
+
lean_io_result_show_error(res);
82
+
lean_dec_ref(res);
83
+
return 1;
84
+
}
85
+
}
86
+
#ifdef __cplusplus
87
+
}
88
+
#endif
+2
-7
readme.md
+2
-7
readme.md
···
1
1
How much pain will the programmer take to make the program run fast?
2
2
3
-
| Command | Mean [µs] | Min [µs] | Max [µs] | Relative |
4
-
|:---|---:|---:|---:|---:|
5
-
| `true` | 272.6 ± 27.3 | 235.1 | 564.7 | 3.40 ± 0.74 |
6
-
| `./true-s` | 80.2 ± 15.6 | 70.0 | 671.2 | 1.00 |
7
-
| `./true-zig` | 85.5 ± 14.9 | 74.2 | 385.7 | 1.07 ± 0.28 |
8
-
| `./true-hare` | 92.7 ± 18.1 | 80.5 | 1041.3 | 1.16 ± 0.32 |
9
-
| `./true-go` | 564.8 ± 43.6 | 484.6 | 2070.5 | 7.04 ± 1.47 |
3
+
See [timings](timings.md).
4
+
+4
-1
run-all
+4
-1
run-all
···
7
7
8
8
go build -o true-go true.go
9
9
10
-
hyperfine --export-markdown timings.md -N 'true' './true-s' './true-zig' './true-hare' './true-go'
10
+
lean -cTrue.c True.lean
11
+
leanc -O3 -o true-lean True.c
12
+
13
+
hyperfine --export-markdown timings.md -N 'true' './true-s' './true-zig' './true-hare' './true-go' './true-lean'
+6
-5
timings.md
+6
-5
timings.md
···
1
1
| Command | Mean [µs] | Min [µs] | Max [µs] | Relative |
2
2
|:---|---:|---:|---:|---:|
3
-
| `true` | 272.6 ± 27.3 | 235.1 | 564.7 | 3.40 ± 0.74 |
4
-
| `./true-s` | 80.2 ± 15.6 | 70.0 | 671.2 | 1.00 |
5
-
| `./true-zig` | 85.5 ± 14.9 | 74.2 | 385.7 | 1.07 ± 0.28 |
6
-
| `./true-hare` | 92.7 ± 18.1 | 80.5 | 1041.3 | 1.16 ± 0.32 |
7
-
| `./true-go` | 564.8 ± 43.6 | 484.6 | 2070.5 | 7.04 ± 1.47 |
3
+
| `true` | 272.9 ± 31.2 | 238.0 | 933.2 | 3.35 ± 1.43 |
4
+
| `./true-s` | 81.5 ± 33.5 | 71.5 | 1460.9 | 1.00 |
5
+
| `./true-zig` | 87.1 ± 43.1 | 76.7 | 1748.2 | 1.07 ± 0.69 |
6
+
| `./true-hare` | 94.7 ± 48.2 | 84.1 | 1904.5 | 1.16 ± 0.76 |
7
+
| `./true-go` | 579.1 ± 133.1 | 499.8 | 4066.2 | 7.11 ± 3.34 |
8
+
| `./true-lean` | 1632.5 ± 75.0 | 1519.5 | 2243.9 | 20.04 ± 8.28 |