Leonardo de Moura
|
91b60cbb22
|
chore: indentation
|
2021-08-04 16:50:57 -07:00 |
|
Leonardo de Moura
|
61cdf93750
|
fix: missing registerMVarErrorImplicitArgInfo
|
2021-08-04 16:09:18 -07:00 |
|
Sebastian Ullrich
|
f5c51ce48c
|
chore: update stage0
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
4b87e69ff5
|
fix: deletion on Windows for real
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
7e2cf59aaf
|
chore: deleting open .olean files on Windows
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
3c91c9e874
|
feat: try memory-mapping .olean files on Windows
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
0aaab9e024
|
chore: remove file_lock.h
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
e4ef665c54
|
feat: atomically (re-)create .olean files
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
2e8075b015
|
chore: raise default profiler.threshold to 100ms
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
88492e38a7
|
chore: CI: run lean --stats src/Lean.lean
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
fbdcaab009
|
feat: show number of mmap-ed modules in --stats
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
5a71a5b18a
|
chore: lean.mk: create .olean atomically
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
05abdf7848
|
perf: move root address of compacted region to the front
for true zero-cost loading
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
4766ee0b5e
|
feat: try to mmap() .olean files on Linux & macOS
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
a00674fcba
|
feat: compute .olean base address from module name
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
4d8da44f50
|
feat: allow specifying virtual base address for compacted region
|
2021-08-04 16:40:57 +02:00 |
|
Sebastian Ullrich
|
c77548c95c
|
fix: accidental truncation of name::hash
|
2021-08-04 16:40:57 +02:00 |
|
Leonardo de Moura
|
2b2311eaa2
|
chore: update stage0
|
2021-08-03 19:53:38 -07:00 |
|
Leonardo de Moura
|
4ca7345956
|
refactor: remove old workaround
|
2021-08-03 19:50:16 -07:00 |
|
Leonardo de Moura
|
4cd7e359df
|
feat: elaborate strict implicit binders
|
2021-08-03 19:40:44 -07:00 |
|
Leonardo de Moura
|
9988264345
|
chore: update stage0
|
2021-08-03 19:13:25 -07:00 |
|
Leonardo de Moura
|
257e38394f
|
feat: add strict implicit binder annotation
|
2021-08-03 19:10:51 -07:00 |
|
Leonardo de Moura
|
64f65d28e7
|
chore: update stage0
|
2021-08-03 18:44:25 -07:00 |
|
Leonardo de Moura
|
d1d7ce1839
|
feat: start support for strict implicit binder annotation
|
2021-08-03 18:42:15 -07:00 |
|
Leonardo de Moura
|
c913886938
|
chore: add private annotations
|
2021-08-03 18:15:39 -07:00 |
|
Leonardo de Moura
|
698ebe0ba8
|
chore: update stage0
|
2021-08-03 17:58:19 -07:00 |
|
Leonardo de Moura
|
68cd66a2b6
|
feat: elaborate visibility modifier at initialization commands
|
2021-08-03 17:56:52 -07:00 |
|
Leonardo de Moura
|
20e07501c4
|
chore: update stage0
|
2021-08-03 14:39:34 -07:00 |
|
Leonardo de Moura
|
f9672fe4c6
|
feat: add optional visibitily modifier to initialize and builtin_initialize commands
|
2021-08-03 14:37:22 -07:00 |
|
Leonardo de Moura
|
01d902f905
|
feat: add register_option command
User-defined options.
|
2021-08-03 14:31:04 -07:00 |
|
Leonardo de Moura
|
526cbfbcd0
|
refactor: add ImportingFlag.lean
|
2021-08-03 14:29:36 -07:00 |
|
Leonardo de Moura
|
65aafc070c
|
chore: remove mkInternalSubobjectFieldName hack
|
2021-08-03 12:05:10 -07:00 |
|
Leonardo de Moura
|
6e1620ca8d
|
refactor: replace IO.Ref with the extern/export hack at MetaM
|
2021-08-03 11:50:57 -07:00 |
|
Sebastian Ullrich
|
e1703bf1ae
|
fix: main return value on 32-bit
Resolves #594
|
2021-08-03 11:00:10 -07:00 |
|
Sebastian Ullrich
|
1dfacb5f84
|
fix: parenthesizer: respect lhsPrec
Fixes #595
|
2021-08-03 15:22:08 +02:00 |
|
Daniel Selsam
|
b8b48b0f72
|
refactor: move FindLevelMVar to Lean/Util
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
0036111db9
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
5a5ed67698
|
refactor: pp.analyze track postponed constraints
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
c0c9d72cc3
|
refactor: pp.analyze put helper in 'where'
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
d56db0a22d
|
doc: pp.analyze one more comment about a failure
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
2afc18323d
|
doc: pp.analyze a few comments about failures
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
f1002cf759
|
feat: delab more thorough 'getParamKinds'
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
652681621a
|
fix: pp.analyze don't type-annotate mdatas
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
d6253e091b
|
fix: pp.analyze _s when forced explicit
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
ea6fca24c2
|
refactor: pp.analyze StateT for analyzeApp
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
be02133ca7
|
feat: pp.analyze default transparency
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
aefd31b2a2
|
feat: better bottom-up/structure-type heuristics
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
ed67bd56e0
|
fix: only unexpand when pp.notation=true
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
4c41142a61
|
chore: pp.analyze new test cases
|
2021-08-03 09:13:18 +02:00 |
|
Daniel Selsam
|
b6be5435cd
|
fix: pp.all should enable binderTypes
|
2021-08-03 09:13:18 +02:00 |
|