У меня тут экзист... в общем, кризис среднего возраста. Были поводы. Пока было солнце, море и пиво две недели, думал, что пройдет. Не прошло. Вокруг какая-то сплошная хуита творится. Нашел какие-то online social support groups. Открыл, посмотрел и закрыл. Только хуже стало. Одни уроды и дебилы. Те же самые, что и в жизни. А где взять глобус с неуродами и недебилами, неизвестно. Уроды и дебилы - депрессия - еще больше уроды и дебилы - еще больше депрессия... Это замкнутый круг какой-то!

В прошлом году на день рождения получил пианино. За год немного научился играть. Хоть одна радость в жизни. А лямбды застопорились. Примерно знаю, чего хочу. Но этого мало, чтобы решение найти. В математике надо четко сформулировать, а потом обычно решение очевидно (особенно в этой теме). Оказывается, сформулировать не так-то просто. А компетентные люди все заняты грантами, конференциями, студентами, рецензиями и прочей хуитой. Внезапно оказалось, что они еще друг друга ненавидят всей душой. Неудивительно, что лямбды в жопе. Уже лет двадцать как, судя по публикациям.

Короче, надо просто всех убить, и все.

Command line

  • POSIX (XCU "Shell & Utilities"): vi(1), awk(1), make(1), bc(1), sed(1), grep(1), sort(1), uniq(1), tee(1), wc(1), etc.
  • GNU Screen (useful to echo exec screen -xR >>~/.profile on a remote host)
  • Git: git-grep(1), git-stash(1), git-bisect(1), etc.
  • Ledger (useful for optimizing both finances and time)
  • Taskwarrior (TODO manager, highly recommended)
  • drive (one of CLIs for Google Drive)
  • Jekyll (generates static websites from markdown)

Web

Chrome OS

  • Google Keep (quite convenient for grocery lists)
  • Google Drive (directly accessible in Chrome OS' Files)
  • Secure Shell (the main SSH client for Chrome OS, supports SFTP in Files and SSH bookmarks, type ssh name@example.com in the address field)
  • Wolfram Alpha (type = universe age in planck times in the address field)

Disclaimer: I'm celebrating five years as a Chromebook user.

Here is one way to profile calendars:

  1. Export calendars in iCalendar format.
  2. Check out this Awk script:

    function parse(dt)
    {
    	Y = substr(dt, 1, 4);
    	M = substr(dt, 5, 2);
    	D = substr(dt, 7, 2);
    	h = substr(dt, 10, 2);
    	m = substr(dt, 12, 2);
    	s = substr(dt, 14, 2);
    
    	return Y "/" M "/" D " " h ":" m ":" s;
    }
    
    /^BEGIN:VEVENT/ {
    	dtstart = "";
    	dtend = "";
    	summary = "";
    }
    
    /^DTSTART:/ {
    	sub(/\r$/, "");
    	sub(/^DTSTART:/, "");
    	dtstart = parse($0);
    }
    
    /^DTEND:/ {
    	sub(/\r$/, "");
    	sub(/^DTEND:/, "");
    	dtend = parse($0);
    }
    
    /^SUMMARY:/ {
    	sub(/\r$/, "");
    	sub(/^SUMMARY:/, "");
    	gsub(/  */, " ");
    	summary = $0;
    }
    
    /^END:VEVENT/ {
    	if (dtstart && dtend && summary) {
    		print "i " dtstart " " prefix summary;
    		print "o " dtend;
    	}
    }
    

  3. Have the Ledger utility installed:
    sudo apt install ledger # or whatever
  4. Convert the exported ICS files to timelog format:
    awk -f ics2tc.awk *.ics >timelog.tc
  5. Generate various reports from timelog, for example:
    ledger -f timelog.tc b -S -T
  6. Optionally specify a prefix:
    awk -f ics2tc.awk -v prefix=Work: Work.ics >Work.tc
  7. Or even create a Makefile like this:

    TIMELOGS = Anna.tc David.tc
    
    all: $(TIMELOGS)
    
    clean:
    	-rm -f $(TIMELOGS)
    
    .SUFFIXES: .ics .tc
    
    .ics.tc:
    	awk -f ics2tc.awk -v prefix=$*: $< >$@
    

  8. ?????
  9. PROFIT!!1oneone

<svg xmlns="http://www.w3.org/2000/svg"
	viewBox="0,0 5,5"
	fill="#8080ff">
<path d="M0,0 L5,0 L5,2 L4,2 L4,1 L1,1
	L1,4 L4,4 L4,3 L5,3 L5,5 L0,5 Z" />
<path d="M2,2 L2,3 L3,3 L3,2 Z">
<animateMotion begin="mouseover" restart="whenNotActive"
	dur="2s"
	calcMode="spline"
	keyPoints="0; .5; .5; 1"
	keyTimes="0; .36; .64; 1"
	keySplines=".5 0 .5 1; 0 0 1 1; .5 0 .5 1"
	path="M0,0 L2,0 Z" />
</path>
</svg>


Один из вариантов того, как можно читать классическую монографию по λ-исчислению [1]:

параграф 2.1;
упр. 2.4.1 (i)-(iii), 2.4.2-2.4.13;
упр. 2.4.15 (только в оригинале [2]);
параграф 2.2;
упр. 2.4.14;

параграфы 3.1-3.3;
упр. 3.5.1 (v), 3.5.1 (i), 3.5.6 (i), 3.5.2, 3.5.3, 3.5.11;
параграфы 13.1-13.2 до приложения 13.2.3 включительно;

часть II (главы 6-10);

параграф 4.1;
упр. 4.3.2, 4.3.4;
главы 15 и 16.

В каком-то приближении именно этот материал изложен чрезвычайно кратко в [3] (по-русски).

[1] Х. Барендрегт. Ламбда-исчисление, его синтаксис и семантика. Москва, 1985.
[2] H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1984.
[3] A. Salikhmetov. Lambda Calculus Synopsis. arXiv:1304.0558, 2013.
Lähetämme Teille ohessa uuden ajokorttinne numero 2013XXXXXXXXXX, joka on voimassa 19.01.2013-19.01.2028. Pyydämme teitä tarkistamaan, että ajokortilla olevat tiedot ovat oikein.

Jos Teillä on aiempi ajokortti, sen voimassaolo on päättynyt. Aiempi ajokortti on palautettava oheisessa palautuskuoressa. Postimaksu on maksettu. Jos aiempi ajokorttinne on kadonnut tai anastettu, Teidän on tehtävä anastus- tai katoamisilmoitus poliisille. Jos olette jo tehnyt ilmoituksen, asia on kunnossa.

Jos olette ajokiellossa, tämän ajokortin vastaanottaminen ei palauta ajo-oikeutta. Teidän on palautettava nyt vastaanottamanne ajokortti poliisille.
Почти пришла пора покинуть это место.

Немного жаль лишаться такого вида из окна зимой и летом:



Ну да ладно.

Посмотрим, как там будет дальше.

Most Popular Tags

Syndicate

RSS Atom

August 2017

S M T W T F S
  12345
6789101112
13141516171819
20212223 2425 26
2728293031  
Powered by Dreamwidth Studios