The compactness theorem for countable (Tarski?) models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted [here](https://mathoverflow.net/questions/228389), in the context of classical logic. The weak König's lemma in constructive mathematics has been extensively studied as noted [here](https://mathoverflow.net/questions/228468). What is the status of the *compactness theorem for countable models* itself in constructive mathematics.

One relevant paper seems to be *Moerdijk, Ieke; Palmgren, Erik. Minimal models of Heyting arithmetic. J. Symbolic Logic  62  (1997),  no. 4, 1448–1460.*

One relevant issue is the mutual relation of the following three items:

(1) compactness theorem for countable models;

(2) weak Koenig's lemma;

(3) lesser limited principle of omniscience (LLPO).

In what constructive setting are these principles equivalent? More specifically: how much of the proof of equivalence sketched in the answer to [this question](https://mathoverflow.net/questions/228389) can be retained in a suitable constructive setting, using references mentioned in the answer to [this question](https://mathoverflow.net/questions/228468)?