Leonardo de Moura
28128e0330
fix(frontends/lean): EXTRA_TYPE info
2014-10-16 12:25:18 -07:00
Leonardo de Moura
158682219f
feat(frontends/lean): allow parameters only in contexts
2014-10-11 17:13:56 -07:00
Leonardo de Moura
3d65b1c25c
fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241
2014-10-10 15:41:55 -07:00
Leonardo de Moura
8f1b6178a7
chore(*): minimize the use of parameters
2014-10-09 07:13:06 -07:00
Leonardo de Moura
8947bf4347
feat(frontends/lean): display type of binders, closes #238
2014-10-08 22:54:10 -07:00
Leonardo de Moura
73aa024c31
refactor(library/logic): remove 'core' subdirectory
2014-10-05 10:50:13 -07:00
Leonardo de Moura
317e910054
refactor(library/data/bool): use new style
2014-10-05 09:50:55 -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
4946f55290
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-02 17:55:34 -07:00
Leonardo de Moura
bc6ebf34be
feat(library/data/bool): do not use !
as notation for bnot, rename band/bor -> and/or
2014-10-01 17:00:03 -07:00
Leonardo de Moura
c46ec6a548
fix(frontends/lean): missing type information for INFO, fixes #218
2014-10-01 14:29:07 -07:00
Leonardo de Moura
113879a7dd
feat(frontends/lean/server): sort exact matches by size in FINDP
2014-09-29 16:44:55 -07:00
Leonardo de Moura
0d6d746d98
feat(frontends/lean): check modification time of imported files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-29 15:17:27 -07:00
Leonardo de Moura
69f50adb2e
fix(frontends/lean/server): must save the starting environment/options when reprocessing file, fixes #209
2014-09-26 15:36:47 -07:00
Leonardo de Moura
10a4148adb
fix(tests): make sure tests can be executed on Windows msys2 shell
2014-09-20 15:51:24 -07:00
Leonardo de Moura
4e2377ddfc
refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
b3e05a2fe9
refactor(frontends/lean/scanner): remove dependency to seekg and unget
...
methods
It is not safe to use seekg for textual files. Here is a fragment from a
C++ manual:
seekg() and seekp()
This pair of functions serve respectively to change the position of stream pointers get and put. Both functions are overloaded with two different prototypes:
seekg ( pos_type position );
seekp ( pos_type position );
Using this prototype the stream pointer is changed to an absolute position from the beginning of the file. The type required is the same as that returned by functions tellg and tellp.
seekg ( off_type offset, seekdir direction );
seekp ( off_type offset, seekdir direction );
Using this prototype, an offset from a concrete point determined by
parameter direction can be specified. It can be:
ios::beg offset specified from the beginning of the stream
ios::cur offset specified from the current position of the stream pointer
ios::end offset specified from the end of the stream
The values of both stream pointers get and put are counted in different
ways for text files than for binary files, since in text mode files some
modifications to the appearance of some special characters can
occur. For that reason it is advisable to use only the first prototype
of seekg and seekp with files opened in text mode and always use
non-modified values returned by tellg or tellp. With binary files, you
can freely use all the implementations for these functions. They should
not have any unexpected behavior.
2014-09-18 15:24:48 -07:00
Leonardo de Moura
78ad24a697
feat(frontends/lean/server): add SYNC command, closes #199
2014-09-16 18:42:34 -07:00
Leonardo de Moura
50f788a427
fix(tests/lean/interactive): adjust test to library reorg
2014-09-16 13:16:46 -07:00
Leonardo de Moura
851444b77a
test(tests/lean/interactive): test for issue #193
2014-09-15 16:07:23 -07:00
Leonardo de Moura
af2c3b1815
fix(frontends/lean/info_manager): bug in save_environment_options,
...
server was displaying old results
2014-09-15 16:05:17 -07:00
Leonardo de Moura
b82092a123
fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172
2014-09-10 08:39:39 -07:00
Leonardo de Moura
9b9adf8831
refactor(library): replace decidable_eq with abbreviation
2014-09-09 16:09:05 -07:00
Leonardo de Moura
ee196bbf1a
fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151
2014-09-09 12:49:32 -07:00
Leonardo de Moura
05c6e1461e
fix(tests/lean/interactive): interactive tests expected output, they must include the new '-- BEGINWAIT' messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-09 09:47:19 -07:00
Leonardo de Moura
6632a50015
refactor(library): add namespaces 'or', 'and' and 'iff'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 21:25:21 -07:00
Leonardo de Moura
364bba2129
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627
refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
ffc871ea8c
feat(frontends/lean/server): only display 'EXTRA_TYPE' info when the column number is provided to the 'INFO' command, closes #133
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 14:02:53 -07:00
Leonardo de Moura
9d0a4d21d4
chore(tests/lean/interactive): adjust test expected output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 10:00:42 -07:00
Leonardo de Moura
e51c4ad2e9
feat(frontends/lean): rename 'using' command to 'open'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 16:00:38 -07:00
Leonardo de Moura
2ca0a22e2c
fix(tests/lean/interactive/in4): adjust test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 01:35:46 -07:00
Leonardo de Moura
b7d7f12b8e
fix(frontends/lean/info_manager): several bugs: invalid flag was not being reset for empty lines, merge with overwrite=false was adding 'poluting' state, --NAY generation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-30 10:35:36 -07:00
Leonardo de Moura
59d3227eaa
fix(tests/lean/interactive): test output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 18:17:07 -07:00
Leonardo de Moura
9a4472cff5
fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 14:32:53 -07:00
Leonardo de Moura
8de9cab62d
test(tests/lean/interactive): add --server test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 07:41:38 -07:00
Leonardo de Moura
c7e9e238ec
fix(frontends/lean/server): ignore output produced by worker thread, fixes #98
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:46:49 -07:00
Leonardo de Moura
dd99e60a00
refactor(frontends/lean/info_manager): store environment+options in the info_manager, fixes #96
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:07:09 -07:00
Leonardo de Moura
cbc81ea6c5
chore(*): minimize dependencies on tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 19:58:48 -07:00
Leonardo de Moura
dbaf81e16d
refactor(library): remove unnecessary 'standard' subdirectory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Leonardo de Moura
c5a44aca44
fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:07:12 -07:00
Leonardo de Moura
4a96fefd96
fix(library/unifier): bug in unifier priority queue
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
1d306c09ee
fix(tests/lean/interactive): remove leftover from test output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 17:29:52 -07:00
Leonardo de Moura
13af81d554
fix(tests/lean/interactive): adjust test output to reflect new features
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 15:23:53 -07:00
Leonardo de Moura
55b0a03e3d
refactor(frontends/lean/info_manager): to allow cache to be used when producing info data, fixes #37 , closes #45
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 12:16:32 -07:00
Leonardo de Moura
a173b7f6e6
test(tests/lean/interactive): add old 'interactive' tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 14:57:08 -07:00
Leonardo de Moura
fc8ddcb0ce
feat(frontends/lean): improve 'check' command when used inside sections
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 14:07:41 +01:00
Leonardo de Moura
2ef7b9be2f
feat(frontends/lean): add basic pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 01:12:36 -07:00
Leonardo de Moura
f5f3816596
chore(tests): cleanup test scripts
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:03:39 -07:00
Leonardo de Moura
930960c54d
fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 10:06:50 -07:00