The compactness theorem for countable models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted [here](http://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](http://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?