search

mit-plv / cross-crypto

Connecting computational and symbolic crypto models
MIT License
8 stars 19 forks source link

Please make your project compile with -w "+compatibility-notation" #9

Closed Zimmi48 closed 6 years ago

Zimmi48 commented 6 years ago

Please make your project compile with -w "+compatibility-notation" to prepare for the Coq 8.9 release. We would appreciate if this could be done ASAP. If you have trouble doing so, please raise your concern at coq/coq#8383.

Zimmi48 commented 6 years ago

As noted by @JasonGross, this seems to actually stem from https://github.com/adampetcher/fcf.

andres-erbsen commented 6 years ago

I don't understand what there is to be done. If I add -arg "-w +compatibility-notation" to _CoqProject, a clean build completes without errors. https://gist.github.com/andres-erbsen/cdb15dbda86ccdc99c8878cf0187ebfd

EDIT: also tried -arg -w -arg +compatibility-notation" , still succeeds.

Zimmi48 commented 6 years ago

In our CI logs, I get:

File "./src/FCF/Lognat.v", line 36, characters 21-26:
Warning: Psucc is Pos.succ [compatibility-notation,deprecated]
File "./src/FCF/Lognat.v", line 43, characters 9-14:
Warning: Psucc is Pos.succ [compatibility-notation,deprecated]
File "./src/FCF/Lognat.v", line 63, characters 24-29:
Warning: Psucc is Pos.succ [compatibility-notation,deprecated]

That's all. That being said, it appears to have been fixed in https://github.com/adampetcher/fcf/pull/21/files#diff-21ba8177aacbd2238d763edd93c1c0eb, so all that remains to do is to update the submodule :tada:

I don't know why you didn't get these errors while compiling. Maybe it is your setup, or maybe it is a coq_makefile bug.

JasonGross commented 6 years ago

This is because the subtarget for fcf is $(MAKE) -C fcf, and so passing -w "+compatibility-notation" in cross-crypto does not build fcf with that flag.

cryslith commented 6 years ago

Fixed in 921e8881aae5443215f4b03a2c2a4f0325f1aef5.