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

30425 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
768ef310a0 refactor: Nix: LeanInk rendering based on packages, not directories 2022-12-03 15:14:17 +01:00
Sebastian Ullrich
ed3fa37341 chore: Nix: add overrideBuildModAttrs 2022-12-03 14:13:31 +01:00
Gabriel Ebner
4b87103931 chore: ignore document version errors 2022-12-03 01:20:47 +01:00
tydeu
fe09c9c824 chore: update Lake 2022-12-03 01:19:29 +01:00
ChrisHughes24
e168806078 chore: rename Prod.ext 2022-12-02 20:24:19 +01:00
Leonardo de Moura
8a573b5d87 fix: fixes #1900 2022-12-02 10:04:01 -08:00
Leonardo de Moura
a999015371 feat: add applicationTime to registerTagAttribute 2022-12-02 09:58:41 -08:00
Leonardo de Moura
50fc4a6ad8 fix: fixes #1907 2022-12-02 08:59:16 -08:00
Gabriel Ebner
681bbe5cf4 feat: ByteArray.hash 2022-12-01 20:18:14 -08:00
Gabriel Ebner
a67a5080e9 chore: fix tests after hash change 2022-12-01 20:18:14 -08:00
Gabriel Ebner
c83e33b06a chore: update stage0 2022-12-01 20:18:14 -08:00
Gabriel Ebner
9b416667e7 chore: replace all hashes by murmurhash 2022-12-01 20:18:14 -08:00
Gabriel Ebner
b0cadbc1fa fix: support escaped field names in deriving FromJson/ToJson 2022-12-02 03:48:19 +01:00
Gabriel Ebner
3d1571896c fix: support escaped field names in dot-notation 2022-12-02 03:48:19 +01:00
Gabriel Ebner
7af80766e3 fix: do not ignore applicationTime in parametric attributes 2022-12-02 02:15:35 +01:00
Leonardo de Moura
ffb0f42aae fix: fixes #1901 2022-12-01 08:39:06 -08:00
Leonardo de Moura
0dda3a8c02 fix: include instance implicits that depend on outParams at outParamsPos 
This fixes the fix for #1852
 2022-12-01 06:11:48 -08:00
Leonardo de Moura
0a031fc9bb chore: replace Expr.forEach with Expr.forEachWhere 2022-12-01 05:19:32 -08:00
Sebastian Ullrich
af5efe0b2d doc: MonadReader 2022-12-01 10:16:04 +01:00
Sebastian Ullrich
50b2ad89b4 test: limit maxRecDepth 2022-12-01 10:06:57 +01:00
Leonardo de Moura
30d625697e chore: use Expr.forEachWhere to implement linter 
closes #1899

TODO: use `Expr.forEachWhere` in other modules. There are many other opportunities.
 2022-11-30 18:44:20 -08:00
Leonardo de Moura
1c5706bcc0 feat: add Expr.forEachWhere 2022-11-30 18:41:12 -08:00
Leonardo de Moura
5a151ca64c chore: fix tests 2022-11-30 17:52:37 -08:00
Leonardo de Moura
0db02c3911 chore: update Lake 2022-11-30 17:05:38 -08:00
Leonardo de Moura
95467dfab7 chore: update stage0 2022-11-30 17:05:38 -08:00
Leonardo de Moura
e5681ac141 feat: replace mixHash implementation 
We are now using part of the murmur hash like Scala.
For additional information and context, see
https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/Increasing.20.60Expr.2Ehash.60.20to.2064.20bits/near/313114719
 2022-11-30 17:03:58 -08:00
Leonardo de Moura
8fc3d77a0b feat: add trace.Meta.Tactic.simp.numSteps and trace.Meta.Tactic.simp.heads 2022-11-30 07:07:07 -08:00
Leonardo de Moura
2a36cf42d2 chore: update stage0 2022-11-30 06:43:57 -08:00
Leonardo de Moura
aee63ee7b0 feat: panic at Name.append if both names have macro scopes 2022-11-30 06:39:49 -08:00
Leonardo de Moura
7c5d91ebc3 fix: avoid hygienic ++ hygienic at Specialize.lean 2022-11-30 06:31:03 -08:00
Leonardo de Moura
a095dabb17 feat: Name.append and macro scopes 2022-11-29 23:06:04 -08:00
Leonardo de Moura
bc21716bad chore: helper simp theorems 2022-11-29 23:05:48 -08:00
Leonardo de Moura
3e45060dd5 fix: disable implicit lambdas for local variables without type information 
Problem reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/why.20doesn't.20this.20unify.3F/near/312806870
 2022-11-29 14:33:16 -08:00
Scott Morrison
1b50292228 chore: protect Prod.Lex 2022-11-29 20:09:08 +01:00
Sebastian Ullrich
bc0684a29c fix: work around VS Code completion bug 2022-11-29 19:14:45 +01:00
Leonardo de Moura
069873d8e5 fix: fixes #1891 2022-11-29 08:59:46 -08:00
Mario Carneiro
40e212c166 feat: infer def/theorem DefKind for let rec 2022-11-29 08:16:47 -08:00
Gabriel Ebner
6e23ced6d9 fix: test 2022-11-29 08:16:09 -08:00
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
6bc919742e chore: update stage0 2022-11-28 07:51:42 -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