Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

added open with codeanywhere badge to README file #1

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

added open with codeanywhere badge to README file #1

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,15 @@ You can temporarily play with Lean using Github codespaces. This requires a Gith

* Make sure the Machine type is `4-core`, and then press `Create codespace`
* After 1-2 minutes you see a VSCode window in your browser. However, it is still busily downloading mathlib in the background, so give it another few minutes (5 to be safe) and then open a `.lean` file to start.
## Using Codeanywhere

You can also use Codeanywhere to work on this project. This requires a Codeanywhere account, and you can only use it for a limited amount of time each month. If you are signed in to Codeanywhere, click here:

[![Open in Codeanywhere](https://codeanywhere.com/img/open-in-codeanywhere-btn.svg)](https://app.codeanywhere.com/#https://github.com/fpvandoorn/LeanCourse23)

This creates a virtual machine in the cloud, and installs Lean and Mathlib. It then presents you with a VS Code window, running in a virtual copy of the repository. You can update the repository by opening a terminal in the browser and typing `git pull` followed by `lake exe cache get!` as above.

Codeanywhere gives you 50 free hours every month. When you are done working, choose `Stop workspace` from the menu on the left. The workspace should also stop automatically 30 minutes after the last interaction or 3 minutes after closing the tab.

### Using Gitpod

Expand Down