lean3 and lean4 within the same git repository

Stream: lean4

[Eric Wieser]

Is it possible to put lean3 and lean4 code within the same git repository? I don't need them to interact with each other, I just want to be able to present them side-by-side.

I tried this at https://github.com/eric-wieser/lean-multiple-inheritance, but when I open it with vscode (say, through gitpod), I can't seem to get the Lean4 extension to work unless I deactivate the Lean3 one

[Kevin Buzzard]

How is this set-up any different to the lean-projects directory on my computer which contains some lean 3 projects and some lean 4 projects? Are you opening the lean3 and lean4 directories in two different VS Code instances, or trying to do something else?

[Eric Wieser]

Perhaps the problem is I'd like to open them both within the same vscode instance.

[Gabriel Ebner]

Yes, a single vscode window cannot run both the Lean 3 and Lean 4 extensions at the same time.

[Filippo A. E. Nuccio]

Not directly related, but sometimes VSCode gets confused and opens lean3 files as lean4 ones (and then complains a lot). What I typically do is to temporary disable the lean4extension, and then everything is OK again. Does this happen to someone else, is there a way to avoid this VSCode confusion?