Enable PR (Gitlab CI) Checks for PR from forks

[antoniivanov]

What is the feature request? What problem does it solve?
When you open a PR from a fork, our Gitlab CI does not trigger. This is because the Gitlab CI/CD mirroring does not handle forks on GitHub SCM
https://gitlab.com/gitlab-org/gitlab/-/issues/5667

This makes it harder for any external contributors to merge and test. So far I've been merging manually any such contributions.

Suggested solution

Trigger Gitlab CI from Github Actions instead using something like https://github.com/marketplace/actions/trigger-gitlab-ci

[antoniivanov]

This looks interesting as potential implementation as well: https://github.com/coq/bot

[sabadzhiev]

Triaged. Closed as stale.

Will be revisit in the future, once we have external contributors, that are not maintainers in the project.

[antoniivanov]

This might be helpful https://github.com/marketplace/actions/trigger-gitlab-ci-through-webhooks