[KIP] - K Online Scratchpad/Notebooks/IDE

[ColmBhandal]

Expose an online "k-scratchpad" (or an online IDE / Notebooks environment) that one can visit within their browser and immediately start writing / compiling / running K code. There are various levels of sophistication possible. The most basic idea is just a scratchpad allowing someone to write/compile/run K code through their browser.

More advanced feature ideas:

1. The ability to save & share a scratchpad with others e.g. via a URL.
2. Online-IDE features like syntax highlighting, autocompletion etc.
3. An interactive K-Notebook for literate-programming (similar to Jupyter Notebook for Python)

Motivation

1. Drive up engagement of newcomers to the K language. Having an interactive scratchpad with zero setup cost may motivate more people to get involved in the language. In particular, Interactive Notebooks for literate programming would likely drive up engagement. More engagement means a larger active community, and that can lead to better quality/popularity of the K-framework.
2. Help existing users (even advanced ones) share interactive K examples. For example, if the online tool allowed people to create a permalink to their scratchpads (like dotnetfiddle does, as just one example), these could be shared, giving recipients instant interactive access to an idea, without having to download/compile anything.

There are similar online IDEs/scratchpads/Noteboooks/compilers for other languages e.g. to name a few:

1. For Coq there's JsCoq. This has got syntax highlighting and an interactive scratchpad, but no ability to share links to examples from what I can tell.
2. For C#, for example there's dotnetfiddle - this allows C# code to be run in the browser and also for examples to be shared with a link.
3. For Python there are many examples but probably most notably Jupyter Notebooks. These allow for a fully interactive literate programming experience without leaving your browser.
4. For Java (and many other languages) there is TutorialsPoint, which allows users to write, compile, run, save and share code examples.

There is an existing GitHub project called KWeb. It looks like this allows someone to host an online K IDE themselves, rather than providing the IDE-as-a-service, so to speak. There is an example link provided on that project but looks like it was just a POC and the link seems to be dead: http://fsl.cs.uiuc.edu/tool/.

Documentation

Here is just a small example of what some documentation might look like leading users to use interactive K Notebooks, for example:

K now supports interactive online literate programming via K-Notebooks, which allow users to simultaneously write, document, run and share K examples and projects all in the one place. Check out BLAH_URL.xyz to get started.

Then perhaps more inline documentation/examples around using K-Notebooks could be hosted at said URL.

Potential Alternatives/Work-arounds

1. For compiling and running, the workaround for this is to just compile and run K locally - as is the state of the art today.
2. For code-sharing, one can use a tool like Git for example, or create a GitHub Gist if the idea is still in a very experimental stage.
3. Also, I guess since K seems to be Dockerized here, a workaround to setting up K locally I guess would be just pull the Docker image and run it as a container. Assuming someone has Docker installed, which many do seem to these days.

[radumereuta]

We would like to do something like this eventually. It's a large task though and we're not sure when we're going to have the resources for it.

[ehildenb]

I put this back on the board as a large task. I'll look at it with @shd101wyy . We have something like this for the prover, we could look at making that a bit more flexible and allowing for any of our tools in some limited capacity.

Also, @tothtamas28 is developing the kit tool, which should be able to help with this.

[ehildenb]

We could call it "KlayGround".

[MirceaS]

Just wanted to give this a +1 from me since I would also love to see this becoming a thing!

[ColmBhandal]

Not a long-term idea or anything, but just as a POC I created a very basic pair of services that would allow someone to access K commands through their browser, via an interactive terminal:

https://github.com/ColmBhandal/kwetty

Not sure how it would work with multiple users logging in or anything. ATM it's just configured with one user people can use to log in over SSH.

Don't have it deployed anywhere, just tested it on localhost.

[ColmBhandal]

I think we should consider Jupyter Notebooks as a platform for this. Here are some advantages to such an approach:

1. Huge community - well supported.
2. Huge community - lots of exposure for K.
3. Feature rich - avoids reinvention of wheel for many things, and that effort instead reduces largely to tweaking various config settings.

To this end, I've hacked together a POC Jupyter Kernel allowing K code to be run interactively in a browser:

k_jupyter_poc

You can try this online:

Binder Demo.

There are 2 Notebooks:

• lesson-02.ipynb - Tutorial lesson 1.2 converted to an interactive notebook.
• lesson-02-soln.ipynb - the solution to said lesson.

Notes:

• I purposely have only packaged this on test PyPi and also I have suffixed the name with "poc". The intention is that this repo will be abandoned at some point and replaced with a more permanent one with a more permanent name (of course, we can always use this repo's code as a starting point).
• The POC is certainly not "feature complete" - but it has enough features to allow someone to do lesson 1.2 interactively in their browser, as demoed in Binder.

[ehildenb]

Related: #2925

[ColmBhandal]

FYI the Binder Demo was broken for a while - pip wasn't installed - I just fixed it there.

[radumereuta]

@ColmBhandal, you may be interested in this: https://marketplace.visualstudio.com/items?itemName=RuntimeVerification.k-vscode I started working on a VSCode extension that brings syntax highlighting, code suggestions, go to definition and find usages. It's still in progress, and I plan to add more features, but this could work as an IDE in the browser. GitHub allows you to view files using the VSCode browser, where you can install extensions from the Marketplace.

Note that you can't install this version online. I need to update the packaging solution.