Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 120
    • Issues 120
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 20
    • Merge Requests 20
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar

Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

  • Why3
  • why3why3
  • Issues
  • #445

Closed
Open
Opened Feb 18, 2020 by Ghost User@ghost

why3 commands not recognized on Cygwin+MinGW installation

I installed fdopen's OCaml for Windows, which currently installs a 4.09.0+mingw64c opam repository, and then installed the why3 package. Installation went fine, but when I run why3 with any command, it either does nothing, or does something weird. For instance:

$ why3 shell

$ why3 shell
Welcome to Why3 shell. Type 'help' for help.

$

The first time, it does nothing, and subsequently, it prints the message but opens no shell.

Trying any command with --help outputs the general usage message (i.e. the same as why3 --help, as if the config were not there):

$ why3 config --help
Usage: why3 [options]
... (rest omitted)

On Linux, the same command outputs the specific usage message for the config command:

Usage: why3 config [options]
... (rest omitted)

I cannot, for instance, configure why3, since why3 config --detect does nothing other than print the same usage message.

I tried adding --debug-all, but it prints nothing other than timing information at the end.

Is there a way to try debugging the issue on Cygwin+MinGW? Anything that could help obtain more details about what is going wrong would be useful (e.g. setting an environment variable, looking for specific binaries...).

I tried both why3 1.2.1 and why3 1.2.0, on switches 4.06.1+mingw64c, 4.07.0+mingw64c, and 4.09.0+mingw64c, and in all cases I have the same issue.

I'm aware the problem may be related to the Windows-based opam repository, but if you could provide some basic information to help debugging, e.g. some sanity checks, it would be very helpful.

Edited Feb 18, 2020 by Ghost User
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
1.3.0
Milestone
1.3.0
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#445