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

59 commits

Author SHA1 Message Date
Sebastian Ullrich
18c2e3739a feat(library/module_mgr): save .olean files of non-dirty .lean files in server mode 
Note, currently there is no way for a dirty file to become non-dirty again
 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
e8c057f1de refactor(library/module_mgr): simplify module loading code 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
1ee945a31f fix(library): store and validate Lean version of .olean files 
Fixes #1770
 2018-01-23 11:14:18 -08:00
Gabriel Ebner
9118079f7f fix(library/module_mgr): error handling in cyclic imports 
Fixes #1807
 2017-09-12 17:22:47 +02:00
Gabriel Ebner
814a5edaf1 fix(library/module_mgr): check for errors when writing olean files 2017-06-21 11:25:25 +02:00
Gabriel Ebner
1e7e440951 fix(library/module_mgr): actually cancel invalidated tasks 2017-06-05 19:36:09 +02:00
Gabriel Ebner
b1e417805e fix(frontends/lean/scanner): do not treat 0xFF as end-of-file 
Fixes #1624.  We just replace 0xFF by 0x00 when reading a new input
byte.  This shows up as an unexpected token error.
 2017-05-31 16:54:04 +02:00
Gabriel Ebner
40eb5d0556 feat(library/module_mgr): skip reverse dependency rebuild if file content is unchanged 2017-05-23 11:14:30 -07:00
Gabriel Ebner
07c25338b9 feat(shell/server): add search command 2017-05-22 09:40:38 -07:00
Gabriel Ebner
f14763b777 fix(library/module_mgr): fall back to olean if lean does not exist 2017-05-01 14:11:39 -07:00
Gabriel Ebner
3810e8950d refactor(util/lean_path,util/path): separate search path functions 2017-05-01 14:11:38 -07:00
Gabriel Ebner
baa4c48f1f refactor(util/lean_path): explicitly pass around search path 2017-05-01 14:11:38 -07:00
Gabriel Ebner
01a7efc007 fix(library/module_mgr): do not crash on missing imports 
Fixes #1506.
 2017-04-04 19:56:33 +02:00
Gabriel Ebner
8c1136c1b6 fix(library/module_mgr): get_first_diff_pos: handle newlines correctly 2017-03-27 14:01:04 -07:00
Gabriel Ebner
318910f99b refactor(frontends/lean/parser): store snapshots in a lazy async list 2017-03-27 14:00:53 -07:00
Gabriel Ebner
c7ca21625c feat(util/log_tree): annotate nodes with detail levels 2017-03-23 09:03:43 +01:00
Gabriel Ebner
2799375d24 chore(*): style 2017-03-23 08:57:56 +01:00
Gabriel Ebner
aebd18f136 feat(shell/server): only compile region of interest 2017-03-23 08:57:56 +01:00
Gabriel Ebner
5f872912e0 refactor(shell/lean): set exit status 1 iff at least one error was reported 2017-03-23 08:57:56 +01:00
Gabriel Ebner
595cbb8fe9 refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
Gabriel Ebner
cbc0bb1f7c feat(library/module): store whether we used sorry in olean 2017-02-05 16:35:32 +01:00
Gabriel Ebner
f3b9439029 feat(library/module_mgr): add function to get combined environment 2017-01-31 09:39:31 +01:00
Gabriel Ebner
0d949e0da7 chore(library/module_mgr): explain exceptional case 2017-01-17 17:10:37 -08:00
Gabriel Ebner
a230c47178 feat(util/task_queue,emacs,*): highlight running tasks with different background color 2017-01-17 17:10:37 -08:00
Gabriel Ebner
1a6629ce3b feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
Leonardo de Moura
eabbc5bb68 chore(library/module_mgr): comment unreachable_code assertion 
@gebner, could you please take a look a check whether there is a better fix.
 2017-01-15 23:18:44 +01:00
Sebastian Ullrich
b180c54c0e feat(shell): move lean.js to server mode 2017-01-13 07:34:54 -08:00
Gabriel Ebner
db81e4b5b8 feat(frontends/lean/parser): gracefully handle scanner exceptions in imports 2017-01-11 23:49:44 -08:00
Gabriel Ebner
7319000c98 fix(library/module_mgr): set up message handling outside of exception handler 2017-01-11 23:49:44 -08:00
Gabriel Ebner
130f80efff fix(library/module_mgr): gracefully handle exceptions during dependency discovery 2017-01-11 23:49:44 -08:00
Gabriel Ebner
70e41305e5 fix(module_mgr): produce olean files with correct mtimes 2017-01-06 01:04:18 -08:00
Gabriel Ebner
063130ee18 feat(kernel/environment): add function that checks whether all proofs are correct 2017-01-05 18:09:28 -08:00
Gabriel Ebner
96398500b6 fix(library/module_mgr): do not cause waits for preimported modules 2017-01-04 16:30:22 -08:00
Gabriel Ebner
f6b8eb6821 feat(util/task_queue): lazy tasks 2017-01-04 16:30:22 -08:00
Gabriel Ebner
e3b3de5cf3 fix(module_mgr): guard all accesses to m_mod_info 2016-12-23 18:01:44 +01:00
Leonardo de Moura
896bc2c75a chore(*): fix style 2016-12-20 11:31:00 -08:00
Gabriel Ebner
8132957391 fix(library/module_mgr): build olean files with mtimes in correct order 2016-12-20 10:55:34 -08:00
Gabriel Ebner
0550d2a6ac refactor(library/module): import all modules in a single call 2016-12-20 10:15:19 -08:00
Gabriel Ebner
99fc13af98 refactor(library/module_mgr): cache olean imports as well 2016-12-20 10:15:19 -08:00
Gabriel Ebner
370d69de3f refactor(library/module): interface to get task dependencies for modifications 2016-12-20 10:15:19 -08:00
Gabriel Ebner
a2bc967fac feat(library/module): reuse pre-imported init module 2016-12-20 10:15:19 -08:00
Gabriel Ebner
a26e2c9108 feat(library/module): intermediary data structure for environment modifications 2016-12-20 10:15:19 -08:00
Gabriel Ebner
6ed538a705 fix(library/module_mgr): finally fix invalidation 2016-12-16 18:18:00 -08:00
Gabriel Ebner
d89512b6fc fix(util/task_queue): fix undefined behavior with null references 2016-12-15 09:48:57 -08:00
Gabriel Ebner
0c8c41bd07 fix(library/module_mgr): make more robust 2016-12-12 12:40:40 -08:00
Gabriel Ebner
67e3c383ac fix(library/module_mgr): fix invalidation 2016-12-12 12:40:40 -08:00
Gabriel Ebner
cf3f398753 fix(library/module_mgr): do not perform unnecessary copy 2016-12-12 08:25:32 -08:00
Jared Roesch
e65d90ac79 feat(*): C++ code generator 
in progress move of Lean.native to init
 2016-12-05 16:11:41 -08:00
Gabriel Ebner
c8a821afd1 fix(library/module_mgr): do not create olean files for modules with errors 2016-12-02 16:48:18 -08:00
Gabriel Ebner
851b64dbbd feat(library/module_mgr): gracefully handle non-existing imports 2016-12-02 08:47:59 -08:00