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

20910 commits

Author SHA1 Message Date
Gabriel Ebner
bdbab653fd fix: synthesize tc instances before propagating expected type 2022-11-29 08:16:09 -08:00
Henrik Böving
5286c2b5aa feat: optimize mul/div into shift operations 2022-11-29 01:05:06 +01:00
Henrik Böving
24cc6eae6d feat: log2 for Fin and UInts 2022-11-29 01:05:06 +01:00
Sebastian Ullrich
a38bc0e6ed refactor: revise server architecture 
Replace complex debouncing logic in watchdog with single `IO.sleep` in
worker `didChange` handler, replace redundant header change logic in
watchdog with special exit code from worker.
 2022-11-29 00:52:24 +01:00
Mario Carneiro
17ef0cea8a feat: intra-line withPosition formatting 2022-11-28 09:02:08 -08:00
Sebastian Ullrich
07953062ed perf: remove unnecessary, cache-defeating withPosition in doReassignArrow 2022-11-28 08:14:03 -08:00
Leonardo de Moura
9dbd9ec554 chore: fix build 2022-11-28 07:53:43 -08:00
Leonardo de Moura
c510d16ef5 fix: fixes #1808 2022-11-28 07:48:54 -08:00
Siddharth Bhat
dfb5548cab fix: update libleanrt.bc, rename to lean.h.bc 
This adds `lean.h.bc`, a LLVM bitcode file of the Lean
runtime that is to be inlined. This is programatically generated.

1. This differs from the previous `libleanrt.ll`, since it produces an
   LLVM bitcode file, versus a textual IR file. The bitcode file
   is faster to parse and build an in-memory LLVM module from.
2. We build `lean.h.bc` by adding it as a target to `shell`,
   which ensures that it is always built.

3. We eschew the need for:

```cpp
```

which causes breakage in the build, since changing the meaning of
`static` messes with definitions in the C++ headers.

Instead, we build `lean.h.bc` by copying everything in
`src/include/lean/lean.h`, renaming `inline` to
`__attribute__(alwaysinline)` [which forces LLVM to generate
`alwaysinline` annotations], then running the `-O3` pass pipeline
to get reasonably optimised IR, and will be perfectly inlined
when linked into the generated LLVM code by
`src/Lean/Compiler/IR/EmitLLVM.lean`.

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-11-28 16:20:12 +01:00
Scott Morrison
a3dfa5516d feat: add HashSet.insertMany 2022-11-28 06:59:21 -08:00
Leonardo de Moura
36cc7c23b6 fix: fixes #1886 2022-11-28 06:50:44 -08:00
Sebastian Ullrich
c112ae7c58 test: fix Lake rename 2022-11-28 15:12:18 +01:00
Scott Morrison
c4ff5fe199 chore: change simp default to decide := false 2022-11-27 09:27:16 -08:00
Sebastian Ullrich
42a080fae2 fix: comments ending in --/ 
Fixes #1883
 2022-11-25 10:32:49 +01:00
Sebastian Ullrich
39f2322f35 fix: save correct environment in info tree for example 2022-11-24 13:11:14 -08:00
Leonardo de Moura
4be7543adb feat: add APIs for issue #1878 
We need `update-stage0` because this commit affects the .olean format.
 2022-11-24 12:55:41 -08:00
Leonardo de Moura
c53c5b5e16 fix: fixes #1882 
Better support for `intro <type-ascription>`.
It was treating it as a pattern before this commit.
 2022-11-24 12:40:25 -08:00
Leonardo de Moura
897ccd3783 chore: spaces 2022-11-24 12:33:21 -08:00
Leonardo de Moura
9d8b324f8d fix: fixes #1869 
Better support for simplifying class projections.
 2022-11-24 11:56:36 -08:00
Leonardo de Moura
71b7562c2f fix: class projection at DiscrTree 2022-11-24 11:56:36 -08:00
Gabriel Ebner
6225a3e415 chore: update Lake 2022-11-23 19:08:14 -08:00
Mario Carneiro
9b572d4e20 chore: make <;> left associative 2022-11-23 07:44:54 -08:00
Leonardo de Moura
0694731af8 fix: fixes #1870 2022-11-23 05:49:19 -08:00
Leonardo de Moura
9c561b593a feat: add withTraceNodeBefore and use it at ExprDefEq 
`withTraceNode` uses the metavariable context after executing
`k`. This is bad when debugging `isDefEq`.
 2022-11-22 14:43:28 -08:00
Leonardo de Moura
dfaf9c6ebd chore: register missing trace options, and fix inherited parameter 
The current setting was bad for debugging `isDefEq` issues.
 2022-11-22 14:43:28 -08:00
Mario Carneiro
6cafcabe46 fix: print universe level lists in lean 4 style 2022-11-21 21:35:56 +01:00
Alex J Best
eff3c95f23 chore: fix typo in getNumBuiltiAttributes name 2022-11-21 09:22:31 -08:00
Sebastian Ullrich
019707ccf4 fix: do method lifting across choice nodes 2022-11-21 17:52:14 +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
1b73fa3fa1 chore: lean.mk: re-suppress find error messages 2022-11-20 19:55:09 +01:00
Sebastian Ullrich
5053cb02b7 chore: don't copy .lean files to stage0 2022-11-20 10:22:20 -08:00
Sebastian Ullrich
7809b269ca chore: avoid xargs in update-stage0 2022-11-20 10:22:20 -08:00
Leonardo de Moura
9022fb8d48 fix: custom update-stage0 for osx 2022-11-19 19:20:13 -08:00
Leonardo de Moura
51a29098ab fix: fixes #1852 2022-11-19 09:37:52 -08:00
Leonardo de Moura
22e96c71e9 fix: fixes #1850 2022-11-19 09:18:12 -08:00
Gabriel Ebner
bbe5cf63b2 perf: pick cache size coprime to pointer alignment 2022-11-19 08:27:38 -08:00
Mario Carneiro
c8859a31d9 fix: Nat.log2_terminates should not be private 2022-11-19 08:26:59 -08:00
Leonardo de Moura
ecac90c522 fix: optParam default value does not count as dependency at anyNamedArgDependsOnCurrent 2022-11-19 07:54:28 -08:00
Leonardo de Moura
ace674cc06 chore: remove unnecessary test 2022-11-19 07:52:53 -08:00
Leonardo de Moura
966e1df96d chore: fix build 2022-11-19 07:46:01 -08:00
Leonardo de Moura
a5ab59a413 fix: fixes #1851 2022-11-19 07:01:02 -08:00
Leonardo de Moura
556b6706ee fix: fixes #1856 2022-11-18 19:34:32 -08:00
Leonardo de Moura
a7107aedb3 fix: fixes #1848 2022-11-18 08:49:10 -08:00
Mario Carneiro
f74fee07e6
doc: document Init.Data.List.Basic (#1828) 
* doc: document Init.Data.List.Basic

* Apply suggestions from code review

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

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-11-18 06:16:50 -08: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
7529e86307
feat: implement workspace/applyEdit server request (#1846) 2022-11-17 19:30:17 +00:00
Leonardo de Moura
d2a5ea137d fix: fixes #1842 2022-11-16 17:29:41 -08:00
Leonardo de Moura
edadd8c034 fix: fixes #1841 
This commit adds the configuration option
`ApplyConfig.approx` (available in Lean 3), and sets it to true by
default like in Lean 3.
 2022-11-16 14:46:05 -08:00
Leonardo de Moura
7b03d9719c fix: fixes #1679 2022-11-16 13:15:53 -08:00