Guía de instalación de sistemas para el curso 2016-17

Índice

1 Instalación de Haskell

  • Instalaciones con apt-get
sudo apt-get install haskell-platform haskell-stack hlint doctest gnuplot 
  • Instalaciones con cabal
sudo cabal update
sudo cabal install primes matrix gnuplot easyplot gloss-examples codeworld-api
  • Librería de I1M
cd /tmp
wget https://github.com/jaalonso/I1M/archive/master.zip .
unzip I1M-master.zip
cd I1M-master
cabal install I1M.cabal

2 Instalación de maxima

  • Instalaciones con apt-get
sudo apt-get install maxima maxima-emacs wxmaxima

3 Configuración de emacs

  • En ~/.emacs escribir
;;; Uso de paquetes
(require 'package)

(setq package-archives
      '(("gnu"          . "http://elpa.gnu.org/packages/")
        ("marmalade"    . "http://marmalade-repo.org/packages/")
        ("melpa-stable" . "https://stable.melpa.org/packages/")
        ))

(package-initialize)
  • Con 'M-x list-packages' instalar los siguientes paquetes de emacs

    Paquete Versión Descripción
    haskell-mode 13.20.1 A Haskell editing mode
    ghc 5.6.0.0 Sub mode for Haskell mode
  • Escribir en ~/.emacs
;;; Emacs
;;; =====

;;; Permite buscar en la historia
(setq comint-history-isearch t)

;;; Suprime el mensaje inicial:
(setq inhibit-startup-message t)

;;; No hace sangrado con tabuladores:
(setq-default indent-tabs-mode nil)

;;; Permite la evaluación de expresiones en el mini-buffer:
(put 'eval-expression 'disabled nil)    ; M-:

;;; Escribe 79 caracteres por línea:
(setq-default fill-column 79)

;;; No hace copias de seguridad:
(setq backup-inhibited t)

;;; Envía los fichero borrados a la papelera:
(setq delete-by-moving-to-trash t)

;;; Añade una nueva línea al final del fichero
(setq require-final-newline t)

;;; Muestra en la línea del modo la fila y columna del cursor.
(column-number-mode 1)   ; en prueba

;;; Completaciones
(dynamic-completion-mode)

;;; Por defecto, en dired no escribe el grupo:
(setq dired-listing-switches "-alGv")

;;; Para poner acentos
(require 'iso-transl)

;;; Para mostrar paréntesis
(show-paren-mode)

;;; Elimina los ecos en la shell
(setq comint-process-echoes t)

;;; Portapapeles
;;; ------------
(menu-bar-enable-clipboard)
(setq x-select-enable-clipboard t)

;;; Pone una región en minúscula
(put 'downcase-region 'disabled nil)

;;; Haskell
;;; =======

(eval-after-load "haskell-mode"
  '(progn
    (define-key haskell-mode-map (kbd "C-x C-d") nil)
    (define-key haskell-mode-map (kbd "C-c C-z") 'haskell-interactive-switch)
    (define-key haskell-mode-map (kbd "C-c C-l") 'haskell-process-load-file)
    (define-key haskell-mode-map (kbd "C-c C-b") 'haskell-interactive-switch)
    (define-key haskell-mode-map (kbd "C-c C-t") 'haskell-process-do-type)
    (define-key haskell-mode-map (kbd "C-c C-i") 'haskell-process-do-info)
    (define-key haskell-mode-map (kbd "C-c M-.") nil)
    (define-key haskell-mode-map (kbd "C-c C-d") nil)))


(add-hook 'haskell-mode-hook 
          '(lambda ()
             (turn-on-auto-fill)
             (setq fill-column 79
                   haskell-process-show-debug-tips nil
                   haskell-ask-also-kill-buffer nil
                   haskell-process-suggest-language-pragmas nil
                   haskell-process-suggest-no-warn-orphans nil
                   haskell-process-suggest-overloaded-strings nil
                   )
             ))        

;;; Maxima
;;; ======

(autoload 'maxima-mode "maxima" "Maxima mode" t)

(autoload 'imaxima "imaxima" "Frontend for maxima with Image support" t)

(autoload 'maxima "maxima" "Maxima interaction" t)

(autoload 'imath-mode "imath" "Imath mode for math formula input" t)

(setq imaxima-use-maxima-mode-flag t)

(add-to-list 'auto-mode-alist '("\\.ma[cx]" . maxima-mode))

(add-hook 'maxima-mode-hook 
          '(lambda ()
             (turn-on-auto-fill)
             (setq fill-column 79)
             ))

;;; Variables de configuración
;;; ==========================

(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 )

(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(default ((t (:family "Ubuntu Mono"
                :foundry "DAMA"
                :slant normal
                :weight normal
                :height 181
                :width normal)))))
  • Escribir en ~/.emacs.d/elpa/haskell-mode-13.20.1/haskell-commands.el (y compilarlo)
(defun haskell-process-cd (&optional _not-interactive)
  ;; FIXME optional arg is not used
  "Change directory."
  (interactive)
  (let* ((session (haskell-interactive-session))
         (dir (haskell-session-prompt-set-current-dir session)))
    (haskell-process-log
     (propertize (format "\nTrabajando en el directorio %s ...\n\n" dir)
                 'face font-lock-comment-face))
    (haskell-process-change-dir session
                                (haskell-interactive-process)
                                dir)))

(defun haskell-process-change-dir (session process dir)
  "Change SESSION's current directory.
Query PROCESS to `:cd` to directory DIR."
  (haskell-process-queue-command
   process
   (make-haskell-command
    :state (list session process dir)
    :go
    (lambda (state)
      (haskell-process-send-string
       (cadr state) (format ":cd %s" (cl-caddr state))))

    :complete
    (lambda (state _)
      (haskell-session-set-current-dir (car state) (cl-caddr state))
      (haskell-interactive-mode-echo (car state)
                                     (format "\nDirectorio: %s\n"
                                             (cl-caddr state)))))))
  • Escribir en ~/.emacs.d/elpa/haskell-mode-13.20.1/haskell-process.el (y compilarlo)
(defconst haskell-process-greetings
  (list "Todo lo que se ignora, se desprecia. ~ Antonio Machado"
        "Todo necio confunde valor y precio. ~ Antonio Machado"
        "Caminante no hay camino, se hace camino al andar. ~ Antonio Machado"
        "Despacito y buena letra, que el hacer las cosas bien, importa más que el hacerlas"
        "Todo lo que se ignora, se desprecia. ~ Antonio Machado"
        "Con cada paso que das alcanzas tu meta. ~ Dicho Zen"
        "La esencia de la matemática es su libertad. ~ G. Cantor"
        "Programación, en sentido amplio, es resolución de problemas. ~ Paul Hudak"
        "Un programa de ordenador es una demostración. ~ Igor Rivin"
        "Matemática es una ciencia experimenta y la computación es el experimento ~ Rivin"
        "El control de la complejidad es la esencia de la programación. ~ B.W. Kernigan"
        "La iteración es humana, la recursión es divina. ~ L. Peter Deutsch"
        "Los ordenadores son inútiles. Sólo pueden darte respuestas. ~ Pablo Picasso"
        "Lo que tenemos que aprender a hacer, lo aprendemos haciéndolo. ~ Aristóteles" 
        )
  "Greetings for when the Haskell process starts up.")

4 Instalación de Prover9

  • Instalaciones con apt-get
sudo apt-get prover9 

5 Instalación de Isabelle

  • Descargar
cd /usr/local/lib
sudo su
wget https://isabelle.in.tum.de/dist/Isabelle2016_app.tar.gz
  • Descomprimir
tar xfz Isabelle2016_app.tar.gz
rm Isabelle2016_app.tar.gz
  • Instalar ejecutables
cd ../bin
ln -s ../lib/Isabelle2016/bin/isa* .
exit
  • Iniciar y compilar teorías
cd
isabelle jedit

6 Instalación de Java (necesaria para Pandora)

  • Instalar Java 8
sudo add-apt-repository ppa:webupd8team/java
sudo apt-get update
sudo apt-get install oracle-java8-installer

7 Instalación de Pandora

  • Descargar Pandora
cd /usr/local/lib
sudo su
mkdir pandora
cd pandora
wget http://www.doc.ic.ac.uk/pandora/newpandora/pandora.jar
  • Escribir el ejecutable en /usr/local/bin/pandora
exec java -jar /usr/local/lib/pandora/pandora.jar
  • Cambiar el modo del ejecutable
sudo su
cd /usr/local/bin
chmod a+x pandora