Leonardo de Moura
40a0465cca
chore(library/tactic/simp_lemmas): fix typo
2018-02-21 15:04:18 -08:00
Leonardo de Moura
02231477f9
chore(library/tactic/ac_tactics): simplify cache management
2018-02-21 15:04:18 -08:00
Leonardo de Moura
bf4d47b560
chore(library/cache_helper): remove dead code
2018-02-21 15:04:18 -08:00
Leonardo de Moura
9e08cab381
chore(library/type_context): simplify cache management
2018-02-21 15:04:18 -08:00
Leonardo de Moura
da032ccc3b
feat(library/init/data/nat/lemmas): add lemma for termination proofs
2018-02-21 10:37:07 -08:00
Leonardo de Moura
afb65f3d3d
feat(library/init/meta/comp_value_tactics): add comp_val interactive tactic
2018-02-21 10:35:26 -08:00
Leonardo de Moura
61930c3d85
fix(library/init/meta/comp_value_tactics): instantiate metavars
2018-02-21 10:28:27 -08:00
Leonardo de Moura
bddc84664c
chore(library/init/data/nat): remove pow.lean
2018-02-20 13:50:23 -08:00
Leonardo de Moura
3f04d041f6
chore(library/time_task): style
2018-02-19 10:30:49 -08:00
Sebastian Ullrich
0c23dab452
chore(script/lib_perf): make interruptible and fix uninitialized variable
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
f247363305
feat(library/time_task): print cumulative times on --profile
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
b206b3bedf
chore(util/timeit): make xtimeit non-copyable
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
782af7e5d6
chore(library/vm/interaction_state): do not profile calls into Lean other than tactic execution
...
Otherwise, we produce a message for e.g. every single interactive tactic parameter
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
9c5df7875a
perf(frontends/lean/elaborator): visit_structure_instance_fn: delay building error message
2018-02-19 09:13:24 -08:00
Leonardo de Moura
56dba5b98a
fix(frontends/lean/elaborator): fixes #1930
...
@kha the following idiom is not safe
```
while (is_pi(t)) {
t = whnf(binding_body(t));
}
```
`whnf(e)` assumes that `e` does not have dangling deBruijn variables.
We should use (the more expensive):
```
while (is_pi(t)) {
t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
}
```
BTW, this problem is not related to the assertion violation at #1930
I just stumbled on it when fixing the violation.
2018-02-19 08:51:26 -08:00
Leonardo de Moura
dbfcc65c60
fix(library/compiler/erase_irrelevant): erase_type
2018-02-19 07:55:43 -08:00
Sebastian Ullrich
a7afedc5c3
chore(.appveyor.yml): fix core update
...
See https://github.com/Alexpux/MSYS2-packages/issues/1141
2018-02-17 22:18:02 +01:00
Leonardo de Moura
aa24c15e61
feat(library/vm): basic performance counters
...
@kha I have added a few performance counters.
I collect their values at each snapshot.
Right now, I am printing only the values in the last snapshot, but if we want
we can even display their progress over time.
Right now, I track the following information
- number of allocated closures
- number of allocated constructors/objects
- number of allocated big numbers
2018-02-16 14:37:11 -08:00
Nuno Lopes
3bb1366b39
chore(api): remove unneeded #include
2018-02-16 12:19:20 -08:00
Leonardo de Moura
3666fac95a
chore(util/parser_exception): avoid thread local storage
2018-02-16 12:12:56 -08:00
Leonardo de Moura
c35f2a2098
chore(library/io_state): avoid thread local storage
2018-02-16 12:12:50 -08:00
Leonardo de Moura
a076f0003d
chore(util/exception): avoid thread local storage
...
The overhead of creating the message eagerly should be really small.
These exceptions are seldom thrown.
2018-02-16 12:12:44 -08:00
Leonardo de Moura
e023b1001a
fix(library/system/random): bug at rand_nat
2018-02-16 11:20:43 -08:00
Leonardo de Moura
96fab5172f
perf(library/compiler): apply lambda lifting after erase trivial structures
...
cc @kha
2018-02-15 16:55:27 -08:00
Leonardo de Moura
a115a1538b
chore(library/vm/vm_io): style
2018-02-15 16:25:17 -08:00
Leonardo de Moura
1c9648a12d
chore(library): remove dead constants
2018-02-15 16:17:43 -08:00
Leonardo de Moura
ac13f8b0f9
feat(library/system/io): add random number generator support in the io monad
...
@aqjune @nunoplopes: See new tests at tests/lean/run/random.lean
We have two actions in `io`. By default, `io` uses the C++
random number generator, but we can force it to use a `std_gen` with
the action `set_rand_gen`.
def rand (lo : nat := std_range.1) (hi : nat := std_range.2) : io nat
def set_rand_gen : std_gen → io unit
2018-02-15 16:12:08 -08:00
Leonardo de Moura
ddfbaa6c8d
fix(library/init/data/nat/basic): missing lemma
2018-02-15 14:36:28 -08:00
Leonardo de Moura
f786d21b0f
feat(library/system): basic support for random numbers
...
@aqjune @nunoplopes: This commit adds basic support for random numbers.
It defines a random number generator interface, and an basic
implementation based on the Haskell one.
We can add more implementations in the future if neeeded.
The new test program has a few examples.
BTW, this is a pure Lean implementation.
If we need more performance we can provide an implementation
using C++.
2018-02-15 14:36:28 -08:00
Leonardo de Moura
f048da4c98
refactor(library/init/data): replace char.zero_lt_d800 proof
...
See issue https://github.com/leanprover/tc/issues/8
cc @dselsam
2018-02-15 14:36:28 -08:00
Scott Morrison
0e6f496b8e
chore(README.md) fixing link to download page
2018-02-15 11:36:12 +01:00
Mario Carneiro
57934479ef
refactor(algebra/ordered_field): move theorems from discrete
...
The theorems themselves are unchanged, although the proofs had to be reordered and changed a bit to accomodate.
Conflicts:
library/init/algebra/ordered_field.lean
2018-02-13 10:51:50 -08:00
Scott Morrison
5d094cf835
cleanup(init/meta/tactic) removing obsolete meta constants
2018-02-13 10:45:04 -08:00
Nuno Lopes
1a9962011d
chore(style): fix cast style
2018-02-13 10:42:08 -08:00
Nuno Lopes
7b45d28e77
chore(unicode): use utf8 chars directly in strings
2018-02-13 10:42:08 -08:00
Nuno Lopes
c43ebd8bf7
fix(msvc): remove another \uXX char that was causing an infinite loop
2018-02-13 10:42:08 -08:00
Nuno Lopes
977e11f9be
fix(warnings): fix warnings on VS. its now /W2 clean
2018-02-13 10:42:08 -08:00
Nuno Lopes
a9078dd13a
fix(doc): link to MSVC build instructions
2018-02-13 10:40:53 -08:00
Leonardo de Moura
96e02613fc
fix(library/compiler/simp_inductive): erase trivial structure bug
2018-02-11 11:43:05 -08:00
Leonardo de Moura
30cfcc0fa6
fix(library/compiler/inliner): missing reduction
2018-02-11 09:28:42 -08:00
Sebastian Ullrich
affe3463ab
fix(frontends/lean/elaborator): fix assertion error: accidental mutation of a variable
2018-02-08 14:07:08 +01:00
Sebastian Ullrich
5736fda1ee
chore(frontends/lean/elaborator): do not name mvars from { .. } catchall
...
We already use the same names for the field mvars, which can be confusing during debugging
2018-02-08 14:04:33 +01:00
Leonardo de Moura
3771748b4c
chore(library/native): remove dead code
...
The deleted code was not finished, and we are going to add a new IR
and compiler.
2018-02-07 17:29:25 -08:00
Nuno Lopes
d01e2d7ae8
fix(msvc): change previous MSVC workaround to change the code less
2018-02-06 10:11:10 -08:00
Nuno Lopes
9c756e24d3
fix(crash) due to calling isalpha with signed char in get_indentatnion()
2018-02-06 10:11:10 -08:00
Nuno Lopes
5cee9f8279
fix(crash) due to calling isalpha/isalnum with signed char in is_id_first() and is_id_rest()
2018-02-06 10:11:10 -08:00
Nuno Lopes
1e03151412
fix(msvc): compiler warning
2018-02-06 10:11:10 -08:00
Nuno Lopes
c01c49d33f
fix(msvc): compile with multi-thread libraries when needed
2018-02-06 10:11:10 -08:00
Nuno Lopes
6c9d77c6fc
fix(msvc): compile with /Zc:implicitNoexcept- to avoid a few hundred warnigns
2018-02-06 10:11:10 -08:00
Nuno Lopes
02d254e25c
build(msvc): disable shared libraries; not working at the moment
2018-02-06 10:11:10 -08:00
