Greg Lehey

Emacs is the only officially supported interactive Agda environment, as other people have noted.

However, I have written a lot of Agda code in other editors (acme and vim). It is certainly feasable to do! In fact I find that it improves my code quality not to use the interactive features. When in interactive mode, I blindly chase the goal trying to get the correct type, and often end up going long detours. When I am on my own I get a better overview of the situation, and can often see the shortest path.

That said, I wish they would continue to support agda interactive mode on the command line, as it is nice to be able to evaluate expressions in context of a hole.

Writing unicode is a breeze with XCompose, in any UTF8-enabled editor. I found a nice XCompose file based on the Plan 9 keyboard file, by Pmarin. It can be downloaded from «Greg 'Groggy' Lehey»'s site:

http://www.lemis.com/grog/programs/XCompose

(1) Lions on Unix (PDF and source), http://www.lemis.com/grog/Documentation/Lions/index.php

http://en.wikipedia.org/wiki/Lions%27_Commentary_on_UNIX_6th_Edition,_with_Source_Code

"Lions' Commentary on UNIX 6th Edition, with Source Code by John Lions (1976) contains the complete source code of the 6th Edition Unix kernel plus a commentary. It is commonly referred to as the Lions book. Despite its age, it is still considered an excellent commentary on simple but high quality code."

(2) Harper's dictionary of classical literature and antiquities (1898), 1750 pages, https://archive.org/details/harpersdictiona00peckgoog

(3) Oxford English Dictionary (1888), 15000 searchable page scans in a Windows app, https://archive.org/details/oed11_201407

Of possible (mostly historical) interest at this point, a similar commentary on a fairly early version of the original Unix kernel, by an Australian cs prof named John Lions -- which was very widely circulated among CS students in the '80s, despite this being technically in violation of AT&T's copyright on the book.

It's availble online here:
http://www.lemis.com/grog/Documentation/Lions/index.php

Note that the code is written in a very archaic dialect of C, and for hardware that didn't support paging in any form (just swapping). Nevertheless, it was an important introduction for a lot of people at the time, not just to the basics of OS implementation details, but also, how to find your way around a nontrivial sized codebase.

This led me to the already mentioned APUE book, written by Stevens. I was saddened by his loss at a yound age of 48. http://www.salon.com/technology/feature/2000/09/01/rich_stevens

That article led me to this:

http://www.salon.com/technology/feature/1999/11/30/lions/index.html which is another fantastic read.

You can read about Lions' efforts here: Lions' Commentary on UNIX 6th Edition, with Source Code http://en.wikipedia.org/wiki/Lions_Commentary_on_UNIX_6th_Edition,_with_Source_Code

http://tinyurl.com/2k9rwr (If the link above doesn't work)

The commentary is available as a PDF file here: http://www.lemis.com/grog/Documentation/Lions/book.pdf

Yes, there is.

John Lion's "A commentary on the Sixth Edition UNIX Operating System", goes through the PDP-11 UNIX kernel line by line.

http://www.lemis.com/grog/Documentation/Lions/book.pdf

Page 37, Section 7.13, "newproc":

1906: Call "xswap" (4368) to copy the data segments into the disk swap area. Because the second parameter is zero, the main memory area will not be released.

1907: Mark the new process as "swapped out".

1908: Return the current process to its normal state.

If your argument is that Caldera might not actually have the rights to UNIX in the first place to grant the license, that's fair.

But the license they provided (http://www.lemis.com/grog/UNIX/ancient-source-all.pdf) explicitly names versions 1, 2, 3, 4, 5, 6, and 7 of UNIX for the 16-bit PDP-11. Yes, these versions originated at AT&T (Bell Labs) but are distinct legally from SysIII and SysV UNIX, also from AT&T, which are explicitly not covered by the Caldera license.