Commit graph

11087 commits

Author SHA1 Message Date
Leonardo de Moura
7982420d8d fix(library/init/lean/expander, frontends/lean/lean_elaborator): conversion issues 2019-03-21 15:06:46 -07:00
Leonardo de Moura
fd7d676a1d fix(library/compiler/emit_cpp): tail call arguments may be neutral elements 2019-03-21 15:06:46 -07:00
Leonardo de Moura
5f2b74df72 fix(frontends/lean/util): another mismatch to naming convention change 2019-03-21 15:06:46 -07:00
Leonardo de Moura
25414a1f8d fix(util/rb_tree.h): make sure it compiles with g++ 2019-03-21 15:06:46 -07:00
Leonardo de Moura
870a0456c4 fix(frontends/lean/builtin_exprs): match name used at elaborator.lean 2019-03-21 15:06:46 -07:00
Sebastian Ullrich
fc40fbb93f chore(util/rb_tree): suppress warning from suppressing unknown warning 2019-03-21 15:06:45 -07:00
Sebastian Ullrich
d5ec4a4606 chore(frontends/lean/pp): ppAnonymousCtor -> ppAsAnonymousCtor 2019-03-21 15:06:45 -07:00
Sebastian Ullrich
b9edaf888f chore(library/init/core): ne -> Ne, not -> Not 2019-03-21 15:06:45 -07:00
Sebastian Ullrich
97e5aa2411 chore(library): s/Punit/PUnit/g etc 2019-03-21 15:06:45 -07:00
Leonardo de Moura
3af69db6fc chore(stage0): update 2019-03-21 15:06:45 -07:00
Leonardo de Moura
1fe3f14ad0 chore(*): Uint => UInt, Usize => USize 2019-03-21 15:06:44 -07:00
Leonardo de Moura
0b5862b6ce chore(*): and => And 2019-03-21 15:06:44 -07:00
Leonardo de Moura
4c50859129 chore(*): or => Or 2019-03-21 15:06:44 -07:00
Leonardo de Moura
2be87ecd92 chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false 2019-03-21 15:06:44 -07:00
Leonardo de Moura
f8113a01eb chore(library): unit => Unit 2019-03-21 15:06:44 -07:00
Leonardo de Moura
855dab52e0 chore(library/init/Lean): more fixes
`elaborator.lean` is almost working
2019-03-21 15:06:44 -07:00
Leonardo de Moura
7ac847877f chore(library/init/Lean/Parser): more fixes 2019-03-21 15:06:44 -07:00
Leonardo de Moura
5bbc80fdad chore(*): fixed token.lean 2019-03-21 15:06:44 -07:00
Leonardo de Moura
300aae08b3 chore(*): more fixes 2019-03-21 15:06:44 -07:00
Leonardo de Moura
35ddd49e7a chore(frontends/lean/structure_cmd): toParent instead of to_Parent 2019-03-21 15:06:44 -07:00
Leonardo de Moura
ac27bd092b chore(*): small fixes 2019-03-21 15:06:44 -07:00
Leonardo de Moura
e0b0ca4830 chore(*): adapt C++ code to camelCase 2019-03-21 15:06:43 -07:00
Leonardo de Moura
bc75a24127 chore(library, frontends): use camelCase for attribute names 2019-03-21 15:06:43 -07:00
Leonardo de Moura
039e7fab48 refactor(library): add suffixes.h with commonly used suffixes such as brec_on 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
beda5f5f43 chore(library): capitalize types and namespaces 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
f7aeeaf237 exclude export/extern, translate constants.txt 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
0279d29741 chore(shell/CMakeLists): add bin_lean_stage0 target 2019-03-21 13:16:34 +01:00
Sebastian Ullrich
beae045ebc fix(CMakeLists): complete move of stage1 from src/ to build dir 2019-03-21 13:16:17 +01:00
Sebastian Ullrich
ab974c1c4c chore(shell/CMakeLists,library/Makefile): store stage1 C++ output in build directory 2019-03-20 14:27:17 +01:00
Leonardo de Moura
5f54b5887b chore(kernel/declaration): fix compilation warnings 2019-03-19 11:25:55 -07:00
Leonardo de Moura
437f446844 chore(library/type_context): error instead of assertion violation 2019-03-19 11:25:55 -07:00
Leonardo de Moura
aa56578a29 fix(library/compiler/compiler): assertion violations 2019-03-19 11:25:55 -07:00
Leonardo de Moura
4d9d4523fa chore(state0/.gitignore): ignore .o 2019-03-18 18:30:28 -07:00
Leonardo de Moura
d5180ffa17 fix(library/init/lean/elaborator): make sure new frontend can parse the latest core.lean 2019-03-18 15:47:05 -07:00
Leonardo de Moura
81a105cb20 chore(stage0): update 2019-03-18 15:33:30 -07:00
Leonardo de Moura
2610ace69d feat(library/init/io): remove init_io
In the Haskell proposal for top level mutable state
https://wiki.haskell.org/Top_level_mutable_state, they describe the
following problems with using the `IO` monad during initialization.

"A more serious problem is that there is nothing to prevent arbitrary
observable IO actions from appearing to the right of the arrow. If we
perform all actions before executing main, then import becomes a
side-effectful operation, rather than simply a way of bringing names
into scope; furthermore we must specify the order in which actions from
different modules are executed, which would appear to be difficult in
general. If we execute actions on demand (as the unsafePerformIO hack
does) then we are building an unsafe syntactic construct into the
language."

I believe this is not applicable to us. First, our imports are already
side-effectful since we update attributes and the order we import
modules already matters. Second, we have already a well-defined order
in which we import modules. Finally, all global constants are already
being initialized eagerly.

Their ACIO proposal (`init_io` in our implementation) is too restrictive
for what we want to do. For example, to implement an environment
extension mechanism like we have discussed, we would also need `io.ref.write` and
`io.ref.read`. I imagine, we would have a global table, and `register`
would update this table. These extra actions do not satisfy the ACIO restrictions
described in the Haskell proposal. From their document:
"AC stands for Affine Central.
An IO action u is affine if its effect is not indirectly observable, hence need not be performed if the result is unneeded. That is, if u >> v === v for all actions v.
It is central if its effect commutes with every other IO action. That is, if do { x <- u; y <- v; w } === do { y <- v; x <- u; w } for all actions v and w."
It feels like we would have to keep fighting with the ACIO
restrictions. As I said above, our initialization order is well
defined. So, we must document the `[init]` feature and tell users they
should be aware that the `import` is important for initialization
purposes, and that their initialization actions should be
affine central whenever possible.
2019-03-18 15:33:29 -07:00
Leonardo de Moura
4e02edf71f fix(library/compiler/emit_cpp): emit code for invoking user provided initialization functions 2019-03-18 15:33:29 -07:00
Leonardo de Moura
b839ecb3d9 fix(library/compiler/emit_cpp): typo 2019-03-18 15:33:29 -07:00
Leonardo de Moura
08f3459ea3 fix(library/compiler/emit_cpp): stop initialization when error is reported 2019-03-18 15:33:29 -07:00
Leonardo de Moura
9b1c5c09fb feat(library/compiler/emit_cpp): thread io state 2019-03-18 15:33:29 -07:00
Leonardo de Moura
15d89b24a3 feat(library/compiler): [init] attribute
TODO: use attribute when emitting code in the backends.
2019-03-18 15:33:29 -07:00
Sebastian Ullrich
c57e3f7736 fix(shell/CMakeLists): fix REBUILD_STAGE0=OFF, somehow? 2019-03-18 21:19:42 +01:00
Leonardo de Moura
06ac89e184 chore(CMakeLists): temporary fix
@kha Added this fix to make sure I can build Lean
2019-03-18 12:49:49 -07:00
Leonardo de Moura
d45da2d5ba fix(shell/lean): check whether output file was created or not 2019-03-18 12:44:28 -07:00
Sebastian Ullrich
6bd3f1168a chore(src/CMakeLists): remove now-useless standard_lib target and introduce stdlib target at stage0 2019-03-18 20:25:59 +01:00
Sebastian Ullrich
bf5c2ea123 chore(src/CMakeLists,library/Makefile): remove stage1 on clean-olean as well 2019-03-18 20:25:59 +01:00
Leonardo de Moura
06695b5942 chore(CMakeLists.txt): update cmake min version 2019-03-18 11:12:56 -07:00
Sebastian Ullrich
246d2914da chore(CMakeLists): remove dead code 2019-03-18 17:56:40 +01:00
Sebastian Ullrich
9df8d97f0f chore(CMakeLists): add bin target 2019-03-18 17:44:21 +01:00
Sebastian Ullrich
0db283023c chore(src/boot): rename to stage0 2019-03-18 17:14:30 +01:00