Sebastian Ullrich
3442634181
fix(library/process): inheriting IO handles on Windows
2017-12-30 19:31:55 +01:00
Sebastian Ullrich
37e2f085e4
chore(shell/CMakeLists): leanpkg integration tests
2017-12-30 19:31:55 +01:00
Sebastian Ullrich
adc0d250fc
fix(shell/lean): show progress messages only when stdout is a terminal
2017-12-30 17:39:53 +01:00
Sebastian Ullrich
6e02ce9b34
fix(.travis.yml): support combining $TEST_LEANPKG_REGISTRY and $UPLOAD
2017-12-22 11:54:29 +01:00
Sebastian Ullrich
a36376a6cf
fix(frontends/lean/builtin_cmds): #eval: set message caption
2017-12-22 11:04:46 +01:00
Sebastian Ullrich
5eaa6efab9
chore(.travis.yml): fix Travis on OS X
2017-12-21 08:28:44 -08:00
Leonardo de Moura
d0dfb3f9f9
fix(library/tactic/simp_lemmas): closes #1863
2017-12-20 15:12:02 -08:00
Mario Carneiro
56c54a478f
fix(init/coe): use Sort instead of Type in subtype coe
2017-12-20 14:02:03 -08:00
Sebastian Ullrich
7e4f348b8c
chore(script/test_registry): Replace with leanpkg. Execute in every artifact-producing build configuration.
2017-12-20 14:01:45 -08:00
Leonardo de Moura
ddf014cc7f
feat(library/init/version): add lean.githash : string
2017-12-20 14:00:41 -08:00
Leonardo de Moura
c6ddc51c2b
fix(library/app_builder): typo at mk_congr
...
closes #1893
2017-12-20 13:13:55 -08:00
Leonardo de Moura
a2dc2b6549
fix(util): null_output_channel
...
On OSX, Lean was often crashing when using trace messages.
I identified a problem in the thread finalization process.
In OSX, the `silent_ios_helper` at `library/trace.cpp` was being
finalized after the `null_streambuf` at `util/null_ostream.cpp`.
There was also a memory corruption problem also related to
`null_streambuf`.
This commit fixes this problem by using the following recipe
for creating null output stream buffers in C++.
https://stackoverflow.com/questions/11826554/standard-no-op-output-stream
2017-12-20 11:50:41 -08:00
Leonardo de Moura
8de8771ee0
chore(library/vm/vm_parser): remove leftover comment
2017-12-17 09:52:44 -08:00
Leonardo de Moura
8b835f9ab6
fix(frontends/lean): fixes #1890
...
It fixes the issue by propagating the correct information to the
equation compiler.
The fix may be a little bit hackish, but it is comapatible with
the approach we are already using: store `m_is_meta` flag in the equation
macro.
Disclaimer: we may still have other instances of this bug, since
the information may still be propagated incorrectly in other places.
I will not refactor this code right now nor accept any PR that
changes the current design. I am busy in other parts of the code
base and do not have time to do the context switch required for
implementing this kind of change and/or review the PR and make sure I'm
happy with it.
2017-12-17 09:42:06 -08:00
Leonardo de Moura
f7bc884ae8
chore(kernel/type_checker): fix compilation warning msgs
2017-12-17 08:44:51 -08:00
Gabriel Ebner
9ef95c9dff
chore(gitignore): ignore autogenerated version.lean file
2017-12-17 15:49:51 +01:00
Gabriel Ebner
860cc95730
fix(library/compiler/rec_fn_macro): do not type-check in non-meta declarations
2017-12-17 15:47:52 +01:00
Leonardo de Moura
e89eece98c
feat(library/init): add lean.version : nat × nat × nat
...
closes #1873
2017-12-15 17:48:26 -08:00
Leonardo de Moura
0252393eb5
doc(library/type_context): relax preconditions for using is_def_eq in new implementation
2017-12-15 17:37:33 -08:00
Leonardo de Moura
91ff183b3e
chore(library): remove out notation for out_param
2017-12-15 15:47:58 -08:00
Leonardo de Moura
f0352d31a1
feat(library/type_context, library): inout ==> out modifier in type class declarations
...
@kha: I decided to implement this change before I start the
type_context modifications. The change did not affect the corelib and
test suite much. The only annoying problem is that `out` cannot be
used to name locals anymore.
2017-12-15 14:46:47 -08:00
Leonardo de Moura
9503ceb832
doc(library/type_context): improve docstring for new design
...
cc @kha
2017-12-15 13:20:26 -08:00
Leonardo de Moura
7106bcf7a5
chore(frontends/lean/inductive_cmds): remove app_builder dependency
2017-12-15 11:35:34 -08:00
Leonardo de Moura
7c1447d615
fix(library/app_builder,library/util): get_level's with slightly different behavior
2017-12-15 11:33:29 -08:00
Leonardo de Moura
aed2c442a3
chore(library/app_builder): add assertion stating that app_builder::mk_app arguments do not contain tmp metavars
2017-12-15 11:22:15 -08:00
Leonardo de Moura
8850099e3d
chore(library/tactic/smt): remove app_builder dependency
2017-12-15 11:18:41 -08:00
Leonardo de Moura
0492e49a3f
fix(library/type_context): fixes #1888
2017-12-15 08:49:45 -08:00
Scott Morrison
a395c26165
chore(.travis.yml): work around change in Travis OS X image
2017-12-15 10:41:09 +01:00
Leonardo de Moura
73c4ea7e35
chore(library/type_context): typos and missing remarks
2017-12-14 18:26:41 -08:00
Leonardo de Moura
f0f2fc42b6
doc(library/type_context): design notes for new type_context
2017-12-14 17:57:28 -08:00
Leonardo de Moura
746134d11c
feat(library/init/meta/interactive): add goal tagging support for by_cases
...
This commit also incorporates changes suggested at commit 84a1911949dec94.
2017-12-13 15:17:13 -08:00
Leonardo de Moura
6eae78da01
chore(library/data/rbtree/insert): provide meaningful names to ins.induction minor premises
...
We use them with `case` tactic.
2017-12-13 14:44:48 -08:00
Leonardo de Moura
6c44dd1b7f
feat(frontends/lean): add hide command
...
cc: @kha
2017-12-13 11:53:21 -08:00
Leonardo de Moura
056a7db7b3
test(tests/lean/run): heap interface experiments
...
They expose limitations in the elaborator.
2017-12-12 18:19:30 -08:00
Mario Carneiro
17f77367cd
chore(library/init/data/fin/ops): revert 107ad36259.
2017-12-12 10:53:12 -08:00
Sean Leather
107ad36259
feat(library/init/data/fin/ops): fin.succ.inj
2017-12-12 04:23:01 -05:00
Leonardo de Moura
cb74ef1670
chore(library/init/meta/interactive): fix docstring
2017-12-11 16:27:04 -08:00
Leonardo de Moura
533ddc0279
fix(library/init/meta/interactive): remove buggy generalizing param from with_cases
2017-12-11 16:27:04 -08:00
Leonardo de Moura
b778d77c0c
chore(doc/changes): with_cases and cases changes, - ==> *
2017-12-11 16:27:04 -08:00
Leonardo de Moura
5217ae735d
feat(library/init/meta/interactive): do not make tag longer when constructor/apply create a single subgoal
2017-12-11 16:27:03 -08:00
Leonardo de Moura
f0231f17bc
feat(library/init/meta): propagate tags in constructor-like tactics
2017-12-11 16:27:03 -08:00
Leonardo de Moura
f18aa1d413
chore(tests/lean): fix tests
2017-12-11 16:27:03 -08:00
Leonardo de Moura
5fa857dc69
fix(library/tactic/tactic_state): do not diplay case for empty tag
2017-12-11 16:27:03 -08:00
Leonardo de Moura
ebeb5f713a
feat(library/init/meta/interactive): do not make tag longer when induction/cases create a single subgoal
2017-12-11 16:27:03 -08:00
Leonardo de Moura
53961b12cb
chore(library/data/rbtree/insert): use new case tactic to cleanup proofs
2017-12-11 16:27:03 -08:00
Leonardo de Moura
8bda71af6f
feat(library/init/meta/interactive): new case tactic with support for with_cases and tagging
2017-12-11 16:27:03 -08:00
Leonardo de Moura
bf8fa50481
feat(library/init/data/list/basic): add is_prefix_of and is_suffix_of
2017-12-11 16:27:03 -08:00
Leonardo de Moura
ddfcc2cb0b
feat(library/init/data/list/basic): define decidable_eq (list A) instance manually
...
Motivation: make sure we can use it before we define the tactic `mk_dec_eq_instance`.
2017-12-11 16:27:03 -08:00
Sebastian Ullrich
205fbd8136
chore(.gitattributes): use union merge strategy for doc/changes.md
...
No more changelog merge conflicts \o/
2017-12-11 12:49:10 +01:00
Leonardo de Moura
f1510a82c7
chore(tests/lean): fix tests
2017-12-10 19:30:43 -08:00
