Compiling Wp-Coq library
ID0001690: This issue was created automatically from Mantis Issue 1690. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001690 | Frama-C | Kernel > Makefile | public | 2014-03-13 | 2014-03-26 |
| Reporter | dpariente | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Windows/Cygwin | OS | Win7 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
[STANCE]
In Frama-C Neon 20140301, when performing a 'make':
[...] Compiling Wp-Coq Library make[1] : on entre dans le répertoire « /frama-c-Neon-rc3/src/wp/share/coqwp » coqc -R . -as "" BuiltIn.v Don't know what to do with ./BuiltIn Usage: coqtop ...
It seems that in {-R . -as ""} the empty string is not managed as expected under Windows/Cygwin.
This topic was already discussed about the RC3. This BTS record is open for traceability.
(Using coq 8.4pl3 with binaries pack for Windows)
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information