In this paper, the relationships between various classical compactness properties, including the constructively acceptable one of total boundedness and completeness, are examined using intuitionistic logic. For instance, although every metric space clearly is totally bounded whenever it possesses the Heine-Borel property that every open cover admits of a finite subcover, we show that one cannot expect a constructive proof that any such space is also complete. Even the Bolzano-Weierstraβ principle, that every sequence in a compact metric space has a convergent subsequence, is brought under our scrutiny; although that principle is essentially nonconstructive, we produce a reasonable, classically equivalent modification of it that is constructively valid. To this end, we require each sequence under consideration to satisfy uniformly a classically trivial approximate pigeonhole principle—that if infinitely many elements of the sequence are close to a finite set of points, then infinitely many of those elements are close to one of these points—whose constructive failure for arbitrary sequences is then detected as the obstacle to any constructive relevance of the traditional Bolzano-Weierstraβ principle.