diff --git a/doc/make/msys2.md b/doc/make/msys2.md index 3aae794510..72f567d0ec 100644 --- 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 deleted file mode 100755 index 39bb866190..0000000000 --- a/script/fetch_emacs_deps.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/bash -# Script for copying the Lean Emacs mode dependencies from https://github.com/leanprover/emacs-dependencies.git. -# We usually use it to test `leanemacs` without installing Lean. -# We execute this script at src/emacs. -read -p "Script will delete directory 'dependencies' and create it again with the content of https://github.com/leanprover/emacs-dependencies.git, Are you sure [y/n]? " -n 1 -r -echo # (optional) move to a new line -if [[ ! $REPLY =~ ^[Yy]$ ]] -then - echo "ABORTED." - exit 1 -fi -rm -r -f dependencies -git clone https://github.com/leanprover/emacs-dependencies.git -rm -r -f emacs-dependencies/.git -mv emacs-dependencies dependencies diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ed6bf766f1..56547e0048 100644 --- 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 index b4c94ab3db..6e73d9d354 100644 --- 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)) - (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 ()