-
Notifications
You must be signed in to change notification settings - Fork 11
fix(entrypoint): clone into dev home for tilde TARGET_DIR (empty app folder) #414
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
skulidropek
merged 6 commits into
ProverCoderAI:main
from
konard:issue-413-cb2a359e0ffa
Jun 17, 2026
Merged
Changes from all commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
5918c68
Initial commit with task details
konard 3c64fdb
chore(release): version packages
github-actions[bot] 2e66e2e
fix(entrypoint): expand tilde TARGET_DIR against dev home, not root $…
konard 62e4916
Merge main into issue-413-cb2a359e0ffa
konard 75a43f5
Revert "Initial commit with task details"
konard 6e2e0bf
Merge main into issue-413: port tilde TARGET_DIR fix into packages/co…
skulidropek File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| --- | ||
| "@prover-coder-ai/docker-git": patch | ||
| --- | ||
|
|
||
| Fix `docker-git clone` leaving the workspace `app` folder empty when `TARGET_DIR` | ||
| is a tilde path. | ||
|
|
||
| The generated entrypoint runs as `root` (sshd), so `$HOME` resolves to `/root`. | ||
| When a `~`/`~/...` `TARGET_DIR` reached the entrypoint (e.g. via the `TARGET_DIR` | ||
| env override), it was expanded against `$HOME`, resolving to `/root/app`. Because | ||
| the auto-clone runs as `su - <sshUser>`, cloning into the root-owned `/root/app` | ||
| failed with "permission denied", so the repository never landed in the prepared | ||
| home and the workspace `app` folder stayed empty. The tilde is now expanded | ||
| against the unprivileged user's home `/home/<sshUser>`, so the clone always lands | ||
| in the dev-owned workspace. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Исправление корректно решает проблему раскрытия тильды, но отсутствует документация согласно coding guidelines.
Техническое изменение верно: когда entrypoint запускается от root (через sshd), переменная
$HOMEуказывает на/root, что приводило к проблеме с правами доступа приgit clone. Явное указание/home/${config.sshUser}гарантирует, что пути с тильдой раскрываются в домашнюю директорию SSH пользователя, где у него есть права на запись.Однако согласно coding guidelines, код должен содержать функциональные комментарии для документирования изменения:
As per coding guidelines, all changes must include CHANGE/WHY/QUOTE/REF/SOURCE/FORMAT THEOREM markers for traceability and formal reasoning.
🤖 Prompt for AI Agents
Source: Coding guidelines