Wolfgang Jeltsch (Sep 21 2021 at 12:07): Wolfgang Jeltsch (Sep 21 2021 at 12:07):Is there anybody here who has successfully used Makarius’s Isabelle Docker image with GitHub actions, for example, to perform automatic builds? I thought it should be as easy as setting up a simple GitHub workflow that employs this Docker image for the actual building, but apparently this is not so.
The concrete problem I’m experiencing is that downloading the current commit from the repository via actions/checkout@v2 runs into a permission problem. A minimal example of a workflow that shows this problem is as follows:
name: Automated checkout
on: [push]
jobs:
checkout:
runs-on: ubuntu-latest
container: makarius/isabelle
steps:
- name: Check out repository
uses: actions/checkout@v2
The error I get is this one:
EACCES: permission denied, open '/__w/⟨repository-name⟩/⟨repository-name⟩/⟨uuid⟩.tar.gz'
A more elaborate problem description is at https://github.com/actions/checkout/issues/587.
Wolfgang Jeltsch (Sep 24 2021 at 17:32):The problem turned out to be that the entry point of the official Isabelle Docker image doesn’t have root privileges. Deriving an image from it that adds USER root fixes this problem.
Notification Bot (Sep 24 2021 at 17:32):Wolfgang Jeltsch has marked this topic as resolved.
Jan van Brügge (Sep 25 2021 at 10:41):Just FYI, this is how I run isabelle in CI: https://github.com/jvanbruegge/isabelle-lambda-calculus/blob/master/.github/workflows/ci.yml
It uses this dockerfile to prebuild the Nominal2 session: https://github.com/jvanbruegge/isabelle-lambda-calculus/blob/master/Dockerfile
Wolfgang Jeltsch (Sep 28 2021 at 16:57):Oh, so much Docker stuff I don’t understand!
My aim was to rely only on standard Docker images, in order to not be too much dependent on other people’s work, which might be abandoned in the future.
Last updated: Dec 21 2024 at 12:33 UTC