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

105 commits

Author SHA1 Message Date
Sebastian Ullrich
eb170d1f43 fix: compiled string literals containing null bytes 2022-05-17 09:24:34 -07:00
Leonardo de Moura
c65537aea5 feat: Option is a Monad again 
TODO: remove `OptionM` after update stage0

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
 2022-05-04 15:27:42 -07:00
Leonardo de Moura
de2e2447d2 chore: style 2022-04-07 17:35:05 -07:00
Leonardo de Moura
85a1a5233b chore: workaround for compiler closed term extraction issue 2022-03-01 09:01:08 -08:00
Leonardo de Moura
4ed5c8405b feat: improve IR checker error messages 2022-02-17 09:51:05 -08:00
Leonardo de Moura
cf3b8d4eb4 chore: cleanup 
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
 2022-01-26 09:18:17 -08:00
Sebastian Ullrich
c59f7a55cf fix: initialize precompiled modules 2022-01-20 18:55:57 +01:00
Leonardo de Moura
9d05023325 chore: remove some [specialize] annotations 2022-01-18 09:24:06 -08:00
Leonardo de Moura
bac91b9b5b chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Leonardo de Moura
b22a3a4cc4 feat: skip code generation for declarations marked with implementedBy, init, and builtinInit 
This is a bit hackish. We should clean up when we rewrite the compiler
in Lean.
 2022-01-14 19:20:16 -08:00
Leonardo de Moura
0e479d1f9f chore: use double ticks 2022-01-03 10:30:05 -08:00
Sebastian Ullrich
ba83721109 chore: add comment for previous fix 2021-12-15 20:10:48 +01:00
Sebastian Ullrich
3c9ea3b113 fix: wait on tasks before Lean program exit 2021-12-15 15:58:24 +01:00
Leonardo de Moura
68bd55af32 chore: fix codebase 2021-12-10 13:12:09 -08: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
8ec9fda6c4 fix: improve widening operator used at the ElimDeadBranches abstract interpreter 2021-10-06 12:54:07 -07:00
Sebastian Ullrich
35ffae6f54 feat: Windows: explicitly export Lean functions only 2021-09-20 18:41:46 +02:00
Leonardo de Moura
53ec43ff9b refactor: lazy evaluation for >>, <*>, <*, and *> 
see issue: #617
 2021-09-07 17:50:34 -07:00
Sebastian Ullrich
07d1735ea2 feat: borrow inference: preserve mutual tail calls 
Fixes #603
 2021-08-05 06:26:06 -07:00
Sebastian Ullrich
e1703bf1ae fix: main return value on 32-bit 
Resolves #594
 2021-08-03 11:00:10 -07:00
Wojciech Nawrocki
a937fa26ba chore: fewer explicit types 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
f51b80060d feat: generic tagged Format 2021-08-01 09:58:44 +02:00
Leonardo de Moura
2018dc0959 fix: disable panic messages during initialization 
This is a temporary workaround until we implement #467.
Fixes #534
 2021-06-29 14:48:48 -07:00
Leonardo de Moura
d8210cd682 feat: mark auxiliary C constants used to store closed terms as static 
This is a workaround to minimize the number of exported symbols in the
Lean executable.
See issues #466 and PR #515
 2021-06-06 18:56:31 -07:00
Leonardo de Moura
37da993032 chore: remove HashableUSize instances 2021-06-02 08:48:11 -07:00
Leonardo de Moura
43812444a7 chore: Hashable => HashableUSize 2021-06-02 07:24:26 -07:00
Leonardo de Moura
6a87bba9c0 chore: mixHash => mixUSizeHash 2021-06-02 07:05:42 -07:00
Daniel Fabian
0238bf8c33 refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Leonardo de Moura
d9273786c7 chore: remove when and «unless» 
They are obsolete.

cc @Kha
 2021-03-20 18:52:18 -07:00
Leonardo de Moura
9a5f239513 refactor: remove Monad Option and Alternative Option 
We should use `OptionM` instead.
`Option` still implements `Functor` and `OrElse`.

cc @Kha
 2021-03-20 18:25:25 -07:00
Leonardo de Moura
51200c916e chore: make explicit user and internal panics 2021-03-04 07:37:33 -08:00
Leonardo de Moura
cf5adbd4fe chore: increase LEAN_MAX_SMALL_OBJECT_SIZE and simplify code 2021-01-30 10:58:34 -08:00
Leonardo de Moura
d71aab5dc4 fix: allow bigger ctor objects 
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
 2021-01-29 18:23:38 -08:00
Leonardo de Moura
31680c1255 fix: do not evaluate code containing sorry 
closes #277
 2021-01-26 15:01:53 -08:00
Leonardo de Moura
72a8fb84b5 feat: add IR.DeclInfo 2021-01-26 12:41:07 -08:00
Leonardo de Moura
0672247ce8 chore: make comments VS Code friendly 2021-01-15 13:53:37 -08:00
Mateja Petrovic
00b11f267a
chore: typos 2021-01-10 22:42:54 +01:00
Leonardo de Moura
78aa3d8e72 chore: use deriving BEq 2020-12-22 18:10:20 -08:00
Leonardo de Moura
3b6d65c3c3 chore: use deriving Inhabited 2020-12-13 10:09:20 -08:00
Sebastian Ullrich
8088145da8 chore: remove obsolete code 2020-12-10 17:15:55 +01:00
Leonardo de Moura
f14826a730 fix: incorrect context used at addDecForDeadParams 2020-12-08 12:38:33 -08:00
Leonardo de Moura
2ebee8d00c fix: missing addJP 2020-12-08 12:09:52 -08:00
Leonardo de Moura
ae5aa51712 chore: add explicit discard 2020-12-08 06:18:18 -08:00
Sebastian Ullrich
2a5c85d9e3 refactor: inline FormatMacro 
@leodemoura: This was just a remnant of the initial frontend porting, correct?
 2020-11-28 12:37:36 +01:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
d6f778bec4 refactor: arbitrary without explicit arguments 
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
 2020-11-25 09:07:38 -08:00
Leonardo de Moura
f67c93191f feat: use |>. 2020-11-19 08:38:47 -08:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
ffc4abed32 fix: UInt* and USize Inhabited instances 2020-11-13 16:30:48 -08:00
Leonardo de Moura
f17e226638 chore: naming convention 
Example: `mkNameStr` => `Name.mkStr`

cc @Kha
 2020-11-11 10:08:55 -08:00