Error when making off of fresh pull

[vizziv]

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]

Wrong version of Coq? I'd bet on 8.4

[vizziv]

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]

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]

Sorry; I meant that I think the code targets 8.4. At least that's what Adam was using in class.

[marklemay]

Should Invariant.v be listed in _CoqProject?

[achlipala]

Thanks for the reports, which I missed by forgetting to watch the repo. Fixed now.