Coqtail icon indicating copy to clipboard operation
Coqtail copied to clipboard

Published 20 hours ago • verified publisher icon whonore

Can't start Coq in theories/Init

Open whonore opened this issue 3 years ago • 0 comments

Trying to start Coq on a file under theories/Init fails.

vim $(coqtop -where)/theories/Init/Nat.v +CoqStart
# Failed to launch Coq.

This seems to be because the -topfile option doesn't like to be used on a file that is also loaded. Removing it or using the-noinit option fixes the problem.

See also coq/coq#10169 and coq/coq#10872.

whonore avatar Mar 19 '21 15:03 whonore