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

8362 commits

Author SHA1 Message Date
Leonardo de Moura
d50da0feb7 feat(library/tactic/induction_tactic): add support for ginductive in the induction tactic 2017-03-04 14:55:35 -08:00
Leonardo de Moura
c456bceafa feat(library/tactic/cases_tactic): remove m_dep_elim since we are now always using dependent eliminators 2017-03-04 14:35:42 -08:00
Leonardo de Moura
22988bb95d feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator 
TODO: make sure the user is not manually using cases_on for the
auxiliary datatype generated by the inductive_compiler to
destruct nested inductives.
 2017-03-04 13:54:44 -08:00
Leonardo de Moura
060d6b66b2 fix(library/inductive_compiler/ginductive): incorrect assertion 2017-03-04 13:31:34 -08:00
Leonardo de Moura
b74740648e fix(library/tactic): fixes #1414 2017-03-03 20:50:00 -08:00
Daniel Selsam
4e1967c242 feat(inductive_compiler): is_pack and is_unpack API 2017-03-03 20:39:47 -08:00
Daniel Selsam
dc5b57bff6 fix(inductive_compiler/ginductive.cpp): populate new fields of entry 2017-03-03 20:39:39 -08:00
Daniel Selsam
616a4ce5c5 fix(inductive_compiler/ginductive.cpp): debug code did not compile 2017-03-03 20:39:27 -08:00
Daniel Selsam
e9c05f727c feat(inductive_compiler): APIs for simulated constructor offsets 2017-03-03 12:43:48 -08:00
Leonardo de Moura
d9da6f05b5 fix(library/tactic/cases_tactic): issue reported by @johoelzl at slack 2017-03-02 18:00:55 -08:00
Daniel Selsam
5ef892bb45 feat(inductive_compiler): cases_on for mutual and nested 2017-03-02 16:08:00 -08:00
Daniel Selsam
9590f2b7d0 feat(inductive_compiler): support nested inductive propositions 2017-03-02 16:01:45 -08:00
Leonardo de Moura
259d9271ab fix(library/equations_compiler): use ginductive API 
fixes #1334
 2017-03-02 15:48:03 -08:00
Leonardo de Moura
6b3e651de7 fix(library/util): get_datatype_level should not assume inductive datatype result type is a sort 
It may be something that is reducible to a sort.
 2017-03-02 11:42:16 -08:00
Leonardo de Moura
b1848efbc4 chore(library/init/meta): add head prefix to head reduction tactics, and add zeta tactic (that applies zeta reduction to all subterms) 2017-03-02 10:55:38 -08:00
Sebastian Ullrich
b9dc1c251e fix(library/inductive_compiler/ginductive_decl): assertion 2017-03-02 08:02:55 -08:00
Sebastian Ullrich
852df8872b fix(library/constructions/drec): assertion 2017-03-02 08:01:38 -08:00
Daniel Selsam
1f6306d068 perf(library/inductive_compiler): simplification with sizeof lemmas 2017-03-01 21:13:20 -08:00
Johannes Hölzl
f44cbb896c fix(src/library/equations_compiler/elim_match): handle mixing of inaccessible terms and variables 2017-03-01 21:12:42 -08:00
Leonardo de Moura
1542cd750f feat(library/tactic/induction_tactic): use drec in the induction tactic 
The new test failed before this change.
 2017-03-01 18:34:24 -08:00
Leonardo de Moura
e9f18502a7 chore(library/user_recursors): add drec_on and dcases_on 2017-03-01 15:56:06 -08:00
Leonardo de Moura
1ded3b70b8 feat(library/constructions/drec): add dcases_on 2017-03-01 15:46:19 -08:00
Leonardo de Moura
132a629eb7 fix(library/tactic/induction_tactic): use whnf when inferring C.rec name 2017-03-01 14:29:26 -08:00
Leonardo de Moura
7b0a18167b feat(library/constructions/drec): add drec_on and refactor 2017-03-01 14:12:10 -08:00
Leonardo de Moura
5fa7d765ac chore(emacs/lean-server): remove leftover from experiment 2017-02-28 22:57:20 -08:00
Leonardo de Moura
17556758cb feat(library/constructions,library/inductive_compiler): automatically generate dependent eliminator for inductive predicates 
The dependent eliminator for an inductive predicate C is called C.drec

TODO: construct dcases_on and drec_on using C.drec

We need this recursor for implementing dependent elimination for
inductive predicates.

We don't need to define acc.drec and eq.drec in the standard library anymore.
 2017-02-28 20:58:04 -08:00
Leonardo de Moura
cad379333d feat(util/memory_pool): put limit on the size of memory_pool free_lists 
See #1405

Memory consumption is still high, but I didn't manage to cross the 2Gb
limit anymore with this commit even after hundreds of modifications.

@gebner I'm not seeing a big difference betwee Lean without memory_pool,
with bounded memory_pool and unbounded memory_pool. We may even consider
removing it in the future after a more careful benchmarking.

In the benchmark (https://gist.github.com/leodemoura/b27fb4203a13a67274b388a602149303),
I'm getting the following numbers:

- No memory_pool: runtimes between 3.532s - 3.556s

- With memory_pool bounded by 8192: runtimes between 3.32s - 3.44s

- With memory_pool (with no limit): runtimes between 3.32s - 3.44s

On the other hand, the small object allocator makes a big difference.
I used your list_rev.lean example.

- with:    2.62s
- without: 3.75s
 2017-02-28 15:16:43 -08:00
Leonardo de Moura
1fa1312c57 chore(CMakeLists,frontends/lean): add SAVE_SNAPSHOT=OFF SAVE_INFO=OFF compilation options 2017-02-28 12:09:19 -08:00
Gabriel Ebner
f5ae60e667 feat(init/init): write allocation stats to stderr 2017-02-28 11:56:52 -08:00
diakopter
cbaf060a80 chore(library): override warning 2017-02-28 11:24:21 -08:00
Leonardo de Moura
db5b709d9c feat(CMakeLists,util): add CUSTOM_ALLOCATORS=OFF compilation option 2017-02-28 11:13:54 -08:00
Leonardo de Moura
544d5c67f4 feat(CMakeLists,kernel): add TRACK_LIVE_EXPRS=ON compilation option 2017-02-28 10:56:14 -08:00
Leonardo de Moura
ba641ce29f feat(CMakeLists,util): add TRACK_CUSTOM_ALLOCATORS=ON compilation option 2017-02-28 10:38:09 -08:00
Leonardo de Moura
1da93c4d28 feat(CMakeLists, shell/lean): add -D ALPHA=ON cmake option for enabling alpha features (i.e., wip) 
@jroesch This commit also marks --compile as an alpha feature.
 2017-02-26 23:06:45 -08:00
Leonardo de Moura
2386c18ee5 fix(library/tactic/eval): make sure old position information nested in the expression being evaluated is not used in type error messages 
see #1401
 2017-02-26 22:38:24 -08:00
Leonardo de Moura
184d505d51 fix(library/compiler/preprocess): do not unfold noncomputable definitions in the compiler 
see #1401
 2017-02-26 22:05:16 -08:00
Leonardo de Moura
d7674dd060 chore(CMakeLists): bumped master branch to 3.1.1 2017-02-25 18:12:04 -08:00
Gabriel Ebner
fcc0f30b84 fix(frontends/lean/definition_cmds): set scope_pos_info when checking examples 2017-02-25 12:56:46 -08:00
Leonardo de Moura
52221cdbd1 fix(frontends/lean/elaborator): {} elaboration issue 2017-02-24 21:20:39 -08:00
Gabriel Ebner
7e3be51a52 chore(*): remove last remnants of mpfr 2017-02-24 21:42:58 +01:00
Gabriel Ebner
9bcfc06bd0 fix(library/module): has_sorry: check examples 2017-02-24 21:08:49 +01:00
Leonardo de Moura
552a185e6a feat(frontends/lean): 'let' in 'do' blocks 2017-02-24 09:10:36 -08:00
Sebastian Ullrich
dd379e5b34 refactor(library/equations_compiler/elim_match): simplify is_complete_transition 2017-02-23 01:52:14 +01:00
Sebastian Ullrich
dfe1874365 refactor(frontends/lean/{parser,util}): extract quote functions 
Also fixes ``f when f is private
 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
1c7ca3f20a feat(frontends/lean/parser): ignore implicit arguments in expr patterns 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
44b27a9a44 chore(library/vm/vm): fix comment 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3 feat(frontends/lean/parser): expr patterns 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
3aa9e32c5f fix(library/equations_compiler/elim_match): always prefer value transitions over complete transitions 2017-02-23 01:21:14 +01:00
Leonardo de Moura
6b76b65881 feat(library/equations_compiler/elim_match): change default max number of steps to 2048 2017-02-21 21:33:10 -08:00
Leonardo de Moura
d9307413b9 feat(library/compiler): skip bytecode optimization for interactive tactics 
This is just overhead for begin...end blocks.
Moreover, "live variable analysis" is currently a recursive
procedure, and Lean will run of stack space when processing big begin
end blocks (> 1000 tactics).
 2017-02-21 21:23:58 -08:00