Leonardo de Moura
3d01327129
chore: remove unnecessary do
2021-01-26 12:41:07 -08:00
Sebastian Ullrich
11e55bf4af
chore: Nix: update Nix client to resolve https://github.com/NixOS/nix/issues/4469
2021-01-26 18:01:39 +01:00
Leonardo de Moura
9d0edab6c3
chore: add issue 297 examples
...
The stack overflow reported on this issue has already been fixed.
closes #297
2021-01-26 08:07:41 -08:00
Sebastian Ullrich
1cfc4cecc1
feat: lean4-mode: lean4-refresh-file-dependencies (C-c C-d)
2021-01-26 12:14:40 +01:00
Sebastian Ullrich
1945ebd275
feat: delaborate sorryAx
2021-01-26 12:08:25 +01:00
Leonardo de Moura
bb3a1a9699
chore: fix comment
2021-01-25 17:29:23 -08:00
Leonardo de Moura
f27ae71231
chore: fix test
2021-01-25 17:22:20 -08:00
Leonardo de Moura
f2f4fdfeb7
feat: first part of the sizeOf spec lemmas for nested inductive types
2021-01-25 17:18:08 -08:00
Leonardo de Moura
fdab5ca835
feat: add helper methods whnfR and whnfI
2021-01-25 17:18:08 -08:00
Leonardo de Moura
0da83dc4ae
feat: add unfoldDefinition
2021-01-25 17:18:08 -08:00
Leonardo de Moura
54168b9070
chore: remove unnecessary MonadLiftT
2021-01-25 17:18:08 -08:00
Leonardo de Moura
7492254353
feat: add natAdd? recognizer
2021-01-25 17:18:08 -08:00
Leonardo de Moura
be7ddef689
refactor: move congr and congrFun to Prelude.lean
...
We use them to generate the `sizeOf` lemmas.
2021-01-25 17:18:08 -08:00
Sebastian Ullrich
e4926e4b14
feat: generalize leanpkg build
2021-01-25 17:07:08 -08:00
Sebastian Ullrich
ae348cd8e1
doc: more about Lean packages
2021-01-25 17:07:08 -08:00
Reid Barton
ccc09d9cbf
chore: fix typo
...
invalide -> invalid
2021-01-25 13:55:39 -08:00
Leonardo de Moura
d408c835d2
fix: defaultInstance priorities for Neg Int and OfScientific Float
2021-01-25 13:21:07 -08:00
Leonardo de Moura
b575087859
fix: unfold class projections when using TransparencyMode.instances
2021-01-25 12:30:26 -08:00
Leonardo de Moura
8bb7cc10ff
chore: cleanup
2021-01-25 11:33:48 -08:00
Sebastian Ullrich
5fea8fcba3
fix: statically link GMP into leanpkg if STATIC=ON
2021-01-25 15:24:16 +01:00
Sebastian Ullrich
38819ef6ea
doc: more on Unicode symbols in LaTeX
2021-01-25 12:44:03 +01:00
Sebastian Ullrich
f9a696fc72
doc: update LaTeX highlighting section
2021-01-25 11:44:49 +01:00
Sebastian Ullrich
ddabe1aa6f
chore: alternative fix to 15185a1
2021-01-25 10:34:34 +01:00
Leonardo de Moura
4848533717
fix: make sure we have "heartbeats" even when `-D SMALL_ALLOC=OFF"
2021-01-24 19:42:45 -08:00
Leonardo de Moura
da5d46cd5d
fix: memory access violation
2021-01-24 18:21:20 -08:00
Leonardo de Moura
83ab2e5555
chore: update stage0
2021-01-24 17:53:36 -08:00
Leonardo de Moura
8bc88bde6b
chore: undefine LEAN_PATH
...
@Kha This doesn't work on my machine. It seems this is a GNU make feature.
2021-01-24 17:52:14 -08:00
Leonardo de Moura
f53e83b182
feat: add options maxHeartbeats and synthInstance.maxHeartbeats
2021-01-24 17:45:50 -08:00
Leonardo de Moura
d834d88b88
fix: performance bottleneck
...
@Kha @dselsam
The instances
```
instance (sep) : Coe (Array Syntax) (SepArray sep)
instance (sep) : Coe (SepArray sep) (Array Syntax)
```
The instances above generate a loop. The current `isNewAnswer`
predicate is too weak and assumes that answers with different
metavariables are different. Note that, using `isDefEq` there is
incorrect and too expensive. I will fix this later in the future.
In the meantime, I am using `CoeTail` to avoid the loop.
2021-01-24 17:45:50 -08:00
Leonardo de Moura
7ff62ee46b
feat: add CoeHTCT
2021-01-24 17:45:50 -08:00
Leonardo de Moura
acfac85ac0
feat: add IO.getNumHeartbeats
2021-01-24 17:45:50 -08:00
Sebastian Ullrich
446f953461
feat: allow hygienic capture of section variables in quotations
2021-01-24 11:46:04 -08:00
Sebastian Ullrich
15185a1775
fix: unset LEAN_PATH before building stdlib
2021-01-24 19:41:16 +01:00
vvs-
b15e770231
fix: crash in IO.Process.wait on 32-bit architecture
...
The implemetation of unbox_uint32 is the same as unbox on 64-bit
but it is different for 32-bit platforms
Fixes #290
2021-01-24 14:37:23 +01:00
Leonardo de Moura
3c631de0d0
chore: update stage0
2021-01-22 14:28:16 -08:00
Leonardo de Moura
51de663e2c
fix: crash when using TransparencyMode.instances
2021-01-22 14:17:19 -08:00
Leonardo de Moura
8f028a41ae
fix: eta-expanded term at levelMVarToParam
...
This issue produced a nested inductive datatype that could not be
handled by the kernel. See new test.
Without the fix, the inductive declaration contained the term
```
((fun α {n : Nat} (t : Vec α n) => ...) Expr n x)
```
The nested occurrence `Vec Expr n` only becomes explicit after
beta-reduction.
2021-01-22 14:17:19 -08:00
Sebastian Ullrich
9aa3b2858f
chore: Nix: search for root directory in lean-dev after all
...
Otherwise `lean4-diff-test-file` will use the Lean version when Emacs was started...
2021-01-22 19:19:37 +01:00
Sebastian Ullrich
2a341c01e0
doc: replace variables
2021-01-22 18:38:49 +01:00
Wojciech Nawrocki
a3f5aca22f
fix: tail-recursive readBinToEnd
2021-01-22 18:02:31 +01:00
Wojciech Nawrocki
d9c6a992b5
feat: specify version in waitForDiagnostics
2021-01-22 18:02:31 +01:00
Wojciech Nawrocki
b9cc6a709f
feat: amortise fileworker restarts and change processing
2021-01-22 18:02:31 +01:00
Wojciech Nawrocki
d5ba10a316
feat: IO API for retrieving monotonic time
2021-01-22 18:02:31 +01:00
Wojciech Nawrocki
8addea6e74
chore: remove Handle.size
2021-01-22 18:02:31 +01:00
Sebastian Ullrich
0c91b3769e
chore: replace variables in src/
2021-01-22 14:36:05 +01:00
Sebastian Ullrich
55102eb548
chore: update stage0
2021-01-22 14:36:05 +01:00
Sebastian Ullrich
8a02dfec4f
feat: subsume variables under variable
...
/cc @leodemoura
2021-01-22 14:36:05 +01:00
Sebastian Ullrich
48f4f6a908
doc: Nix: clarify .#executable command
2021-01-22 12:41:18 +01:00
Leonardo de Moura
7ae861f6bd
test: simplify
2021-01-21 18:32:23 -08:00
Leonardo de Moura
9fb5118990
chore: update stage0
2021-01-21 17:45:55 -08:00
