Leonardo de Moura
85b98f08e9
fix(frontends/lean): bad position at spurious 'end' token
2016-12-29 19:51:36 -08:00
Leonardo de Moura
cc077554b5
fix(library/tactic/change_tactic): use id_locked in the change tactic to create checkpoint
...
closes #1260
2016-12-21 11:29:03 -08:00
Gabriel Ebner
a26e2c9108
feat(library/module): intermediary data structure for environment modifications
2016-12-20 10:15:19 -08:00
Leonardo de Moura
d853136b82
chore(frontends/lean/builtin_cmds): leftover
2016-12-18 23:00:51 -08:00
Leonardo de Moura
6577cc87a3
feat(library): add pre_monad
...
closes #1235
2016-12-08 12:48:55 -08:00
Leonardo de Moura
b85ccefbff
fix(frontends/lean/builtin_cmds): information position (use the same approach used in other commands)
2016-11-29 16:47:34 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
6978906a78
chore(frontends/lean): remove namespace documentation
...
We will add module level doc strings /-! -/
2016-11-27 11:57:03 -08:00
Leonardo de Moura
338a46c225
fix(library/documentation): do not store doc strings for namespaces and declarations in the same name_map
2016-11-26 09:41:07 -08:00
Leonardo de Moura
97dd2f34d5
feat(library,frontends/lean): add basic doc string support
2016-11-25 18:52:56 -08:00
Leonardo de Moura
701fa0d1f4
fix(frontends/lean/builtin_cmds): make sure declarations generated by run_command get line/col info
2016-11-24 09:21:49 -08:00
Leonardo de Moura
e16e9880f7
chore(library/system): enforce Lean naming conventions IO ==> io
2016-11-17 11:27:37 -08:00
Leonardo de Moura
b0d6d171be
feat(library/tactic/vm_monitor): add basic io support for VM monad
2016-11-15 18:42:14 -08:00
Leonardo de Moura
7232e3a076
feat(library/vm/vm): invoke debugger (aka vm_monitor)
2016-11-14 14:45:49 -08:00
Sebastian Ullrich
ba1b6165e3
feat(frontends, shell): implement basic server 'info' command
2016-11-08 08:37:41 -08:00
Sebastian Ullrich
395ddd9d38
fix(frontends/lean/builtin_cmds): fix positioning of vm_eval output
2016-11-04 09:36:55 -07:00
Leonardo de Moura
9465f25f09
feat(library/vm): profiler for VM bytecode
2016-11-03 21:15:29 -07:00
Leonardo de Moura
0bb155a427
chore(*): remove .clean support
...
In Lean2, we used to cache elaborated definitions in .clean files. The
main goal was to optimize each flycheck invocation produced by Emacs.
The Lean3 definition package was not updating this cache. Moreover, it
is not necessary because the new compilation server subsumes it.
2016-10-13 19:58:58 -07:00
Gabriel Ebner
66be9c31db
refactor(library/flycheck): use flycheck_message_stream instead of option
2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2
refactor(*): structured message objects
2016-10-13 18:49:10 -07:00
Leonardo de Moura
3fbdb71f3e
feat(library/tactic/simplifier): remove simp_extensions
2016-10-06 20:50:23 -07:00
Leonardo de Moura
d59410cc41
refactor(kernel): support only proof irrelevant mode
2016-09-27 17:18:52 -07:00
Leonardo de Moura
d0d75c0923
refactor(kernel): reduce number of configurations supported in the kernel
...
Now, eta and impredicativity are assumed to be always true.
Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
2016-09-27 17:07:01 -07:00
Leonardo de Moura
9ef3ebbd5b
refactor(*): delete HoTT support
2016-09-27 16:33:39 -07:00
Leonardo de Moura
89f62edaf0
refactor(library): reduce dependecies on old code, simplify normalize module
2016-09-19 22:12:34 -07:00
Leonardo de Moura
a1d36b6c4d
chore(library): remove legacy_type_context
2016-09-19 21:31:21 -07:00
Leonardo de Moura
d43764b6fb
refactor(library/tactic/defeq_simplifier): move defeq_simp_lemmas to library
...
This commit also renames them to "rfl_lemmas".
Reason: these lemmas will be used at type_context::is_def_eq and type_context::whnf
2016-09-12 10:36:11 -07:00
Leonardo de Moura
a74f02546b
refactor(*): remove abbreviation command
2016-09-03 17:11:29 -07:00
Leonardo de Moura
a93eada058
feat(library/type_context): improved (and simplified) cache management for type_context
2016-08-23 17:56:58 -07:00
Leonardo de Moura
803c956d18
feat(util/sexpr/option_declarations): allow options to be registered after initialization
2016-08-19 16:58:30 -07:00
Leonardo de Moura
cd77f7167e
chore(frontends/lean): run_tactic ==> run_command
...
add `command` as alias for `tactic unit`
2016-08-18 12:53:21 -07:00
Leonardo de Moura
ddc3789929
feat(frontends/lean): add run_tactic command
...
This commit also adds the tactic `add_decl`.
2016-08-18 10:56:18 -07:00
Daniel Selsam
a9b01991c2
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
...
Conflicts:
src/frontends/lean/CMakeLists.txt
src/frontends/lean/structure_cmd.h
2016-08-17 07:34:03 -07:00
Sebastian Ullrich
751f2d8b02
refactor(frontends/lean): delegate all attribute parsing to decl_attributes
2016-08-16 13:49:03 -07:00
Leonardo de Moura
11043bc888
chore(frontends/lean/builtin_cmds): remove dead code
2016-08-11 08:38:39 -07:00
Leonardo de Moura
8ba17af50b
fix(frontends/lean/builtin_cmds): non-determinism
2016-08-11 08:01:44 -07:00
Leonardo de Moura
594c7ca4c5
chore(frontends/lean/find_cmd): remove find_decl command
2016-08-03 17:32:47 -07:00
Leonardo de Moura
186d82d58d
chore(frontends/lean/builtin_cmds): remove dead code
2016-08-02 15:18:05 -07:00
Leonardo de Moura
8993d0738a
feat(frontends/lean): remove #elab command
...
The check command is now using the new elaborator.
2016-08-02 15:05:24 -07:00
Leonardo de Moura
9fc222b9af
chore(library/pp_options): remove option pp.metavar_args
2016-07-31 16:00:21 -07:00
Leonardo de Moura
1aeda0e74b
feat(frontends/lean/elaborator): invoke tactics
2016-07-31 11:56:52 -07:00
Sebastian Ullrich
e69b508492
refactor(library/export_decl): Re-implement for new scoped_ext
...
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
2016-07-29 23:44:22 -04:00
Sebastian Ullrich
c4edad0372
feat(frontends/lean, library): remove attribute and metaclass scoping
...
All data is now part of either a global, permanent scope or a local,
temporary one
2016-07-29 23:44:21 -04:00
Leonardo de Moura
931251d403
feat(frontends/lean): remove local_context from parser
2016-07-28 16:19:31 -07:00
Leonardo de Moura
de9075b19d
chore(frontends/lean/builtin_cmds): support 'sorry' at #elab command
2016-07-27 17:09:36 -07:00
Leonardo de Moura
3a5f6f2e64
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
2016-07-27 15:29:25 -07:00
Leonardo de Moura
461b5f289c
feat(frontends/lean/elaborator): new elaborator skeleton
2016-07-23 19:02:17 -07:00
Leonardo de Moura
d8e6915366
fix(frontends/lean/builtin_cmds): fail if expression contain metavars
2016-07-19 13:22:10 -04:00
Leonardo de Moura
579f643d1d
refactor(library): move kabstract to tactic folder
2016-07-18 09:57:02 -04:00
Leonardo de Moura
fbefda9b1c
feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences'
2016-07-16 15:41:32 -04:00
