host 32-bit VM at digitalocean.com, build lean.js regularly

[soonhokong]

The build process is automated. The instructions are available at https://github.com/soonhokong/build.lean.js

[soonhokong]

https://leanprover.com is on

• 32-bit VM is running (512MB, 1 Core, 20GB SSD, 1TB traffic) to build lean.js. ($5/month, 20-month free, thanks to digitalocean)
• lean.js is hosted at http://leanprover.com/lean.js which can be linked from anywhere (i.e. github pages).
• Domain name is linked.
• SSL certificate is purchased. ($9/year, one year for free, thanks to namecheap.com)

[leodemoura]

The plan is to host the lean.js source code at github (like we discussed yesterday), right? BTW, we also have leanprover.net (which we never update).

The build process and scripts for lean.js should also be stored in the leanprover github. I think we should be able to easily setup new build machines easily by simply cloning the repository. We should not depend on digitalocean.

We should integrate the whole process.

• github.com/leanprover/build.lean.js repository (for build scripts) and javascript source code to glue ACE editor and Lean.
• github.com/leanprover/lean.js repository (for compiled javascript) we perform destructive updates to save space
• github.com/leanprover/leanprover.github.io (official lean page) it links to github.com/leanprover/lean.js for live demos and tutorials

BTW, we need simple instructions for how to setup a server machine to update github.com/leanprover/lean.js when lean is updated.

[soonhokong]

Hi Leo,

Yes, that's the plan. I just needed to have a VM to run build.lean.js and tested it how much we can go with it. Here is the plan (almost the same as you described):

• Host ace-editor and compiled javascript at leanprover org
  • [x] source: leanprover/ace/master
  • [x] javascript: leanprover/ace/gh-pages, generated via travis-ci.
• Host build instruction for lean.js and compiled lean.js at leanprover org
  • [x] instructions: leanprover/lean.js/master
  • [x] javascript: leanprover/lean.js/gh-pages, generated via a VM.
• Host source code of live demo and tutorial at leanprover org
  • [x] source code: leanprover/leanprover.github.io/master

[soonhokong]

http://leanprover.github.com/live is up.

[leodemoura]

It seems Dropbox needs to be notified whenever the website moves. I get the following error when I try to access my account

Error (400)
It seems the app you were using submitted a bad request. If you would like to report this error to the app's developer, include the information below.

More details for developers

Invalid redirect_uri: u'http://leanprover.github.io/live/'. It must exactly match one of the redirect URIs you've pre-configured for your app (including the path)

[soonhokong]

For the record:

• Dropbox only supports https, not http.
• github pages do not allow us to use .htaccess trick to automatically redirect visitors to our https page.
• I'll disable dropbox feature if users visit the page with http protocol. #15
• There are some javascript tricks for redirecting. Let me dig what we can do with them.