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

26228 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
d3cf0b8098 fix: deriving Ord on parameterized types 
Fixes #732
 2021-10-18 10:08:13 +02:00
Wojciech Nawrocki
e843fb7ca5 fix: widget messages 2021-10-17 10:01:23 +02:00
tydeu
b1bd3fc304 chore: update Lake 2021-10-15 17:12:29 +02:00
Siddharth Bhat
3374806d0f refactor: eliminate unused ExtractMonadResult.hasBindInst 2021-10-15 06:57:24 -07:00
Sebastian Ullrich
c2c418b651 chore: update Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
08dbf239a6 chore: server: redundant let 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
7fdc208c1f chore: update Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
7372e2f6cd chore: update Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
7a91c494b9 chore: submodule hints 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
74b813fbcd doc: restructure make/index.md 
debug builds are not very interesting currently given the state of
debugging Lean code
 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
6296151034 chore: update Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
e67e096086 fix: patch bin/lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
674e473c84 feat: server: support LAKE env var 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
e422ce4917 chore: update Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
6a1897302b chore: server: use exit code to communicate absence of package 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
765ed37409 feat: server: support Lake 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
89f9045646 test: add lake tests 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
524be36d23 feat: build & bundle Lake 2021-10-15 06:56:02 -07:00
Chris Lovett
f57e61fead
chore: remove manual shell scripting for compiling libleanrt 2021-10-15 08:08:31 +02:00
Siddharth
66fcfcce37
doc: tutorial on parsing the arithmetic grammar using macros 
* add arith

* Fixup based on Sebastian's feedback

* style nits

* add explanation about parsing precedence

* add Sebastian's suggest test case

Add the test case into the example to make sure we parse a*b+c as well
as a+b*c correctly.

* grammar pass

* Update doc/tutorial/metaprogramming-arith.md

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

* Update doc/tutorial/metaprogramming-arith.md

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

* use pretty arrows, 2 spaces, [Arith| ... ]

* typo: :+ and :* had sneaked back in

* Update doc/tutorial/metaprogramming-arith.md

Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>

* Update doc/tutorial/metaprogramming-arith.md

Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>

* Update doc/tutorial/metaprogramming-arith.md

Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>

* Update doc/tutorial/metaprogramming-arith.md

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* move all #print to #check

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2021-10-12 08:51:17 +02:00
Gabriel Ebner
d6ba8e597a feat: add range parameter to getInteractiveDiagnostics 2021-10-11 22:59:47 +02:00
Sebastian Ullrich
e068833e8d fix: register missing simp trace classes 2021-10-11 15:37:56 +02:00
Leonardo de Moura
48a40c4d0a fix: quoteString at EmitC.lean 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20escaping.20of.20.5Cr.20.3F/near/257061704
 2021-10-11 06:16:56 -07:00
Leonardo de Moura
002fb7f446 fix: make sure pattern is tried on partial applications 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256939753
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
04fae18fe4 fix: make sure stop conv pattern stop at first match 2021-10-10 15:47:04 -07:00
Leonardo de Moura
e8bdb66dda fix: make sure we can match pattern inside binders 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256890867
 2021-10-10 15:47:04 -07:00
Chris Lovett
2860ba96f5
doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02:00
Sebastian Ullrich
8d10197164 fix: leanpkg print-paths with longer output 2021-10-10 11:25:11 +02:00
Leonardo de Moura
fb27537b8e fix: appUnexpander name resolution 
fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Scoping.20for.20delaborator.3F
 2021-10-09 08:29:26 -07:00
Sebastian Ullrich
2ab8a38daa fix: macOS build, once more 2021-10-09 10:24:30 +02:00
Sebastian Ullrich
1f1dc0b471 fix: macOS Nix build 2021-10-08 21:46:50 +02:00
Gabriel Ebner
34eda689a1 fix: use eraseMacroScopes on trace classes 2021-10-08 11:13:19 -07:00
Leonardo de Moura
d77c99bd2f chore: update stage0 2021-10-08 09:37:47 -07:00
Leonardo de Moura
81729d96f9 fix: make sure Quot primitives stay in eta expanded form 
fixes #716
 2021-10-08 09:36:06 -07:00
Leonardo de Moura
15ac3c2542 test: small repro for issue #716 2021-10-08 09:36:06 -07:00
Sebastian Ullrich
89d6c70273 fix: macOS build 2021-10-08 18:34:28 +02:00
Sebastian Ullrich
c8b998a607 chore: update stage0 2021-10-08 17:11:30 +02:00
Sebastian Ullrich
0a43a9c466 refactor: use JSON to communicate between server & package manager 2021-10-08 11:28:04 +02:00
Leonardo de Moura
305d035f17 chore: use lean_always_assert at erase_irrelevant.cpp 
The performance impact should be insignificant, and it should help
debugging issue https://github.com/leanprover/lean4/issues/716
 2021-10-07 07:44:56 -07:00
Sebastian Ullrich
db755b6081 doc: temp fix 
/cc @leodemoura
 2021-10-07 12:59:14 +02:00
Sebastian Ullrich
4ac9873880 fix: update-stage0 2021-10-07 12:55:55 +02:00
Leonardo de Moura
b742f0005f chore: fix test 2021-10-06 19:58:29 -07:00
Leonardo de Moura
697e0ce2db feat: apply cleanup tactic before applying decreasing tactic 
Alternative design: apply it only before reporting a failure.
 2021-10-06 19:56:57 -07:00
Leonardo de Moura
91d2f6d4fc feat: add cleanup tactic 2021-10-06 19:54:28 -07:00
Leonardo de Moura
c02b4f2675 refactor: move to Meta namespace 2021-10-06 19:05:37 -07:00
Leonardo de Moura
def7641926 feat: add helper methods for checking dependencies 2021-10-06 19:04:02 -07:00
Leonardo de Moura
f10101cd58 fix: preserve user variable names in decreasing goals 2021-10-06 18:45:48 -07:00
Leonardo de Moura
85150731b7 test: put unit back, but rename it to someVal 
It is the simple and more efficient.
We just set `someVal` with the first value of `vars`.
Recall that `vars` is never empty.
 2021-10-06 18:09:06 -07:00
Leonardo de Moura
f64753c106 test: simplify ac_expr.lean 
We don't want to avoid proofs at `List.getIdx` and `Expr` when doing proofs by reflection.
The new encoding avoids that by using the fact that `vars` in
`Context` should never be empty.

To be honest, the best approach is still the old `unit`. We can just
rename it to `inhabitant` to make sure users don't assume it is the
unit of the AC operator. Then, we can just set it with the first element
of `vars` and avoid proofs at `denote`.
 2021-10-06 17:56:26 -07:00
Leonardo de Moura
079ad47f02 fix: mixed unary and non-unary functions 2021-10-06 17:33:51 -07:00