Ed. note: Sorry this is more like a blog post.
Having recorded the Molin Upper Elementary 5th Grade Christmas Concert using my video camera, I wanted to extract just the audio portion so that I could listen to the music all by itself without having to play the video. Besides, I could send the audio portion much more easily than I could send the 948 MB video file through email. The half-hour concert produced a lossless .ogg file of 21 MB and 14 MB in lossy mp3 format.
The Video Editing article gives some examples for using mencoder and ffmpeg, but in this case I found using ffmpeg on the command line was the easiest tool after some initial trial and error. I was surprised to find out that Avidemux didn't just do what I wanted. With Avidemux, I tried 'save audio' which produced a relatively large file, that didn't play in anything. I ran ffmpeg -i on it, and it reported "unknown format"
# try mplayer, but it did not work
mplayer -dumpaudio VID00001.AVI -dumpfile molin-5th-grade-xmas-concert.mp3
## Try instead to use ffmpeg
# tell me information about my source file
ffmpeg -i VID00001.AVI
# copy the audio codec; but name the output .mp3 (of course this will not work)
ffmpeg -i VID00001.AVI -acodec copy molin-5th-grade-xmas-concert.mp3
# copy the audio codec; disable video; but name the output .mp3 (of course this will not work)
ffmpeg -i VID00001.AVI -vn -acodec copy molin-5th-grade-xmas-concert.mp3
# disable video; use mp3 codec (that is not the name of a valid codec)
ffmpeg -i VID00001.AVI -vn -acodec mp3 molin-5th-grade-xmas-concert.mp3
# let ffmpeg figure out what I want (WORKED)
ffmpeg -i VID00001.AVI -vn molin-5th-grade-xmas-concert.mp3
For creating the .ogg file, I went with the easier GUI approach and used SoundConverter