# Should we need Coq on Android?

**URL:** <https://discourse.rocq-prover.org/t/should-we-need-coq-on-android/1293>\
**Category:** Using Rocq\
**Created:** [May 4, 2021, 6:09am UTC](https://discourse.rocq-prover.org/t/should-we-need-coq-on-android/1293 "2021-05-04T06:09:46Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![hhiim](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hhiim/32/394_2.png) [@hhiim](https://discourse.rocq-prover.org/u/hhiim)\
**Post date:** [May 4, 2021, 6:09am UTC](https://discourse.rocq-prover.org/t/should-we-need-coq-on-android/1293/1 "2021-05-04T06:09:47Z")

</div>

The Coq installer is huge (at least on Windows), so is it possible to port Coq to Android phones?

This way, we can prove theorems at our leisure time without having to open the computer.  
We can also use it to make a “math game” with the goal of proving theorems.  
This looks like interesting!

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [May 4, 2021, 7:00am UTC](https://discourse.rocq-prover.org/t/should-we-need-coq-on-android/1293/2 "2021-05-04T07:00:38Z")

</div>

Coq is already available in a browser ([https://jscoq.github.io/](https://jscoq.github.io/)) so it should allow making use of it from any tablet.

I don’t think the porting effort to Android would be worth it, but if someone wants to make an (unofficial) port, they are welcome to do so (Coq is free and open source software).

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [May 4, 2021, 7:50am UTC](https://discourse.rocq-prover.org/t/should-we-need-coq-on-android/1293/3 "2021-05-04T07:50:36Z")

</div>

In the past (i.e. when I had an Android device), I installed a Debian  
“chroot” inside the Android system. That means you can basically install  
any console application from typical GNU/Linux distributions – you use  
the Linux kernel from Android + the GNU &al tools from Debian. The  
downside of this approach is that you need root access to your device.

Inside this Debian environment, I installed Emacs and OCaml (from the  
package manager), opam2 (from the official download site), and compiled  
Coq using opam2.

There’s also an alternative without root access requirement, where you  
basically install Debian _inside_ an App. E.g., have a look at Termux:

[https://f-droid.org/en/packages/com.termux/](https://f-droid.org/en/packages/com.termux/)

---

<div class="post-metadata">

**Author:** ![AhpheeS7](https://avatars.discourse-cdn.com/v4/letter/a/3e96dc/32.png) [@AhpheeS7](https://discourse.rocq-prover.org/u/AhpheeS7)\
**Post date:** [October 21, 2024, 6:15pm UTC](https://discourse.rocq-prover.org/t/should-we-need-coq-on-android/1293/4 "2024-10-21T18:15:09Z")

</div>

Yes, and Termux has a bunch of packages even without Debian (and it is much more efficient than installing a proot Debian inside). However, there seems some difficulties packaging OCaml: [[Package request] Ocaml core · Issue #6201 · termux/termux-packages · GitHub](https://github.com/termux/termux-packages/issues/6201)