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

8714 commits

Author SHA1 Message Date
Gabriel Ebner
1b8533130b feat(system/io): add function to get environment variables 2017-05-04 16:41:11 -07:00
Daniel Selsam
b7d20a333f chore(src/library/constants): rm unused constants 2017-05-04 16:34:32 -07:00
Daniel Selsam
d727abeefc chore(library/inductive_compiler/nested.cpp): prove all theorems in C++ 2017-05-04 16:34:32 -07:00
Leonardo de Moura
4c9247d220 test(tests/library/phashtable): another perf test 2017-05-04 16:29:19 -07:00
Leonardo de Moura
9d5dacd554 test(tests/library/phashtable): add tests 2017-05-04 16:18:03 -07:00
Leonardo de Moura
bdf4d69702 feat(library): add persistent hashtable based on parray 2017-05-04 15:35:25 -07:00
Leonardo de Moura
39165ad66b feat(library/parray): add helper methods and exclusive_access helper class 2017-05-04 15:35:14 -07:00
Leonardo de Moura
ae96ebf6ee feat(library/parray): split "long" delta paths 2017-05-03 16:07:49 -07:00
Leonardo de Moura
90e434f78c refactor(library/parray): minor refactoring 2017-05-03 13:44:42 -07:00
Sebastian Ullrich
3c525bef6a fix(frontends/lean/pp): parenthesize Type u where necessary 2017-05-03 13:27:35 -07:00
Sebastian Ullrich
7eb04f0d44 fix(frontends/lean/elaborator): instantiate mvars in [reflected a] params 
Fixes #1562
 2017-05-03 13:27:35 -07:00
Sebastian Ullrich
b37b1fb7c6 refactor(library/type_context,frontends/lean/elaborator): move reflected code back into elaborator 
Since we do not want recursive special handling of `reflected`, this seems to be
the simpler design.
 2017-05-03 13:27:35 -07:00
Leonardo de Moura
6092966702 fix(library/parray): missing desctrutor/constructor invocations at reroot 2017-05-03 13:17:26 -07:00
Leonardo de Moura
97ab603325 feat(library/parray): add ensure_unshared 2017-05-03 12:57:15 -07:00
Leonardo de Moura
2e5702d31e fix(library/parray): it is unsafe to return reference 
A reroot operation performed by another thread may invalidate the reference.
 2017-05-03 10:02:10 -07:00
Leonardo de Moura
a8cc5c4e31 fix(library/parray): race conditions 2017-05-03 09:36:35 -07:00
Gabriel Ebner
c6490be500 chore(vim): remove vim files 
They are now at https://github.com/leanprover/lean.vim
 2017-05-03 18:28:36 +02:00
Leonardo de Moura
a69052e7ee feat(library/parray): add parray thread safe version 
We will use the thread safe version for implementing persistent hash maps.
The hash maps will be used to implement decision procedures and refactor
the congruence closure and ematching modules.
The persistent hash maps based on thread safe parrays are performant
when most of the time there is a single thread updating them.

We use a small hack to make sure we don't have any overhead for

   parray<T, false>

i.e., the thread unsafe version used in the VM.
 2017-05-02 17:15:09 -07:00
Leonardo de Moura
ff916b3a93 chore(library/parray): avoid T m_elem; field at cell 
This was bad since T default constructor would be invoked even when not
needed.
 2017-05-02 16:20:15 -07:00
Leonardo de Moura
915c5c5ad8 chore(library/parray): remove unnecessary conditional 2017-05-02 15:20:42 -07:00
Leonardo de Moura
c3aa1ce444 fix(CMakeLists): install leanpkg 
fixes #1561

@jroesch Could you please check if this patch works on your OSX machine?
 2017-05-02 13:25:55 -07:00
Leonardo de Moura
73b4e42485 chore(frontends/lean,library): fix character pretty printer 2017-05-02 13:17:22 -07:00
Leonardo de Moura
a0a8103804 chore(frontends/lean): go back to 'c' as notation for characters 
This suggestion has been discussed at Slack.
We have decided to use #"c" as notation because we wanted to allow `'`
in the beginning of identifiers like in SML and F*. In particular,
we wanted to allow users to use 'a 'b 'c for naming type parameters
like in SML. However, nobody used this notation. In the Lean standard
library, we are using greek letters for naming type parameters.
So, there is no real motivation for the ugly #"c" syntax.
 2017-05-02 13:00:51 -07:00
Leonardo de Moura
f64b3cb874 chore(frontends/lean): do not allow identifiers starting with ' 2017-05-02 10:43:44 -07:00
Sebastian Ullrich
1102234932 fix(frontends/lean/elaborator): guard against unexpected sorry macro 
Fixes #1559
 2017-05-02 13:57:16 +02:00
Sebastian Ullrich
07b1cfb268 fix(frontends/lean/structure_cmd): do not combine field default overrides and parent field short-hands 
Fixes #1557
 2017-05-02 13:42:15 +02:00
Leonardo de Moura
55fee26b36 feat(library/class): add attribute for tracking symbols occurring in instances of type classes 
For more information see:
https://github.com/leanprover/lean/wiki/Refactoring-structures
The new attribute [algebra] implements the [algebraic_class] described
in the page above.
 2017-05-01 18:02:30 -07:00
Daniel Selsam
8b8814cfbe fix(frontends/lean/inductive_cmd.cpp): fixes #1525 2017-05-01 14:57:25 -07:00
Gabriel Ebner
d33df6a063 fix(emacs): reduce refresh rate for task overlays 2017-05-01 14:11:39 -07:00
Gabriel Ebner
40fc254760 feat(emacs/lean-server): reduce delays 2017-05-01 14:11:39 -07:00
Gabriel Ebner
44bfceb6a6 feat(library/process): support working directory on windows 2017-05-01 14:11:39 -07:00
Gabriel Ebner
c14221f6d4 chore(CMakeLists): add target to build olean files for leanpkg 2017-05-01 14:11:39 -07:00
Gabriel Ebner
acb03fb704 feat(shell): emscripten build with webassembly 2017-05-01 14:11:39 -07:00
Gabriel Ebner
f14763b777 fix(library/module_mgr): fall back to olean if lean does not exist 2017-05-01 14:11:39 -07:00
Gabriel Ebner
dc4337779a fix(util/lean_path): fix emscripten build 2017-05-01 14:11:38 -07:00
Gabriel Ebner
3810e8950d refactor(util/lean_path,util/path): separate search path functions 2017-05-01 14:11:38 -07:00
Gabriel Ebner
504a198517 feat(emacs): support leanpkg.path files 2017-05-01 14:11:38 -07:00
Gabriel Ebner
c8bb77a3df fix(emacs): demote errors 2017-05-01 14:11:38 -07:00
Gabriel Ebner
d79909a1b8 refactor(util/lean_path): support leanpkg.path files 2017-05-01 14:11:38 -07:00
Gabriel Ebner
baa4c48f1f refactor(util/lean_path): explicitly pass around search path 2017-05-01 14:11:38 -07:00
Leonardo de Moura
ba5eccdca8 refactor(library/init/core): rename out_param => inout_param 
It is really input/output.
 2017-05-01 14:01:41 -07:00
Leonardo de Moura
74550fbebc feat(library/init/core): add notation for out_param 2017-05-01 13:52:17 -07:00
Leonardo de Moura
66a1fec94e feat(library/init/category): add has_orelse type class 2017-05-01 09:58:27 -07:00
Leonardo de Moura
5cef84709f refactor(library): avoid auxiliary definitions such as add/mul/le/etc 
See Section "Other goodies" at
https://github.com/leanprover/lean/wiki/Refactoring-structures

This commit also improves the support for projections in the
unifier/matcher.

Now, we consider the extra case-split for projections.
Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce.
This is needed in the standard library because we now have constraints such as:
```
@has_le.le ?A ?s ?a ?b  =?=  @has_le.le nat nat.has_add x y
```
If we reduce the right hand side, we get the unsolvable constraint
```
@has_le.le ?A ?s ?a ?b  =?=  nat.le x y
```
Before this change, the constraint was `@le ?A ?s ?a ?b  =?=  @le nat nat.has_add x y`, and we already perform a case-split in this case.
Moreover, projections were eagerly reduced whenever possible.
The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out.
I worked around this issue by performing the case-split only when the constraint contains meta-variables.
There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
 2017-05-01 08:52:19 -07:00
Gabriel Ebner
3e2e9ed98a fix(frontends/lean/module_parser): make the #exit command end at the end of the file 
Fixes #1553.
 2017-05-01 13:22:26 +02:00
Gabriel Ebner
e6a62b8030 fix(util/sexpr/format): incorrect assertion 2017-05-01 13:13:07 +02:00
Gabriel Ebner
8554b8eac1 fix(frontends/lean/pp): insert line breaks in notations 2017-05-01 13:13:07 +02:00
Gabriel Ebner
ca2eab3a2f fix(frontends/lean/structure_cmd): instantiate universe levels in projections to parents 2017-04-29 15:00:17 +02:00
Scott Morrison
832c38d3cb fix(library/vm/vm_environment) use is_structure rather than try to catch an assertion 2017-04-29 12:55:50 +02:00
Scott Morrison
41c648905e fix(library/tactic/smt/ematch.cpp) check if new_states is empty before pushing 2017-04-28 08:50:45 -07:00