fix(coq): unescape \: to : by Alizter · Pull Request #9231 · ocaml/dune

Alizter · 2023-11-20T18:26:17Z

coqdep outputs escaped paths for makefile which means on Windows that C:\foo\bar gets escaped to C\:\\foo\\bar causing Dune to interpret escaped absolute Windows directories as relative ones.

This patch searches for \: in the deps output of coqdep and replaces it with : allowing the paths to be interpreted correctly.

I couldn't write any tests for this since we don't run Coq tests on Windows and I don't plan to.

fix #9218

Alizter · 2023-11-20T20:23:29Z

@MSoegtropIMC I've tested this using a Coq platform setup and it is able to build coq-mathcomp-analysis, coq-mathcomp-word and coq-hott. I think that this patch is ready to be used in the Coq platform.

src/dune_rules/coq/coq_rules.ml

MSoegtropIMC · 2023-11-21T08:48:35Z

@Alizter : I don't see a CI run triggered by you in Coq Platform. Can you please point me to the CI results?

I will test it today evening with local runs.

Alizter · 2023-11-21T12:07:33Z

@MSoegtropIMC I didn't trigger the Coq Platform CI since I ran out of time to look into it yesterday. I had tested this myself on a Windows VM with Coq platform.

ejgallego · 2023-11-21T14:33:49Z

This also needs a changelog (do we have a needs: changes entry tag?)

Alizter · 2023-11-21T14:40:01Z

@ejgallego I'll add a changelog entry.

Alizter · 2023-11-27T12:31:19Z

@MSoegtropIMC Did you get a chance to test this?

MSoegtropIMC · 2023-11-27T12:33:55Z

Yes, it works. I am still having issues on Windows, but with projects which use classic make (coq-elpi). All coq projects using dune work fine on Windows.

If the patch is appropriate is a different question - as @ejgallego pointed out, dune should exactly undo the quoting coqdep injects, and I tend to agree to this. Still it is fine to keep this change as quick fix IMHO.

Alizter · 2023-11-27T12:36:02Z

Good to hear! I'll leave it up to @ejgallego to decide whether he wants an improved version of this or if he is happy with merging this.

ejgallego · 2023-11-27T17:20:30Z

I'm happy with un-escaping : only for now (what about spaces in paths?)

Un-escaping logic should be placed into their own function tho.

Alizter · 2023-11-27T17:22:32Z

@ejgallego Feel free to push any improvements here. I won't spend much more time on this for now.

ejgallego · 2023-11-28T15:42:58Z

@ejgallego Feel free to push any improvements here. I won't spend much more time on this for now.

I will put the escape logic in its own function, IMO this is important to maintain separation of concerns in the code.

coqdep outputs escaped paths for makefile which means on Windows that `C:\foo\bar` gets escaped to `C\:\\foo\\bar` causing Dune to interpret escaped absolute Windows directories as relative ones. This patch searches for `:\` in the deps output of coqdep and replaces it with `:` allowing the paths to be interpreted correctly. Signed-off-by: Ali Caglayan <alizter@gmail.com>

@rgrinberg

CHANGES: - Do not ignore `(formatting ..)` settings in context or workspace files (ocaml/dune#8447, @rgrinberg) - Add command `dune cache clear` to completely delete all traces of the Dune cache. (ocaml/dune#8975, @nojb) - Fixed a bug where Dune was incorrectly parsing the output of coqdep when it was escaped, as is the case on Windows. (ocaml/dune#9231, fixes ocaml/dune#9218, @Alizter) - Copying mode for sandboxes will now follow symbolic links (ocaml/dune#9282, @rgrinberg) - Forbid the empty `(binaries ..)` field in the `env` stanza in the workspace file unless language version is at least 3.2. - [coq] Fix bug in computation of flags when composed with boot theories. (ocaml/dune#9347, fixes ocaml/dune#7909, @ejgallego) - Fixed a bug where the `(select)` field of the `(libraries)` field of the `(test)` stanza wasn't working properly. (ocaml/dune#9387, fixes ocaml/dune#9365, @Alizter) - Allow to disable Coq 0.8 deprecation warning (ocaml/dune#9439, @ejgallego) - Fix handling of the `PATH` argument to `dune init proj NAME PATH`. An intermediate directory called `NAME` is no longer created if `PATH` is supplied, so `dune init proj my_project .` will now initialize a project in the current working directory. (ocaml/dune#9447, fixes ocaml/dune#9209, @shonfeder) - Allow `OCAMLFIND_TOOLCHAIN` to be set per context in the workspace file through the `env` stanza. (ocaml/dune#9449, @rgrinberg) - Experimental doc rules: Correctly handle the case when a package depends upon its own sublibraries (ocaml/dune#9461, fixes ocaml/dune#9456, @jonludlam) - Resolve various public binaries to their build location, rather than to where they're copied in the `_build/install` directory (ocaml/dune#9496, fixes ocaml/dune#7908, @rgrinberg). - Menhir: generate `.conflicts` file by default. Add new field to the `(menhir)` stanza to control the generation of this file: `(explain <blang expression>)`. Introduce `(menhir (flags ...) (explain ...))` field in the `(env)` stanza, delete `(menhir_flags)` field. All changes are guarded under a new version of the Menhir extension, 3.0. (ocaml/dune#9512, @nojb) - Correctly ignore warning flags in vendored projects (ocaml/dune#9515, @rgrinberg) - Directory targets can now be caches. (ocaml/dune#9535, @rleshchinskiy) - Remove warning 30 from default set for projects where dune lang is at least 3.13 (ocaml/dune#9568, @gasche) - It is now possible to use special forms such as `(:include)` and variables `%{read-lines:}` in `(modules)` and similar fields. Note that the dependencies introduced in this way (ie the files being read) must live in a different directory than the stanza making use of them. (ocaml/dune#9578, @nojb) - Use watch exclusions in watch mode on MacOS (ocaml/dune#9643, fixes ocaml/dune#9517, @PoorlyDefinedBehaviour) - Fix merlin configuration for `(include_subdirs qualified)` modules (ocaml/dune#9659, fixes ocaml/dune#8297, @rgrinberg) - Fix handling of `enabled_if` in binary install stanzas. Previously, we'd ignore the result of `enabled_if` when evaluating `%{bin:..}` (ocaml/dune#9707, @rgrinberg) - Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter) - ctypes: fix an error where `(ctypes)` with no `(function_description)` would cause an error trying refer to a nonexistent `_stubs.a` dependency (ocaml/dune#9302, fix ocaml/dune#9300, @emillon)

@nojb

CHANGES: ### Added - Add command `dune cache clear` to completely delete all traces of the Dune cache. (ocaml/dune#8975, @nojb) - Allow to disable Coq 0.8 deprecation warning (ocaml/dune#9439, @ejgallego) - Allow `OCAMLFIND_TOOLCHAIN` to be set per context in the workspace file through the `env` stanza. (ocaml/dune#9449, @rgrinberg) - Menhir: generate `.conflicts` file by default. Add new field to the `(menhir)` stanza to control the generation of this file: `(explain <blang expression>)`. Introduce `(menhir (flags ...) (explain ...))` field in the `(env)` stanza, delete `(menhir_flags)` field. All changes are guarded under a new version of the Menhir extension, 3.0. (ocaml/dune#9512, @nojb) - Directory targets can now be cached. (ocaml/dune#9535, @rleshchinskiy) - It is now possible to use special forms such as `(:include)` and variables `%{read-lines:}` in `(modules)` and similar fields. Note that the dependencies introduced in this way (ie the files being read) must live in a different directory than the stanza making use of them. (ocaml/dune#9578, @nojb) - Remove warning 30 from default set for projects where dune lang is at least 3.13 (ocaml/dune#9568, @gasche) - Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter) - ctypes: fix an error where `(ctypes)` with no `(function_description)` would cause an error trying refer to a nonexistent `_stubs.a` dependency (ocaml/dune#9302, fix ocaml/dune#9300, @emillon) ### Changed - Check that package names in `(depends)` and related fields in `dune-project` are well-formed. (ocaml/dune#9472, fixes ocaml/dune#9270, @ElectreAAS) ### Fixed - Do not ignore `(formatting ..)` settings in context or workspace files (ocaml/dune#8447, @rgrinberg) - Fixed a bug where Dune was incorrectly parsing the output of coqdep when it was escaped, as is the case on Windows. (ocaml/dune#9231, fixes ocaml/dune#9218, @Alizter) - Copying mode for sandboxes will now follow symbolic links (ocaml/dune#9282, @rgrinberg) - Forbid the empty `(binaries ..)` field in the `env` stanza in the workspace file unless language version is at least 3.2. - [coq] Fix bug in computation of flags when composed with boot theories. (ocaml/dune#9347, fixes ocaml/dune#7909, @ejgallego) - Fixed a bug where the `(select)` field of the `(libraries)` field of the `(test)` stanza wasn't working properly. (ocaml/dune#9387, fixes ocaml/dune#9365, @Alizter) - Fix handling of the `PATH` argument to `dune init proj NAME PATH`. An intermediate directory called `NAME` is no longer created if `PATH` is supplied, so `dune init proj my_project .` will now initialize a project in the current working directory. (ocaml/dune#9447, fixes ocaml/dune#9209, @shonfeder) - Experimental doc rules: Correctly handle the case when a package depends upon its own sublibraries (ocaml/dune#9461, fixes ocaml/dune#9456, @jonludlam) - Resolve various public binaries to their build location, rather than to where they're copied in the `_build/install` directory (ocaml/dune#9496, fixes ocaml/dune#7908, @rgrinberg). - Correctly ignore warning flags in vendored projects (ocaml/dune#9515, @rgrinberg) - Use watch exclusions in watch mode on MacOS (ocaml/dune#9643, fixes ocaml/dune#9517, @PoorlyDefinedBehaviour) - Fix merlin configuration for `(include_subdirs qualified)` modules (ocaml/dune#9659, fixes ocaml/dune#8297, @rgrinberg) - Fix handling of `enabled_if` in binary install stanzas. Previously, we'd ignore the result of `enabled_if` when evaluating `%{bin:..}` (ocaml/dune#9707, @rgrinberg)

Regression from ocaml#9231 Fixes ocaml#10088 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

Regression from ocaml#9231 Fixes ocaml#10088

Regression from ocaml#9231 Fixes ocaml#10088 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

Regression from #9231 Fixes #10088 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org> Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

@nojb

CHANGES: ### Added - Add command `dune cache clear` to completely delete all traces of the Dune cache. (ocaml/dune#8975, @nojb) - Allow to disable Coq 0.8 deprecation warning (ocaml/dune#9439, @ejgallego) - Allow `OCAMLFIND_TOOLCHAIN` to be set per context in the workspace file through the `env` stanza. (ocaml/dune#9449, @rgrinberg) - Menhir: generate `.conflicts` file by default. Add new field to the `(menhir)` stanza to control the generation of this file: `(explain <blang expression>)`. Introduce `(menhir (flags ...) (explain ...))` field in the `(env)` stanza, delete `(menhir_flags)` field. All changes are guarded under a new version of the Menhir extension, 3.0. (ocaml/dune#9512, @nojb) - Directory targets can now be cached. (ocaml/dune#9535, @rleshchinskiy) - It is now possible to use special forms such as `(:include)` and variables `%{read-lines:}` in `(modules)` and similar fields. Note that the dependencies introduced in this way (ie the files being read) must live in a different directory than the stanza making use of them. (ocaml/dune#9578, @nojb) - Remove warning 30 from default set for projects where dune lang is at least 3.13 (ocaml/dune#9568, @gasche) - Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter) - ctypes: fix an error where `(ctypes)` with no `(function_description)` would cause an error trying refer to a nonexistent `_stubs.a` dependency (ocaml/dune#9302, fix ocaml/dune#9300, @emillon) ### Changed - Check that package names in `(depends)` and related fields in `dune-project` are well-formed. (ocaml/dune#9472, fixes ocaml/dune#9270, @ElectreAAS) ### Fixed - Do not ignore `(formatting ..)` settings in context or workspace files (ocaml/dune#8447, @rgrinberg) - Fixed a bug where Dune was incorrectly parsing the output of coqdep when it was escaped, as is the case on Windows. (ocaml/dune#9231, fixes ocaml/dune#9218, @Alizter) - Copying mode for sandboxes will now follow symbolic links (ocaml/dune#9282, @rgrinberg) - Forbid the empty `(binaries ..)` field in the `env` stanza in the workspace file unless language version is at least 3.2. - [coq] Fix bug in computation of flags when composed with boot theories. (ocaml/dune#9347, fixes ocaml/dune#7909, @ejgallego) - Fixed a bug where the `(select)` field of the `(libraries)` field of the `(test)` stanza wasn't working properly. (ocaml/dune#9387, fixes ocaml/dune#9365, @Alizter) - Fix handling of the `PATH` argument to `dune init proj NAME PATH`. An intermediate directory called `NAME` is no longer created if `PATH` is supplied, so `dune init proj my_project .` will now initialize a project in the current working directory. (ocaml/dune#9447, fixes ocaml/dune#9209, @shonfeder) - Experimental doc rules: Correctly handle the case when a package depends upon its own sublibraries (ocaml/dune#9461, fixes ocaml/dune#9456, @jonludlam) - Resolve various public binaries to their build location, rather than to where they're copied in the `_build/install` directory (ocaml/dune#9496, fixes ocaml/dune#7908, @rgrinberg). - Correctly ignore warning flags in vendored projects (ocaml/dune#9515, @rgrinberg) - Use watch exclusions in watch mode on MacOS (ocaml/dune#9643, fixes ocaml/dune#9517, @PoorlyDefinedBehaviour) - Fix merlin configuration for `(include_subdirs qualified)` modules (ocaml/dune#9659, fixes ocaml/dune#8297, @rgrinberg) - Fix handling of `enabled_if` in binary install stanzas. Previously, we'd ignore the result of `enabled_if` when evaluating `%{bin:..}` (ocaml/dune#9707, @rgrinberg)

Alizter changed the title ~~fix(coq): unescape :\ to :~~ fix(coq): unescape \: to : Nov 20, 2023

Alizter requested a review from ejgallego November 20, 2023 18:26

ejgallego reviewed Nov 20, 2023

View reviewed changes

src/dune_rules/coq/coq_rules.ml Outdated Show resolved Hide resolved

ejgallego approved these changes Nov 20, 2023

View reviewed changes

ejgallego added the coq label Nov 20, 2023

ejgallego self-assigned this Nov 20, 2023

Alizter force-pushed the ps/branch/fix_coq___unescape____to__ branch from 7269ef8 to 84be2fb Compare November 21, 2023 14:21

Alizter force-pushed the ps/branch/fix_coq___unescape____to__ branch from 84be2fb to 5fbaa70 Compare November 21, 2023 14:43

Alizter marked this pull request as ready for review November 27, 2023 12:31

ejgallego force-pushed the ps/branch/fix_coq___unescape____to__ branch from 5fbaa70 to ee0c78e Compare November 28, 2023 17:25

ejgallego merged commit 23bee95 into ocaml:main Nov 28, 2023

emillon mentioned this pull request Jan 12, 2024

[new release] dune (15 packages) (3.13.0~alpha1) ocaml/opam-repository#25067

Closed

emillon mentioned this pull request Jan 16, 2024

[new release] dune (15 packages) (3.13.0) ocaml/opam-repository#25081

Merged

ejgallego mentioned this pull request Feb 22, 2024

[performance] Zero-build regression 3.11 - 3.14 #10088

Closed

ejgallego added a commit to ejgallego/dune that referenced this pull request Feb 22, 2024

fix(coq): Fix performance regression in coqdep unescaping

663108a

Regression from ocaml#9231 Fixes ocaml#10088 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

ejgallego mentioned this pull request Feb 22, 2024

fix(coq): Fix performance regression in coqdep unescaping #10115

Merged

ejgallego added a commit to ejgallego/dune that referenced this pull request Feb 22, 2024

fix(coq): Fix performance regression in coqdep unescaping

dfd5f0f

Regression from ocaml#9231 Fixes ocaml#10088

Leonidas-from-XIV pushed a commit to Leonidas-from-XIV/dune that referenced this pull request Mar 4, 2024

fix(coq): Fix performance regression in coqdep unescaping

4577cab

Regression from ocaml#9231 Fixes ocaml#10088 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

Leonidas-from-XIV mentioned this pull request Mar 4, 2024

[3.14] backport #10115 #10206

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix(coq): unescape \: to :#9231

fix(coq): unescape \: to :#9231
ejgallego merged 1 commit intoocaml:mainfrom
Alizter:ps/branch/fix_coq_unescapeto

Alizter commented Nov 20, 2023 •

edited

Loading

Uh oh!

Alizter commented Nov 20, 2023 •

edited

Loading

Uh oh!

Uh oh!

MSoegtropIMC commented Nov 21, 2023

Uh oh!

Alizter commented Nov 21, 2023

Uh oh!

ejgallego commented Nov 21, 2023

Uh oh!

Alizter commented Nov 21, 2023

Uh oh!

Alizter commented Nov 27, 2023

Uh oh!

MSoegtropIMC commented Nov 27, 2023

Uh oh!

Alizter commented Nov 27, 2023

Uh oh!

ejgallego commented Nov 27, 2023

Uh oh!

Alizter commented Nov 27, 2023

Uh oh!

ejgallego commented Nov 28, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

Alizter commented Nov 20, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Alizter commented Nov 20, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

MSoegtropIMC commented Nov 21, 2023

Uh oh!

Alizter commented Nov 21, 2023

Uh oh!

ejgallego commented Nov 21, 2023

Uh oh!

Alizter commented Nov 21, 2023

Uh oh!

Alizter commented Nov 27, 2023

Uh oh!

MSoegtropIMC commented Nov 27, 2023

Uh oh!

Alizter commented Nov 27, 2023

Uh oh!

ejgallego commented Nov 27, 2023

Uh oh!

Alizter commented Nov 27, 2023

Uh oh!

ejgallego commented Nov 28, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Alizter commented Nov 20, 2023 •

edited

Loading

Alizter commented Nov 20, 2023 •

edited

Loading