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
Alex J Best
808bb9b579
perf: dont repeatedly elab term in rw at multiple locations #2317
2023-07-24 08:47:52 -07:00
Bulhwi Cha
3b6bc4a87d
style: remove unnecessary space characters
2023-07-23 16:11:11 +02:00
Mario Carneiro
dd313c6894
feat: add IO.FS.rename
2023-07-22 23:21:32 +02:00
Bulhwi Cha
7809d49a62
doc: fix type signature of Coe
2023-07-22 14:16:21 +02:00
Sebastian Ullrich
544b704a25
test: add Lake tests
2023-07-21 09:19:19 +02:00
Sebastian Ullrich
d991f5efe0
fix: ship libLake.a
2023-07-21 09:19:19 +02:00
Sebastian Ullrich
e2fbfb5731
chore: remove Lake flake
...
Fixes leanprover/lake#165
2023-07-21 09:19:19 +02:00
Jannis Limperg
6407197e54
chore: better error message for loose bvar in whnf
2023-07-20 13:47:20 -07:00
Bulhwi Cha
367b38701f
refactor: simplify String.splitOnAux ( #2271 )
2023-07-19 11:50:27 +00:00
Wojciech Nawrocki
e1b3f10250
doc: fix contradictory docstring
2023-07-19 10:53:47 +02:00
F. G. Dorais
d10e3da673
fix: protect sizeOf lemmas
2023-07-19 08:50:59 +02:00
Leonardo de Moura
634193328b
fix: fixes #2327
2023-07-18 07:18:27 -07:00
Sebastian Ullrich
daae36d44d
chore: remove obsolete file
2023-07-17 10:38:35 +02:00
Sebastian Ullrich
bf76eca0cd
chore: merge Lake into src/lake
2023-07-17 10:38:20 +02:00
Sebastian Ullrich
9a3657df3f
chore: remove Lake submodule
2023-07-15 12:03:41 +02:00
tydeu
d37bbf4292
chore: update Lake
2023-07-14 23:43:04 -04:00
Floris van Doorn
1a6663a41b
chore: write "|-" as "|" noWs "-" ( #2299 )
...
* remove |- as an alias for ⊢
* revert false positive |->
* fix docstring
* undo previous changes
* [unchecked] use suggestion
* next attempt
* add test
2023-07-14 09:48:20 -07:00
Leonardo de Moura
212cd9c3e6
fix: fixes #2321
2023-07-13 14:41:32 -07:00
Scott Morrison
0d5c5e0191
feat: relax test in checkLocalInstanceParameters to allow instance implicits
2023-07-13 10:54:06 -07:00
Leonardo de Moura
6d857a93b5
perf: pointer set for traversing DAGs
2023-07-11 19:19:42 -07:00
Leonardo de Moura
264e376741
chore: add helper function
2023-07-11 19:19:42 -07:00
Adrien Champion
d8a548fe51
chore: fix Int.div docstring examples
2023-07-10 09:09:07 -07:00
Scott Morrison
60b8fdd8d6
feat: use nat_pow in the kernel
2023-07-10 09:01:14 -07:00
Mario Carneiro
51694cd6de
fix: calling convention for module initializers
2023-07-10 09:00:17 -07:00
Mario Carneiro
76023a7c6f
fix: don't run [builtin_init] when builtin = false
2023-07-10 08:58:02 -07:00
Sebastian Ullrich
c268d7e97b
fix: kill descendant processes on worker exit
2023-07-05 23:42:53 +02:00
Sebastian Ullrich
9901804a49
feat: SpawnArgs.setsid, Child.kill
2023-07-05 23:42:53 +02:00
Leonardo de Moura
32d5def5b8
feat: add bne_iff_ne
2023-07-05 08:51:34 -07:00
Mario Carneiro
f1b2a8acce
fix: lazy_binop + coercion bug
...
fixes #2300
2023-07-01 06:05:25 -07:00
Leonardo de Moura
94d4a427e2
fix: fixes #2115
2023-06-30 19:54:38 -07:00
Leonardo de Moura
a002ce6d0d
fix: fixes #2077
2023-06-30 19:26:00 -07:00
tydeu
aee9ce4321
chore: update Lake
2023-06-30 09:44:26 +02:00
Leonardo de Moura
ec42581d1f
perf: use Core.transform instead of Meta.transform at betaReduceLetRecApps
...
Observed big performance improvement on files containing big proofs
generated using tactics.
2023-06-28 12:29:12 -07:00
Leonardo de Moura
eece499da9
fix: fixes #2282
2023-06-27 16:46:38 -07:00
Sebastian Ullrich
f0583c3fd6
feat: trace nodes for SizeOf and injectivity theorem generation
2023-06-27 16:17:46 -07:00
Wojciech Nawrocki
ba4bfe26f2
fix: add missing instantiateMVars
2023-06-27 16:13:56 -07:00
Mario Carneiro
3104c223d8
fix: reference implementation for Array.mapM
2023-06-27 14:21:22 -07:00
tydeu
46c77afeaf
chore: update Lake
2023-06-27 21:35:51 +01:00
Sebastian Ullrich
e1999ada7f
fix: make "elaboration" metric work in language server
2023-06-27 15:56:34 +01:00
Mario Carneiro
bb8cc08de8
chore: compact objects in post-order
2023-06-26 08:35:19 -07:00
Leonardo de Moura
4036be4f50
fix: add missing check at IR checker
2023-06-23 08:43:39 -07:00
Mario Carneiro
123c1ff7f0
fix: basic ident fallback in identComponents
2023-06-22 09:50:24 +01:00
Floris van Doorn
32e93f1dc1
fix: delete Measure and SizeOfRef ( #2275 )
...
* move Measure to Nat namespace
We could (and maybe should) also move various other declarations to namespaces, like measure. However, measure seems to be used a lot in termination_by statements, so that requires other fixes as well. Measure seems to be almost unused
* fix
* delete Measure and SizeOfRef instead
2023-06-21 22:51:28 -07:00
Mario Carneiro
e0893b70e5
fix: incorrect type for SpecInfo.argKinds
2023-06-21 22:50:29 -07:00
Leonardo de Moura
425f42cd83
feat: better support for Nat literals at DiscrTree.lean
2023-06-21 22:30:09 -07:00
Leonardo de Moura
bebf1927f8
chore: remove workarounds
2023-06-21 20:35:33 -07:00
Leonardo de Moura
184f2ed597
chore: improve isNonTrivialProof
2023-06-21 20:28:17 -07:00
Leonardo de Moura
7367f2edc6
fix: unfold constant theorems when transparency is set to .all
2023-06-21 20:28:17 -07:00
Leonardo de Moura
9df2f6b0c9
fix: bump transparency to .all when reducing the major premise of Acc.rec and WellFounded.rec
2023-06-21 20:28:17 -07:00
