Guinea pigs wanted!

Stream: Lean Together 2019

[Gabriel Ebner]

Due to popular demand, I hacked up something in the vscode extension. Interested victims can now build the git version of the extension and try out ctrl+shift+p "open documentation view" and then try "try it!".

[Bryan Gin-ge Chen]

This is cool! I did miss having a button or command to navigate "back" in the history of the documentation viewer. Adding that might involve having to write a history feature, though. An alternative might be just to add links at the top of the webview to the manual and TPIL and to somehow change the CSS so that the section navigation sidebar is more accessible, since for me the editor width is usually narrow enough that I have to scroll to the bottom to see it.

[Patrick Massot]

When I launch the debugger mode to use this new feature it tells me "Activating extension 'jroesch.lean' failed: Cannot find module 'axios'."

[Patrick Massot]

Oh, I forgot to npm install, sorry about the noise

[Patrick Massot]

It is awesome :open_mouth:

[Patrick Massot]

I agree with Bryan that it would be even better with a navigation history. But more importantly it would be much better if the hardcoded list of books could be extended by typing in urls. This way Kevin (who is already using Sphynx) could tell people to try his url. It would be also very nice to allow using a local download so that we can continue learning Lean offline

[Patrick Massot]

For people who didn't follow the story, I should add that this feature is something I've requested on the bus this morning around 8:45. Then Gabriel attended the documentation discussion sessions between 9 and 10:30, when I requested it again, and was seconded by popular clamor. And this was added to the VScode extension at 13:59. That's how efficient Gabriel is.

[Mario Carneiro]

Can someone say what the feature does?

[Patrick Massot]

It open either TPIL or the reference manual in VScode, as you would see it online. But when you click the little "Try it!" links it opens the Lean file in VScode which then uses your local install of Lean instead of the javascript one!

[Patrick Massot]

@Gabriel Ebner if you need more guinea pigs then I guess you should ask on the general stream