Skip to content

Fixing bug with different HOST_DIRECTORY#2315

Open
Didayolo wants to merge 2 commits intodevelopfrom
fix-host-path
Open

Fixing bug with different HOST_DIRECTORY#2315
Didayolo wants to merge 2 commits intodevelopfrom
fix-host-path

Conversation

@Didayolo
Copy link
Copy Markdown
Member

@Didayolo Didayolo commented Apr 2, 2026

Original PR from @jbehley: #2311

Description

This is again a pull request with the (only) necessary changes to allow a different HOST_DIRECTORY`.

In our setup, we want to have a different HOST_DIRECTORY than /codabench. Note that the problem does not occur if the directory on host and inside the container are /codabench.

Let's say we have HOST_DIRECTORY = /home/codabench/ and the desired directory is /codabench/data/temp/. Then makedirs will try to create /home/codabench/data/temp inside the container, which leads to an error.

Btw, we run the worker with podman and with the change it runs now since quite some time with over 350 submissions.

Checklist

  • Code review by me
  • Hand tested by me
  • I'm proud of my work
  • Code review by reviewer
  • Hand tested by reviewer
  • CircleCi tests are passing
  • Ready to merge

@Didayolo
Copy link
Copy Markdown
Member Author

Didayolo commented Apr 2, 2026

CircleCI tests are passing.

Doubts to check:

Having first the directory creation:

        # Create if necessary
        os.makedirs(path, exist_ok=True)

And then the path concatenation:

        path = os.path.join(HOST_DIRECTORY, path)
        return path

It means that the path returned by the function is not the path passed to makedirs. It looks like we have then no guarantee that the directory exists. I may need to check it out more in depth I feel like this could introduce a bug.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants