refactor(emacs/load-lean): install emacs dependencies directly from (…

…M)ELPA
GaloisInc · Dec 3, 2016 · 92f0772 · 92f0772
1 parent 9ecac28
commit 92f0772
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 40 deletions.
diff --git a/doc/make/msys2.md b/doc/make/msys2.md
@@ -46,9 +46,6 @@ In the [msys2] shell, execute the following commands.
 ```bash
 cd /c/
 git clone https://github.com/leanprover/lean
-git clone http://github.com/leanprover/emacs-dependencies
-mkdir -p lean/src/emacs/dependencies
-cp -R emacs-dependencies/* lean/src/emacs/dependencies
 cd lean
 mkdir build && cd build
 cmake -D CMAKE_CXX_COMPILER=g++.exe -G Ninja ../src

diff --git a/script/fetch_emacs_deps.sh b/script/fetch_emacs_deps.sh
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -53,10 +53,6 @@ option(USE_GITHASH        "GIT_HASH"          ON)
 # When ON thread storage is automatically finalized, it assumes platform support pthreads.
 # This option is important when using Lean as library that is invoked from a different programming language (e.g., Haskell).
 option(AUTO_THREAD_FINALIZATION "AUTO_THREAD_FINALIZATION" ON)
-# Directory that include lean emacs mode dependecies
-set(EMACS_DEPENDENCIES "${CMAKE_SOURCE_DIR}/emacs/dependencies")
-
-message(STATUS "Emacs dependecies directory " ${EMACS_DEPENDENCIES})
 
 # emacs site-lisp dir
 set(EMACS_LISP_DIR        "share/emacs/site-lisp/lean" CACHE STRING "emacs site-lisp dir")
@@ -476,16 +472,6 @@ install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION "${LEAN_EXT_INCLUDE_DIR}"
 install(FILES "${CMAKE_SOURCE_DIR}/../src/emacs/lean.pgm"
         DESTINATION "${EMACS_LISP_DIR}")
 
-if(EXISTS "${EMACS_DEPENDENCIES}")
-  install(DIRECTORY "${EMACS_DEPENDENCIES}/" DESTINATION "${EMACS_LISP_DIR}/dependencies"
-    FILES_MATCHING
-    PATTERN "*.el"
-    PATTERN "dir"
-    PATTERN "*.info*")
-else()
-  message(STATUS "Emacs dependencies directory does not exist. Therefore, they will not be included in the binary installation package. The Emacs packages required by Lean Emacs mode can be retrieved from the repository https://github.com/leanprover/emacs-dependencies. The cmake option EMACS_DEPENDENCIES can be used to specify where these files are located.")
-endif()
-
 if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
   # TODO(Leo): do not use hardlinks to required DLLs.
   # For example, we can try to use ldd to retrieve the list of required DLLs.

diff --git a/src/emacs/load-lean.el b/src/emacs/load-lean.el
@@ -8,21 +8,21 @@
     (setq-local lean-emacs-path (getenv "LEAN_EMACS_PATH"))
     (error "LEAN_EMACS_PATH environment variable must be set"))
 
-(setq lean-emacs-dependencies-path (format "%s/dependencies" lean-emacs-path))
-
 (setq lean-logo
       (condition-case nil
           (create-image (format "%s/lean.pgm" lean-emacs-path))
         (error nil)))
-(setq lean-required-packages '(company dash dash-functional f fill-column-indicator flycheck let-alist s seq))
 
-(setq load-path
-      (append
-       (list lean-emacs-path)
-       (mapcar (lambda (p) (format "%s/%s" lean-emacs-dependencies-path p)) lean-required-packages)
-       load-path))
+(setq lean-required-packages '(company dash dash-functional f fill-column-indicator flycheck let-alist s seq))
 
 (require 'package)
+(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
+(package-initialize)
+(unless package-archive-contents (package-refresh-contents))
+(dolist (pkg lean-required-packages) (package-install pkg))
+
+(setq load-path (cons lean-emacs-path load-path))
+
 (require 'lean-mode)
 
 (defun lean-welcome ()