Thomas Baruchel (Nov 15 2022 at 15:54): Thomas Baruchel (Nov 15 2022 at 15:54):Hi, just fall upon jsCoq and wondering if it could be useful on small Android devices when on the go. Would it be possible to turn it into a true webapp. Not an expert myself, but truly "installable" webapps have several interesting features (separate windows with a dedicated title vs a simple tab in the browser, taking advantage of the whole space on the screen with no URL bar or browser buttons, etc.)
Shachar Itzhaky (Nov 15 2022 at 15:58):A very popular approach today is to use one of several frameworks that basically "wrap" a website with an Android app object, giving the feel of a native app while in fact what's inside is a WebView instance with HTML+JS. This approach would definitely work for jsCoq.
The problem, I believe lies elsewhere: the UI design and interaction mode are very much keyboard-and-mouse oriented and not suited for a small touchscreen. I have no experience developing mobile apps, but if you know someone who can suggest a better design for mobile I can make a mobile version of the website according to their description.
Huỳnh Trần Khanh (Nov 15 2022 at 16:06):The OP probably meant a progressive web app though. We just need to add a few manifest files to make a progressive web app. But yeah, the hardest part is elsewhere. Probably we could work on making the text editor actually usable on mobile?
Karl Palmskog (Nov 15 2022 at 16:09):it sounds like what is really needed in mobile is an alternative "input paradigm" like here: https://link.springer.com/chapter/10.1007/3-540-57887-0_94
This paper presents a principle for using locations in logical expressions to guide the process of building proofs. Using a sequent-style presentation of theorem provers, we annotate the inference rules to specify an algorithm that associates the construction of a proof tree to a location within a goal sequent. This principle provides a natural and effective use of the mouse in the user-interface of computer proof assistants. The implementation of the algorithm in a variety of theorem provers is discussed.
Karl Palmskog (Nov 15 2022 at 16:09):(obviously replace "mouse" by "finger")
Shachar Itzhaky (Nov 15 2022 at 16:09):Huỳnh Trần Khanh said:
The OP probably meant a progressive web app though.
yeah thanks for the Silicon Valley lingo to go with my half-thoughts :laughing:
Shachar Itzhaky (Nov 15 2022 at 16:11):I've been wanting forever to create a gesture-based interface for Coq using jsCoq; I know there have been a few not-so-successful attempts so I was a bit demotivated. But perhaps in this paper we can find some good pointers.
Karl Palmskog (Nov 15 2022 at 16:12):there were actually quite a few papers, and even a Java prototype that was discontinued. Yves said that it was popular in teaching.
Karl Palmskog (Nov 15 2022 at 16:12):https://www-sop.inria.fr/lemme/pcoq/
Karl Palmskog (Nov 15 2022 at 16:14):I'm sure Yves Bertot and/or Laurent Théry would be happy to at least give input to any new gesture stuff for jsCoq. (They are on the Zulip if you want to to ping)
Shachar Itzhaky (Nov 15 2022 at 16:14):this is definitely one of those that I've looked at. So you say it was popular and the only problem is that perhaps it has become outdated relative to modern UX. Interesting! Should look at it again.
Shachar Itzhaky (Nov 15 2022 at 16:15):@Emilio Jesús Gallego Arias one of the things in our roadmap was "talk to HCI dudes", so we can maybe invest in it.
Karl Palmskog (Nov 15 2022 at 16:16):I think this was in the same style: https://www.sciencedirect.com/science/article/pii/S1571066112000254
The main problem was to my knowledge maintainability. UI code bitrots insanely quickly.
Karl Palmskog (Nov 15 2022 at 16:19):an even older prototype (1996): https://link.springer.com/chapter/10.1007/BFb0014352
Shachar Itzhaky (Nov 15 2022 at 16:19):Karl Palmskog said:
an even older prototype (1996): https://link.springer.com/chapter/10.1007/BFb0014352
oh totally
Karl Palmskog (Nov 15 2022 at 16:20):I think there has been plenty of successful UI research in terms of papers, but very little remains in executable form
Emilio Jesús Gallego Arias (Nov 15 2022 at 17:14):Yes, maintenance is pretty hard and the main worry, often having a very strict coding style drives away contributors, but we got already 7 years experience maintaining jsCoq so I'm positive we can help people to integrate stuff like this easily.
Emilio Jesús Gallego Arias (Nov 15 2022 at 17:15):Main problem UI face in Coq is Coq itself in terms of lack of proper architecting and tech debt, hopefully we can improve on that, tho with the new coq-lsp we are able to isolate UI developers from most of the pain of it, also jsCoq being in NPM is very very good, and the new branch having a start of types / interfaces, the UI developer experience is IMHO much better than it used to be.
Last updated: Oct 13 2024 at 01:02 UTC