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

28475 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
a9cc57c81c chore: CI: more cache setup 2022-06-28 22:31:51 +02:00
Sebastian Ullrich
920fa1109b
chore: CI: ccache permissions 2022-06-28 18:53:36 +02:00
Sebastian Ullrich
9816331562 chore: clean up bootstrapping cleanup 2022-06-28 16:28:36 +02:00
Sebastian Ullrich
995d92d10e chore: CI: fix ccache cache group 2022-06-28 16:24:10 +02:00
Sebastian Ullrich
8f3fda4777 chore: update stage0 2022-06-28 16:01:43 +02:00
Sebastian Ullrich
77c6f433c7 chore: clean up bootstrapping workarounds 2022-06-28 16:01:07 +02:00
Sebastian Ullrich
74c4437874 chore: CI: simplify Nix setup, bring back macOS 2022-06-28 12:50:19 +02:00
Sebastian Ullrich
5bba20d6a9 refactor: revert toParserDescr signature change 2022-06-28 11:50:59 +02:00
Sebastian Ullrich
89a101e9b8 refactor: remove group(·)s 2022-06-28 11:50:59 +02:00
Sebastian Ullrich
9490328429 chore: update stage0 2022-06-28 11:50:59 +02:00
Sebastian Ullrich
eab64997cd fix: auto-group syntax parsers where necessary 2022-06-28 11:50:59 +02:00
Timo
e49a81bb56 doc: fix typo 2022-06-27 19:48:45 -07:00
Leonardo de Moura
34dc2572f3 fix: make sure OfScientific Float instance is never unfolded during type class resolution 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818

Type class resolution was diverging when trying to synthesize
```lean
 HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
 instance : OfScientific Float where
   ofScientific m s e :=
     if s then
       let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
       let m := (m <<< (3 * e + s)) / 5^e
       Float.ofBinaryScientific m (-4 * e - s)
     else
       Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.

Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.
 2022-06-27 17:40:34 -07:00
Sebastian Ullrich
ca19ce1e6f chore: CI: fix Windows 2022-06-28 00:38:19 +02:00
Sebastian Ullrich
18d2296b1c doc: add typed macros to RELEASES.md 2022-06-27 23:42:13 +02:00
Leonardo de Moura
5901fef43a feat: protected aliases 
See message: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/287633118
 2022-06-27 13:56:58 -07:00
Sebastian Ullrich
19c2644d88 chore: add more comments 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
544a046678 chore: use Syntax.Level 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
22475b8669 refactor: introduce common TSyntax abbreviations 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
db42874be4 chore: update Lake 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
e47f248161 doc: TSyntax 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
8b4d8b8dc9 feat: TSyntax singleton kind unexpanders 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
6f7ff3b492 chore: remove unnecessary type annotations 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
6af00ff23e chore: changes to placate coercions 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
d9cfda4893 refactor: make more use of quotations 
Automatically fixes many TSyntax type errors
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
7043c4ebe7 refactor: mkSimpleDelab 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
0b28f059f6 chore: work around "unknown free variable" bug 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
3a56db2812 chore: fix tests 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
c3585dbbbb chore: raw syntax kind accesses 
Sometimes just checking the kind simply is the simplest solution.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
c2166fc602 chore: work around parameterized parser syntax kinds 
We should find a better solution for calling parameterized parsers such
as `matchAlt` than these helper definitions that confuse the antiquotations.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
d499e67c87 fix: incorrect antiquotation kind annotations 
Apparently, none of them led to incorrect syntax trees, but `TSyntax`
still disapproves.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
6c64b1b20b chore: work around for type inference 
It seems type information often flows from the body to the loop
variable, which is problematic with coercions.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
5e334b3e90 chore: postpone TSyntax adoption for some parts 
The namespace `TSyntax.Compat` can be opened for a coercion
`Syntax -> TSyntax k` for any `k`, as otherwise this PR would never be done.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
fe22d84143 fix: unclear TSyntax breakage 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
86cd656fc6 refactor: adapt raw syntax manipulations to TSyntax 
Sometimes there's just no structure to work on
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
498c7a6a97 refactor: remove some unnecessary antiquotation kind annotations 
These are just the ones I stumbled upon, there should be a lot more now
rendered obsolete by the coercions.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
a78302243c refactor: strengthen Syntax signatures 
Most notable change: `Quote` is now parameterized by the target kind.
Which means that `Name` etc. could actually have different
implementations for quoting into `term` and `level`, if that need ever
arises.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
f90e4ae30c feat: more TSyntax API & coercions 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
a12cde41e1 chore: work around macro limitations 
It would be nice if `macro` was as expressive as syntax quotations, but
right now it's not.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
c202a2c013 feat: more antiquotation kinds 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
7bc95d3a95 chore: update stage0 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
9db8bac040 chore: prepare for next stage 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
d50b1aab89 feat: <|> may produce a choice node of antiquotations 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
ab08bffbec chore: Nix: fix stage0-from-input 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
4b78d02a5e fix: do not discriminate anonymous antiquots after all 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
9b71fbb461 chore: default pp.rawOnError to true for stage 0 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
43ba121e98 feat: upgrade TSyntax to union of kinds 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
3a61cc247e chore: introduce doSeq antiquotation 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
330245816c fix: macro: inferred syntax kinds for literal parsers 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
2ef3636022 fix: elaborating category quotations 2022-06-27 22:37:02 +02:00