hakarlsson/hol4-devcontainer repository overview

⁠HOL4 ITP Dev Container (Rootless)

This is a specialized development container for the HOL4 Interactive Theorem Prover. It is designed specifically for Rootless Docker installations using VS Code.

⁠Key Features:

• Ready-to-use HOL4: Includes a complete, pre-built installation of the HOL4 ITP.
• VS Code Extension: Bundles the hol4-vscode extension for VS Code.
• Rootless Compatibility: Configured to run as the root user within the container. When used with Rootless Docker, this ensures all generated files and build artifacts automatically map to your host user’s UID/GID, eliminating permission conflicts.

⁠Quick Start

1. Requirements: Install VS Code, the VS Code Dev Containers extension, and rootless Docker.
2. Devcontainer Configuration: Use the following snippet in your VS Code project's .devcontainer/devcontainer.json:

   {
     "name": "HOL4 Development",
     "image": "hakarlsson/hol4-devcontainer"
   }
   

   Copy
3. Launch: Open your folder in VS Code and run "Dev Containers: Reopen in Container" from the Command Palette.

⁠Technical Notes

• User Mapping: This container utilizes the root user to leverage Docker's rootless namespace mapping. This allows you to edit files on your host and run the prover in the container without chown or permission errors.
• Container Environment Variables:
  • HOLDIR is set to /HOL for compatibility with the hol4-vscode extension.
  • /HOL/bin is added to the PATH for immediate access to hol and Holmake in the terminal.