search

sagemathinc / cocalc

CoCalc: Collaborative Calculation in the Cloud
https://CoCalc.com
Other
1.17k stars 216 forks source link

lean: make it possible to customize the leader key (the backslash) #3650

Closed williamstein closed 1 week ago

williamstein commented 5 years ago

Also I don't know if CoCalc allows to choose the leader key as the VScode extension does: https://github.com/leanprover/vscode-lean/blob/a0acab03d6a039c47679f12ca7a21ba411c54fa6/package.json#L86-L90 (remember the \ key is very inconvenient to reach on certain keyboard, eg French keyboard).

This is in reference to this code.

williamstein commented 1 week ago

I consider our lean support deprecated and see no point in fixing or maintaining it further. Instead, use vscode via a compute server or in a project.

I especially don't care about scalability issues for this old lean stuff.