coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] extract logical path name of a .vo file
- Date: Tue, 23 Nov 2021 11:39:51 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f46.google.com
- Ironport-data: A9a23:6N/r764J5fCDwqZGzUpFYgxRtFjGchMFZxGqfqrLsXjdYENS0mAEzmNMUGiBPa6MYjDxct1yYIi180sH7JTQyNNjSFAd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t63yUjRxRSwNZie0SiyFb/6x8hGQ6YnSHuClUbeeYXgqLeNZYH5JZSxLy7ZRbrFA2oDR7zOl4bsekuWHULOX82Yc3lE8t8pvnChSUMHa41v0iLCRicdj5zcyn1FNZH4WyDrYw3HQGuG4FcbiLwrPIS3Qw4/Xw/stIovNfrfTd0QLRvvTOlHLhCYIHaelhRdGq2o51aNT2Pg0Mx8GzWXU2YkvlpMR6/RcSi9xVkHIsOYUSB5eHDt5JrYX0LDCKHm798eUyiUqdlOxnq0wVhxrVWEf0r8vXTsmGeYjADsKd1WIg/+86KmqT/FlwMUlNsjieo0F0kyMZxnNVaN8B8/XGvCSo4dMhmJowJofTK/KPJ9BL2d7M0HpfTlkP3M7CLYflcGUnF3BchhM8QrA+O5n9wA/1yR02bnpddvSI5mEGZsTkUGfqWbLuW/+B3kn2BWk4WLt2hqRaiXnxEsXmb7+FYFUMtZviVyXg20UUVgYCQX9rv6+hUqzHdlYLiT4PwJGQbcarCSWohvVBnVUY0JoejYTXtNRF6sx7wTlJm/8/VOCHmZdJtJeQIVOiSL1LADGEneGmtroAXpkt7j9pbe1nluLhWvaBBX55lPuqcPJocXpLjUjTEwOYsrzc+te
- Ironport-hdrordr: A9a23:DLOrJKzNDRoJubAkRMN3KrPwMb1zdoMgy1knxilNoH1uA6+lfq+V7ZEmPHPP5gr5O0tBpTn/AtjjfZq0z/cciuMs1NGZPTUO01HFEGgN1+bfKkXbdBHDyg==
- Ironport-phdr: A9a23:dBm+uhNMeJkYWlQa5DIl6nYODRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv6wr0AGCBN+Fo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6v95HJbAhFhTWxba5sIBi3sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAe4bMuZDqIn9oUYFoxqkBQmrH+Pv0SJDi3j03aIgyOQhFgfG3AM6H9IJq3TUt9H4ObwdUeCw1qbIzDHDY+lK1jf67YjFaxYsquyDUrxsa8Te01UvFx/bgVWKr4zoJzGY2+YRvmWa4OdtV+OihnI7pg1sojWiwsMhh4rXi4wayF3K+zh0zYUxKNGmSEB2f96qHZtNuyyUKod7Q98uTm5utS0nybMGoYa2cDYWxJkj3RLSaPyKf5KV7h/iVeudOzh1iXNjdbminRi961Kgxff5VsSs0FZFsC5Fkt7Uu3AIzRPT68yHRuJ8/kemxDqDzg7T5+5FLEwumqrbLJkhwrE0lpUNq0jMAij2mEDugK+XcEUr5PSo5vz5brn6opKQLYx5hwHkPqgzm8GyAP40PwcPUmSD/OSzzrzj/Un3QLVQif02l7HUsJLAKsQAoa65BQBV0pwk6xakFDer1M8VnXYCLF1feRKHi5LlNE3JIPD9Ffu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDGmIG+qSNL7Y+QuD4ftqKO2RbqcUviz8Ir4r/ai9o2U+nAo/dLKu29M4cnejBbwyIUyCZnzjmNAaCjYisQ83Teisg1qHB20AL02uVr4xs2loQLmtCp3OE9jFaFmp0yKyH5kQbWdDWAjk+ZbAcoyFX7INb3vXLJM/1DMDUrelRskq0hT87GcSJJJoK+PV/msTspexjbBI
You can use bash pipes to feed input to votour, e.g.,
$ VOFILE="$( eval "$(coqc -config | grep COQLIB)"; echo "$COQLIB/theories/Arith/Arith.vo" )"
$ echo -n "$(printf '0\n0\n0\n' | votour "$VOFILE" | sed -n '/^Here: dirpath.list.string/,$p' | grep -o '^\s\+[0-9]\+: string \[[^]]\+' | grep -o '[^\[]\+$' | tac)" | tr '\n' '.'; echo
Coq.Arith.Arith
Best,
Jason
On Tue, Nov 23, 2021 at 10:27 AM Jim Fehrle <jim.fehrle AT gmail.com> wrote:
A Coq command or a seperate executable? How about Locate?Locate Arith. (* Module Coq.Arith.Arith *)
- [Coq-Club] extract logical path name of a .vo file, Abhishek Anand, 11/23/2021
- Re: [Coq-Club] extract logical path name of a .vo file, Jim Fehrle, 11/23/2021
- Re: [Coq-Club] extract logical path name of a .vo file, Jason Gross, 11/23/2021
- Re: [Coq-Club] extract logical path name of a .vo file, Jim Fehrle, 11/23/2021
Archive powered by MHonArc 2.6.19+.