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
dbb519d826
feat(library/init/lean/environment): importModules draft
2019-05-14 08:58:29 -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
Leonardo de Moura
99e3cdc01b
chore(frontends/lean): delete lean_environment
2019-05-13 13:05:04 -07:00
Leonardo de Moura
02f90485e6
feat(library/init/lean): use Environment in the new frontend
2019-05-13 13:04:57 -07:00
Leonardo de Moura
8aeff535fc
chore(tests): remove old tests
2019-05-13 12:43:11 -07:00
Leonardo de Moura
edb4d76ecd
feat(kernel/environment): environment as a Lean object
2019-05-13 12:41:33 -07:00
Leonardo de Moura
c57731f8c6
chore(tests/compiler/rbmap): fix test
2019-05-13 12:30:01 -07:00
Leonardo de Moura
deb2310b6d
feat(util/map_foreach): add helper functions for traversing Lean maps
2019-05-13 12:27:59 -07:00
Sebastian Ullrich
de5b68f126
fix(CMakeLists,bin/leanc.in): fix installed leanc
2019-05-12 13:43:36 +02:00
Sebastian Ullrich
13603060cc
fix(tests/playground/binarytrees): fix test
2019-05-12 13:43:36 +02:00
Leonardo de Moura
4392ed2466
fix(library/init/lean/default): make sure environment.lean is initialized
2019-05-11 18:05:11 -07:00
Leonardo de Moura
25879c97fa
test(tests/playground/envtest): add small environment extension test
2019-05-11 17:53:27 -07:00
Leonardo de Moura
f1d16c261d
fix(library/compiler/csimp): do not inline constants with [init] attribute
2019-05-11 17:51:46 -07:00
Leonardo de Moura
2cd2bec831
fix(init/init.cpp): initialization bug
2019-05-11 17:51:23 -07:00
Leonardo de Moura
06390337c6
chore(library/module): fix linker error
2019-05-11 17:08:58 -07:00
Leonardo de Moura
750384142e
perf(library/init/control/estate): missing [inline]
2019-05-11 16:38:25 -07:00
Leonardo de Moura
c46608ced5
feat(library/init/io): implement unsafeIO in Lean
...
Motivation: avoid closure allocation.
2019-05-11 16:28:11 -07:00
Leonardo de Moura
76f643fbf6
chore(library/init/control/estate): add EState.run and EStage.run'
2019-05-11 16:26:51 -07:00
Leonardo de Moura
5f563973f3
feat(library/init/lean/environment): lower level interface for C++
2019-05-11 15:50:02 -07:00
Leonardo de Moura
77c6aa6693
chore(library/init/io): mark unsafeIO as unsafe
...
@kha The previous declaration was fine from the logical point of
view. That is, nobody would be able to prove `false` using the opaque
constant `unsafeIO`. However, its runtime implementation breaks
referencial transparency, and counterintuitive behavior may happen if
it is not used carefully.
2019-05-11 15:46:45 -07:00
Leonardo de Moura
1270353313
feat(library/init/lean/environment): add auxiliary functions
2019-05-11 14:30:06 -07:00
Leonardo de Moura
8ca1b7b2cb
chore(kernel/environment): dead code
2019-05-11 14:13:40 -07:00
Leonardo de Moura
b2f1bad2c7
chore(stage0): update
2019-05-10 17:03:49 -07:00
Leonardo de Moura
7580ad8fe8
feat(library/init/lean/environment): add auxiliary functions for refactoring environment.cpp
2019-05-10 17:02:27 -07:00
Leonardo de Moura
06727e9ca4
chore(kernel/environment): remove dead code
2019-05-10 16:37:13 -07:00
Leonardo de Moura
f5725abb57
refactor(library/init/lean/environment): cleanup and improve
2019-05-10 15:54:29 -07:00
Leonardo de Moura
e0b5f9a018
feat(library/init/lean/environment): extensions can only be registered during initialization
2019-05-10 11:51:42 -07:00
Leonardo de Moura
fd2a5dd45e
feat(library/init/io): add IO.initializing
2019-05-10 11:26:49 -07:00
Leonardo de Moura
708bc42e0a
feat(library/init/lean/environment): generate ModuleData
2019-05-10 11:21:17 -07:00
Leonardo de Moura
251890b490
feat(library/init/control/combinators): add Nat.mfold and rename Nat.for => Nat.fold
2019-05-10 10:47:57 -07:00
Leonardo de Moura
f6b3bc868a
fix(library/init/lean/environment, library/compiler): compilation error and add [implementedBy] attribute
2019-05-10 07:22:56 -07:00
Leonardo de Moura
ecb50b553d
feat(library/init/lean/environment): environment extension registration and API
2019-05-09 16:53:04 -07:00
Leonardo de Moura
3b80ec89b7
feat(library/init/lean/environment): add Environment
...
TODO: finish environment extension
2019-05-09 12:30:52 -07:00
