Lean4 on VS Code and Remote-Containers

Stream: new members

[Stefano Rando]

Hi everyone

I would like to use a Docker image to work on Lean4 together with the Remote-Containers extension of VS Code.

However, everything I have tried so far proved ineffective. One main problem that I have is that the lean4 extension does not seem to work well inside a container development environment.

Has anyone managed to do it? If so, could you please show me how? (Like sharing a Dockerfile or a devcontainer directory).

Thank you all in advance!

[Arthur Paulino]

What's the issue you're facing with the extension in the container?