[Munich-lisp] Haskell Hackathon 23.11.2014 - Agda, HoTT, Android

Haskell Hackathon haskell.hackathon at gmail.com
Sat Nov 22 19:23:10 UTC 2014


Hi *,
am Sonntag, 23. November 2014 treffen wir uns um 16:00 in India King
für unser Hackathon. Bringt eure Laptops!


Themen:

- Agda: wir versuchen ein einfaches Programm zu schreiben

oder

- Buch: Homotopy Type Theory (HoTT)

oder

- wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu
schreiben welches auf Android Apps runterkompiliert


-- BERICHT --

5. November 2014
- wir haben Agda 2.4.2 installiert. Es hat ein paar Probleme auf Grund
von cabal gegeben, die konnte man aber lösen indem man --constraint
benutzt hat.
- man kann Agda übrigens auch im sandbox installieren
- einer von uns hat zuvor Agda 2.3.2 aus einen .deb installiert. Das
hat auch einige haskell-libraries zurückgelassen; nach deren
entfernung waren die noch im ghc index vorhanden, aber kaputt (.so
Dateien nicht vorhanden). Das haben wir mit cabal install --reinstall
gelöst.
- man muss zuerst das agda-mode Plugin für Emacs installieren: agda-mode setup
- danach muss man die stlib runterladen:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
- und das src von stdlib Unterverzeichnis in Emacs als include-path
für agda2-mode hinterlegen: in Emacs über M-x customize-group RET
agda2 RET
- wir haben ein einfaches Tutorial angefangen:
http://www.stephendiehl.com/posts/agda.html
- es gibt auch "agda summer school":
https://github.com/UlfNorell/agda-summer-school/ -- die benutzte
library ("agda prelude") ist aber mit der stdlib von Agda inkompatibel
- wir haben über online-foren für HoTT gesprochen:
"hott amateurs": https://groups.google.com/forum/#!forum/hott-amateurs
das offizielle Forum für HoTT:
https://groups.google.com/forum/#!forum/homotopytypetheory
IRC: ##hott auf Freenode



-- ANFAHRT --

Wir treffen uns in India King, Landsbergerstr. 491.
Webseite: http://www.indiaking.de
Karte: https://goo.gl/maps/5g9m6

Anfahrtmöglichkeiten:

- S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram
19 nach Offenbachstraße (2 Haltestellen)
- Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße
- Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing
umsteigen, bis Offenbachstraße
- Bus 160 oder 162 nach Offenbachstraße

India King befindet sich genau gegenüber der Tramhaltestelle.




Twitter: https://twitter.com/Haskell_hackers
Web: http://haskell-hackathon.no-ip.org
English: http://haskell-hackathon.no-ip.org/index_en.html




More information about the munich-lisp mailing list