Soonho Kong
39645390ff
chore(util/*): add cstddef header before including gmp.h/mpfr.h
...
Reference: https://gcc.gnu.org/gcc-4.9/porting_to.html
------
Header <cstddef> changes
The <cstddef> header was updated for C++11 support and this breaks some
libraries which misuse macros meant for internal use by GCC only. For
instance with GMP versions up to 5.1.3, you may see:
/usr/include/c++/4.9.0/cstddef:51:11: error: ‘::max_align_t’ has not been declared
using ::max_align_t;
^
Another possible error is:
someheader.h:99:13: error: ‘ptrdiff_t’ does not name a type
A workaround until libraries get updated is to include <cstddef> or
<stddef.h> before any headers from that library.
2014-10-07 02:36:57 -04:00
Soonho Kong
4350382b90
doc(make/msys2): update instructions
2014-10-06 15:13:24 -07:00
Soonho Kong
7eebefb3e9
chore(.travis.osx.yml): add configurations using clang++
2014-10-06 14:45:28 -07:00
Soonho Kong
286aae933c
chore(CMakeLists.txt): add EMACS_LIB option to specify installation path for emacs stuff
2014-10-06 11:20:13 -07:00
Soonho Kong
e41573afc4
chore(tests/*/test.sh): change working dir; avoid using ls in for-loop
2014-10-06 11:20:13 -07:00
Leonardo de Moura
dc92f67588
feat(frontends/lean/server): CLEAR_CACHE forces buffer to be reprocessed
2014-10-06 08:42:20 -07:00
Leonardo de Moura
f7e1b67f6c
test(tests/lean/run/print): add tests for 'print' cmd
2014-10-05 19:06:29 -07:00
Leonardo de Moura
16562adb87
feat(frontends/lean): add 'coercions' and 'instances' to 'print' command, closes #71
2014-10-05 18:50:48 -07:00
Leonardo de Moura
c9e5e40477
refactor(library/data/num): cleanup
2014-10-05 13:47:51 -07:00
Leonardo de Moura
86591c7272
refactor(library/data/prod): cleanup
2014-10-05 13:38:08 -07:00
Leonardo de Moura
1306d08399
feat(emacs/lean-input): add shortcuts for subscripts
2014-10-05 13:34:05 -07:00
Leonardo de Moura
d56266c524
refactor(data/sum): use sections
2014-10-05 13:20:04 -07:00
Leonardo de Moura
15779c5d1e
refactor(data/list): use '!' operator, and new name convention for declaration names
2014-10-05 13:10:35 -07:00
Leonardo de Moura
efaeeb0726
refactor(data/nat/sub): use new policy for marking implicit arguments and '!' operator
2014-10-05 12:39:13 -07:00
Leonardo de Moura
fa96596bf7
refactor(data/int/order): use '!' operator
2014-10-05 11:44:18 -07:00
Leonardo de Moura
a0d4d82f3f
refactor(data/nat/order): use new policy for marking implicit arguments and '!' operator
2014-10-05 11:36:39 -07:00
Leonardo de Moura
e91a64fb38
chore(library/logic): fix comments
2014-10-05 11:11:48 -07:00
Leonardo de Moura
73aa024c31
refactor(library/logic): remove 'core' subdirectory
2014-10-05 10:50:13 -07:00
Leonardo de Moura
0f90d10a13
refactor(logic/core/eq): use sections
2014-10-05 10:19:50 -07:00
Leonardo de Moura
317e910054
refactor(library/data/bool): use new style
2014-10-05 09:50:55 -07:00
Leonardo de Moura
60d8369688
fix(library/unifier): missing justification when updating choice constraints
...
The bug was not producing incorrect results, but really bad error
messages.
See: empty.lean.expected.out
2014-10-04 10:40:53 -07:00
Leonardo de Moura
a9741c5c30
chore(frontends/lean/placeholder_elaborator): indent code
2014-10-04 10:36:10 -07:00
Leonardo de Moura
0a288aec40
chore(frontends/lean/proof_qed_elaborator): remove obsolete comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-04 09:19:33 -07:00
Leonardo de Moura
64f6601fe3
fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost
2014-10-04 09:15:42 -07:00
Leonardo de Moura
7073f036d8
test(tests/lean/run): add additional tests for section parameter/variable and strict implicit argument
2014-10-04 08:15:43 -07:00
Leonardo de Moura
bf01cfeec5
fix(frontends/lean): avoid superfluous local references of the form @-1 (@ f)
,
...
This kind of term also confuses the elaborator
2014-10-04 07:55:32 -07:00
Leonardo de Moura
e71d4548de
fix(frontends/lean): universe levels associated with section variables should not be fixed in the section
2014-10-04 07:13:19 -07:00
Leonardo de Moura
5a927b6db4
refactor(library/logic/cast): define heq using inductive datatypes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-03 21:40:51 -07:00
Soonho Kong
b2c8e7d364
feat(bin/linja): delete MSYSTEM env variable on Windows
2014-10-03 17:30:29 -07:00
Soonho Kong
f8164b6a7e
feat(bin/linja): enforce path separator '\' on Windows platform
2014-10-03 17:28:00 -07:00
Leonardo de Moura
b9e7fecb1f
fix(frontends/lean/elaborator): style
2014-10-03 16:26:28 -07:00
Leonardo de Moura
a1bb6d6017
refactor(frontends/lean/elaborator): expose elaborator class
2014-10-03 16:10:36 -07:00
Leonardo de Moura
dccf8a3a75
chore(frontends/lean/elaborator): fix field name
2014-10-03 15:34:23 -07:00
Leonardo de Moura
938e12baa1
feat(frontends/lean/notation_cmd): allow local numeric notation
2014-10-03 13:55:57 -07:00
Leonardo de Moura
dbb7f834af
refactor(frontends/lean/parser_config): merge notation_ext and mpz_notation_ext
2014-10-03 13:55:57 -07:00
Leonardo de Moura
73eca1ef44
feat(frontends/lean/notation_cmd): notation defined in context overrides existing ones
2014-10-03 13:55:57 -07:00
Leonardo de Moura
fd013e8d07
chore(tests/lean/run/group3): cleanup test
2014-10-03 13:55:57 -07:00
Soonho Kong
7ea9c32ec8
feat(emacs/lean-server): send SYNC command when visiting a modified buffer
...
Close #201
2014-10-03 10:11:21 -07:00
Soonho Kong
b78043ae24
feat(emacs/lean-mode): add 'clean-cache' to the menu
...
Related issue: #75
2014-10-03 10:11:21 -07:00
Soonho Kong
fffb4e6019
feat(emacs/lean-server): delete cache file (.clean) after visit/load
...
fix #75
2014-10-03 10:11:21 -07:00
Soonho Kong
e255b02fca
fix(emacs/lean-changes): visit file before process any changes
...
This solves many instances of the modified buffer problem.
2014-10-03 10:11:21 -07:00
Leonardo de Moura
c0725d1934
refactor(frontends/lean): remove 'including' expressions
2014-10-03 09:09:27 -07:00
Leonardo de Moura
01d4644026
fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored
2014-10-03 08:52:35 -07:00
Leonardo de Moura
284f300440
feat(frontends/lean): add 'include' and 'omit' commands, closes #184
2014-10-03 07:23:24 -07:00
Leonardo de Moura
6950b4aa9b
fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables
2014-10-02 18:29:41 -07:00
Leonardo de Moura
a52b21c92d
refactor(library): using section variables
2014-10-02 18:25:00 -07:00
Leonardo de Moura
d5cad765a0
feat(frontends/lean): enforce new semantics for section 'variables'
...
The library file logic/core/connectives uses the new feature.
2014-10-02 17:55:34 -07:00
Leonardo de Moura
f006d93794
feat(frontends/lean): section variables occur after section parameters
2014-10-02 17:55:34 -07:00
Leonardo de Moura
0a13e7863a
feat(frontends/lean): enforce rule section parameters cannot depend on section variables
2014-10-02 17:55:34 -07:00
Leonardo de Moura
bf081ed431
refactor(kernel): rename var_decl to constant_assumption
...
Motivation: it matches the notation used to declare it.
2014-10-02 17:55:34 -07:00