Error when making off of fresh pull
Closed this issue · 6 comments
vizziv commented
Specifically, the last few lines when running make
are
"coqc" -q -R "." Frap Sets
"coqc" -q -R "." Frap Map
"coqc" -q -R "." Frap Var
"coqc" -q -R "." Frap Relations
make[1]: *** No rule to make target `Invariant.vo', needed by `Frap.vo'. Stop.
make: *** [coq] Error 2
If I manually execute
"coqc" -q -R "." Frap Invariant
and then run make
again, I get
"coqc" -q -R "." Frap Frap
"coqc" -q -R "." Frap BasicSyntax_template
= 1
: nat
= 5
: nat
= 1
: nat
= 5
: nat
File "./BasicSyntax_template.v", line 42, characters 0-4:
Error: Attempt to save a proof with given up goals. If this is really what
you want to do, use Admitted in place of Qed. (in proof depth_le_size)
make[1]: *** [BasicSyntax_template.vo] Error 1
make: *** [coq] Error 2
cpitclaudel commented
Wrong version of Coq? I'd bet on 8.4
vizziv commented
I don't think so? Installed it with brew
today. (Maybe the fact that I'm on OS X is important?)
$ coqc -v
The Coq Proof Assistant, version 8.5 (January 2016)
compiled on Jan 24 2016 19:16:15 with OCaml 4.02.3
vizziv commented
Okay, doing a simple find-replace to replace admit. Qed.
with Admitted.
fixes the second error, as suggested by the message. I don't know how to fix the first Invariant.vo
error.
cpitclaudel commented
Sorry; I meant that I think the code targets 8.4. At least that's what Adam was using in class.
marklemay commented
Should Invariant.v
be listed in _CoqProject
?
achlipala commented
Thanks for the reports, which I missed by forgetting to watch the repo. Fixed now.