search

leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

Installation instructions incomplete #102

Open dsb-y opened 10 months ago

dsb-y commented 10 months ago

Possibly having a reminder in the installation instructions to add /*/lean4/build/release/stage1/bin to your path in your .bashrc could be helpful.

Kha commented 10 months ago

Hi, could you elaborate on which instructions you are talking about? There shouldn't be anything on leanprover.github.io that leads you to a development build.

dsb-y commented 10 months ago

Oh you're right I suppose it's not wise to choose that option. The instructions I was talking about were https://leanprover.github.io/lean4/doc/make/index.html It does say that the binaries go into the stage1 subfolder and it was probably considered obvious that they must be added to the path. On a different note, people that are looking for a theorem prover to download and study and like to use vim as their editor might turn away from lean with the understanding that only emacs and vscode are supported since it is not advertised that there is support for vim with the lean.vim plugin. Specifically it's omitted on downloads page https://leanprover.github.io/download/