max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

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

Browse source
This commit is contained in:
Gabriel Ebner 2016-12-02 17:04:46 -05:00 • committed by Leonardo de Moura
parent 9ecac28061
commit 92f07720f2
4 changed files with 8 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
doc/make/msys2.md
View file

@ -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

15
script/fetch_emacs_deps.sh
View file

@ -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

14
src/CMakeLists.txt
View file

@ -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.

16
src/emacs/load-lean.el
View file

@ -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 ()