In the "The Rising Sea" by Vakil one can find the base change theorem for proper morphisms over a locally Noetherian base (28.1.6). He later indicates (28.2.M) how one could exchange the locally Noetherian condition by finitely presented using a result of Grothendieck. And indeed, it does not seem too hard to show this.
I am wondering if this version of the theorem is written down anywhere else in the literature (with or without a proof), as I seem unable to find it. I see the stronger version getting applied quite often (most recently in Olsson's book "Algebraic Spaces and Stacks" proof of lemma 8.4.6) but always without a proper reference (Olsson references Hartshorne, who only shows the statement for projective morphisms).
I could imagine that there is a formulation for algebraic spaces or stacks such that the theorem for schemes is just a special case. The closest thing I could find was theorem 1.9 / 1.10 in "Compatifying the Picard Scheme" by Altman and Kleiman, but this also does not seem to imply the base change theorem as stated by Vakil. It just seems really odd to me that such a prominent theorem can not be found in the Stacks Project or any other reputable source (without implying that Vakil is not reputable...)
Edit: To add to the list below: In Conrad, Brian, Grothendieck duality and base change, Lecture Notes in Mathematics. 1750. Berlin: Springer. x, 296 p. (2000). ZBL0992.14001. in Chapter 5.1 one can find an argument how to remove the Noetherian condition. But he only does so for a slightly weaker statement.
