search

mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

bbv/theories checkin breaks all projects using bbv #10

Closed vmurali closed 6 years ago

vmurali commented 6 years ago

Looks like I didn't realize this affects all the projects using bbv :(

In my setup, my _CoqProject using bbv has the following:

-R . Kami -R ../bbv bbv

And inside my files (in Kami), I do "Require Import bbv/Word.".

The following change to _CoqProject does not work. -R . Kami -R ../bbv/theories bbv

Also, why is this a good idea as opposed to storing the .vo files directly in the directories named after the project?

samuelgruetter commented 6 years ago

I'm surprised that this change doesn't work for you, because for bedrock2, it worked: https://github.com/mit-plv/bedrock2/commit/0d1e6ebc60e7b4f269a4a91f9c27fa8c1034a4e9 And for riscv-coq too: https://github.com/mit-plv/riscv-coq/commit/913b98984eafcec3a876af84cdf89651192a044d I really just had to insert /theories in the right place. Are you sure that's not just a "should have started from a fresh clone"?

vmurali commented 6 years ago

I had changed only _CoqProject, not the Makefile.

It works if I change the Makefile also. We need automate this process of setting the flags in the Makefile, since it is already there in the _CoqProject!