Build break in Kami/Ext/Extraction.v

mit-plv / kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

https://plv.csail.mit.edu/kami/

MIT License

142 stars 24 forks source link

Build break in Kami/Ext/Extraction.v #7

Closed satnam6502 closed 5 years ago

satnam6502 commented 5 years ago

Build break:

COQC Kami/Ext/Extraction.v
File "./Kami/Ext/Extraction.v", line 6, characters 20-25:
Syntax error: [tactic:language] expected after 'Language' (in [vernac:command]).
make[1]: *** [Makefile.coq.all:367: Kami/Ext/Extraction.vo] Error 1
make[1]: Leaving directory '/usr/local/google/home/satnam/forked-kami'
make: *** [Makefile:23: coq] Error 2

The line:

Extraction Language OCaml.

should be:

Extraction Language Ocaml.

because OCaml show now be Ocaml.

satnam6502 commented 5 years ago

Oh, this was due to a confusion between two different versions of Coq I was using! Reverting and closing.

satnam6502 commented 5 years ago

My confusion, due to using different versions of Coq in coqtop and coqide.