Also, how do different sets of principles affect the results we can get in our meta-theory?
The more concrete questions that lead me to ask the above two questions are stated below.
If we are studying intuitionistic logic, should we also drop the excluded middle rule in our meta-theory?
Besides, in classic logic, I seem to notice that a proof of the compactness theorem must utilise the axiom of choice, be it directly or indirectly. The proofs I ever saw so far all implicitly assumed the axiom of choice in its meta-theory. (Actually, so are the proofs of the completeness theorem.) Does that mean, if we are to drop the AC, we can't even have the compactness theorem?
What if we are studying a set theory without the AC? Should we assume the AC in our meta-theory when studying a set theory with the axiom of determinacy instead of AC? Or maybe we should adopt the AD instead of AC? Are we supposed to use the same rules in meta-theory as those in our formal theory?
No, there's no "rule" that you need to adopt the same principles in the metatheory as in the theory you're studying.
In my experience, it's far more common to study intuitionistic logic in a classical metatheory than a constructive metatheory. There's no inherent philosophical problem with this: intuitionistic logic is a model of certain kinds of constructive reasoning... there's no reason why we need to be confined to this mode of reasoning in order to talk about it. There would have to be some other philosophical considerations in play to motivate disallowing nonconstructive reasoning (e.g. being a constructivist).
Conversely, it's perfectly cromulent for a constructive logician to study classical logic using only constructive methods. As a simple example, there's nothing non-constructive in understanding truth tables in propositional logic... but one can certainly go much deeper than that.
The compactness theorem for propositional logic is equivalent (over ZF) to the ultrafilter lemma, a weaker form of the axiom of choice. But that's for general sets of propositional variables. If we have a countable (or even just well-orderable) set of propositional variables, then we can prove compactness in ZF.
To the part about AC, as with the case of intuitionistic logic in the first bullet, there's really no rule here. Moreover, it's often admissible to use AC in the study of set theory without AC. For instance, if we want to show the consistency of some proposition with ZF (e.g. "the reals are a countable union of countable sets" or "every set is linearly-orderable, but countable choice fails"), we're entitled to work in a model of ZFC, since any model of ZF has a model of ZFC inside it. More generally, in set theory, one often constructs a model of a given principle from a model of something contradictory to it.