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

21030 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
51a53cdc19 chore: update stage0 2020-09-14 16:13:31 -07:00
Leonardo de Moura
e66f6cdd6c feat: using indentation 2020-09-14 16:12:23 -07:00
Leonardo de Moura
ca90ff8b59 test: have-by in tactic mode 
@Kha By adding `have-by` macro (in term mode), we got `have-by` in
tactic mode without writing a single line of code :)
 2020-09-14 15:17:25 -07:00
Leonardo de Moura
a6b19cd4af feat: expand show-by and have-by macros 2020-09-14 15:08:28 -07:00
Leonardo de Moura
8586ec1759 chore: update stage0 2020-09-14 15:01:46 -07:00
Leonardo de Moura
c49ccda46a feat: add antiquotation for indentedNonEmptySeq 2020-09-14 14:57:38 -07:00
Leonardo de Moura
05e6a779ba fix: can't use maxPrec at by 
If `by` uses `maxPrec`, then `have A by B ...` is parsed as
`have (A by B) ...` :(

cc @Kha
 2020-09-14 14:57:14 -07:00
Leonardo de Moura
f95675dc22 feat: add have-by and show-by syntax 2020-09-14 14:25:35 -07:00
Leonardo de Moura
fc4ab139b5 feat: indented by 
@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
  have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
  Eq.trans this (by assumption)
```
 2020-09-14 14:20:02 -07:00
Leonardo de Moura
4c6a589e6c feat: indented do blocks 
@Kha it is soooooo much nicer :)
 2020-09-14 13:44:51 -07:00
Leonardo de Moura
163b0a7a3f fix: protected 
- `protected` outside of a namespace is an error.
- Fix `protected` in recursive definitions.

cc @Kha
 2020-09-14 13:09:04 -07:00
Leonardo de Moura
7c0216595e fix: remove duplicate error messages due to variable(s) 
In Lean4, we re-elaborate `variable`(s) for each command, but we don't
want the error messages due to `variable` to appear in the log
multiple times.
 2020-09-14 12:44:25 -07:00
Sebastian Ullrich
f3ab43e453 doc: task_object state machine 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
fce8ca304b fix: reintroduce code that cancels all remaining tasks on task manager shutdown 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
63d60e6564 fix: more robust m_keep_alive implementation not reliant on RC 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
e8a1f36d0c fix: prevent storing ST closure in MT task 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
b214b27557 fix: prevent storing ST value in MT task object 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
e946aa9135 fix: interpreter thread-unsafety 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
a1c17ade3a fix: use-after-free in keep-alive tasks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
ac56a9e79f fix: run tasks to completion on task_manager shutdown to prevent leaks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
fc4428f621 fix: mark Task closures as MT 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
a93a53b4b5 feat: more IO Task functions 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
469a822cc6 chore: checkInterrupted ~> checkCanceled, requestInterrupt ~> cancel 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
77cbaa752c fix: Task: make reference and -j0 semantics eager, simplify 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
5b83ceb1b5 feat: IO.mapTask, IO.bindTask 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
307a833798 feat: implement IO.asTask as primitive using always-run tasks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
1782352af1 feat: optionally run tasks even when already cancelled 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
c672bd657f feat: IO.asTask 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
e14e76775f fix: ensure *println functions are atomic 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
bdea7c7b14 feat: lean: initialize task manager from -j flag 2020-09-14 17:57:33 +02:00
Leonardo de Moura
c3623e9a0a chore: reduce default max steps 2020-09-13 16:18:53 -07:00
Leonardo de Moura
c58252ad74 chore: move more tests to new frontend 2020-09-13 16:13:20 -07:00
Leonardo de Moura
5da7f0b50b fix: set constApprox := false at SynthInstance 
We don't want contraints such as
```
?m a =?= Nat
```
to be solved as
```
?m := fun a => Nat
```
durint type class resolution.
 2020-09-13 16:11:27 -07:00
Leonardo de Moura
21c8366645 chore: fix test output 2020-09-13 13:50:00 -07:00
Leonardo de Moura
2ee1821f13 fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
Leonardo de Moura
32e26799ed chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
Leonardo de Moura
498d7886eb chore: fix test output 2020-09-13 13:21:58 -07:00
Leonardo de Moura
7b90f7d956 fix: synthesize pending mvars before trying coercions to Fun 
`tests/lean/repr_issue.lean` cannot be elaborated with this modification.
 2020-09-13 13:19:05 -07:00
Leonardo de Moura
2de7f1f4d9 doc: possible improvement 2020-09-13 13:16:03 -07:00
Leonardo de Moura
d6a3e22992 chore: add auxiliary function 2020-09-13 13:13:34 -07:00
Leonardo de Moura
fd7dca9bc1 fix: do not cache if term contains Expr-metavariables 2020-09-13 13:13:05 -07:00
Leonardo de Moura
98a8867d90 chore: add coercions for new frontend 2020-09-13 12:00:32 -07:00
Leonardo de Moura
d936b9461f fix: always ensure expectedType when processing overloaded symbols and/or notation 2020-09-13 11:59:13 -07:00
Leonardo de Moura
3493d1871d feat: improve "ambiguous" error message 2020-09-13 11:39:59 -07:00
Leonardo de Moura
c080d42692 chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
Leonardo de Moura
3c2044f06b chore: add coercion for new frontend 2020-09-13 10:12:25 -07:00
Leonardo de Moura
897289599a fix: ignore auxiliary declarations at subst and assumption 2020-09-13 09:59:37 -07:00
Leonardo de Moura
ac6fd1382d fix: collectDeps issue 2020-09-13 09:47:00 -07:00
Leonardo de Moura
d9b4338923 chore: update stage0 2020-09-12 16:50:36 -07:00
Leonardo de Moura
e181c1adee refactor: add DefEqM 
The idea is to make clear that the field `posponed` is transient
state. It is only used during `isDefEq`.
The refactoring was motivated by a bug I found where the `posponed`
constraints were not being handled correctly. For example,
the `check (e : Expr)` method was returning `true`, but leaving pending
universe constraints at `postponed`.

cc @Kha
 2020-09-12 16:42:16 -07:00