On 30/10/2018 19:10, Matthew Flatt wrote:
> At Tue, 30 Oct 2018 17:54:46 +0100, "'Paulo Matos' via Racket Users" wrote:
>> On 30/10/2018 16:39, Matthew Flatt wrote:
>>> You need to close the output port after `gunzip-through-ports` finishes.
>> OK, that was a mistake of writing this smallish example. The problem
>> persists, if I write (close-output-port out) after (gunzip-through-ports
>> ➜ zipping-through-ports wc -l foo1
>> 12987 foo1
>> ➜ zipping-through-ports wc -l foo2
>> 12987 foo2
>> ➜ zipping-through-ports wc -l foo3
>> 12987 foo3
>> ➜ zipping-through-ports wc -l foo.txt
>> 12988 foo.txt
>> I was expecting foo.txt to be the same as
>> $ cat foo1 foo2 foo3 > foo.txt
> Oh, I see. The gzip format lets `gunzip-through-ports` stop when it
> gets to the end of a compressed stream, so if you want to decompress
> multiple concatenated streams until an EOF:
> (let loop ()
> (unless (eof-object? (peek-byte cin))
> (gunzip-through-ports cin out)
Yes! That makes sense. :)
(define paths '("foo1" "foo2" "foo3"))
(lambda (op p)
(for ([f (in-list paths)])
(lambda (i) (gzip-through-ports i op #false (current-seconds)))
(define-values (in out) (make-pipe))
(let loop ()
(unless (eof-object? (peek-byte cin))
(gunzip-through-ports cin out)
(lambda (op p)
(let loop ([l (read-line in)])
(unless (eof-object? l)
(display l op)
(loop (read-line in))))))
>> Still, I should point out that the reason I didn't close it originally
>> was because the documentation mentions that it's not necessary to close
>> make-pipe ports:
>> "Unlike some other kinds of ports, pipe ports do not need to be
>> explicitly closed to be reclaimed by garbage collection."
> It isn't necessary to close the pipe for the pipe to be GCed when it's
> no longer referenced. But if you want to get an EOF from the input end
> of the pipe, then the write end needs to be closed.
Thanks for the clarification.
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
For more options, visit https://groups.google.com/d/optout.