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