hakarlsson/hol4 repository overview

⁠HOL4 ITP

This is a container with the HOL4 Interactive Theorem Prover. Used as the base image for hakarlsson/hol4-devcontainer, and for HOL4 CI/CD pipelining.

⁠Key Features:

• Ready-to-use HOL4: Includes a complete, pre-built installation of the HOL4 ITP.
• 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.

⁠Example usage for CI/CD

Add the following to .github/workflow/build.yml:

name: CI Build 

on: 
  schedule:
    - cron: "0 3 * * 0"
  push:
    branches: [ '**' ]

jobs:
  build:
    name: Build
    runs-on: ubuntu-latest
    container:
      image: hakarlsson/hol4:latest
    steps:
      - name: Checkout code
        uses: actions/checkout@v4
      - name: Build theory
        timeout-minutes: 5
        run: Holmake

⁠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.