[racket] proof assistants, DrRacket and Bootstrap

   Just do the obvious. Click in Interactions, cmd-p (or whatever
   incantations are appropriate for your favorite OS), save the file,
   and voila you have a PDF of your interactions. 

Thanks, Matthias!  It worked, and I feel foolish I didn't see this earlier.   On a Linux box where I compiled drracket, I type C-d (Show Interactions), and I'm in the Interactions buffer, and click
Files -> Print Interactions
and get a Print window, where I have only one option
Print to File
and I get a PDF of my interactions!  But I won't put it on my web page, because it is really slow.  It's a 69 page PDF, and all I've been able to see is the first 9 pages, and I've been waiting of while for the rest to appear.  If anyone wants to check, they can hit my Racket Interactions file and try Print to File:
http://www.math.northwestern.edu/~richter/10-31-2014.rkt
But Dr Racket fires this Interactions file and I easily blast through the whole thing.  It's a long file, and maybe Print to File could only handle the first part of it. 

I went through 10-31-2014.rkt with my 7th student, and I think he liked it.  I said that the purpose of Sudoku is to find the simplest mathematical proofs.  If you look at a 2-column High School Geometry proof, the n-th statement is proved by using all the previous n-1 statements.  What we're looking for is 2-column Sudoku proofs where the n-th statement is proved by using only the previous statement, and this n-th step proof is supposed to be simple.  You can find Sudoku puzzles that are so hard that you can't do that, but it almost never happens in the Chicago Trib comic section Sudokus.  This puzzle was the Trib puzzle on 10-31-2014 (every Friday they have a #4 puzzle, their hardest rating). 

-- 
Best,
Bill