Zulip Chat Archive

Stream: new members

Topic: Lean4 on VS Code and Remote-Containers

Stefano Rando (Jun 23 2022 at 10:27):

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 (Jun 23 2022 at 10:47):

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

Last updated: Dec 20 2023 at 11:08 UTC