fix provers detection in presence of paths that need escaping
Paths with spaces in particular will currently make prover autodetection fail: query_prover_version
fails to properly quote file paths when constructing the shell command.
This patch thus uses Filename.quote
to quote file paths.
Merge request reports
Activity
added 1 commit
- bc114ce8 - fix provers detection in presence of paths that need escaping
413 413 let cmd_regexp = Re.Str.regexp "%\\([.]?.\\)" in 414 414 let replace s = match Re.Str.matched_group 1 s with 415 415 | "%" -> "%" 416 | "f" -> use_stdin := false; file 416 | "f" -> use_stdin := false; Filename.quote file changed this line in version 4 of the diff
You're right, I was a bit too fast here and did not notice the splitting logic happening before. I was not able to decipher the logic of the code that uses the command after splitting (looks like it sends them to a socket separated by
;
); do you know where the code is for the receiving end?In any case I removed that last commit---the first commit is really the one that fixes the issue that we were observing.
Edited by Armaël Guéneau
GitLab does not let me merge your pull request, because the CI was not run on it, presumably because you have not enabled the CI on your own repository. (I think you are the first one to ever submit a pull request from an external repository, so it is possible that it is also a misconfiguration on our side.)
right. now it looks like the dockerfile contains an outdated link to cvc4 (the cvc4 repo is now called cvc4-archived), which makes the build fail: https://gitlab.inria.fr/agueneau/why3/-/jobs/3962422
(though intuitively I'd imagined PRs would be run against why3's usual CI pipeline, without having to setup one on my fork)
Your pipelines and jobs are private, so we cannot see them (which is why I could not distinguish a disabled CI from a failing CI). Anyway, if you fix
misc/Dockerfile.build
, do not forgot to also update the date in.gitlab-ci.yml
(as explained inmisc/ci.md
). You can also run the following commands (completely untested):docker pull registry.gitlab.inria.fr/why3/why3:ci-master-2023-11-13 docker tag registry.gitlab.inria.fr/why3/why3:ci-master-2023-11-13 registry.gitlab.inria.fr/agueneau/why3:ci-master-2023-11-13 docker login -u agueneau -p the_access_token_from_your_settings registry.gitlab.inria.fr docker push registry.gitlab.inria.fr/agueneau/why3:ci-master-2023-11-13
As for why the CI is run on the source repository rather than the target repository, it is a security reason. The target repository might be running custom CI workers or have some deployment jobs, so it is critical to prevent random people from triggering an unsanctioned pipeline on it.
mentioned in merge request !1037 (merged)
Reopened as !1037 (merged) (I timeouted on making CI work on my fork).