documentation view

Stream: general

[Patrick Massot]

@Gabriel Ebner What happened to the documentation view feature of vscode-lean?

[Gabriel Ebner]

@Patrick Massot I'm a bit busy at the moment so there's nothing new (though it's available in the released version now). In the other thread you suggested that the documentation view should have back/forward buttons and a way to input your own url. I completely agree. (The webview api in vscode is unfortunately really, really stripped down... Not even hyperlinks work by default, we are changing them to vscode commands on the fly....)
@Edward Ayers if you want to look at this, I can give you pointers.

[Gabriel Ebner]

In case anybody has too much free time and wants to give feedback, run "ctrl+shift+p open documentation view" and post your complaints here.

[Patrick Massot]

Thanks Gabriel! Did you intend to ping Bryan instead of Ed?

[Patrick Massot]

@Jeremy Avigad Did you see that feature?

[Gabriel Ebner]

No, Ed asked me in Amsterdam to please give him work on the vscode extension. But I'm happy about contributions from all sides.

[Patrick Massot]

By the way, am I correct in thinking that this was not in the previous release? If not then please forgive me for asking today

[Gabriel Ebner]

I made a release for Ed's translations PR yesterday, that's the first release with the documentation view.

[Patrick Massot]

Weird... I did try to check before posting. Sorry

[Jeremy Avigad]

I just tried documentation view. It's great! Here are two comments.

The bigger one: once we move from the table of contents to a specific chapter, as far as I can tell it is impossible to go back to the table of contents without pressing ctrl-shift-P and choosing "open documentation view" again. That makes it less convenient to browse. I don't know the ideal solution here. Maybe the best solution is to assign a keystroke to "open documentation view", so that pressing that would return to the TOC.

The smaller issue: the natural way to play with the text and examples is to split the screen, put the text in the left, and then run the examples in the right. But even when I have a split screen, when I click on the "try it" button, the window opens on the left, and I have to manually move it to the right. Would it be possible to have the window open on the right?

[Patrick Massot]

I just tried to use the VScode Lean documentation view in our computer rooms, with no success. Could it be that it tries to access TPIL without using the system-wide proxy setup?

[Patrick Massot]

@Edward Ayers @Gabriel Ebner

[Gabriel Ebner]

Yes, I'm pretty sure it doesn't look at proxy settings.

[Patrick Massot]

Note that VScode does successfully use the proxy when downloading the Lean extension

[Patrick Massot]

Fixing this would be a nice improvement

[Edward Ayers]

Did you have to set the http.proxy in the vscode settings for the extension downloading to work?

[Gabriel Ebner]

Ideally, we could use the system proxy settings that vscode uses itself, but it looks like this is not possible yet: https://github.com/Microsoft/vscode/issues/12588

[Gabriel Ebner]

The http.proxy* settings are the older (now deprecated) way to set the proxy in vscode (and it is ignored by most of vscode). We could use this setting (but Patrick needs to set it).

[Patrick Massot]

I didn't have to set anything to get the extension

[Gabriel Ebner]

@Patrick Massot vscode has two settings for proxies: one is taken directly from the system settings and is used for extension fetching, etc. But this is unfortunately not accessible to extensions (i.e., us).

[Kevin Buzzard]

issues/12588. Wow -- and I thought we had issues.

[Kevin Buzzard]

When there are 4621 open issues, how do you get people to work on the one you want to be fixed?

[Mario Carneiro]

in big companies the issues process has to be a lot more formal. There is triage and tagging, periodic review of priorities, and work is often aimed for milestones. Quite often the issues system is the force behind all work - i.e. if you want to change something you should make an issue first, so that the intent is logged and prioritized

[Mario Carneiro]

so you have people working on the most important things and other people adding and organizing new issues

[Mario Carneiro]

For a big github project, you can vote on your favorite issues by adding a thumbs up reaction to it; this sometimes helps, depending on the team, but it's just a suggestion

[Mario Carneiro]

apparently people really want floating windows https://github.com/Microsoft/vscode/issues?q=is%3Aopen+is%3Aissue+sort%3Areactions-%2B1-desc