# HG changeset patch # User Oleksandr Gavenko # Date 1242222448 -10800 # Node ID 703b527d0279263790ab55e7c0e9516ecdaa8156 # Parent c065527d633271441689202bfc638dda016a72d0# Parent b6885557d64359f969283d9e518075428fd30b06 Automated merge with file:///srv/hg/admin-doc diff -r b6885557d643 -r 703b527d0279 auto-proof.rst --- a/auto-proof.rst Wed May 13 16:47:07 2009 +0300 +++ b/auto-proof.rst Wed May 13 16:47:28 2009 +0300 @@ -73,6 +73,22 @@ http://formalmath.tiddlyspot.com/ +* HOL Light. + +HOL Light is a computer program to help users prove interesting mathematical +theorems completely formally in higher order logic. It sets a very exacting +standard of correctness, but provides a number of automated tools and +pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and +real analysis) to save the user work. It is also fully programmable, so users +can extend it with new theorems and inference rules without compromising its +soundness. + +Ocalm. + +See + + http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html + * ACL2. ACL2 (A Computational Logic for Applicative Common Lisp) is a software system @@ -156,3 +172,12 @@ http://www.ijcar.org/ http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning + +* Top 100. + + http://www.cs.ru.nl/~freek/100/ + (winner) + http://personal.stevens.edu/~nkahl/Top100Theorems.html + (orig list) + http://www.cse.unsw.edu.au/~kleing/top100/#5 + (Isabelle) diff -r b6885557d643 -r 703b527d0279 blog.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/blog.rst Wed May 13 16:47:28 2009 +0300 @@ -0,0 +1,7 @@ +-*- outline -*- + +* Blogspot and Emacs. + +See + + http://code.google.com/p/e-blog/ diff -r b6885557d643 -r 703b527d0279 cmd.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/cmd.rst Wed May 13 16:47:28 2009 +0300 @@ -0,0 +1,9 @@ +-*- outline -*- + +* CMD tricks. + + $ set /p TOOLOUTPUT= < temp.txt + + $ for /f "tokens=*" %%i in ('%~dp0sometool.exe') do set TOOLOUTPUT=%%i + + $ for /f "tokens=1 delims=" %%s in (users.txt) do (echo %%S & command "%%S") >> outputfile.txt diff -r b6885557d643 -r 703b527d0279 date.rst --- a/date.rst Wed May 13 16:47:07 2009 +0300 +++ b/date.rst Wed May 13 16:47:28 2009 +0300 @@ -141,3 +141,7 @@ Here is that TZ value again, this time on standard output so that you can use the /usr/bin/tzselect command in shell scripts: Europe/Kiev + +** Debian Lenny. + + $ sudo dpkg-reconfigure tzdata diff -r b6885557d643 -r 703b527d0279 iso-9660.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/iso-9660.rst Wed May 13 16:47:28 2009 +0300 @@ -0,0 +1,10 @@ +-*- outline -*- + +* Mounting ISO Images in Solaris. + + $ /usr/sbin/lofiadm -d /dev/lofi/1 + $ /usr/sbin/lofiadm -a /var/tmp/CDImage.iso + $ [ -d /mnt ] && echo OK || echo FAILURE + $ /usr/sbin/umount /mnt + $ /usr/sbin/mount -F hsfs -o ro /dev/lofi/1 /mnt + $ cd /mnt diff -r b6885557d643 -r 703b527d0279 mail.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/mail.rst Wed May 13 16:47:28 2009 +0300 @@ -0,0 +1,31 @@ +-*- outline -*- + +* Sending email via gmail in emacs. + +; install starttls from here (no need for patch) +; http://josefsson.org/emacs-smtp-starttls.html + +(setq send-mail-function 'smtpmail-send-it + message-send-mail-function 'smtpmail-send-it + smtpmail-starttls-credentials + '(("smtp.gmail.com" 587 nil nil)) + smtpmail-auth-credentials + (expand-file-name "~/.authinfo") + smtpmail-default-smtp-server "smtp.gmail.com" + smtpmail-smtp-server "smtp.gmail.com" + smtpmail-smtp-service 587 + smtpmail-debug-info t + starttls-extra-arguments nil + smtpmail-warn-about-unknown-extensions t + starttls-use-gnutls nil) + +machine smtp.gmail.com login [your name]@gmail.com password [your password] + +And finally download, unzip, make and install startttls: + +http://josefsson.org/emacs-smtp-starttls.html + +See + + http://justinsboringpage.blogspot.com/2009/02/sending-email-via-gmail-in-emacs.html + http://obfuscatedcode.wordpress.com/2007/04/26/configuring-emacs-for-gmails-smtp diff -r b6885557d643 -r 703b527d0279 svn.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/svn.rst Wed May 13 16:47:28 2009 +0300 @@ -0,0 +1,7 @@ +-*- outline -*- + +* Copy repo from SourceForge to GoogleCode. + + $ svnsync init https://PROJ.googlecode.com/svn https://PROJ.svn.sourceforge.net/svnroot/PROJ + $ svnsync --username NAME --password PASSWORD \ + sync https://PROJ.googlecode.com/svn https://PROJ.svn.sourceforge.net/svnroot/PROJ diff -r b6885557d643 -r 703b527d0279 video-file.rst --- a/video-file.rst Wed May 13 16:47:07 2009 +0300 +++ b/video-file.rst Wed May 13 16:47:28 2009 +0300 @@ -14,6 +14,10 @@ Then do: + $ ffmpeg -i test.3gp -f mpegvideo -ar 44100 -ac 1 -acodec mp3 test.mpg + + $ for i in `ls -1 *.3gp | cut -d. -f1`; do ffmpeg -y -i $i.3gp -sameq -f mpegvideo -s cif -r 25 -ar 32000 -ac 1 mpegs/$i.mpg; done + $ ffmpeg -i video-in.3gp -b 250 -s 160×120 -r 15 -f avi -an video-out.avi or $ mencoder -oac mp3lame -ovc lavc -o video-out.avi -vf pp,2xsai,scale video-in.3gp @@ -21,3 +25,20 @@ $ mencoder -o video-in.avi -vf pp,2xsai,scale -ovc lavc video-out.3gp or $ mencoder -o video-in.avi -vf rotate=2 -oac pcm -ovc divx4 video-out.3gp + + +You need to compile FFmpeg with AMR support (--enable-amr_nb +--enable-amr_wb) + +AMR WB FLOAT NOTICE ! Make sure you have downloaded TS26.204 +V5.1.0 from +http://www.3gpp.org/ftp/Specs/archive/26_series/26.204/26204-510.zip +and extracted the source to libavcodec/amrwb_float + + +AMR NB FLOAT NOTICE ! Make sure you have downloaded TS26.104 +REL-5 V5.1.0 from +http://www.3gpp.org/ftp/Specs/latest/Rel-5/26_series/26104-5??.zip +and extracted the source to libavcodec/amr_float +and if u try this on an alpha, u may need to change Word32 to int in +amr/typedef.h diff -r b6885557d643 -r 703b527d0279 virtualization.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/virtualization.rst Wed May 13 16:47:28 2009 +0300 @@ -0,0 +1,11 @@ +-*- outline -*- + +* VirtualBox. + +x86 virtualization solution. + +In Debian Etch use backport repo. + + $ sudo apt-get install virtualbox-ose + +