max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
37034 commits 1 branch 0 tags 5.3 GiB
Commit graph

107 commits

Author SHA1 Message Date
Cameron Zwarich
a05311d1ec
chore: split IR types out into their own header file (#9264) 2025-07-08 19:49:27 +00:00
Sebastian Ullrich
aadc74bee2 perf: do not import non-meta IR 2025-06-27 08:13:31 -07:00
Mac Malone
2a8cd373ca
feat: respect lean --setup module name in code generation (#8780) 
This PR makes Lean code generation respect the module name provided
through `lean --setup`.

This is accomplished by porting to Lean the portion of `shell.cpp` that
spans running the frontend to exiting the process. This makes it easier
to load the module setup and control how its name is passed to the code
generation functions. This port attempts to minimize the changes made to
Lean. It marks the new Lean functions `private` and tries to preserve as
faithfully as possible the behavior of the original C++ code. Exposing
the new Lean interface publicly and/or further improving the code now
that is written in Lean is left for the future.
 2025-06-15 01:11:58 +00:00
Sebastian Ullrich
3d0f41e323
chore: fix interpreter lean_assert 2025-03-21 09:38:50 +01:00
Sebastian Ullrich
086d45f27c
perf: interpreter: use global native symbol cache (#7575) 
With parallelism, a thread-local cache is not sufficient anymore.
 2025-03-20 12:51:27 +00:00
Sebastian Ullrich
bab10cc2b5 feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
Sebastian Ullrich
3770808b58
feat: split Lean.Kernel.Environment from Lean.Environment (#5145) 
This PR splits the environment used by the kernel from that used by the
elaborator, providing the foundation for tracking of asynchronously
elaborated declarations, which will exist as a concept only in the
latter.

Minor changes:
* kernel diagnostics are moved from an environment extension to a direct
environment as they are the only extension used directly by the kernel
* `initQuot` is moved from an environment header field to a direct
environment as it is the only header field used by the kernel; this also
makes the remaining header immutable after import
 2025-01-18 18:42:57 +00:00
Leonardo de Moura
633c825ff3
feat: add Float32 support (#6366) 
This PR adds support for `Float32` and fixes a bug in the runtime.
 2024-12-11 02:55:58 +00:00
Leonardo de Moura
5c333ef969
fix: Float32 runtime support (#6350) 
This PR adds missing features and fixes bugs in the `Float32` support
 2024-12-10 01:37:01 +00:00
Sebastian Ullrich
c5114c971a fix: Windows needs more LEAN_EXPORTs 2024-08-12 14:14:42 +02:00
Sebastian Ullrich
d020a9c5a6
feat: introduce Std (#4499) 
Situated between `Init` and `Lean`, provides functionality not in the
prelude to both Lean's implementation and external users
 2024-06-21 07:08:45 +00:00
Sebastian Ullrich
1f732bb3b7
fix: missing unboxing in interpreter when loading initialized value (#4512) 
Fixes #4457
 2024-06-20 10:06:24 +00:00
Sebastian Ullrich
6e731b4370 chore: delete interpreter copy constructor just to be safe 2024-04-30 10:36:40 +02:00
Leonardo de Moura
b8b6b219c3
chore: move trace.cpp to kernel (#4014) 
Motivation: trace kernel `is_def_eq`
 2024-04-28 17:24:48 +00:00
Scott Morrison
f1b274279b
feat: helpful error message about supportInterpreter (#2912) 
Following [@Kha's
suggestion](https://github.com/leanprover/lean4/issues/2897#issuecomment-1816043031)
from #2897.

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
 2023-11-21 10:31:26 +01:00
Sebastian Ullrich
46b6391c77 fix: inconsistent use of precompiled symbols from interpreter on Windows 2022-11-18 06:16:05 -08:00
Sebastian Ullrich
a4abbf07b8 chore: remove remnants of C++ format 2022-11-18 06:11:24 -08:00
Sebastian Ullrich
7460878e05 chore: define WIN32_LEAN_AND_MEAN 2022-04-06 09:38:19 +02:00
Sebastian Ullrich
f2d5470f19 feat: allow interpretation of constants initialized by native code 2022-03-07 10:59:49 +01:00
Sebastian Ullrich
c59f7a55cf fix: initialize precompiled modules 2022-01-20 18:55:57 +01:00
Gabriel Ebner
ab276a5ae3 chore: show declaration with sorry in #eval 2022-01-17 13:18:22 -08:00
Sebastian Ullrich
fdd939fc40 fix: accidental memory leak in last commit 2021-12-21 19:43:02 +01:00
Sebastian Ullrich
3318f1fb05 feat: record declaration name in interpretation profile 2021-12-21 19:04:58 +01:00
Gabriel Ebner
e65f3fe810 fix: use redirected stderr for tout() 2021-12-16 10:23:05 -08:00
Joshua Seaton
a9317760e7
chore: update IR interpreter enum hygiene 
This change addresses -Wreturn type and -Wimplicit-fallthrough
infractions in the IR interpreter. Moreover, default switch cases on
enum classes are removed to leverage compiler complaints of missing
cases, which ensures that all related switch logic gets thoughtfully
extended when the enums are extended themselves.
 2021-11-28 10:29:08 +01:00
Leonardo de Moura
352391bfcb chore: remove mpz_get_d dependency 2021-10-26 12:40:20 -07:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Sebastian Ullrich
5f4b1b1d44 Revert "Revert "feat: reintroduce libleanshared, link lean & leanpkg against it"" 
This reverts commit ccbc9d00db.
 2021-08-20 09:42:05 -07:00
Sebastian Ullrich
ccbc9d00db Revert "feat: reintroduce libleanshared, link lean & leanpkg against it" 2021-08-20 15:39:00 +02:00
Sebastian Ullrich
58d6f3b817 fix: search all loaded modules for symbols on Windows 2021-08-18 13:54:52 +02:00
Leonardo de Moura
14b611af96 refactor: move buffer.h and *_ref.h files to runtime 2021-08-16 15:39:38 -07:00
Sebastian Ullrich
917eb4d081 chore: collect stdlib compilation flags in new header 2021-08-12 07:51:50 -07:00
Sebastian Ullrich
e1703bf1ae fix: main return value on 32-bit 
Resolves #594
 2021-08-03 11:00:10 -07:00
Wojciech Nawrocki
b7cd68a91e feat: complain more verbosely 2021-06-06 15:34:44 +02:00
Leonardo de Moura
cf5adbd4fe chore: increase LEAN_MAX_SMALL_OBJECT_SIZE and simplify code 2021-01-30 10:58:34 -08:00
Leonardo de Moura
d71aab5dc4 fix: allow bigger ctor objects 
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
 2021-01-29 18:23:38 -08:00
Leonardo de Moura
31680c1255 fix: do not evaluate code containing sorry 
closes #277
 2021-01-26 15:01:53 -08:00
Sebastian Ullrich
79abd5fec6 chore: remove C++ messages 2021-01-12 09:51:14 -08:00
Sebastian Ullrich
a6c319a25c chore: remove message_builder from time_task 2021-01-12 09:51:14 -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
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
Sebastian Ullrich
7964b727e5 chore: improve error message 2020-10-22 21:40:58 +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