Semplicemente nel manuale pdftex c’è un errore di stampa, dove c’è scritto “divided”, che doveva essere indicato con “multiplied”. Insomma è la stessa differenza fra i points e gli scaled points.
Tan’è che ho provato a girare la soluzione in un modo diverso, forse ridondante, ma chiarissimo: assegno il numero prodotto da \pdfelapsedtime ad un registro dimensionale (di tipo TeX, non LaTeX) specificando l’unità di misura sp (scaled points); poi definisco una macro che contiene il valore del registro dimensionale a cui sono state “strappate” le unità di misura. ne ottengo il nomero di punti senza il pt dopo. Stampo poi questa macro:
`
\AfterEndDocument{\dimen256=\pdfelapsedtime sp
\edef\@tempA{\strip@pt\dimen256}
\PackageInfo{MacroGuida}{Il tempo di esecuzione e' stato pari a \@tempA\space s}}
`
Invece di \PackageInfo (che scrive solo sul file .log) si potrebbe usare anche \PackageWarningNoLine che scrive anche sulla console.
\AfterEndDocument è un comando prodotto dal pacchetto etoolbox, ma il comando e il pacchetto di Enrico fanno lo stesso mestiere.
Però questo esempio che ti produce direttamente il numero di secondi con il punto decimale seguita da 5 cifre per la parte fratta, è anche la prova provata dell’errore di stampa nella documentazione di pdftex.
Ho eseguite alcune volte la compilazione dell’Introduzione, senza apportare modifiche di nessuna genere ai file sorgente (seicento e passa pagine con molte figure importate e molte disegnte direttamente) e il tempo di compilazione ogni volta è diverso, perché, appunto si tratta di tempo trascorso da quando il processo è cominciato; nel frattempo il sistema operativo multitasking (nel mio caso SnowLeopard) fa anche altre cose, quindi distribuisce il suo tempo fra i vari processi a cui deve fornire le sue prestazioni. L’Introduzione si compila quindi in tempi che vanno da 11s a 12s (arrotondati all’intero) quindi è del tutto superfluo per processi così “lunghi” stare a specificare i millesimi o frazioni di secondo ancora più piccole, come avviene con il codice indicato sopra.
Se invece il processo è rapido le frazioni di secondo sono importanti; nel tuo esempio controllato dal comando time del sistema operativo, dove non superi un quinto di secondo, le frazioni sono decisamente importanti, anche se probabilmente non saranno mai le stesse.