feat!: Set up gitpod IDE - a browser-based/zero-install VSCode clone - #591

lemmy · 2020-04-11T00:02:19Z

Set up gitpod IDE - a browser-based/zero-install VSCode clone - for the Dafny online tutorial.

Try it out yourself at https://gitpod.io/#https://github.com/dafny-lang/dafny/

Screencast/demo at https://tla.msr-inria.inria.fr/kuppe/gitpod-dafny.mp4

rise4fun has reached its lifetime and capacity (TLA has started to use a similar setup for its examples: https://github.com/tlaplus/Examples/blob/master/README.md)

for the Dafny online tutorial.

lemmy · 2020-04-11T23:36:28Z

If the image statement in .gitpod.yml is changed from:

image:
  file: .gitpod.dockerfile

to:

image: lemmster/gitpod-dafny:latest

the initial time to spin up the instances is reduced from a few minutes to 20-30 seconds. However, it adds an additional dependency (to my custom docker image).

robin-aws · 2020-04-13T18:24:58Z

#594 should fix the SSL-related build failure once it's merged

robin-aws

This is an awesome approach! I love being able to leverage the VS Code plugin for this.

A few top-level suggestions:

Can we add the "Ready to Code" link to the readme as gitpod suggests too? [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-Ready--to--Code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/dafny-lang/dafny)
It would be good to address a couple additional gaps between what's in the repo and whats on rise4fun.com as well (this could be in a follow-up PR though):
- https://rise4fun.com/Dafny/tutorial/Guide has links at the bottom to the additional tutorial files (Lemmas.md etc.)
- https://rise4fun.com/Dafny has several nice, simple Dafny samples linked in the bottom left corner (e.g. Hello.dfy) which would be good to include
It's unfortunate that the gitpod preview window doesn't highlight Dafny code correctly, but that's something I happen to be investigating right now anyway. :)

robin-aws · 2020-04-13T18:41:17Z

.gitpod.yml

+ - command: gp open Docs/OnlineTutorial/guide.md
+ - command: gp open Docs/OnlineTutorial/guide.dfy


This is a good start, but can we go a little further and open the guide.md preview automatically as well? Ideally I'd love for the initial state to be guide.dfy on the left and the preview on the right.

I pinged the authors of gitpod and they say neither is currently supported.

That's too bad. I would suggest we add some instructions at the top of guide.dfy for opening the preview then.

Alternatively, we could render the content with a markdown engine that supports Dafny syntax (I'm about to add a KDE syntax definition which pandoc can use) and commit the result, just as we do for the Dafny reference.

robin-aws · 2020-04-13T18:45:44Z

.gitpod.yml

@@ -0,0 +1,11 @@
+image: lemmster/gitpod-dafny:latest


Let's just use the dockerfile for now as you suggested, to avoid the dependency. I'm assuming you only have to wait for the instance spin-up the first time you open a repo in gitpod?

I'd assume they have clever caching for all users, but I actually don't know. Here is what I did to create the image:

sudo apt install docker.io ## login with your docker hub credentials. docker login ## in the local git repository: docker build -t lemmster/gitpod-dafny -f .gitpod.dockerfile . ## Publish on docker hub. docker push lemmster/gitpod-dafny

In other words, you could create your own pre-build image.

Cool - I'd be happy to consider maintaining such an image under the dafny-lang umbrella in the future. Are you comfortable with deferring that for now?

robin-aws · 2020-04-13T18:46:01Z

.gitpod.yml

+
+vscode:
+ extensions:
+ - [email protected]:y0vNEkuQw4SUFvPIFxLkEA==


Do you know what the ID after the colon is for?

With gitpod one has to manually install extension by:

a) Manually download VSCode extension from https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode
b) Spin-up a gitpod instance
c) Manually install correctnessLab.dafny-vscode-0.17.1.vsix in gitpod
d) .gitpod.yml is modified and lists new extension

Fair enough, I read up on the docs and this looks standard, I was just curious.

robin-aws · 2020-04-13T19:07:25Z

One further thought: it might make sense to move the tutorial and samples to a separate repository, just as TLA+ has done. It may be somewhat confusing to assume that someone loading the Dafny repo itself in gitpod is intending to use the tutorial rather than develop Dafny itself.

lemmy · 2020-04-13T19:27:57Z

One further thought: it might make sense to move the tutorial and samples to a separate repository, just as TLA+ has done. It may be somewhat confusing to assume that someone loading the Dafny repo itself in gitpod is intending to use the tutorial rather than develop Dafny itself.

Please have a look at https://github.com/lemmy/dafny-sort/

lemmy · 2020-04-13T19:30:22Z

This is an awesome approach! I love being able to leverage the VS Code plugin for this.

A few top-level suggestions:

* Can we add the "Ready to Code" link to the readme as gitpod suggests too? `[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-Ready--to--Code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/dafny-lang/dafny)`

* It would be good to address a couple additional gaps between what's in the repo and whats on rise4fun.com as well (this could be in a follow-up PR though):
  
  * https://rise4fun.com/Dafny/tutorial/Guide has links at the bottom to the additional tutorial files (Lemmas.md etc.)
  * https://rise4fun.com/Dafny has several nice, simple Dafny samples linked in the bottom left corner (e.g. Hello.dfy) which would be good to include

* It's unfortunate that the gitpod preview window doesn't highlight Dafny code correctly, but that's something I happen to be investigating right now anyway. :)

For gitpod, it might make more sense to convert the markdown guide into a single or set of .dfy files => No need to copy snippets from markdown.

robin-aws

Shoot, just realized I never hit the submit button on this.

For gitpod, it might make more sense to convert the markdown guide into a single or set of .dfy files => No need to copy snippets from markdown.

I think these end up being different beasts, though - a markdown guide can narrate things selectively, out of order, etc. A source file with lots of comments can't do that.

robin-aws · 2020-04-14T16:19:12Z

.gitpod.yml

@@ -0,0 +1,11 @@
+image: lemmster/gitpod-dafny:latest


Cool - I'd be happy to consider maintaining such an image under the dafny-lang umbrella in the future. Are you comfortable with deferring that for now?

robin-aws · 2020-04-14T16:19:30Z

.gitpod.yml

+
+vscode:
+ extensions:
+ - [email protected]:y0vNEkuQw4SUFvPIFxLkEA==


Fair enough, I read up on the docs and this looks standard, I was just curious.

robin-aws · 2020-04-14T16:21:38Z

.gitpod.yml

+ - command: gp open Docs/OnlineTutorial/guide.md
+ - command: gp open Docs/OnlineTutorial/guide.dfy


That's too bad. I would suggest we add some instructions at the top of guide.dfy for opening the preview then.

Alternatively, we could render the content with a markdown engine that supports Dafny syntax (I'm about to add a KDE syntax definition which pandoc can use) and commit the result, just as we do for the Dafny reference.

lemmy · 2020-04-28T23:37:59Z

@robin-aws May I assume that you are going to put on the finishing touches that you mention above?

robin-aws · 2020-04-29T17:20:20Z

@robin-aws May I assume that you are going to put on the finishing touches that you mention above?

I'm not sure when we'll have the time to in the immediate future, to be honest, but I'm willing in theory.

We're also still thinking about the best way to host the tutorial, so we may let this sit for a little while longer just to make sure the experience is optimal for new users/contributors to Dafny.

parno · 2020-09-21T15:33:50Z

This seems like a cool idea! I'd love to use something like this in my classes.

FWIW, when I try running the GitPod (https://gitpod.io/#https://github.com/dafny-lang/dafny/), it looks like it's setup to work on the Dafny project, but when I open a Dafny file (e.g., myfile.dfy), it seems like the Dafny extension is not installed; it doesn't prompt me to install the Dafny extension, and when I search for extensions via VS Code, it doesn't find any.

lemmy · 2020-09-21T16:37:08Z

This seems like a cool idea! I'd love to use something like this in my classes.

FWIW, when I try running the GitPod (https://gitpod.io/#https://github.com/dafny-lang/dafny/), it looks like it's setup to work on the Dafny project, but when I open a Dafny file (e.g., myfile.dfy), it seems like the Dafny extension is not installed; it doesn't prompt me to install the Dafny extension, and when I search for extensions via VS Code, it doesn't find any.

The link only works with this PR merged (it is not). If you want to toy with Dafny on Gitpod, you can try https://gitpod.io/#https://github.com/lemmy/dafny-sort/

In the long run, Github codespaces are, perhaps, be the better infrastructure to build all of this on.

parno · 2020-09-21T21:05:17Z

Ah, okay, thanks that makes sense. I didn't look carefully enough at the URLs.

lemmy · 2021-01-27T01:46:53Z

Is there still interest in this PR?

robin-aws · 2021-01-27T23:33:14Z

Hi lemmy! I agreed with your point about codespaces being potentially a better option, and I've been trying to find time to evaluate that before investing any more here. Since codespaces isn't generally available yet there's still a possibility this is the right call.

Let's keep this open for a bit longer at least while I investigate.

robin-aws · 2021-02-03T01:07:46Z

@lemmy: I followed your TLA link to look at how they hooked gitpod up, but I don't see any evidence of it there any more: https://github.com/tlaplus/Examples/blob/master/README.md

Am I missing something or was the integration removed?

lemmy · 2021-02-03T17:54:17Z

@lemmy: I followed your TLA link to look at how they hooked gitpod up, but I don't see any evidence of it there any more: https://github.com/tlaplus/Examples/blob/master/README.md

Am I missing something or was the integration removed?

I haven't gotten around to adding it for all examples. It's only on for one of them: https://gitpod.io/#https://github.com/lemmy/BlockingQueue/blob/master/BlockingQueue.tla

The config is at https://github.com/lemmy/BlockingQueue/blob/master/.gitpod.yml

ghuntley · 2022-03-10T00:14:18Z

👋 from Gitpod. I've added all of the folks in the dafny-lang GitHub organization as pre-qualified for automatic plan upgrades as part of our open-source program which provides unlimited compute. Let me know if you have any questions or need any help.

https://www.gitpod.io/blog/gitpod-for-opensource

parno · 2022-03-20T00:36:11Z

In light of the comment above re: free Gitpod, and given that GitHub Codespaces have been out for a while now, should we try to pick one for hosting (a) A version of the interactive Dafny tutorial, and/or (b) a setup for people wanting to help develop Dafny? The old Rise4Fun was a useful resource to point newcomers at as a zero-effort way to trying out Dafny.

cpitclaudel · 2022-03-20T02:47:18Z

That would be very nice. In the long run, though, I would like to do something a bit more ambitious for the Dafny tutorial (something like Alectryon or fslit).

cpitclaudel · 2022-03-20T02:48:36Z

(I'm not sure whether it's a one-time thing or whether it's like that every time but I tried opening the GitPod link above and "pulling the container image" takes a very long time — compare with the experience of loading up F* + Z3 in https://people.csail.mit.edu/cpitcla/fstar.js/stlc.html, which is a few seconds at most)

lemmy · 2022-03-21T17:46:10Z

@cpitclaudel I assume startup takes longer with custom Docker containers. If you open, e.g., https://gitpod.io/#https://github.com/lemmy/z3_tutorial, the IDE appears within 10 seconds and is fully provisioned in under 30 seconds.
Gitpod/Codespaces cannot compete with an entirely browser-based in terms of startup time. On the other hand, you get a full-blown IDE with all the bangs and whistles.

cpitclaudel · 2022-03-21T18:08:05Z

@lemmy very nice, thanks!

lemmy · 2022-03-24T15:43:21Z

Not Gitpod, but still: Prebuild Github Codespaces (https://docs.github.com/en/codespaces/prebuilding-your-codespaces).

feat!: Set up gitpod IDE - a browser-based/zero-install VSCode clone -

a0f3041

for the Dafny online tutorial.

Use custom docker image to reduce initial spin-up time.

215221d

robin-aws requested changes Apr 13, 2020

View reviewed changes

robin-aws reviewed Apr 28, 2020

View reviewed changes

		- command: gp open Docs/OnlineTutorial/guide.md
		- command: gp open Docs/OnlineTutorial/guide.dfy

feat!: Set up gitpod IDE - a browser-based/zero-install VSCode clone - #591

Are you sure you want to change the base?

feat!: Set up gitpod IDE - a browser-based/zero-install VSCode clone - #591

Conversation

lemmy commented Apr 11, 2020 • edited Loading

lemmy commented Apr 11, 2020

robin-aws commented Apr 13, 2020

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws commented Apr 13, 2020

lemmy commented Apr 13, 2020

lemmy commented Apr 13, 2020

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lemmy commented Apr 28, 2020

robin-aws commented Apr 29, 2020

parno commented Sep 21, 2020

lemmy commented Sep 21, 2020

parno commented Sep 21, 2020

lemmy commented Jan 27, 2021

robin-aws commented Jan 27, 2021

robin-aws commented Feb 3, 2021

lemmy commented Feb 3, 2021 • edited Loading

ghuntley commented Mar 10, 2022

parno commented Mar 20, 2022

cpitclaudel commented Mar 20, 2022

cpitclaudel commented Mar 20, 2022 • edited Loading

lemmy commented Mar 21, 2022

cpitclaudel commented Mar 21, 2022

lemmy commented Mar 24, 2022

lemmy commented Apr 11, 2020 •

edited

Loading

lemmy commented Feb 3, 2021 •

edited

Loading

cpitclaudel commented Mar 20, 2022 •

edited

Loading