Leonardo de Moura
403699f5e4
fix: elim_array_cases
2021-01-04 16:10:49 -08:00
Sebastian Ullrich
34cf4bc3ff
chore: fix LEAN_SPECIAL_VERSION_DESC
2021-01-04 15:44:03 +01:00
Leonardo de Moura
f0ac477d2e
feat: add sanity checks
2021-01-01 18:31:28 -08:00
Sebastian Ullrich
6e33020da4
feat: version information API
2020-12-29 14:42:48 -08:00
Leonardo de Moura
8c2cb44ac0
fix: error message produced by lean_mk_projections
2020-12-22 17:40:32 -08:00
Leonardo de Moura
340cade575
fix: bug at specialize.cpp
2020-12-20 17:48:46 -08:00
Leonardo de Moura
76eb163a0f
chore: use new pretty printer at specialize trace messages
2020-12-20 16:44:55 -08:00
Leonardo de Moura
2da48e8739
feat: use new pretty printer to trace all compiler steps
2020-12-20 16:44:40 -08:00
Sebastian Ullrich
0ddc932052
fix: interpreter cache leak by simplifying it after all
2020-12-18 17:06:35 +01:00
Sebastian Ullrich
dcfef05c8e
perf: reuse interpreter caches a bit more
2020-12-17 23:18:43 +01:00
Sebastian Ullrich
22bb2fbd06
perf: reuse thread-local interpreter
2020-12-17 23:18:43 +01:00
Sebastian Ullrich
af7e44f017
fix: interpreter: make sure to retain options after switching threads
2020-12-17 23:18:43 +01:00
Sebastian Ullrich
65c1bc8952
fix: gen_constants_cpp.py: mark constants as persistent
2020-11-29 18:59:39 +01:00
Sebastian Ullrich
f649f24014
fix: compilation on Windows
2020-11-29 14:08:53 +01:00
Sebastian Ullrich
c0f94c902e
fix: memory leak in interpreter
2020-11-29 14:08:53 +01:00
Sebastian Ullrich
99383d97e1
feat: measure interpreter time & fix enabling interpreter traces
2020-11-28 17:36:20 +01:00
Leonardo de Moura
6830291fd5
chore: remove dead code at Class.lean used by old frontend
2020-11-20 16:51:44 -08:00
Leonardo de Moura
34178034a0
chore: fix warning
2020-11-11 11:15:31 -08:00
Leonardo de Moura
7b5f283507
chore: remove Expr.localE constructor
...
It was used by the old frontend
2020-11-01 09:37:48 -08:00
Leonardo de Moura
d87b8b876f
chore: add temporary workaround
...
cc @Kha
2020-10-28 16:57:46 -07:00
Leonardo de Moura
de568b1268
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
852bd66542
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
227faa0aad
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
c2b2f62bc4
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
ffc5ccf118
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
01f8bcfc87
chore: remove dead code
2020-10-27 19:23:14 -07:00
Leonardo de Moura
1fba699b2c
chore: remove unused names
2020-10-27 16:28:19 -07:00
Leonardo de Moura
270f6df5cb
chore: remove aux_match module
...
This is not needed anymore since the old equation compiler was removed.
2020-10-27 09:51:55 -07:00
Leonardo de Moura
7d8c079d71
chore: remove abstract_context_cache
2020-10-27 09:37:21 -07:00
Leonardo de Moura
95acb5cf3a
chore: remove old fun_info module
2020-10-27 09:37:21 -07:00
Leonardo de Moura
c841f83c04
chore: remove dead code
2020-10-27 09:37:21 -07:00
Leonardo de Moura
503504e962
chore: cleanup
2020-10-27 09:37:21 -07:00
Leonardo de Moura
16710581ad
chore: remove dead code
2020-10-27 09:37:21 -07:00
Leonardo de Moura
bad6233389
chore: remove legacy support for modification objects
2020-10-26 08:10:51 -07:00
Leonardo de Moura
289ba6583c
chore: remove dead code
2020-10-26 07:58:15 -07:00
Leonardo de Moura
7a24fe73ca
chore: remove dead code
2020-10-25 20:49:30 -07:00
Leonardo de Moura
4838fb5c16
chore: remove source code for old frontend, equation compiler and tactics
2020-10-25 10:22:06 -07:00
Leonardo de Moura
e28b337a2c
chore: remove old frontend support from lean.cpp
...
We also remove the option `-n` (for new frontend)
2020-10-25 10:16:52 -07:00
Leonardo de Moura
3f0cc1d2ec
fix: library/constructions primitives crash at kernel_exception
2020-10-24 18:52:01 -07:00
Sebastian Ullrich
0720334450
feat: make profileit actually usable
2020-10-23 18:34:47 +02:00
Leonardo de Moura
4f6538fa9f
fix: extern detection
2020-10-22 16:30:02 -07:00
Sebastian Ullrich
7964b727e5
chore: improve error message
2020-10-22 21:40:58 +02:00
Sebastian Ullrich
c32f843efc
fix: profiling from the new frontend; use trace out for the time being
2020-10-22 16:00:03 +02:00
Sebastian Ullrich
ecece59cc3
fix: tracing the compiler from the new frontend
2020-10-22 14:50:26 +02:00
Sebastian Ullrich
b562cb8a2a
fix: exception while tracing in the old frontend
2020-10-22 14:50:26 +02:00
Sebastian Ullrich
4e74e36331
feat: run initializers on import
...
Also, refuse to evaluate an `[init]` decl in the same module (since we don't know whether the initialization is
backtrackable) and always use native symbol of a `[builtinInit]` decl
2020-10-22 11:59:55 +02:00
Sebastian Ullrich
86fe95898d
fix: don't try to interpret [builtinInit] constants
2020-10-22 11:59:55 +02:00
Sebastian Ullrich
b06f8311e8
fix: avoid using native code during bootstrap
2020-10-21 11:21:56 +02:00
Sebastian Ullrich
438b3351dd
feat: add interpreter.prefer_native option
2020-10-21 11:21:56 +02:00
Leonardo de Moura
e54a207986
refactor: provide Options to lean_eval_const
...
add `ImportM` monad for `addImportedFn`
cc @Kha
2020-10-19 10:21:38 -07:00
