Leonardo de Moura
9a3a01fa6e
feat(library/compiler/compiler): invoke new IR compiler implemented in Lean
2019-05-16 16:08:52 -07:00
Leonardo de Moura
9d7191feca
chore(library/compiler): remove support for fully boxed
2019-05-16 15:48:33 -07:00
Leonardo de Moura
ac69f802e1
feat(library/compiler): interface with new IR compiler entry point
2019-05-16 15:41:47 -07:00
Leonardo de Moura
aa138fe686
chore(*): get_obj_arg => to_obj_arg
2019-05-16 14:42:02 -07:00
Leonardo de Moura
9d9f546ad8
refactor(util/sexpr): move options and option_declarations to util
2019-05-16 14:37:24 -07:00
Leonardo de Moura
367b3ec4a3
chore(tests/util): remove old test
2019-05-16 14:29:26 -07:00
Leonardo de Moura
9c4da289b2
refactor(util/sexpr/options): options as a Lean object
2019-05-16 14:27:44 -07:00
Leonardo de Moura
31d4fa9f71
chore(util/sexpr/options): shrink options API
...
Motivation: move to the Lean implementation
2019-05-16 14:08:11 -07:00
Leonardo de Moura
5482a11642
feat(library/init/lean/compiler/ir/default): add new entry point
2019-05-16 10:20:00 -07:00
Leonardo de Moura
2d065c7ded
feat(library/init/lean/compiler/ir): add Lean.IR.CompilerM
...
and environment extension for storing Lean IR declarations.
2019-05-16 10:20:00 -07:00
Sebastian Ullrich
7a19f246e6
fix(shell/lean): re-add missing short-only option
2019-05-16 10:27:18 +02:00
Leonardo de Moura
739008f8d4
chore(library/init/lean/compiler/llnf): disable
...
I am going to refactor the interface with the new IR compiler.
2019-05-15 19:02:51 -07:00
Leonardo de Moura
77768c504e
feat(shell/lean): import time stats
2019-05-15 17:16:19 -07:00
Leonardo de Moura
9b3421b63b
feat(library/compiler/closed_term_cache): remove C++ implementation and use Lean one
2019-05-15 15:33:46 -07:00
Leonardo de Moura
b87afdcbfd
chore(library/init/lean/compiler/closedtermcache): naming convention
2019-05-15 15:19:09 -07:00
Leonardo de Moura
816e83970b
refactor(util/object_ref, kernel/environment): move to_optional
2019-05-15 15:16:29 -07:00
Leonardo de Moura
09df708af2
feat(library/init/lean/compiler): implement close term cache env extension in Lean
2019-05-15 11:01:25 -07:00
Leonardo de Moura
89e01368cd
fix(library/init/lean/environment): throw error if environment already contains constant
2019-05-15 11:01:25 -07:00
Leonardo de Moura
3193e91aff
feat(library/init/lean/environment): add Environment.displayStats and --stats command line argument
2019-05-15 11:01:25 -07:00
Leonardo de Moura
bc809643ec
feat(library/init/lean/expr): add Expr.quickLt, Expr.eqv
2019-05-15 11:01:25 -07:00
Leonardo de Moura
8ab15536a7
perf(library/init/data/array/binsearch): add binSearchContains
2019-05-14 20:52:57 -07:00
Leonardo de Moura
45eda6d81b
perf(library/init/lean/modifiers): add only local entries to state
...
We can use `getModuleEntries` and `getModuleIdxFor` to test whether a
constant is protected or not.
2019-05-14 20:30:46 -07:00
Leonardo de Moura
dc71fafac1
feat(library/init/data/array): add Array.binSearch
2019-05-14 18:25:54 -07:00
Leonardo de Moura
2e4f5951e3
feat(library/init/data/array/qsort): simple quicksort
...
@kha I added `qsort` for sorting environment extension entries, but I am
wondering if we could use it as a benchmark in our paper. It is a pure implementation; it is
fast; it implements the real quick sort algorithm with in-place updates if the
input array is not shared. If the array is shared it performs
a single copy and then switches to in-place updates.
2019-05-14 17:46:34 -07:00
Leonardo de Moura
431c0a2525
chore(stage0): update
2019-05-14 16:28:25 -07:00
Leonardo de Moura
c957450d05
feat(library/protected): replace C++ implementation with Lean one
2019-05-14 16:12:56 -07:00
Leonardo de Moura
da5b900cbd
feat(library/init/lean): add protected extension
2019-05-14 16:04:24 -07:00
Leonardo de Moura
b888b6f3b6
feat(library/init/lean/environment): process imported entries
2019-05-14 15:32:07 -07:00
Leonardo de Moura
a24a1562ea
fix(library/init/lean/environment): import order
2019-05-14 12:41:19 -07:00
Leonardo de Moura
5df0b05cc7
chore(library/init/lean/environment): remove get_modifications_core
2019-05-14 11:26:04 -07:00
Leonardo de Moura
edeae776da
chore(library/module): module::add for declarations is not needed anymore
2019-05-14 11:23:35 -07:00
Leonardo de Moura
7696c28fe1
feat(library/module): module manager in Lean is alive
2019-05-14 11:10:49 -07:00
Leonardo de Moura
d5fd5d86ee
fix(library/init/lean/environment): quotInit initialization
2019-05-14 10:31:06 -07:00
Leonardo de Moura
02e558d781
feat(library/init/lean/environment): export module I/O in Lean
2019-05-14 10:15:33 -07:00
Leonardo de Moura
642c4c59bd
feat(library/init/lean/environment): support for serializing/performing legacy modification objects
2019-05-14 10:08:31 -07:00
Leonardo de Moura
67d14705b0
chore(library/module): simplify write_module
2019-05-14 08:08:09 -07:00
Leonardo de Moura
427852d759
feat(library/init/lean/environment): add findOLean
2019-05-14 08:02:26 -07:00
Leonardo de Moura
e616def866
chore(library/module): remove dead declaration
2019-05-14 07:53:44 -07:00
Leonardo de Moura
22d2848d21
chore(library/module): store search_path in a global variable
...
Remark: I will use it to expose the following primitive in Lean
```
constant findOLean : Name -> IO String
```
2019-05-14 07:49:00 -07:00
Leonardo de Moura
1a610607b1
chore(library/module): remove old comment
2019-05-14 07:37:20 -07:00
Leonardo de Moura
358b731581
chore(library/module): simplify import_modules
...
Remark: `lean.cpp` is a total mess at this point. It contains
leftovers from the Lean2 and Lean3 designs, and hacks for supporting
the Lean4 transition.
2019-05-14 07:26:50 -07:00
Leonardo de Moura
9596fae665
chore(library/module): remove import errors
2019-05-14 07:13:50 -07:00
Leonardo de Moura
53ec9ee181
chore(*): style
2019-05-14 07:08:58 -07:00
Leonardo de Moura
5844913102
feat(library/module, library/init/lean/environment): add primitives for reading/writing files as compacted regions
2019-05-13 17:26:28 -07:00
Leonardo de Moura
40f9704540
chore(library/init/lean/environment): add placeholders for writing/reading .olean files
2019-05-13 15:48:23 -07:00
Leonardo de Moura
31d140adab
refactor(library/module): use Lean modification list environment extension
2019-05-13 15:26:28 -07:00
Leonardo de Moura
5480d22be6
feat(library/init/lean/environment): add getModifications
2019-05-13 15:18:03 -07:00
Leonardo de Moura
ec846f1552
chore(library/init/lean/environment): rename primitive
2019-05-13 15:15:29 -07:00
Leonardo de Moura
3b3e50d315
chore(library/module): std::shared_ptr<modification> ==> modification*
...
Remark: this commit introduce memory leaks, but this is just an
intermediate step to get modification objects in Lean.
Recall that, we will eventually remove modification objects from Lean.
2019-05-13 15:05:21 -07:00
Leonardo de Moura
2e3604e80a
chore(library/module): remove unnecessary field module_ext::m_imported
2019-05-13 14:34:03 -07:00
