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)