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

9578 commits

Author SHA1 Message Date
Leonardo de Moura
429edd7a5e fix(frontends/lean/definition_cmds): fixes #1956 2018-04-11 16:48:04 -07:00
Leonardo de Moura
ee8a79a270 chore(*): remove C API 2018-04-10 16:48:02 -07:00
Leonardo de Moura
e1322491c5 chore(*): remove discr_tree 2018-04-10 16:31:55 -07:00
Leonardo de Moura
ce0467638e chore(*): remove unification hints 2018-04-10 16:29:04 -07:00
Leonardo de Moura
10ddfdafbd chore(*): remove VM monitor 2018-04-10 16:08:47 -07:00
Leonardo de Moura
1b1495aea4 chore(*): remove norm_num 2018-04-10 15:59:29 -07:00
Leonardo de Moura
6234c60aae chore(*): disable test suite 2018-04-10 12:56:55 -07:00
Leonardo de Moura
47cd2ee61a chore(leanpkg): delete 2018-04-10 12:43:17 -07:00
Leonardo de Moura
b14d69b1d7 chore(*): remove converter, ac_tactics, hole_commands, rbtree/rbmap proofs, bitvec 2018-04-10 12:25:51 -07:00
Leonardo de Moura
a2f0bf7c1b chore(*): disable SMT tactic framework and backward chaining 2018-04-10 12:05:51 -07:00
Leonardo de Moura
d36b859c65 chore(library/delayed_abstraction): add missing 'virtual' 2018-04-09 17:07:57 -07:00
Leonardo de Moura
c08a3bc557 refactor(library/typed_expr): move typed_expr to frontends/lean 2018-04-09 15:25:40 -07:00
Leonardo de Moura
bcaa0b2ad3 refactor(library/typed_expr): do not use macros for implementing typed_expr 
Remark: in Lean4, we will not have macro_defs.
 2018-04-09 15:16:46 -07:00
Leonardo de Moura
8dd53cd94f chore(*): rename expr_struct_* to expr_* 
We don't need to modifier `_struct` anymore since we don't use the
pointer equality based hashtables anymore.
 2018-04-09 12:55:48 -07:00
Leonardo de Moura
faf8e025e7 chore(kernel): remove m_hash_alloc field from expressions 
This field was originally added to create hashtables based on pointer
equality. We don't use them anymore, and the caches based on
m_hash_alloc can be implemented using m_hash without any performance
impact. This commit also fixes two places where `expr_set` was used
instead of `expr_struct_set`.

This commit is also important for the Lean4 plans where `expr` will
be implemented in Lean, and fields like `m_hash_alloc` would require us
to track state.
 2018-04-09 10:05:56 -07:00
Sebastian Ullrich
96c932ab21 fix(util/numeric/mpbq): remove unimplemented move constructor 
Apparently g++ started preferring it over the copy constructor in more places
 2018-04-02 23:29:39 +02:00
Sebastian Ullrich
17affbd45d chore(library/util): don't hide commit hash for nightlies 2018-04-02 10:44:43 +02:00
Leonardo de Moura
66e7873c22 fix(library/type_context): elim_delayed_abstraction must check whether metavariable is already assigned 
fixes #1952
 2018-03-29 15:53:17 -07:00
Leonardo de Moura
8e8232605a chore(library/compiler/inliner): fix weird include 2018-03-29 13:08:43 -07:00
Sebastian Ullrich
3fefe94757 refactor(library/init/core,library/init/unit): make unit an abbreviation of punit.{0} 2018-03-27 10:33:04 -07:00
Leonardo de Moura
efa9d7e110 perf(library/type_context): performance issue when proving equation lemmas 2018-03-26 12:57:19 -07:00
Sebastian Ullrich
0c0646f03b chore(leanpkg/lean_version): recognize nightlies as releases separate from master 2018-03-20 15:14:45 -07:00
Sebastian Ullrich
1c6861528b refactor(init/category): move monad laws into separate type classes defined after the tactic framework 2018-03-20 14:58:35 -07:00
Sebastian Ullrich
29d1911f50 chore(.appveyor.yml,src/CMakeLists): make cxx and linker flags configurable and use them to disable slow LTO on AppVeyor 2018-03-08 10:30:58 -08:00
Sebastian Ullrich
340e056dee chore(shell/CMakeLists): copy mpir.dll when building with MSVC 
Also simplify code a bit
 2018-03-08 10:30:47 -08:00
Sebastian Ullrich
854475808d chore(shell/CMakeLists): make bin/lean a proper target 
This ensures that it will be re-copied when removed, which is a quick way of
switching between debug and release builds.
 2018-03-08 10:30:38 -08:00
Sebastian Ullrich
fbe6b70295 perf(library/module_mgr): fix module_info reference cycle 2018-03-08 10:06:20 -08:00
Sebastian Ullrich
191d1e7321 chore(shell/server): sync_output command for debugging 2018-03-08 10:06:09 -08:00
Leonardo de Moura
2e66449feb fix(library/tactic/tactic_state): build 2018-03-08 09:58:07 -08:00
Leonardo de Moura
169cd87dbe feat(library/system/io): add io.run_tactic 
@nunoplopes @aqjune
I had to add a new primitive to allow you to execute a tactic from the
`main` function. The `main` function is in the `io` monad. The new
primitive has type:
```
meta constant io.run_tactic {α : Type} (a : tactic α) : io α
```
I also added a new test that shows how to use it.
The test displays all declarations that have the `nat` prefix.

cc @kha
 2018-03-07 12:15:26 -08:00
Nuno Lopes
9152aaa7d6 fix(bit_tricks): make sure no one calls math.h's log2() 
this fixes the bit_trick test with MSVC
 2018-03-06 11:21:28 -08:00
Leonardo de Moura
3e81f88887 feat(library): implement new cache API for fun_info 2018-03-05 15:46:42 -08:00
Leonardo de Moura
eddc64d154 chore(library/abstract_context_cache): remove unnecessary argument 2018-03-05 14:40:47 -08:00
Leonardo de Moura
a5ace58fb3 feat(library): add elab_context 2018-03-05 13:11:55 -08:00
Leonardo de Moura
bdea7d420d chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
Leonardo de Moura
f873def910 refactor(library/type_context): move unification_hints to cache object 2018-03-05 12:17:09 -08:00
Sebastian Ullrich
d6d44a1994 fix(frontends/lean/pp): fix #1922 
Fixes #1922
 2018-03-02 13:02:48 -08:00
Sebastian Ullrich
48147646bc refactor(library): mk_result/get_result_* ~> mk_success/get_success_* 2018-03-01 14:56:01 +01:00
Sebastian Ullrich
e1fc2bdbea refactor(library): encapsulate tactic's Lean implementation better 2018-03-01 14:56:01 +01:00
Nuno Lopes
39270fd46f fix(tactic): build on MSVC 2018-02-28 10:38:50 -08:00
Sebastian Ullrich
f72a700e34 fix(frontends/lean/decl_cmds): attribute cmd: save info for first ident 2018-02-28 17:42:19 +01:00
Sebastian Ullrich
76843717c4 chore(frontends/lean/elaborator): style 2018-02-28 12:49:22 +01:00
Sebastian Ullrich
1abf8738fc feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration 2018-02-28 12:49:22 +01:00
Sebastian Ullrich
f3ca420b64 feat(frontends/lean/elaborator): hide opt/auto param types when elaborating structure field values 2018-02-28 12:49:22 +01:00
Sebastian Ullrich
cf8dd9e75e feat(fronteds/lean/builtin_exprs): do notation: use overloadable bind instead of has_bind.bind 2018-02-28 12:49:22 +01:00
Leonardo de Moura
b72d465835 refactor(library/init/meta): remove tactic_state.mk_empty 
The tactic_state object will contain a name_generator for creating fresh
names. `tactic_state.mk_empty` is bad because it does not have sufficient
information to create this name_generator.
Moreover `tactic_state.mk_empty` was only being used to convert
`tactic A` into a `parser A`.
We implement this primitive now in C++. In C++, we will be able
to use the parser name generator to initialize a fresh `tactic_state`.
 2018-02-27 14:45:47 -08:00
Leonardo de Moura
902445c56f chore(frontends/lean): remove parser_state object 
This is dead code. We have decided to implement the new parser in Lean.
 2018-02-27 14:05:02 -08:00
Leonardo de Moura
221931492e feat(library/name_generator): add nest_with 2018-02-27 13:17:58 -08:00
Leonardo de Moura
3895fd8511 chore(library): use type_context to update metavar_context 2018-02-27 12:23:26 -08:00
Sebastian Ullrich
5279f92dae fix(library/tactic/simp_lemmas): avoid rewrite failure with more robust code 
The old code assumed `emetas` to be descendingly ordered by tmp idx, which is
not true for rfl lemmas.
 2018-02-27 10:59:51 -08:00