How to reduce UNSAT problems so that less than $7/8+\epsilon$ of clauses are unsatisfied? In this question I ask about what use is a solver that can find an assignment that satisfies, say, 90% of the clauses of a known satisfiable 3SAT problem in polynomial time.  The answer seems to be: given a problem ϕ that may or may not be satisfiable, you perform a reduction on an input formula ϕ to another formula ϕ′ such that ϕ′ is 90% satisfied iff ϕ is SAT and run my hypothetical algorithm on ϕ′, which will tell you if ϕ is SAT or not.

My question is a follow-up: what is the reduction from ϕ to ϕ'?
The reference is Håstad's classic paper, Some optimal inapproximability results. It relies on the PCP theorem and on Raz's parallel repetition theorem. The proof is not particularly easy, and even the reduction itself is not so simple to state (if you take into account the PCP component).