From c445199747c60bea3c1a0a04ca8c9560bd63500d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Nov 2019 05:35:15 -0800 Subject: [PATCH] chore: `library/Init` ==> `src/Init` cc @Kha @dselsam @cipher1024 --- library/library.md | 34 ----------------- src/CMakeLists.txt | 35 ++++-------------- {library => src}/Init/Coe.lean | 0 {library => src}/Init/Control.lean | 0 .../Init/Control/Alternative.lean | 0 .../Init/Control/Applicative.lean | 0 .../Init/Control/Conditional.lean | 0 {library => src}/Init/Control/EState.lean | 0 {library => src}/Init/Control/Except.lean | 0 {library => src}/Init/Control/Functor.lean | 0 {library => src}/Init/Control/Id.lean | 0 {library => src}/Init/Control/Lift.lean | 0 {library => src}/Init/Control/Monad.lean | 0 {library => src}/Init/Control/MonadFail.lean | 0 {library => src}/Init/Control/Option.lean | 0 {library => src}/Init/Control/Reader.lean | 0 {library => src}/Init/Control/State.lean | 0 {library => src}/Init/Core.lean | 0 {library => src}/Init/Data.lean | 0 {library => src}/Init/Data/Array.lean | 0 {library => src}/Init/Data/Array/Basic.lean | 0 .../Init/Data/Array/BinSearch.lean | 0 {library => src}/Init/Data/Array/QSort.lean | 0 {library => src}/Init/Data/AssocList.lean | 0 {library => src}/Init/Data/Basic.lean | 0 {library => src}/Init/Data/BinomialHeap.lean | 0 .../Init/Data/BinomialHeap/Basic.lean | 0 {library => src}/Init/Data/ByteArray.lean | 0 .../Init/Data/ByteArray/Basic.lean | 0 {library => src}/Init/Data/Char.lean | 0 {library => src}/Init/Data/Char/Basic.lean | 0 {library => src}/Init/Data/DList.lean | 0 {library => src}/Init/Data/Fin.lean | 0 {library => src}/Init/Data/Fin/Basic.lean | 0 {library => src}/Init/Data/HashMap.lean | 0 {library => src}/Init/Data/HashMap/Basic.lean | 0 {library => src}/Init/Data/HashSet.lean | 0 {library => src}/Init/Data/Hashable.lean | 0 {library => src}/Init/Data/Int.lean | 0 {library => src}/Init/Data/Int/Basic.lean | 0 {library => src}/Init/Data/List.lean | 0 {library => src}/Init/Data/List/Basic.lean | 0 {library => src}/Init/Data/List/BasicAux.lean | 0 {library => src}/Init/Data/List/Control.lean | 0 .../Init/Data/List/Instances.lean | 0 {library => src}/Init/Data/Nat.lean | 0 {library => src}/Init/Data/Nat/Basic.lean | 0 {library => src}/Init/Data/Nat/Bitwise.lean | 0 {library => src}/Init/Data/Nat/Control.lean | 0 {library => src}/Init/Data/Nat/Div.lean | 0 {library => src}/Init/Data/Option.lean | 0 {library => src}/Init/Data/Option/Basic.lean | 0 .../Init/Data/Option/BasicAux.lean | 0 .../Init/Data/Option/Instances.lean | 0 .../Init/Data/PersistentArray.lean | 0 .../Init/Data/PersistentArray/Basic.lean | 0 .../Init/Data/PersistentHashMap.lean | 0 .../Init/Data/PersistentHashMap/Basic.lean | 0 .../Init/Data/PersistentHashSet.lean | 0 {library => src}/Init/Data/Queue.lean | 0 {library => src}/Init/Data/Queue/Basic.lean | 0 {library => src}/Init/Data/RBMap.lean | 0 {library => src}/Init/Data/RBMap/Basic.lean | 0 .../Init/Data/RBMap/BasicAux.lean | 0 {library => src}/Init/Data/RBTree.lean | 0 {library => src}/Init/Data/RBTree/Basic.lean | 0 {library => src}/Init/Data/Random.lean | 0 {library => src}/Init/Data/Repr.lean | 0 {library => src}/Init/Data/Stack.lean | 0 {library => src}/Init/Data/Stack/Basic.lean | 0 {library => src}/Init/Data/String.lean | 0 {library => src}/Init/Data/String/Basic.lean | 0 {library => src}/Init/Data/ToString.lean | 0 {library => src}/Init/Data/UInt.lean | 0 {library => src}/Init/Default.lean | 0 {library => src}/Init/Fix.lean | 0 {library => src}/Init/Lean.lean | 0 {library => src}/Init/Lean/Attributes.lean | 0 {library => src}/Init/Lean/AuxRecursor.lean | 0 {library => src}/Init/Lean/Class.lean | 0 {library => src}/Init/Lean/Compiler.lean | 0 .../Init/Lean/Compiler/ClosedTermCache.lean | 0 .../Init/Lean/Compiler/ConstFolding.lean | 0 .../Init/Lean/Compiler/ExportAttr.lean | 0 .../Init/Lean/Compiler/ExternAttr.lean | 0 {library => src}/Init/Lean/Compiler/IR.lean | 0 .../Init/Lean/Compiler/IR/Basic.lean | 0 .../Init/Lean/Compiler/IR/Borrow.lean | 0 .../Init/Lean/Compiler/IR/Boxing.lean | 0 .../Init/Lean/Compiler/IR/Checker.lean | 0 .../Init/Lean/Compiler/IR/CompilerM.lean | 0 .../Init/Lean/Compiler/IR/CtorLayout.lean | 0 .../Lean/Compiler/IR/ElimDeadBranches.lean | 0 .../Init/Lean/Compiler/IR/ElimDeadVars.lean | 0 .../Init/Lean/Compiler/IR/EmitC.lean | 0 .../Init/Lean/Compiler/IR/EmitUtil.lean | 0 .../Lean/Compiler/IR/ExpandResetReuse.lean | 0 .../Init/Lean/Compiler/IR/Format.lean | 0 .../Init/Lean/Compiler/IR/FreeVars.lean | 0 .../Init/Lean/Compiler/IR/LiveVars.lean | 0 .../Init/Lean/Compiler/IR/NormIds.lean | 0 .../Init/Lean/Compiler/IR/PushProj.lean | 0 .../Init/Lean/Compiler/IR/RC.lean | 0 .../Init/Lean/Compiler/IR/ResetReuse.lean | 0 .../Init/Lean/Compiler/IR/SimpCase.lean | 0 .../Init/Lean/Compiler/IR/UnboxResult.lean | 0 .../Init/Lean/Compiler/ImplementedByAttr.lean | 0 .../Init/Lean/Compiler/InitAttr.lean | 0 .../Init/Lean/Compiler/InlineAttrs.lean | 0 .../Init/Lean/Compiler/NameMangling.lean | 0 .../Init/Lean/Compiler/NeverExtractAttr.lean | 0 .../Init/Lean/Compiler/Specialize.lean | 0 {library => src}/Init/Lean/Compiler/Util.lean | 0 {library => src}/Init/Lean/Declaration.lean | 0 {library => src}/Init/Lean/Elaborator.lean | 0 .../Init/Lean/Elaborator/Alias.lean | 0 .../Init/Lean/Elaborator/Basic.lean | 0 .../Init/Lean/Elaborator/Command.lean | 0 .../Lean/Elaborator/ElabStrategyAttrs.lean | 0 .../Init/Lean/Elaborator/PreTerm.lean | 0 .../Init/Lean/Elaborator/ResolveName.lean | 0 .../Init/Lean/Elaborator/Term.lean | 0 {library => src}/Init/Lean/Environment.lean | 0 {library => src}/Init/Lean/EqnCompiler.lean | 0 .../Init/Lean/EqnCompiler/MatchPattern.lean | 0 {library => src}/Init/Lean/Expr.lean | 0 {library => src}/Init/Lean/Format.lean | 0 {library => src}/Init/Lean/KVMap.lean | 0 {library => src}/Init/Lean/LBool.lean | 0 {library => src}/Init/Lean/LOption.lean | 0 {library => src}/Init/Lean/Level.lean | 0 {library => src}/Init/Lean/Linter.lean | 0 {library => src}/Init/Lean/LocalContext.lean | 0 {library => src}/Init/Lean/Message.lean | 0 {library => src}/Init/Lean/Meta.lean | 0 {library => src}/Init/Lean/Meta/Basic.lean | 0 {library => src}/Init/Lean/Meta/Check.lean | 0 .../Init/Lean/Meta/Exception.lean | 0 .../Init/Lean/Meta/ExprDefEq.lean | 0 {library => src}/Init/Lean/Meta/FunInfo.lean | 0 .../Init/Lean/Meta/InferType.lean | 0 .../Init/Lean/Meta/LevelDefEq.lean | 0 {library => src}/Init/Lean/Meta/Offset.lean | 0 {library => src}/Init/Lean/Meta/WHNF.lean | 0 .../Init/Lean/MetavarContext.lean | 0 {library => src}/Init/Lean/Modifiers.lean | 0 {library => src}/Init/Lean/MonadCache.lean | 0 {library => src}/Init/Lean/Name.lean | 0 {library => src}/Init/Lean/NameGenerator.lean | 0 {library => src}/Init/Lean/Options.lean | 0 {library => src}/Init/Lean/Parser.lean | 0 .../Init/Lean/Parser/Command.lean | 0 .../Init/Lean/Parser/Identifier.lean | 0 {library => src}/Init/Lean/Parser/Level.lean | 0 {library => src}/Init/Lean/Parser/Module.lean | 0 {library => src}/Init/Lean/Parser/Parser.lean | 0 {library => src}/Init/Lean/Parser/Term.lean | 0 .../Init/Lean/Parser/Transform.lean | 0 {library => src}/Init/Lean/Parser/Trie.lean | 0 {library => src}/Init/Lean/Path.lean | 0 {library => src}/Init/Lean/Position.lean | 0 {library => src}/Init/Lean/ProjFns.lean | 0 .../Init/Lean/ReducibilityAttrs.lean | 0 {library => src}/Init/Lean/Runtime.lean | 0 {library => src}/Init/Lean/SMap.lean | 0 {library => src}/Init/Lean/Scopes.lean | 0 {library => src}/Init/Lean/Syntax.lean | 0 {library => src}/Init/Lean/ToExpr.lean | 0 {library => src}/Init/Lean/Trace.lean | 0 {library => src}/Init/Lean/TypeClass.lean | 0 .../Init/Lean/TypeClass/Basic.lean | 0 .../Init/Lean/TypeClass/Context.lean | 0 .../Init/Lean/TypeClass/Synth.lean | 0 {library => src}/Init/Lean/Util.lean | 0 {library => src}/Init/Lean/WHNF.lean | 0 {library => src}/Init/System.lean | 0 {library => src}/Init/System/FilePath.lean | 0 {library => src}/Init/System/IO.lean | 0 {library => src}/Init/System/Platform.lean | 0 {library => src}/Init/Util.lean | 0 {library => src}/Init/WF.lean | 0 {library => src}/Makefile.in | 11 +++--- {library => src}/relative.py | 0 src/shell/CMakeLists.txt | 37 +++---------------- 184 files changed, 19 insertions(+), 98 deletions(-) delete mode 100644 library/library.md rename {library => src}/Init/Coe.lean (100%) rename {library => src}/Init/Control.lean (100%) rename {library => src}/Init/Control/Alternative.lean (100%) rename {library => src}/Init/Control/Applicative.lean (100%) rename {library => src}/Init/Control/Conditional.lean (100%) rename {library => src}/Init/Control/EState.lean (100%) rename {library => src}/Init/Control/Except.lean (100%) rename {library => src}/Init/Control/Functor.lean (100%) rename {library => src}/Init/Control/Id.lean (100%) rename {library => src}/Init/Control/Lift.lean (100%) rename {library => src}/Init/Control/Monad.lean (100%) rename {library => src}/Init/Control/MonadFail.lean (100%) rename {library => src}/Init/Control/Option.lean (100%) rename {library => src}/Init/Control/Reader.lean (100%) rename {library => src}/Init/Control/State.lean (100%) rename {library => src}/Init/Core.lean (100%) rename {library => src}/Init/Data.lean (100%) rename {library => src}/Init/Data/Array.lean (100%) rename {library => src}/Init/Data/Array/Basic.lean (100%) rename {library => src}/Init/Data/Array/BinSearch.lean (100%) rename {library => src}/Init/Data/Array/QSort.lean (100%) rename {library => src}/Init/Data/AssocList.lean (100%) rename {library => src}/Init/Data/Basic.lean (100%) rename {library => src}/Init/Data/BinomialHeap.lean (100%) rename {library => src}/Init/Data/BinomialHeap/Basic.lean (100%) rename {library => src}/Init/Data/ByteArray.lean (100%) rename {library => src}/Init/Data/ByteArray/Basic.lean (100%) rename {library => src}/Init/Data/Char.lean (100%) rename {library => src}/Init/Data/Char/Basic.lean (100%) rename {library => src}/Init/Data/DList.lean (100%) rename {library => src}/Init/Data/Fin.lean (100%) rename {library => src}/Init/Data/Fin/Basic.lean (100%) rename {library => src}/Init/Data/HashMap.lean (100%) rename {library => src}/Init/Data/HashMap/Basic.lean (100%) rename {library => src}/Init/Data/HashSet.lean (100%) rename {library => src}/Init/Data/Hashable.lean (100%) rename {library => src}/Init/Data/Int.lean (100%) rename {library => src}/Init/Data/Int/Basic.lean (100%) rename {library => src}/Init/Data/List.lean (100%) rename {library => src}/Init/Data/List/Basic.lean (100%) rename {library => src}/Init/Data/List/BasicAux.lean (100%) rename {library => src}/Init/Data/List/Control.lean (100%) rename {library => src}/Init/Data/List/Instances.lean (100%) rename {library => src}/Init/Data/Nat.lean (100%) rename {library => src}/Init/Data/Nat/Basic.lean (100%) rename {library => src}/Init/Data/Nat/Bitwise.lean (100%) rename {library => src}/Init/Data/Nat/Control.lean (100%) rename {library => src}/Init/Data/Nat/Div.lean (100%) rename {library => src}/Init/Data/Option.lean (100%) rename {library => src}/Init/Data/Option/Basic.lean (100%) rename {library => src}/Init/Data/Option/BasicAux.lean (100%) rename {library => src}/Init/Data/Option/Instances.lean (100%) rename {library => src}/Init/Data/PersistentArray.lean (100%) rename {library => src}/Init/Data/PersistentArray/Basic.lean (100%) rename {library => src}/Init/Data/PersistentHashMap.lean (100%) rename {library => src}/Init/Data/PersistentHashMap/Basic.lean (100%) rename {library => src}/Init/Data/PersistentHashSet.lean (100%) rename {library => src}/Init/Data/Queue.lean (100%) rename {library => src}/Init/Data/Queue/Basic.lean (100%) rename {library => src}/Init/Data/RBMap.lean (100%) rename {library => src}/Init/Data/RBMap/Basic.lean (100%) rename {library => src}/Init/Data/RBMap/BasicAux.lean (100%) rename {library => src}/Init/Data/RBTree.lean (100%) rename {library => src}/Init/Data/RBTree/Basic.lean (100%) rename {library => src}/Init/Data/Random.lean (100%) rename {library => src}/Init/Data/Repr.lean (100%) rename {library => src}/Init/Data/Stack.lean (100%) rename {library => src}/Init/Data/Stack/Basic.lean (100%) rename {library => src}/Init/Data/String.lean (100%) rename {library => src}/Init/Data/String/Basic.lean (100%) rename {library => src}/Init/Data/ToString.lean (100%) rename {library => src}/Init/Data/UInt.lean (100%) rename {library => src}/Init/Default.lean (100%) rename {library => src}/Init/Fix.lean (100%) rename {library => src}/Init/Lean.lean (100%) rename {library => src}/Init/Lean/Attributes.lean (100%) rename {library => src}/Init/Lean/AuxRecursor.lean (100%) rename {library => src}/Init/Lean/Class.lean (100%) rename {library => src}/Init/Lean/Compiler.lean (100%) rename {library => src}/Init/Lean/Compiler/ClosedTermCache.lean (100%) rename {library => src}/Init/Lean/Compiler/ConstFolding.lean (100%) rename {library => src}/Init/Lean/Compiler/ExportAttr.lean (100%) rename {library => src}/Init/Lean/Compiler/ExternAttr.lean (100%) rename {library => src}/Init/Lean/Compiler/IR.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/Basic.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/Borrow.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/Boxing.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/Checker.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/CompilerM.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/CtorLayout.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/ElimDeadBranches.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/ElimDeadVars.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/EmitC.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/EmitUtil.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/ExpandResetReuse.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/Format.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/FreeVars.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/LiveVars.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/NormIds.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/PushProj.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/RC.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/ResetReuse.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/SimpCase.lean (100%) rename {library => src}/Init/Lean/Compiler/IR/UnboxResult.lean (100%) rename {library => src}/Init/Lean/Compiler/ImplementedByAttr.lean (100%) rename {library => src}/Init/Lean/Compiler/InitAttr.lean (100%) rename {library => src}/Init/Lean/Compiler/InlineAttrs.lean (100%) rename {library => src}/Init/Lean/Compiler/NameMangling.lean (100%) rename {library => src}/Init/Lean/Compiler/NeverExtractAttr.lean (100%) rename {library => src}/Init/Lean/Compiler/Specialize.lean (100%) rename {library => src}/Init/Lean/Compiler/Util.lean (100%) rename {library => src}/Init/Lean/Declaration.lean (100%) rename {library => src}/Init/Lean/Elaborator.lean (100%) rename {library => src}/Init/Lean/Elaborator/Alias.lean (100%) rename {library => src}/Init/Lean/Elaborator/Basic.lean (100%) rename {library => src}/Init/Lean/Elaborator/Command.lean (100%) rename {library => src}/Init/Lean/Elaborator/ElabStrategyAttrs.lean (100%) rename {library => src}/Init/Lean/Elaborator/PreTerm.lean (100%) rename {library => src}/Init/Lean/Elaborator/ResolveName.lean (100%) rename {library => src}/Init/Lean/Elaborator/Term.lean (100%) rename {library => src}/Init/Lean/Environment.lean (100%) rename {library => src}/Init/Lean/EqnCompiler.lean (100%) rename {library => src}/Init/Lean/EqnCompiler/MatchPattern.lean (100%) rename {library => src}/Init/Lean/Expr.lean (100%) rename {library => src}/Init/Lean/Format.lean (100%) rename {library => src}/Init/Lean/KVMap.lean (100%) rename {library => src}/Init/Lean/LBool.lean (100%) rename {library => src}/Init/Lean/LOption.lean (100%) rename {library => src}/Init/Lean/Level.lean (100%) rename {library => src}/Init/Lean/Linter.lean (100%) rename {library => src}/Init/Lean/LocalContext.lean (100%) rename {library => src}/Init/Lean/Message.lean (100%) rename {library => src}/Init/Lean/Meta.lean (100%) rename {library => src}/Init/Lean/Meta/Basic.lean (100%) rename {library => src}/Init/Lean/Meta/Check.lean (100%) rename {library => src}/Init/Lean/Meta/Exception.lean (100%) rename {library => src}/Init/Lean/Meta/ExprDefEq.lean (100%) rename {library => src}/Init/Lean/Meta/FunInfo.lean (100%) rename {library => src}/Init/Lean/Meta/InferType.lean (100%) rename {library => src}/Init/Lean/Meta/LevelDefEq.lean (100%) rename {library => src}/Init/Lean/Meta/Offset.lean (100%) rename {library => src}/Init/Lean/Meta/WHNF.lean (100%) rename {library => src}/Init/Lean/MetavarContext.lean (100%) rename {library => src}/Init/Lean/Modifiers.lean (100%) rename {library => src}/Init/Lean/MonadCache.lean (100%) rename {library => src}/Init/Lean/Name.lean (100%) rename {library => src}/Init/Lean/NameGenerator.lean (100%) rename {library => src}/Init/Lean/Options.lean (100%) rename {library => src}/Init/Lean/Parser.lean (100%) rename {library => src}/Init/Lean/Parser/Command.lean (100%) rename {library => src}/Init/Lean/Parser/Identifier.lean (100%) rename {library => src}/Init/Lean/Parser/Level.lean (100%) rename {library => src}/Init/Lean/Parser/Module.lean (100%) rename {library => src}/Init/Lean/Parser/Parser.lean (100%) rename {library => src}/Init/Lean/Parser/Term.lean (100%) rename {library => src}/Init/Lean/Parser/Transform.lean (100%) rename {library => src}/Init/Lean/Parser/Trie.lean (100%) rename {library => src}/Init/Lean/Path.lean (100%) rename {library => src}/Init/Lean/Position.lean (100%) rename {library => src}/Init/Lean/ProjFns.lean (100%) rename {library => src}/Init/Lean/ReducibilityAttrs.lean (100%) rename {library => src}/Init/Lean/Runtime.lean (100%) rename {library => src}/Init/Lean/SMap.lean (100%) rename {library => src}/Init/Lean/Scopes.lean (100%) rename {library => src}/Init/Lean/Syntax.lean (100%) rename {library => src}/Init/Lean/ToExpr.lean (100%) rename {library => src}/Init/Lean/Trace.lean (100%) rename {library => src}/Init/Lean/TypeClass.lean (100%) rename {library => src}/Init/Lean/TypeClass/Basic.lean (100%) rename {library => src}/Init/Lean/TypeClass/Context.lean (100%) rename {library => src}/Init/Lean/TypeClass/Synth.lean (100%) rename {library => src}/Init/Lean/Util.lean (100%) rename {library => src}/Init/Lean/WHNF.lean (100%) rename {library => src}/Init/System.lean (100%) rename {library => src}/Init/System/FilePath.lean (100%) rename {library => src}/Init/System/IO.lean (100%) rename {library => src}/Init/System/Platform.lean (100%) rename {library => src}/Init/Util.lean (100%) rename {library => src}/Init/WF.lean (100%) rename {library => src}/Makefile.in (87%) rename {library => src}/relative.py (100%) diff --git a/library/library.md b/library/library.md deleted file mode 100644 index 8093c718c5..0000000000 --- a/library/library.md +++ /dev/null @@ -1,34 +0,0 @@ -The Lean Core Library -========================= - -The Lean core library is contained in the following files and directories: - -* [init](init/) : constants and theorems needed for low-level system operations -* [init/logic.lean](init/logic.lean) : logical constructs and axioms -* [init/data](init/data/) : concrete datatypes and type constructors -* [init/algebra](init/algebra/) : algebraic structures - -Lean's default logical framework is a version of the Calculus of -Constructions with: - -* an impredicative, proof-irrelevant type `Prop` of propositions -* universe polymorphism -* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... above `Prop` -* inductively defined types -* quotient types - -Most of the `core` library does not rely on any axioms beyond this -framework, and is hence fully constructive. - -The following additional axioms are defined in `init`: - -* quotients and propositional extensionality (in `quot`) -* Hilbert choice (in `classical`) - -Function extensionality is derived from the quotient construction, and -excluded middle is derived from Hilbert choice. For Hilbert choice and -excluded middle, use `open classical`. The additional axioms are used -sparingly. For example: - -You can use `#print axioms foo` to see which axioms `foo` depends -on. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ff48a8f9f4..60decc40fd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -182,8 +182,7 @@ if("${CMAKE_C_COMPILER}" MATCHES "emcc") set(CFLAGS_EMSCRIPTEN "-Oz -O3") set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} ${CFLAGS_EMSCRIPTEN} -D LEAN_EMSCRIPTEN") set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} --memory-init-file 0 --llvm-lto 1 -s ALLOW_MEMORY_GROWTH=1 -s DISABLE_EXCEPTION_CATCHING=0 ${CFLAGS_EMSCRIPTEN}") - set(LEAN_JS_LIBRARY "${CMAKE_CURRENT_SOURCE_DIR}/../library" CACHE STRING - "location of olean files for lean.js") + set(LEAN_JS_LIBRARY "${CMAKE_CURRENT_SOURCE_DIR}" CACHE STRING "location of olean files for lean.js") endif() if (CMAKE_CROSSCOMPILING_EMULATOR) # emscripten likes to quote "node" @@ -490,7 +489,7 @@ configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h") configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h") install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}") if(NOT STAGE0) - configure_file("${LEAN_SOURCE_DIR}/../library/Makefile.in" "${LEAN_SOURCE_DIR}/../library/Makefile") + configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile") endif() include_directories("${LEAN_BINARY_DIR}") @@ -515,7 +514,7 @@ set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(initialize) set(LEAN_OBJS ${LEAN_OBJS} $) if(STAGE0) - add_subdirectory(../library stdlib) + add_subdirectory(Init stdlib) set(LEAN_OBJS ${LEAN_OBJS} $) endif() if(EMSCRIPTEN) @@ -622,25 +621,13 @@ add_style_check_target(style "${LEAN_SOURCES}") add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py" ${LEAN_SOURCES}) endif() -# add_custom_target( -# leanpkg ALL -# COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS} -# DEPENDS standard_lib -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg" -# ) - add_custom_target(clean-stdlib - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" - COMMAND find . -name *.olean -delete - COMMAND find . -name *.depend -delete + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init" + COMMAND find . -name '*.olean' -delete + COMMAND find . -name '*.depend' -delete COMMAND rm -r ../src/stage1 "${CMAKE_BINARY_DIR}/stage1" || true ) -add_custom_target(clean-leanpkg - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg" - COMMAND "${CMAKE_COMMAND}" -P "${CMAKE_MODULE_PATH}/CleanOlean.cmake" - ) - add_custom_target(clean-olean DEPENDS clean-stdlib) @@ -654,18 +641,10 @@ install(FILES "${CMAKE_SOURCE_DIR}/../bin/leanpkg" DESTINATION bin PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE) -install(DIRECTORY "${CMAKE_SOURCE_DIR}/../library" DESTINATION "${LIBRARY_DIR}" +install(DIRECTORY "${CMAKE_SOURCE_DIR}/Init" DESTINATION "${LIBRARY_DIR}" FILES_MATCHING PATTERN "*.lean" PATTERN "*.olean" - PATTERN "leanpkg.toml" - PATTERN "*.md") - -install(DIRECTORY "${CMAKE_SOURCE_DIR}/../leanpkg" DESTINATION "${LIBRARY_DIR}" - FILES_MATCHING - PATTERN "*.lean" - PATTERN "*.olean" - PATTERN "leanpkg.toml" PATTERN "*.md") install(DIRECTORY "${CMAKE_SOURCE_DIR}/runtime" DESTINATION "${INCLUDE_DIR}" diff --git a/library/Init/Coe.lean b/src/Init/Coe.lean similarity index 100% rename from library/Init/Coe.lean rename to src/Init/Coe.lean diff --git a/library/Init/Control.lean b/src/Init/Control.lean similarity index 100% rename from library/Init/Control.lean rename to src/Init/Control.lean diff --git a/library/Init/Control/Alternative.lean b/src/Init/Control/Alternative.lean similarity index 100% rename from library/Init/Control/Alternative.lean rename to src/Init/Control/Alternative.lean diff --git a/library/Init/Control/Applicative.lean b/src/Init/Control/Applicative.lean similarity index 100% rename from library/Init/Control/Applicative.lean rename to src/Init/Control/Applicative.lean diff --git a/library/Init/Control/Conditional.lean b/src/Init/Control/Conditional.lean similarity index 100% rename from library/Init/Control/Conditional.lean rename to src/Init/Control/Conditional.lean diff --git a/library/Init/Control/EState.lean b/src/Init/Control/EState.lean similarity index 100% rename from library/Init/Control/EState.lean rename to src/Init/Control/EState.lean diff --git a/library/Init/Control/Except.lean b/src/Init/Control/Except.lean similarity index 100% rename from library/Init/Control/Except.lean rename to src/Init/Control/Except.lean diff --git a/library/Init/Control/Functor.lean b/src/Init/Control/Functor.lean similarity index 100% rename from library/Init/Control/Functor.lean rename to src/Init/Control/Functor.lean diff --git a/library/Init/Control/Id.lean b/src/Init/Control/Id.lean similarity index 100% rename from library/Init/Control/Id.lean rename to src/Init/Control/Id.lean diff --git a/library/Init/Control/Lift.lean b/src/Init/Control/Lift.lean similarity index 100% rename from library/Init/Control/Lift.lean rename to src/Init/Control/Lift.lean diff --git a/library/Init/Control/Monad.lean b/src/Init/Control/Monad.lean similarity index 100% rename from library/Init/Control/Monad.lean rename to src/Init/Control/Monad.lean diff --git a/library/Init/Control/MonadFail.lean b/src/Init/Control/MonadFail.lean similarity index 100% rename from library/Init/Control/MonadFail.lean rename to src/Init/Control/MonadFail.lean diff --git a/library/Init/Control/Option.lean b/src/Init/Control/Option.lean similarity index 100% rename from library/Init/Control/Option.lean rename to src/Init/Control/Option.lean diff --git a/library/Init/Control/Reader.lean b/src/Init/Control/Reader.lean similarity index 100% rename from library/Init/Control/Reader.lean rename to src/Init/Control/Reader.lean diff --git a/library/Init/Control/State.lean b/src/Init/Control/State.lean similarity index 100% rename from library/Init/Control/State.lean rename to src/Init/Control/State.lean diff --git a/library/Init/Core.lean b/src/Init/Core.lean similarity index 100% rename from library/Init/Core.lean rename to src/Init/Core.lean diff --git a/library/Init/Data.lean b/src/Init/Data.lean similarity index 100% rename from library/Init/Data.lean rename to src/Init/Data.lean diff --git a/library/Init/Data/Array.lean b/src/Init/Data/Array.lean similarity index 100% rename from library/Init/Data/Array.lean rename to src/Init/Data/Array.lean diff --git a/library/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean similarity index 100% rename from library/Init/Data/Array/Basic.lean rename to src/Init/Data/Array/Basic.lean diff --git a/library/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean similarity index 100% rename from library/Init/Data/Array/BinSearch.lean rename to src/Init/Data/Array/BinSearch.lean diff --git a/library/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean similarity index 100% rename from library/Init/Data/Array/QSort.lean rename to src/Init/Data/Array/QSort.lean diff --git a/library/Init/Data/AssocList.lean b/src/Init/Data/AssocList.lean similarity index 100% rename from library/Init/Data/AssocList.lean rename to src/Init/Data/AssocList.lean diff --git a/library/Init/Data/Basic.lean b/src/Init/Data/Basic.lean similarity index 100% rename from library/Init/Data/Basic.lean rename to src/Init/Data/Basic.lean diff --git a/library/Init/Data/BinomialHeap.lean b/src/Init/Data/BinomialHeap.lean similarity index 100% rename from library/Init/Data/BinomialHeap.lean rename to src/Init/Data/BinomialHeap.lean diff --git a/library/Init/Data/BinomialHeap/Basic.lean b/src/Init/Data/BinomialHeap/Basic.lean similarity index 100% rename from library/Init/Data/BinomialHeap/Basic.lean rename to src/Init/Data/BinomialHeap/Basic.lean diff --git a/library/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean similarity index 100% rename from library/Init/Data/ByteArray.lean rename to src/Init/Data/ByteArray.lean diff --git a/library/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean similarity index 100% rename from library/Init/Data/ByteArray/Basic.lean rename to src/Init/Data/ByteArray/Basic.lean diff --git a/library/Init/Data/Char.lean b/src/Init/Data/Char.lean similarity index 100% rename from library/Init/Data/Char.lean rename to src/Init/Data/Char.lean diff --git a/library/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean similarity index 100% rename from library/Init/Data/Char/Basic.lean rename to src/Init/Data/Char/Basic.lean diff --git a/library/Init/Data/DList.lean b/src/Init/Data/DList.lean similarity index 100% rename from library/Init/Data/DList.lean rename to src/Init/Data/DList.lean diff --git a/library/Init/Data/Fin.lean b/src/Init/Data/Fin.lean similarity index 100% rename from library/Init/Data/Fin.lean rename to src/Init/Data/Fin.lean diff --git a/library/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean similarity index 100% rename from library/Init/Data/Fin/Basic.lean rename to src/Init/Data/Fin/Basic.lean diff --git a/library/Init/Data/HashMap.lean b/src/Init/Data/HashMap.lean similarity index 100% rename from library/Init/Data/HashMap.lean rename to src/Init/Data/HashMap.lean diff --git a/library/Init/Data/HashMap/Basic.lean b/src/Init/Data/HashMap/Basic.lean similarity index 100% rename from library/Init/Data/HashMap/Basic.lean rename to src/Init/Data/HashMap/Basic.lean diff --git a/library/Init/Data/HashSet.lean b/src/Init/Data/HashSet.lean similarity index 100% rename from library/Init/Data/HashSet.lean rename to src/Init/Data/HashSet.lean diff --git a/library/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean similarity index 100% rename from library/Init/Data/Hashable.lean rename to src/Init/Data/Hashable.lean diff --git a/library/Init/Data/Int.lean b/src/Init/Data/Int.lean similarity index 100% rename from library/Init/Data/Int.lean rename to src/Init/Data/Int.lean diff --git a/library/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean similarity index 100% rename from library/Init/Data/Int/Basic.lean rename to src/Init/Data/Int/Basic.lean diff --git a/library/Init/Data/List.lean b/src/Init/Data/List.lean similarity index 100% rename from library/Init/Data/List.lean rename to src/Init/Data/List.lean diff --git a/library/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean similarity index 100% rename from library/Init/Data/List/Basic.lean rename to src/Init/Data/List/Basic.lean diff --git a/library/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean similarity index 100% rename from library/Init/Data/List/BasicAux.lean rename to src/Init/Data/List/BasicAux.lean diff --git a/library/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean similarity index 100% rename from library/Init/Data/List/Control.lean rename to src/Init/Data/List/Control.lean diff --git a/library/Init/Data/List/Instances.lean b/src/Init/Data/List/Instances.lean similarity index 100% rename from library/Init/Data/List/Instances.lean rename to src/Init/Data/List/Instances.lean diff --git a/library/Init/Data/Nat.lean b/src/Init/Data/Nat.lean similarity index 100% rename from library/Init/Data/Nat.lean rename to src/Init/Data/Nat.lean diff --git a/library/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean similarity index 100% rename from library/Init/Data/Nat/Basic.lean rename to src/Init/Data/Nat/Basic.lean diff --git a/library/Init/Data/Nat/Bitwise.lean b/src/Init/Data/Nat/Bitwise.lean similarity index 100% rename from library/Init/Data/Nat/Bitwise.lean rename to src/Init/Data/Nat/Bitwise.lean diff --git a/library/Init/Data/Nat/Control.lean b/src/Init/Data/Nat/Control.lean similarity index 100% rename from library/Init/Data/Nat/Control.lean rename to src/Init/Data/Nat/Control.lean diff --git a/library/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean similarity index 100% rename from library/Init/Data/Nat/Div.lean rename to src/Init/Data/Nat/Div.lean diff --git a/library/Init/Data/Option.lean b/src/Init/Data/Option.lean similarity index 100% rename from library/Init/Data/Option.lean rename to src/Init/Data/Option.lean diff --git a/library/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean similarity index 100% rename from library/Init/Data/Option/Basic.lean rename to src/Init/Data/Option/Basic.lean diff --git a/library/Init/Data/Option/BasicAux.lean b/src/Init/Data/Option/BasicAux.lean similarity index 100% rename from library/Init/Data/Option/BasicAux.lean rename to src/Init/Data/Option/BasicAux.lean diff --git a/library/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean similarity index 100% rename from library/Init/Data/Option/Instances.lean rename to src/Init/Data/Option/Instances.lean diff --git a/library/Init/Data/PersistentArray.lean b/src/Init/Data/PersistentArray.lean similarity index 100% rename from library/Init/Data/PersistentArray.lean rename to src/Init/Data/PersistentArray.lean diff --git a/library/Init/Data/PersistentArray/Basic.lean b/src/Init/Data/PersistentArray/Basic.lean similarity index 100% rename from library/Init/Data/PersistentArray/Basic.lean rename to src/Init/Data/PersistentArray/Basic.lean diff --git a/library/Init/Data/PersistentHashMap.lean b/src/Init/Data/PersistentHashMap.lean similarity index 100% rename from library/Init/Data/PersistentHashMap.lean rename to src/Init/Data/PersistentHashMap.lean diff --git a/library/Init/Data/PersistentHashMap/Basic.lean b/src/Init/Data/PersistentHashMap/Basic.lean similarity index 100% rename from library/Init/Data/PersistentHashMap/Basic.lean rename to src/Init/Data/PersistentHashMap/Basic.lean diff --git a/library/Init/Data/PersistentHashSet.lean b/src/Init/Data/PersistentHashSet.lean similarity index 100% rename from library/Init/Data/PersistentHashSet.lean rename to src/Init/Data/PersistentHashSet.lean diff --git a/library/Init/Data/Queue.lean b/src/Init/Data/Queue.lean similarity index 100% rename from library/Init/Data/Queue.lean rename to src/Init/Data/Queue.lean diff --git a/library/Init/Data/Queue/Basic.lean b/src/Init/Data/Queue/Basic.lean similarity index 100% rename from library/Init/Data/Queue/Basic.lean rename to src/Init/Data/Queue/Basic.lean diff --git a/library/Init/Data/RBMap.lean b/src/Init/Data/RBMap.lean similarity index 100% rename from library/Init/Data/RBMap.lean rename to src/Init/Data/RBMap.lean diff --git a/library/Init/Data/RBMap/Basic.lean b/src/Init/Data/RBMap/Basic.lean similarity index 100% rename from library/Init/Data/RBMap/Basic.lean rename to src/Init/Data/RBMap/Basic.lean diff --git a/library/Init/Data/RBMap/BasicAux.lean b/src/Init/Data/RBMap/BasicAux.lean similarity index 100% rename from library/Init/Data/RBMap/BasicAux.lean rename to src/Init/Data/RBMap/BasicAux.lean diff --git a/library/Init/Data/RBTree.lean b/src/Init/Data/RBTree.lean similarity index 100% rename from library/Init/Data/RBTree.lean rename to src/Init/Data/RBTree.lean diff --git a/library/Init/Data/RBTree/Basic.lean b/src/Init/Data/RBTree/Basic.lean similarity index 100% rename from library/Init/Data/RBTree/Basic.lean rename to src/Init/Data/RBTree/Basic.lean diff --git a/library/Init/Data/Random.lean b/src/Init/Data/Random.lean similarity index 100% rename from library/Init/Data/Random.lean rename to src/Init/Data/Random.lean diff --git a/library/Init/Data/Repr.lean b/src/Init/Data/Repr.lean similarity index 100% rename from library/Init/Data/Repr.lean rename to src/Init/Data/Repr.lean diff --git a/library/Init/Data/Stack.lean b/src/Init/Data/Stack.lean similarity index 100% rename from library/Init/Data/Stack.lean rename to src/Init/Data/Stack.lean diff --git a/library/Init/Data/Stack/Basic.lean b/src/Init/Data/Stack/Basic.lean similarity index 100% rename from library/Init/Data/Stack/Basic.lean rename to src/Init/Data/Stack/Basic.lean diff --git a/library/Init/Data/String.lean b/src/Init/Data/String.lean similarity index 100% rename from library/Init/Data/String.lean rename to src/Init/Data/String.lean diff --git a/library/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean similarity index 100% rename from library/Init/Data/String/Basic.lean rename to src/Init/Data/String/Basic.lean diff --git a/library/Init/Data/ToString.lean b/src/Init/Data/ToString.lean similarity index 100% rename from library/Init/Data/ToString.lean rename to src/Init/Data/ToString.lean diff --git a/library/Init/Data/UInt.lean b/src/Init/Data/UInt.lean similarity index 100% rename from library/Init/Data/UInt.lean rename to src/Init/Data/UInt.lean diff --git a/library/Init/Default.lean b/src/Init/Default.lean similarity index 100% rename from library/Init/Default.lean rename to src/Init/Default.lean diff --git a/library/Init/Fix.lean b/src/Init/Fix.lean similarity index 100% rename from library/Init/Fix.lean rename to src/Init/Fix.lean diff --git a/library/Init/Lean.lean b/src/Init/Lean.lean similarity index 100% rename from library/Init/Lean.lean rename to src/Init/Lean.lean diff --git a/library/Init/Lean/Attributes.lean b/src/Init/Lean/Attributes.lean similarity index 100% rename from library/Init/Lean/Attributes.lean rename to src/Init/Lean/Attributes.lean diff --git a/library/Init/Lean/AuxRecursor.lean b/src/Init/Lean/AuxRecursor.lean similarity index 100% rename from library/Init/Lean/AuxRecursor.lean rename to src/Init/Lean/AuxRecursor.lean diff --git a/library/Init/Lean/Class.lean b/src/Init/Lean/Class.lean similarity index 100% rename from library/Init/Lean/Class.lean rename to src/Init/Lean/Class.lean diff --git a/library/Init/Lean/Compiler.lean b/src/Init/Lean/Compiler.lean similarity index 100% rename from library/Init/Lean/Compiler.lean rename to src/Init/Lean/Compiler.lean diff --git a/library/Init/Lean/Compiler/ClosedTermCache.lean b/src/Init/Lean/Compiler/ClosedTermCache.lean similarity index 100% rename from library/Init/Lean/Compiler/ClosedTermCache.lean rename to src/Init/Lean/Compiler/ClosedTermCache.lean diff --git a/library/Init/Lean/Compiler/ConstFolding.lean b/src/Init/Lean/Compiler/ConstFolding.lean similarity index 100% rename from library/Init/Lean/Compiler/ConstFolding.lean rename to src/Init/Lean/Compiler/ConstFolding.lean diff --git a/library/Init/Lean/Compiler/ExportAttr.lean b/src/Init/Lean/Compiler/ExportAttr.lean similarity index 100% rename from library/Init/Lean/Compiler/ExportAttr.lean rename to src/Init/Lean/Compiler/ExportAttr.lean diff --git a/library/Init/Lean/Compiler/ExternAttr.lean b/src/Init/Lean/Compiler/ExternAttr.lean similarity index 100% rename from library/Init/Lean/Compiler/ExternAttr.lean rename to src/Init/Lean/Compiler/ExternAttr.lean diff --git a/library/Init/Lean/Compiler/IR.lean b/src/Init/Lean/Compiler/IR.lean similarity index 100% rename from library/Init/Lean/Compiler/IR.lean rename to src/Init/Lean/Compiler/IR.lean diff --git a/library/Init/Lean/Compiler/IR/Basic.lean b/src/Init/Lean/Compiler/IR/Basic.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/Basic.lean rename to src/Init/Lean/Compiler/IR/Basic.lean diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/src/Init/Lean/Compiler/IR/Borrow.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/Borrow.lean rename to src/Init/Lean/Compiler/IR/Borrow.lean diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/src/Init/Lean/Compiler/IR/Boxing.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/Boxing.lean rename to src/Init/Lean/Compiler/IR/Boxing.lean diff --git a/library/Init/Lean/Compiler/IR/Checker.lean b/src/Init/Lean/Compiler/IR/Checker.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/Checker.lean rename to src/Init/Lean/Compiler/IR/Checker.lean diff --git a/library/Init/Lean/Compiler/IR/CompilerM.lean b/src/Init/Lean/Compiler/IR/CompilerM.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/CompilerM.lean rename to src/Init/Lean/Compiler/IR/CompilerM.lean diff --git a/library/Init/Lean/Compiler/IR/CtorLayout.lean b/src/Init/Lean/Compiler/IR/CtorLayout.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/CtorLayout.lean rename to src/Init/Lean/Compiler/IR/CtorLayout.lean diff --git a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Init/Lean/Compiler/IR/ElimDeadBranches.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/ElimDeadBranches.lean rename to src/Init/Lean/Compiler/IR/ElimDeadBranches.lean diff --git a/library/Init/Lean/Compiler/IR/ElimDeadVars.lean b/src/Init/Lean/Compiler/IR/ElimDeadVars.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/ElimDeadVars.lean rename to src/Init/Lean/Compiler/IR/ElimDeadVars.lean diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/src/Init/Lean/Compiler/IR/EmitC.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/EmitC.lean rename to src/Init/Lean/Compiler/IR/EmitC.lean diff --git a/library/Init/Lean/Compiler/IR/EmitUtil.lean b/src/Init/Lean/Compiler/IR/EmitUtil.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/EmitUtil.lean rename to src/Init/Lean/Compiler/IR/EmitUtil.lean diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Init/Lean/Compiler/IR/ExpandResetReuse.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/ExpandResetReuse.lean rename to src/Init/Lean/Compiler/IR/ExpandResetReuse.lean diff --git a/library/Init/Lean/Compiler/IR/Format.lean b/src/Init/Lean/Compiler/IR/Format.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/Format.lean rename to src/Init/Lean/Compiler/IR/Format.lean diff --git a/library/Init/Lean/Compiler/IR/FreeVars.lean b/src/Init/Lean/Compiler/IR/FreeVars.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/FreeVars.lean rename to src/Init/Lean/Compiler/IR/FreeVars.lean diff --git a/library/Init/Lean/Compiler/IR/LiveVars.lean b/src/Init/Lean/Compiler/IR/LiveVars.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/LiveVars.lean rename to src/Init/Lean/Compiler/IR/LiveVars.lean diff --git a/library/Init/Lean/Compiler/IR/NormIds.lean b/src/Init/Lean/Compiler/IR/NormIds.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/NormIds.lean rename to src/Init/Lean/Compiler/IR/NormIds.lean diff --git a/library/Init/Lean/Compiler/IR/PushProj.lean b/src/Init/Lean/Compiler/IR/PushProj.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/PushProj.lean rename to src/Init/Lean/Compiler/IR/PushProj.lean diff --git a/library/Init/Lean/Compiler/IR/RC.lean b/src/Init/Lean/Compiler/IR/RC.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/RC.lean rename to src/Init/Lean/Compiler/IR/RC.lean diff --git a/library/Init/Lean/Compiler/IR/ResetReuse.lean b/src/Init/Lean/Compiler/IR/ResetReuse.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/ResetReuse.lean rename to src/Init/Lean/Compiler/IR/ResetReuse.lean diff --git a/library/Init/Lean/Compiler/IR/SimpCase.lean b/src/Init/Lean/Compiler/IR/SimpCase.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/SimpCase.lean rename to src/Init/Lean/Compiler/IR/SimpCase.lean diff --git a/library/Init/Lean/Compiler/IR/UnboxResult.lean b/src/Init/Lean/Compiler/IR/UnboxResult.lean similarity index 100% rename from library/Init/Lean/Compiler/IR/UnboxResult.lean rename to src/Init/Lean/Compiler/IR/UnboxResult.lean diff --git a/library/Init/Lean/Compiler/ImplementedByAttr.lean b/src/Init/Lean/Compiler/ImplementedByAttr.lean similarity index 100% rename from library/Init/Lean/Compiler/ImplementedByAttr.lean rename to src/Init/Lean/Compiler/ImplementedByAttr.lean diff --git a/library/Init/Lean/Compiler/InitAttr.lean b/src/Init/Lean/Compiler/InitAttr.lean similarity index 100% rename from library/Init/Lean/Compiler/InitAttr.lean rename to src/Init/Lean/Compiler/InitAttr.lean diff --git a/library/Init/Lean/Compiler/InlineAttrs.lean b/src/Init/Lean/Compiler/InlineAttrs.lean similarity index 100% rename from library/Init/Lean/Compiler/InlineAttrs.lean rename to src/Init/Lean/Compiler/InlineAttrs.lean diff --git a/library/Init/Lean/Compiler/NameMangling.lean b/src/Init/Lean/Compiler/NameMangling.lean similarity index 100% rename from library/Init/Lean/Compiler/NameMangling.lean rename to src/Init/Lean/Compiler/NameMangling.lean diff --git a/library/Init/Lean/Compiler/NeverExtractAttr.lean b/src/Init/Lean/Compiler/NeverExtractAttr.lean similarity index 100% rename from library/Init/Lean/Compiler/NeverExtractAttr.lean rename to src/Init/Lean/Compiler/NeverExtractAttr.lean diff --git a/library/Init/Lean/Compiler/Specialize.lean b/src/Init/Lean/Compiler/Specialize.lean similarity index 100% rename from library/Init/Lean/Compiler/Specialize.lean rename to src/Init/Lean/Compiler/Specialize.lean diff --git a/library/Init/Lean/Compiler/Util.lean b/src/Init/Lean/Compiler/Util.lean similarity index 100% rename from library/Init/Lean/Compiler/Util.lean rename to src/Init/Lean/Compiler/Util.lean diff --git a/library/Init/Lean/Declaration.lean b/src/Init/Lean/Declaration.lean similarity index 100% rename from library/Init/Lean/Declaration.lean rename to src/Init/Lean/Declaration.lean diff --git a/library/Init/Lean/Elaborator.lean b/src/Init/Lean/Elaborator.lean similarity index 100% rename from library/Init/Lean/Elaborator.lean rename to src/Init/Lean/Elaborator.lean diff --git a/library/Init/Lean/Elaborator/Alias.lean b/src/Init/Lean/Elaborator/Alias.lean similarity index 100% rename from library/Init/Lean/Elaborator/Alias.lean rename to src/Init/Lean/Elaborator/Alias.lean diff --git a/library/Init/Lean/Elaborator/Basic.lean b/src/Init/Lean/Elaborator/Basic.lean similarity index 100% rename from library/Init/Lean/Elaborator/Basic.lean rename to src/Init/Lean/Elaborator/Basic.lean diff --git a/library/Init/Lean/Elaborator/Command.lean b/src/Init/Lean/Elaborator/Command.lean similarity index 100% rename from library/Init/Lean/Elaborator/Command.lean rename to src/Init/Lean/Elaborator/Command.lean diff --git a/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean b/src/Init/Lean/Elaborator/ElabStrategyAttrs.lean similarity index 100% rename from library/Init/Lean/Elaborator/ElabStrategyAttrs.lean rename to src/Init/Lean/Elaborator/ElabStrategyAttrs.lean diff --git a/library/Init/Lean/Elaborator/PreTerm.lean b/src/Init/Lean/Elaborator/PreTerm.lean similarity index 100% rename from library/Init/Lean/Elaborator/PreTerm.lean rename to src/Init/Lean/Elaborator/PreTerm.lean diff --git a/library/Init/Lean/Elaborator/ResolveName.lean b/src/Init/Lean/Elaborator/ResolveName.lean similarity index 100% rename from library/Init/Lean/Elaborator/ResolveName.lean rename to src/Init/Lean/Elaborator/ResolveName.lean diff --git a/library/Init/Lean/Elaborator/Term.lean b/src/Init/Lean/Elaborator/Term.lean similarity index 100% rename from library/Init/Lean/Elaborator/Term.lean rename to src/Init/Lean/Elaborator/Term.lean diff --git a/library/Init/Lean/Environment.lean b/src/Init/Lean/Environment.lean similarity index 100% rename from library/Init/Lean/Environment.lean rename to src/Init/Lean/Environment.lean diff --git a/library/Init/Lean/EqnCompiler.lean b/src/Init/Lean/EqnCompiler.lean similarity index 100% rename from library/Init/Lean/EqnCompiler.lean rename to src/Init/Lean/EqnCompiler.lean diff --git a/library/Init/Lean/EqnCompiler/MatchPattern.lean b/src/Init/Lean/EqnCompiler/MatchPattern.lean similarity index 100% rename from library/Init/Lean/EqnCompiler/MatchPattern.lean rename to src/Init/Lean/EqnCompiler/MatchPattern.lean diff --git a/library/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean similarity index 100% rename from library/Init/Lean/Expr.lean rename to src/Init/Lean/Expr.lean diff --git a/library/Init/Lean/Format.lean b/src/Init/Lean/Format.lean similarity index 100% rename from library/Init/Lean/Format.lean rename to src/Init/Lean/Format.lean diff --git a/library/Init/Lean/KVMap.lean b/src/Init/Lean/KVMap.lean similarity index 100% rename from library/Init/Lean/KVMap.lean rename to src/Init/Lean/KVMap.lean diff --git a/library/Init/Lean/LBool.lean b/src/Init/Lean/LBool.lean similarity index 100% rename from library/Init/Lean/LBool.lean rename to src/Init/Lean/LBool.lean diff --git a/library/Init/Lean/LOption.lean b/src/Init/Lean/LOption.lean similarity index 100% rename from library/Init/Lean/LOption.lean rename to src/Init/Lean/LOption.lean diff --git a/library/Init/Lean/Level.lean b/src/Init/Lean/Level.lean similarity index 100% rename from library/Init/Lean/Level.lean rename to src/Init/Lean/Level.lean diff --git a/library/Init/Lean/Linter.lean b/src/Init/Lean/Linter.lean similarity index 100% rename from library/Init/Lean/Linter.lean rename to src/Init/Lean/Linter.lean diff --git a/library/Init/Lean/LocalContext.lean b/src/Init/Lean/LocalContext.lean similarity index 100% rename from library/Init/Lean/LocalContext.lean rename to src/Init/Lean/LocalContext.lean diff --git a/library/Init/Lean/Message.lean b/src/Init/Lean/Message.lean similarity index 100% rename from library/Init/Lean/Message.lean rename to src/Init/Lean/Message.lean diff --git a/library/Init/Lean/Meta.lean b/src/Init/Lean/Meta.lean similarity index 100% rename from library/Init/Lean/Meta.lean rename to src/Init/Lean/Meta.lean diff --git a/library/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean similarity index 100% rename from library/Init/Lean/Meta/Basic.lean rename to src/Init/Lean/Meta/Basic.lean diff --git a/library/Init/Lean/Meta/Check.lean b/src/Init/Lean/Meta/Check.lean similarity index 100% rename from library/Init/Lean/Meta/Check.lean rename to src/Init/Lean/Meta/Check.lean diff --git a/library/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean similarity index 100% rename from library/Init/Lean/Meta/Exception.lean rename to src/Init/Lean/Meta/Exception.lean diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean similarity index 100% rename from library/Init/Lean/Meta/ExprDefEq.lean rename to src/Init/Lean/Meta/ExprDefEq.lean diff --git a/library/Init/Lean/Meta/FunInfo.lean b/src/Init/Lean/Meta/FunInfo.lean similarity index 100% rename from library/Init/Lean/Meta/FunInfo.lean rename to src/Init/Lean/Meta/FunInfo.lean diff --git a/library/Init/Lean/Meta/InferType.lean b/src/Init/Lean/Meta/InferType.lean similarity index 100% rename from library/Init/Lean/Meta/InferType.lean rename to src/Init/Lean/Meta/InferType.lean diff --git a/library/Init/Lean/Meta/LevelDefEq.lean b/src/Init/Lean/Meta/LevelDefEq.lean similarity index 100% rename from library/Init/Lean/Meta/LevelDefEq.lean rename to src/Init/Lean/Meta/LevelDefEq.lean diff --git a/library/Init/Lean/Meta/Offset.lean b/src/Init/Lean/Meta/Offset.lean similarity index 100% rename from library/Init/Lean/Meta/Offset.lean rename to src/Init/Lean/Meta/Offset.lean diff --git a/library/Init/Lean/Meta/WHNF.lean b/src/Init/Lean/Meta/WHNF.lean similarity index 100% rename from library/Init/Lean/Meta/WHNF.lean rename to src/Init/Lean/Meta/WHNF.lean diff --git a/library/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean similarity index 100% rename from library/Init/Lean/MetavarContext.lean rename to src/Init/Lean/MetavarContext.lean diff --git a/library/Init/Lean/Modifiers.lean b/src/Init/Lean/Modifiers.lean similarity index 100% rename from library/Init/Lean/Modifiers.lean rename to src/Init/Lean/Modifiers.lean diff --git a/library/Init/Lean/MonadCache.lean b/src/Init/Lean/MonadCache.lean similarity index 100% rename from library/Init/Lean/MonadCache.lean rename to src/Init/Lean/MonadCache.lean diff --git a/library/Init/Lean/Name.lean b/src/Init/Lean/Name.lean similarity index 100% rename from library/Init/Lean/Name.lean rename to src/Init/Lean/Name.lean diff --git a/library/Init/Lean/NameGenerator.lean b/src/Init/Lean/NameGenerator.lean similarity index 100% rename from library/Init/Lean/NameGenerator.lean rename to src/Init/Lean/NameGenerator.lean diff --git a/library/Init/Lean/Options.lean b/src/Init/Lean/Options.lean similarity index 100% rename from library/Init/Lean/Options.lean rename to src/Init/Lean/Options.lean diff --git a/library/Init/Lean/Parser.lean b/src/Init/Lean/Parser.lean similarity index 100% rename from library/Init/Lean/Parser.lean rename to src/Init/Lean/Parser.lean diff --git a/library/Init/Lean/Parser/Command.lean b/src/Init/Lean/Parser/Command.lean similarity index 100% rename from library/Init/Lean/Parser/Command.lean rename to src/Init/Lean/Parser/Command.lean diff --git a/library/Init/Lean/Parser/Identifier.lean b/src/Init/Lean/Parser/Identifier.lean similarity index 100% rename from library/Init/Lean/Parser/Identifier.lean rename to src/Init/Lean/Parser/Identifier.lean diff --git a/library/Init/Lean/Parser/Level.lean b/src/Init/Lean/Parser/Level.lean similarity index 100% rename from library/Init/Lean/Parser/Level.lean rename to src/Init/Lean/Parser/Level.lean diff --git a/library/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean similarity index 100% rename from library/Init/Lean/Parser/Module.lean rename to src/Init/Lean/Parser/Module.lean diff --git a/library/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean similarity index 100% rename from library/Init/Lean/Parser/Parser.lean rename to src/Init/Lean/Parser/Parser.lean diff --git a/library/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean similarity index 100% rename from library/Init/Lean/Parser/Term.lean rename to src/Init/Lean/Parser/Term.lean diff --git a/library/Init/Lean/Parser/Transform.lean b/src/Init/Lean/Parser/Transform.lean similarity index 100% rename from library/Init/Lean/Parser/Transform.lean rename to src/Init/Lean/Parser/Transform.lean diff --git a/library/Init/Lean/Parser/Trie.lean b/src/Init/Lean/Parser/Trie.lean similarity index 100% rename from library/Init/Lean/Parser/Trie.lean rename to src/Init/Lean/Parser/Trie.lean diff --git a/library/Init/Lean/Path.lean b/src/Init/Lean/Path.lean similarity index 100% rename from library/Init/Lean/Path.lean rename to src/Init/Lean/Path.lean diff --git a/library/Init/Lean/Position.lean b/src/Init/Lean/Position.lean similarity index 100% rename from library/Init/Lean/Position.lean rename to src/Init/Lean/Position.lean diff --git a/library/Init/Lean/ProjFns.lean b/src/Init/Lean/ProjFns.lean similarity index 100% rename from library/Init/Lean/ProjFns.lean rename to src/Init/Lean/ProjFns.lean diff --git a/library/Init/Lean/ReducibilityAttrs.lean b/src/Init/Lean/ReducibilityAttrs.lean similarity index 100% rename from library/Init/Lean/ReducibilityAttrs.lean rename to src/Init/Lean/ReducibilityAttrs.lean diff --git a/library/Init/Lean/Runtime.lean b/src/Init/Lean/Runtime.lean similarity index 100% rename from library/Init/Lean/Runtime.lean rename to src/Init/Lean/Runtime.lean diff --git a/library/Init/Lean/SMap.lean b/src/Init/Lean/SMap.lean similarity index 100% rename from library/Init/Lean/SMap.lean rename to src/Init/Lean/SMap.lean diff --git a/library/Init/Lean/Scopes.lean b/src/Init/Lean/Scopes.lean similarity index 100% rename from library/Init/Lean/Scopes.lean rename to src/Init/Lean/Scopes.lean diff --git a/library/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean similarity index 100% rename from library/Init/Lean/Syntax.lean rename to src/Init/Lean/Syntax.lean diff --git a/library/Init/Lean/ToExpr.lean b/src/Init/Lean/ToExpr.lean similarity index 100% rename from library/Init/Lean/ToExpr.lean rename to src/Init/Lean/ToExpr.lean diff --git a/library/Init/Lean/Trace.lean b/src/Init/Lean/Trace.lean similarity index 100% rename from library/Init/Lean/Trace.lean rename to src/Init/Lean/Trace.lean diff --git a/library/Init/Lean/TypeClass.lean b/src/Init/Lean/TypeClass.lean similarity index 100% rename from library/Init/Lean/TypeClass.lean rename to src/Init/Lean/TypeClass.lean diff --git a/library/Init/Lean/TypeClass/Basic.lean b/src/Init/Lean/TypeClass/Basic.lean similarity index 100% rename from library/Init/Lean/TypeClass/Basic.lean rename to src/Init/Lean/TypeClass/Basic.lean diff --git a/library/Init/Lean/TypeClass/Context.lean b/src/Init/Lean/TypeClass/Context.lean similarity index 100% rename from library/Init/Lean/TypeClass/Context.lean rename to src/Init/Lean/TypeClass/Context.lean diff --git a/library/Init/Lean/TypeClass/Synth.lean b/src/Init/Lean/TypeClass/Synth.lean similarity index 100% rename from library/Init/Lean/TypeClass/Synth.lean rename to src/Init/Lean/TypeClass/Synth.lean diff --git a/library/Init/Lean/Util.lean b/src/Init/Lean/Util.lean similarity index 100% rename from library/Init/Lean/Util.lean rename to src/Init/Lean/Util.lean diff --git a/library/Init/Lean/WHNF.lean b/src/Init/Lean/WHNF.lean similarity index 100% rename from library/Init/Lean/WHNF.lean rename to src/Init/Lean/WHNF.lean diff --git a/library/Init/System.lean b/src/Init/System.lean similarity index 100% rename from library/Init/System.lean rename to src/Init/System.lean diff --git a/library/Init/System/FilePath.lean b/src/Init/System/FilePath.lean similarity index 100% rename from library/Init/System/FilePath.lean rename to src/Init/System/FilePath.lean diff --git a/library/Init/System/IO.lean b/src/Init/System/IO.lean similarity index 100% rename from library/Init/System/IO.lean rename to src/Init/System/IO.lean diff --git a/library/Init/System/Platform.lean b/src/Init/System/Platform.lean similarity index 100% rename from library/Init/System/Platform.lean rename to src/Init/System/Platform.lean diff --git a/library/Init/Util.lean b/src/Init/Util.lean similarity index 100% rename from library/Init/Util.lean rename to src/Init/Util.lean diff --git a/library/Init/WF.lean b/src/Init/WF.lean similarity index 100% rename from library/Init/WF.lean rename to src/Init/WF.lean diff --git a/library/Makefile.in b/src/Makefile.in similarity index 87% rename from library/Makefile.in rename to src/Makefile.in index 817eee0fcb..d85c67ff47 100644 --- a/library/Makefile.in +++ b/src/Makefile.in @@ -2,12 +2,13 @@ # Released under Apache 2.0 license as described in the file LICENSE. # Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura LEAN = ../bin/lean +LEANC = ../bin/leanc SRCS = $(shell find . -name '*.lean') OBJS = $(SRCS:.lean=.olean) DEPS = $(SRCS:.lean=.depend) OPTS = @LEAN_EXTRA_MAKE_OPTS@ STAGE0_DIR = ../stage0 -STAGE1_DIR = ../src/stage1 +STAGE1_DIR = stage1 ifndef STAGE1_OUT $(error "`STAGE1_OUT` must be set (use cmake)") endif @@ -42,19 +43,19 @@ $(STAGE1_DIR)/%.c: %.olean $(STAGE1_OUT)/%.o: $(STAGE1_DIR)/%.c @echo "[ ] Building $<" @mkdir -p "$(@D)" - ../bin/leanc -c -o $@ $< $(LEANC_OPTS) + $(LEANC) -c -o $@ $< $(LEANC_OPTS) $(STAGE1_OUT)/libleanstdlib.a: $(addprefix $(STAGE1_OUT)/,$(patsubst %.lean,%.o,$(SRCS))) @rm -f $@ @ar rcs $@ $^ update-stage0: - -rm -r $(STAGE0_DIR)/src $(STAGE0_DIR)/library + -rm -r $(STAGE0_DIR)/src -mkdir $(STAGE0_DIR) # don't copy untracked crap git ls-files -z ../src | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}' - cp -R $(STAGE1_DIR) $(STAGE0_DIR)/library - echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/library/CMakeLists.txt + cp -R $(STAGE1_DIR) $(STAGE0_DIR) + echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/CMakeLists.txt -git add $(STAGE0_DIR) .PRECIOUS: %.depend $(STAGE1_DIR)/%.c diff --git a/library/relative.py b/src/relative.py similarity index 100% rename from library/relative.py rename to src/relative.py diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index de3f017814..5ec0ef8b84 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -13,7 +13,7 @@ if(NOT STAGE0) add_custom_target(make_stdlib # '-G Ninja' complains otherwise BYPRODUCTS "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}" COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$" "LEANC_OPTS=${LEANC_OPTS}" "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1" DEPENDS stage0) set_target_properties(leanstdlib PROPERTIES @@ -25,7 +25,7 @@ if(NOT STAGE0) add_custom_target(update-stage0 COMMAND make update-stage0 "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1" DEPENDS leanstdlib - WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library") + WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}") endif() add_executable(lean lean.cpp) @@ -43,7 +43,7 @@ if(NOT STAGE0) set(NODE_JS "node --stack_size=8192") file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path - "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/../../library ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n") + "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n") execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path) ADD_CUSTOM_TARGET(bin_lean ALL @@ -97,34 +97,9 @@ add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v) endif() add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g) add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash) -add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/../library/Init/Core.lean") +add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean") add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") -# The following test needs new elaborator to support match -# add_test(NAME "lean_eqn_macro" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./test_eqn_macro.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -# add_test(NAME "lean_print_notation" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_tests.lean") -# add_test(NAME "issue_597" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./issue_597.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -# add_test(NAME "issue_616" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./issue_616.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -# add_test(NAME "show_goal" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./show_goal.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -# add_test(NAME "issue_755" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./issue_755.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -# add_test(NAME "print_info" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -# add_test(NAME "dir_option" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" -# COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" "--dir=${LEAN_SOURCE_DIR}/../library/data/nat" "dir_option.lean") if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) # The following test cannot be executed on Windows because of the # bash script timeout.sh @@ -245,10 +220,10 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") # Skip stdlib tests on Windows message(STATUS "skipping stdlib tests") else() - file(GLOB_RECURSE STDLIBFILES RELATIVE "${LEAN_SOURCE_DIR}/../library" "${LEAN_SOURCE_DIR}/../library/*.lean") + file(GLOB_RECURSE STDLIBFILES RELATIVE "${LEAN_SOURCE_DIR}/Init" "${LEAN_SOURCE_DIR}/Init/*.lean") FOREACH(T ${STDLIBFILES}) add_test(NAME "stdlib_${T}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init" COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" "${T}") ENDFOREACH(T) endif()