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

6118 commits

Author SHA1 Message Date
Alexander Bentkamp
7dc1618ca5
feat: Web Assembly Build (#2599) 
Co-authored-by: Rujia Liu <rujialiu@user.noreply.github.com>
 2023-10-04 09:04:20 +02:00
Joachim Breitner
06e057758e chore: Remove unused variables from kernel 
when I build lean locally, I get a nice and warning-free build
experience with the exception of these two unused variables. They can
probably go?
 2023-09-27 09:43:07 -07:00
Sebastian Ullrich
63d2bdd490 fix: integer type in llvm_count_params 2023-08-18 19:34:21 +02:00
Sebastian Ullrich
4e52283728 fix: FFI signature mismatches 2023-08-18 19:34:21 +02:00
Henrik
35aa2c91a2 feat: LLVM backend: implement the equivalent of -fstack-clash-protection 2023-08-15 14:45:58 +02:00
Siddharth Bhat
0eddc167b9 feat: LLVM linkage bindings 2023-08-12 16:51:58 +02:00
Siddharth Bhat
073c8fed86 feat: LLVM backend: support for visibility Style & DLL storage 
Changes peeled from:
https://github.com/leanprover/lean4/pull/2340

to allow a `stage0` bump on master before merging in the
changes that allow LLVM to build in stage1+.
 2023-07-25 11:03:16 +02:00
Gabriel Ebner
4544443d98 feat: reorder tc subgoals according to out-params 2023-04-10 13:00:04 -07:00
Sebastian Ullrich
41a3ebed02 fix: profiler threshold in C++ 2023-04-10 16:57:54 +02:00
Sebastian Ullrich
d51e404d6a refactor: move profiling options to Lean 2023-04-10 16:57:54 +02:00
Sebastian Ullrich
b076d488e3 feat: show typeclass and tactic names in profile output 2023-03-27 17:47:52 +02:00
Sebastian Ullrich
c826168cfa fix: atomic --profile output for xargs -P 2023-02-11 17:41:07 +01:00
Siddharth
5349a089e5
feat: add --target flag for LLVM backend to build objects of a different architecture (#2034) 
* feat: add --target flag for LLVM backend to build objects of a different architecture

* chore: remove dead comment

* Update src/Lean/Compiler/IR/EmitLLVM.lean

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* chore: normalize indentation in src/util/shell.cpp

* chore: strip trailing whitespace

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-01-15 12:00:10 -08:00
Siddharth
b6eb780144
feat: LLVM backend (#1837) 2022-12-30 12:45:30 +01:00
Sebastian Ullrich
636afc654a fix: avoid mapping .oleans in the way of the stack 2022-12-13 22:11:41 +01:00
Leonardo de Moura
ffb0f42aae fix: fixes #1901 2022-12-01 08:39:06 -08:00
Mario Carneiro
6cafcabe46 fix: print universe level lists in lean 4 style 2022-11-21 21:35:56 +01:00
Siddharth
4d47c8abc6
feat: add LLVM C API bindings (#1497) 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2022-11-21 09:50:01 +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
Leonardo de Moura
723b87ad63 chore: fix build 
Incorrect assertion in the old code generator has been exposed by new test.
 2022-11-10 15:27:43 -08:00
Mario Carneiro
4fefb2097f feat: hover/go-to-def/refs for options 2022-11-07 20:01:13 +01:00
Mario Carneiro
dd5948d641 chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
Gabriel Ebner
ba57ad3480 feat: add implementation-detail hypotheses 2022-10-11 17:24:35 -07:00
Leonardo de Moura
2c825de6a1 fix: elim_scalar_array_cases 2022-07-24 14:46:46 -07:00
Leonardo de Moura
5253cc6742 fix: compiler support for FloatArray.casesOn and ByteArray.casesOn 
closes #1311
 2022-07-24 12:36:08 -07:00
Leonardo de Moura
8de798c4a6 feat: reject [macroInline] declarations in recursive declarations 
closes #1363
 2022-07-24 07:26:35 -07:00
Gabriel Ebner
b48061ed23 feat: expose lower level compile function 2022-07-11 12:26:53 -07:00
Gabriel Ebner
18a299f576 feat: allow implementedBy on constructors and casesOn 2022-07-11 12:26:53 -07:00
Leonardo de Moura
2472a6a1ea chore: fix build 
Another ugly hack to survive until we port the code generator to Lean.
 2022-07-08 10:34:50 -07:00
Leonardo de Moura
bf91956449 fix: add workaround for issue #1293 
This is a temporary hack until we port the C++ code to Lean.

closes #1293
 2022-07-07 23:39:35 -07:00
Leonardo de Moura
6ef81e1cdf fix: bug at the code specialization cache 
closes #1292
 2022-07-07 22:59:18 -07:00
Leonardo de Moura
dd924e5270 chore: remove codegen option 
We should use `noncomputable` modifier instead.

closes #1288
 2022-07-07 08:18:30 -07:00
Leonardo de Moura
ffc90f6a35 fix: bug at ll_infer_type 2022-07-04 13:55:55 -07:00
Leonardo de Moura
14260f454b feat: improve is_def_eq for projections 
It implements in the kernel the optimization in the previous commit.

This commit addresses the following issue raised on Zulip.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unfold.20essentially.20loops/near/288083209
 2022-06-30 17:50:44 -07:00
Leonardo de Moura
a888b21bce fix: compiler bug at And.casesOn 
Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28libc.2B.2Babi.29.20lean.3A.3Aexception.3A.20incomplete.20case/near/287839995
 2022-06-29 06:56:17 -07:00
Sebastian Ullrich
23d157a3ff chore: remove dead code 2022-06-15 12:43:59 +02:00
Leonardo de Moura
944063682e fix: another specialize.cpp bug 
This is just a workaround. This code has to be ported to Lean.

The issue has been reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20unknown.20constant/near/283750650
 2022-05-25 20:36:18 -07:00
Leonardo de Moura
16ed5a3213 fix: erase_irrelevant.cpp 
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'unreachable'.20code.20was.20reached.20by.20termination.20check/near/281159704
 2022-05-04 08:06:59 -07:00
Leonardo de Moura
081dff288f fix: debug build 2022-04-13 13:12:53 -07:00
Leonardo de Moura
efb859013e chore: ignore {} annotations at mk_projections 2022-04-13 10:16:41 -07:00
Sebastian Ullrich
7460878e05 chore: define WIN32_LEAN_AND_MEAN 2022-04-06 09:38:19 +02:00
Leonardo de Moura
1900efd91a chore: add pp_expr helper function 2022-03-25 18:16:18 -07:00
Leonardo de Moura
7307b02fd7 fix: missing test at has_trivial_structure 
see #1074
 2022-03-25 17:36:30 -07:00
Leonardo de Moura
1afee372f7 refactor: move consume_type_annotations declaration to expr.h 2022-03-10 08:00:39 -08:00
Leonardo de Moura
33883e9d2a fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam) 2022-03-10 07:47:38 -08:00
Sebastian Ullrich
f2d5470f19 feat: allow interpretation of constants initialized by native code 2022-03-07 10:59:49 +01:00
Leonardo de Moura
049273afee fix: add workarounds to code generator 
The issue is only going to be properly fixed when we rewrite `csimp`
in Lean. The `csimp` performs transformations that do not preserve
typability, but it also uses the kernel `infer_type` which assumes the
input is type correct. In the new `csimp`, we must have a different
`infer_type` which returns an `Any` type in this kind of situation.

The workaround in this commit simply disables optimizations when
`infer_type` fails. It does not fix all occurrences of this problem,
but the two places that issue #1030 triggered.

closes #1030
 2022-02-25 08:47:56 -08:00
Leonardo de Moura
dedb6ee01b fix: skip value if type is computationally irrelevant 2022-02-17 10:41:16 -08:00
Leonardo de Moura
ba0904060b chore: missing trace_pp_expr 2022-02-17 10:40:21 -08:00