jasongross / bedrock Goto Github PK

This project forked from mit-plv/bedrock

Not necessarily up-to-date mirror of hg bedrock repository

Home Page: http://plv.csail.mit.edu/bedrock/

License: Other

Emacs Lisp 0.01% Coq 98.22% Makefile 0.50% Assembly 0.37% C 0.42% Standard ML 0.05% OCaml 0.19% Verilog 0.22% Shell 0.01%

bedrock's People

Contributors

Watchers

Forkers

ppedrot maximedenes

bedrock's Issues

Compatibility with Coq 8.6 / trunk

Something strange in the Travis Coq build here:

https://travis-ci.org/ejgallego/coq/jobs/204977514

somehow the Coq mode gets reverted to 8.4, it is weird as I cannot reproduce locally. In my machine,

make src facade

fails with

File "./Bedrock/ILTac.v", line 17, characters 0-25:
Error: while loading
/home/emilio/external/coq-master/bedrock/Bedrock/reification/reif.cmxs:
no implementation available for Tacinterp

which again for some reason is strange, as if it was not using the proper coq_makefile.

Using local Coq

Is there a way to play with this using a locally compiled Coq (./configure -local when compiling Coq)?
There's some complicated compatibility mechanism in the Makefile and I have no idea what's going on.

Recommend Projects