Email Gateway (Oct 02 2023 at 20:16): Email Gateway (Oct 02 2023 at 20:16):From: David Fuenmayor <davfuenmayor@gmail.com>
I am a big fan of Isabelle's PIDE and think it was a very smart move to
adopt the notebook-like paradigm for an ITP back in the day (long before
everyone started buzzing about Jupyter notebooks!). However, I feel that
Isabelle has been lagging behind in terms of usability in recent years. Not
only has the bar been raised a lot when it comes to UX and documentation
(interactive tutorials and the like), but notebooks have also been evolving
towards enabling real-time collaborative work (e.g., think of LaTeX before
vs. after Overleaf).
For example, the lack of a web interface for Isabelle is a big pain point
for me, particularly because it has seriously hindered my Isabelle
'proselytising' activities. I've had to turn down offers to introduce
Isabelle to large classrooms simply because I know I will end up spending
most of the time troubleshooting installation problems (from my experience,
at least 5 different sources of trouble for a small 20-person room).
Admittedly, most problems are not Isabelle's, but rather the user's fault
(myriad issues ranging from not enough disk space to overprotective
OS/antivirus). Nonetheless, the deterring effect is the same.
I find it very useful to have a web interface (even if self-hosted) to
showcase Isabelle formalization work for people to quickly review and adapt
(it is difficult to convince people to install desktop software these
days!). On a more ambitious note, I believe that a real-time collaborative
notebook-like ITP could really be a game-changer in maths and logic
teaching (we have tried this for programming using Livebook
<https://livebook.dev/> with good results).
I was under the (false?) impression that work on the VSCode extension was a
step towards bringing Isabelle to the web. Is this something on the
roadmap? If so, I would be glad to contribute what I can to make this
happen.
David
Email Gateway (Oct 04 2023 at 15:11):From: Makarius <makarius@sketis.net>
On 10/2/23 22:15, David Fuenmayor wrote:
For example, the lack of a web interface for Isabelle is a big pain
point for me, particularly because it has seriously hindered my Isabelle
'proselytising' activities. I've had to turn down offers to introduce
Isabelle to large classrooms simply because I know I will end up
spending most of the time troubleshooting installation problems (from my
experience, at least 5 different sources of trouble for a small
20-person room). Admittedly, most problems are not Isabelle's, but
rather the user's fault (myriad issues ranging from not enough disk
space to overprotective OS/antivirus). Nonetheless, the deterring effect
is the same.
Thanks for the experience report on user exposure. Can you say a bit
more about the target audience? Are people more from Mathematics
background (i.e. weak Windows machine with little memory) or
Computer-Science (i.e. strong Linux or macOS system)?
Over the decades we did foster a bias to the ancient notion of
"engineering workstation", although that now means MacBook Pro Apple
Silicon M2 instead of Sun Sparcstation 10 or 20.
I find it very useful to have a web interface (even if self-hosted) to
showcase Isabelle formalization work for people to quickly review and
adapt (it is difficult to convince people to install desktop software
these days!). On a more ambitious note, I believe that a real-time
collaborative notebook-like ITP could really be a game-changer in maths
and logic teaching (we have tried this for programming using Livebook
<https://livebook.dev/> with good results).
I will look more closely at https://livebook.dev later --- presently I
am on a conference.
Generally note that fundamental changes of the Prover IDE will require
substantial work and lots of work.
I was under the (false?) impression that work on the VSCode extension
was a step towards bringing Isabelle to the web. Is this something on
the roadmap? If so, I would be glad to contribute what I can to make
this happen.
VSCode is an Electron application. The idea of the Electron platform is
to bring typical web technologies to the desktop (HTML/SVG/CSS, Node.js,
Chromium).
So that is a move of the web onto the desktop, not of a desktop
application into the web.
Makarius
Email Gateway (Oct 05 2023 at 10:48):From: David Fuenmayor <davfuenmayor@gmail.com>
Thanks for the experience report on user exposure. Can you say a bit
more about the target audience? Are people more from Mathematics
background (i.e. weak Windows machine with little memory) or
Computer-Science (i.e. strong Linux or macOS system)?
I have had everything in my audience. Although maybe people working in
modal/non-classical logics tend to align with the former stereotype you
mention.
Early undergrad's computers are remarkably heterogeneous!
VSCode is an Electron application. The idea of the Electron platform is
to bring typical web technologies to the desktop (HTML/SVG/CSS, Node.js,
Chromium).
I see. Maybe I am being overspeculative here, since I have no clue how PIDE
is built.
When I first learnt of the VSCode extension, I immediately thought of the
possibility of a Monaco-based web editor (+LSP, etc) for a 'light' subset
of Isabelle's functionalities (enough to motivate people to install the
real thing for big game).
Maybe what I need is already covered in VSCode with the CodeServer
<https://vscode.dev/> and/or LiveShare
<https://code.visualstudio.com/learn/collaboration/live-share>
functionalities (assuming the current Isabelle VSCode distribution plays
well with that).
In my experience the current VSCode PIDE still has many rough corners.
Functionalities like semantic highlighting are too brittle and break
easily, bold symbols (and sometimes sub/superscripts) are not rendered,
etc. I am looking forward to the next developments and improvements on this
front.
David
Email Gateway (Oct 05 2023 at 11:04):From: Lawrence Paulson <lp15@cam.ac.uk>
Fun fact: when I first used the ARPANET in the 1970s, one of its advertised purposes was to allow you to run software on someone else’s computer. I wanted to use Macsyma
https://en.wikipedia.org/wiki/Macsyma
and to do that, you had to log into MIT’s Incompatible Timesharing System. That worked fine, only at 110 baud (bits/sec). A shame we cannot do that with today’s high-speed networks and a dedicated processor somewhere.
On the other hand, Isabelle really is trivial to install. I wish people understood that.
Larry Paulson
Email Gateway (Oct 05 2023 at 18:41):From: Makarius <makarius@sketis.net>
On 10/5/23 13:03, Lawrence Paulson wrote:
Fun fact: when I first used the ARPANET in the 1970s, one of its advertised purposes was to allow you to run software on someone else’s computer. I wanted to use Macsyma
https://en.wikipedia.org/wiki/Macsyma
and to do that, you had to log into MIT’s Incompatible Timesharing System. That worked fine, only at 110 baud (bits/sec). A shame we cannot do that with today’s high-speed networks and a dedicated processor somewhere.
Indeed. Maybe you know the saying by the famous philosopher Karl
Valentin from Munich: "In the good old times, even the future looked
brighter!"
On the other hand, Isabelle really is trivial to install. I wish people understood that.
I do agree, and usually aim at exactly that.
But we do have certain cultural assumptions, e.g. some basic
understanding that hard work needs decent hardware resources.
Makarius
Email Gateway (Oct 06 2023 at 03:32):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
You can run VS Code over the web in a browser using code-server, which I
believe was open-sourced by Microsoft in 2021. Full IDE in your browser,
works essentially the same as the desktop app. Before VSCodium was bundled
with Isabelle, when the Isabelle VSCode plugin was standalone and available
in the marketplace, I played around with using Isabelle on an HPC cluster
via code-server. Had code-server/Isabelle running on a compute node in the
cluster, and connected with my browser through a ssh tunnel. It worked
surprisingly well.
Email Gateway (Oct 12 2023 at 12:45):From: Makarius <makarius@sketis.net>
On 05/10/2023 12:48, David Fuenmayor wrote:
Maybe what I need is already covered in VSCode with the CodeServer
<https://vscode.dev/> and/or LiveShare
<https://code.visualstudio.com/learn/collaboration/live-share> functionalities
(assuming the current Isabelle VSCode distribution plays well with that).
I need to look more closely at these projects, they definitely look interesting.
Searching the web for < 5min, I've also found
https://github.com/coder/code-server and its producer https://coder.com --- Or
is that the same as https://vscode.dev ?
In my experience the current VSCode PIDE still has many rough corners.
Functionalities like semantic highlighting are too brittle and break easily,
bold symbols (and sometimes sub/superscripts) are not rendered, etc. I am
looking forward to the next developments and improvements on this front.
Well, Isabelle/VSCode it is all still experimental. There is a difference in a
proof-of-concept and a full-scale working environment.
(Maybe I should stop pointing that out, and instead get things moving forward
again.)
Makarius
Last updated: Apr 28 2024 at 20:16 UTC