I installed from OpenSUSE: emacs install

Using Emacs

C-<chr> means hold the CONTROL key while typing the character <chr>
Thus, C-f would be: hold the CONTROL key and type f.
M-<chr> means hold the META or EDIT or ALT key


Click on desktop Icon


Installing Melpa

Repository of Emacs packages. Packages such as idris-mode or Coq are loaded into Emacs using melpa:


Enable installation of packages from MELPA by adding an entry to package-archives after (require 'package) and before the call to package-initialize in your init.el or .emacs file:

;;; File name: ` ~/.emacs '
;;; ---------------------
;;; If you need your own personal ~/.emacs
;;; please make a copy of this file
;;; an placein your changes and/or extension.
;;; Copyright (c) 1997-2002 SuSE Gmbh Nuernberg, Germany.
;;; Author: Werner Fink,  1997,98,99,2002
;;; Test of Emacs derivates
;;; -----------------------
(if (string-match "XEmacs\\|Lucid" emacs-version)
  ;;; XEmacs
  ;;; ------
     (if (file-readable-p "~/.xemacs/init.el")
        (load "~/.xemacs/init.el" nil t))
  ;;; GNU-Emacs
  ;;; ---------
  ;;; load ~/.gnu-emacs or, if not exists /etc/skel/.gnu-emacs
  ;;; For a description and the settings see /etc/skel/.gnu-emacs
  ;;;   ... for your private ~/.gnu-emacs your are on your one.
  (if (file-readable-p "~/.gnu-emacs")
      (load "~/.gnu-emacs" nil t)
    (if (file-readable-p "/etc/skel/.gnu-emacs")
	(load "/etc/skel/.gnu-emacs" nil t)))

  ;; Custom Settings
  ;; ===============
  ;; To avoid any trouble with the customization system of GNU emacs
  ;; we set the default file ~/.gnu-emacs-custom
  (setq custom-file "~/.gnu-emacs-custom")
  (load "~/.gnu-emacs-custom" t t)
;; load emacs 24's package system. Add MELPA repository.
(when (>= emacs-major-version 24)
  (require 'package)
   ;; '("melpa" . "http://stable.melpa.org/packages/") ; many packages won't show if using stable
   '("melpa" . "http://melpa.milkbox.net/packages/")
 To use the stable package repository instead of the default "bleeding-edge" repository, use this instead
 of "melpa":

(add-to-list 'package-archives
             '("melpa-stable" . "https://stable.melpa.org/packages/") t)

Install package

Options -> Manage Emacs Packages

Select the package to install (in this case idris-mode)

load a package

click on install

It says : idris-mode is an available obsolete package.

Update all MELPA packages

M-x package-list-packages


Using Idris

(page about Idris here) Scroll down to installation notes on site here:


Somehow Emacs needs to know about Idris. emacs path
I setup the startup Icon to my application directory. emacpath

Using Coq

For more information about coq see this page .

Proof-general runs on emacs



M-x package-refresh-contents

M-x package-install RET

This will these recogise:


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.