Separability vs. metrizability in compact Hausdorff Exercise #4 in Section 34 of Munkres' Topology (2nd ed) states the following:

Let $X$ be a compact Hausdorff space. Show that $X$ is metrizable if and only if it has a countable basis.

However, even though (under Countable Choice) any metric space is second countable iff it is separable, we cannot a priori modify this exercise to read

Let $X$ be a compact Hausdorff space. Show that $X$ is metrizable if and only if it is $\color{red}{separable}$

because it is not true in arbitrary topological spaces that separability implies second countable.
My Question: Is there an example of a compact Hausdorff space which is separable but not metrizable? Or is the modified Munkres exercise correct?
Note: I would prefer a construction of the offending space or a proof no such space exists, which is doable in $\mathsf{ZF}$. However, feel free to use any degree of choice necessary.
 A: There are many counterexamples.  The "universal" counterexample is $\beta\mathbb{N}$, the Stone-Cech compactification of $\mathbb{N}$ with the discrete topology.  By the universal property of the Stone-Cech compactification, this is the "largest possible" separable compact Hausdorff space.  To see that it cannot be metrizable, note that no subsequence of the natural numbers can converge in $\beta\mathbb{N}$, since then the universal property would imply that the corresponding subsequence of every sequence in any compact Hausdorff space converges, which is obviously false.  So $\beta\mathbb{N}$ is compact but has a sequence with no convergent subsequence, so it is not metrizable.
Another example is $[0,1]^{[0,1]}$ with the product topology.  This is clearly not metrizable (for instance, it is not first-countable at any point).  Perhaps surprisingly, it is separable: for instance, the set functions that take only rational values and are constant on each set of a finite partition of $[0,1]$ into intervals with rational endpoints is dense.
The examples above require the axiom of choice to prove they are compact (or, depending how you define $\beta\mathbb{N}$, to prove it even exists).  For an example that works in ZF, consider $[0,1]\times\{0,1\}$ with the lexicographic order topology.  The lexicographic order is complete so this space is compact, and it is separable (the set of points with rational first coordinate is dense) and even first-countable as well.  To see that it is not second-countable and hence not metrizable, note that it has uncountably many clopen subsets: for any $a<b$, the interval $[(a,1),(b,0)]=((a,0),(b,1))$ is clopen.  A second-countable compact space can only have countably many clopen subsets, since each clopen set is (by compactness) a finite union of basic open sets.
