Stream: Coq users

Topic: ✔ coqc -Q . ""


view this post on Zulip Michael Soegtrop (Oct 25 2023 at 16:37):

I tend to pass -Q . "" to coqtop to bind the current folder to the logical root. This usually works fine, but spending an hour to do something automatically in a ms I can do manually in 10s I tried:

coqtop $(grep "[-]Q" _CoqProject | tr '\n' ' ') <file>

to pass to coqtop the same options as I have in _CoqProject. Unfortunately this doesn't work because the "" doesn't get converted to an empty word as it happens when passed directly. Is there an elegant way to do this - or an option to tell coqtop to take options from _CoqProject? Or is there a more shell friendly synonym for logical root than an empty word?

view this post on Zulip Gaëtan Gilbert (Oct 25 2023 at 16:40):

I don't think so
Why use coqtop directly?

view this post on Zulip Michael Soegtrop (Oct 25 2023 at 16:41):

I am using coqtop for Ltac batch debugging. Naturally one calls this on individual files.

view this post on Zulip Michael Soegtrop (Oct 25 2023 at 16:45):

In extra eval works:

eval "coqtop $(grep '[-]Q' _CoqProject | tr '\n' ' ') -lv <file>"

view this post on Zulip Notification Bot (Oct 25 2023 at 16:46):

Michael Soegtrop has marked this topic as resolved.


Last updated: Jun 23 2024 at 05:02 UTC