The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Thanks for details,

How would you see the state of your goal in one-buffer mode? Would you
switch between the three buffers?

Pierre

2017-10-18 6:23 GMT+02:00 Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>:
> (Thanks Kyle for your response and your work.)
>
> I totally agree that it is much less efficient to use Coq on a phone instead
> of a regular desktop.
> Nevertheless, there are times when a desktop is not an option at all: when
> waiting in a queue to check in for a flight, or waiting for food in a
> restaurant when dining alone, or being stuck without a laptop in a talk
> whose title was deceptive.
>
> On phones with large screens, one can make productive use of Coq.
> For example, if one is stuck on a proof, and then stuck waiting for food,
> they can look up the proof state where there are stuck and perhaps even make
> small changes so that their thought process has better ideas to chew on when
> the food finally arrives.
> On my phone, I mainly use the console mode of emacs (emacs -nw) with
> company-coq.
> I usually SSH to my work desktop and open the proof I am stuck on in "emacs
> -nw".
>
> On phones, it does not make sense to split the screen into several buffers.
> Disabling the "three-buffer mode" of proof general helps.
> It would help to have a "one-buffer mode" in proof general.
> When my phone is in the landscape orientation, it is very unhelpful when
> proof-general splits my screen vertically to show both the code and the
> subgoal buffers at once.
> In landscape mode, the lower ~half of the screen is already occupied by the
> keyboard. So there is only a quarter of a phone's width available for each
> buffer.
>
> SSHing to my work desktop usually suffices for me, except when I am
> traveling for many days, especially to other countries. Then I do have to
> install everything, including Coq, on my phone itself, for times when I have
> no (or high-latency) connectivity.
> Apps like GNURoot Debian make it possible to run a full-fledged "linux
> virtual machine" inside Android, at least until Android 6.1.
> IIRC, CoqIDE works properly in GNURoot Debian.
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
>
> On Tue, Oct 17, 2017 at 5:16 AM, Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
> wrote:
>>
>> Yeah, and how do you use it? Does coqide work well on android?
>> Multi-touch screens is certainly something we want to try for
>> human/proof-assistant interactions.
>>
>> P.
>>
>> 2017-10-17 7:25 GMT+02:00 Daniel Galvez 
>> <dt.galvez AT gmail.com>:
>> > It's been a long time since I've done any serious work in Coq, but
>> > curiosity
>> > brings me out of the depths of lurking on this mailing list.
>> >
>> > I'm surprised no one has asked yet: what has motivated more than a few
>> > of
>> > you to want to install coq on android?
>> >
>> > Sincerely,
>> > Daniel
>> >
>> > On Mon, Oct 16, 2017 at 9:58 PM, Nicolas Pelletier
>> > <nicolas.pelletier3 AT gmail.com>
>> >  wrote:
>> >>
>> >> Thank you for these links. I could very well need the kind of patch
>> >> discussed in the PR, but for Coq. I am not familiar enough with the ARM
>> >> ABI
>> >> to know which parts of it are necessary for 64bits; but this is worth
>> >> investigating further.
>> >>
>> >> As for getting OCaml and opam to work, I didn't need anything beyond
>> >> the
>> >> termux patches and fixing a few pathes... so 64bits work better than
>> >> 32bits
>> >> in this case.
>> >>
>> >> Regards,
>> >>
>> >> -- Nicolas
>> >
>> >
>> >
>> >
>> > --
>> > Daniel Galvez
>
>