Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1114

Closed
Open
Created Mar 13, 2014 by Dillon Pariente@dillon

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
Assignee
Assign to
Time tracking