In this famous paper by Borel and Harish-Chandra, Arithmetic Subgroups of Algebraic Groups, it is proved that, in characterisitic zero, arithmetic groups are finitely presented. I have an extremely vague idea of how the argument goes, but I was wondering if anything was known about how this would be done algorithmically. To be specific, (following work by Grunewald and Segal) an arithmetic group $\Gamma \leq \mathrm{GL}(n,\mathbb C)$ is said to be expicitly given if the following are satisfied:

• $\Gamma$ is arithmetic, and moreover
• we are given a system $S$ of polynomial equations defining the algebraic group $V(S)= \mathcal G$ (which contains $\Gamma$),
• there is a known upper bound $k$ for the index $[\mathrm{GL}(n,\mathbb Z)\cap \mathcal G:\Gamma]$, and
• there is a procedure which given $g \in \mathrm{GL}(n,\mathbb Z)\cap \mathcal G$ will decide if $g \in \Gamma$.

Then my question is: If $\Gamma$ is an explicitly given arithmetic group, is it possible to compute the presentation of $\Gamma$ or, even better, to get the orbihedron whose fundamental group is $\Gamma$, which is used in the construction of Borel and Harish-Chandra?

If there is a reference for this, or if this is known to be impossible, that would be awesome!