Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions doc/sphinx/practical-tools/utilities.rst
Original file line number Diff line number Diff line change
Expand Up @@ -636,16 +636,17 @@ line. Comments are ignored.
Quoting arguments to rocq c
+++++++++++++++++++++++++++
Any string in a ``_RocqProject`` file may be enclosed in double quotes to include
whitespace characters or ``#``. For example, use ``-arg "-w all"`` to pass the
argument ``-w all`` to `rocq compile`. If the argument to `rocq compile` needs some quotes as well,
whitespace characters or ``#``. Furthermore, the argument to ``-arg`` is split at
whitespaces, so multiple argument can be passed at once. For example, use ``-arg "-w all"`` to pass the
two arguments ``-w`` and ``all`` to `rocq compile`. If the argument to `rocq compile` contains spaces,
use single-quotes inside the double-quotes. For example ``-arg "-set 'Default
Goal Selector=!'"`` gets passed to `rocq compile` as ``-set 'Default Goal Selector=!'``.
Goal Selector=!'"`` gets passed to `rocq compile` as the two arguments ``-set`` and ``Default Goal Selector=!``.

But note, that single-quotes in a ``_RocqProject`` file are only special
characters if they appear in the string following ``-arg``. And on their own
they don't quote spaces. For example ``-arg 'foo bar'`` in ``_RocqProject`` is
equivalent to ``-arg foo "bar'"`` (in ``_RocqProject`` notation). ``-arg "'foo

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This part here is still confusing me, or maybe it is wrong. Somehow the first ', the one before foo, is apparently getting lost?

bar'"`` behaves differently and passes ``'foo bar'`` to `rocq compile`.
bar'"`` behaves differently and passes the single argument ``foo bar`` to `rocq compile`.

Forbidden filenames
+++++++++++++++++++
Expand Down
Loading