ACL2 newbie

I'm learning ACL2: after spending a day understanding what most people feel when they try to program a computer (why the *#@* doesn't it accept my program?), I seem to have a breakthrough that at least allows me to write some functions and make a little progress. Mostly this involves learning "The Method", and becoming a lot more sensitive to all those nagging little corner cases that don't normally ever happen. But of course, the proof system doesn't know they can't happen..

I've gotten it to accept a dozen or so functions, which for me was non-trivial. I'm having trouble now because I need to define a custom :measure on my last function, and I don't understand enough about how ACL2 does rationals (rationalp, natp, numberp, o-p, o<, etc). I assume it will make sense if I read the doc...

It's fun, in a strange way, to be a newbie... I started programming so long ago I have forgotten what it is like to not know how. But ACL2 is letting me remember!

My Vonage Disaster

Last August I decided to sign up for Vonage, to try it out. I made a few calls and it seemed to work. So I requested that my home number be converted to a Vonage number. I waited and waited. Nothing happened. I called them every month or so for the next six months to check the status, but nothing happened. Perhaps SBC was not willing to make the transfer. Perhaps Vonage dropped the ball.

Updated Date: Number Transfer Progress History
August 15, 2004: Awaiting Letter of Authorization
November 24, 2004: Letter of Authorization (LOA) Received
November 24, 2004: Transfer Sent to Carrier
November 24, 2004: Transfer Sent to Carrier
April 18, 2005: LNP Transfer Cancelled

All this time I was paying service charges for a service that didn't work. The gave me a months credit when I asked for it. Finally I was annoyed and asked them to cancel the service. But I couldn't find the original box to send the equipment back, so they charged me for that. $386 later I have nothing but a useless Vonage box.

I guess that is one way to make money...

I've noticed that all my posts so far have been tips, tricks and annoyances. There are several reasons for this:

1) I have a backlog of useful bits that I feel I should post.
2) I feel guilty that I've been using solutions to problems I find on the internet, but haven't been posting my own.
3) Perhaps I'm still getting used to the medium.

Eventually I will start writing about higher-level issues....

Windows backups

I had a disk completely die, and my backups are not as good as they should have been. Fortunately, the data recovery people know their job.

This motivated me to figure out Windows backups. I am not sure that this is the greatest backup script, but it works for me. Here is what it does:
* creates a full backup every week (on monday)
* creates differential backups (with changes from the full backup) every day
* cycles N different backups so you have several weeks/days of backup
* copies the files from one backup media to another, MASTER to SECOND
* just requires one scheduled job
* uses a single selection of files for all backups

To set this up:
* create MASTER and SECOND directories and set the paths in the script
* use NTBackup.exe to create the file "backupList.bks" which lists what files to back up
* put the script into the MASTER directory
* schedule a job to run it every day

This script is provided as is, with no guarantee that it will work for you. Let me know if you have improvements.

set MASTER=K:\Backups
set SECOND=L:\Backups
set keepWeekly=2
set keepDaily=2

REM set test=echo to test the script
set test=

rem echo Backup# %x%

IF "%DATE:~0,3%" == "Mon" GOTO WEEKLY

    ECHO Running Daily backup
    for /F %%m in (%MASTER%\dailyNumber.txt) do set /a x="%%m"
    set type=differential 
    set file=Daily%x%
    set /a x="( %x% + 1) %% (%keepDaily%)"
    echo %x% > %MASTER%\dailyNumber.txt

goto DONE
:WEEKLY

    ECHO Running Weekly backup
    for /F %%m in (%MASTER%\weeklyNumber.txt) do set /a x="%%m"
    set type=normal 
    set file=Weekly%x%
    set /a x="( %x% + 1) %% (%keepWeekly%)"
    echo %x% > %MASTER%\weeklyNumber.txt

:DONE

%test% ntbackup.exe backup "@%MASTER%\backupList.bks" ^
    /n "%file%" /d "%DATE%"                           ^
    /v:no /r:no /rs:no /hc:off                        ^
    /m %type% /j "%file%" /l:s /f                     ^
    "%MASTER%\%file%.bkf"

%test% copy /Y /B "%MASTER%\%file%.bkf"               ^
    "%SECOND%\%file%.bkf"

set local=%USERPROFILE%\Local Settings
set data=%local%\Application Data\Microsoft
move "%data%\Windows NT\NTBackup\data"\*.log          ^
    "%MASTER%"