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 15
    • Merge Requests 15
  • 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
  • Why3
  • why3why3
  • Issues
  • #333

Closed
Open
Opened Jun 05, 2019 by François Bobot@bobotOwner4 of 8 tasks completed4/8 tasks

Why3 shell improvements

Some proposed improvements:

[EDITED by SD: for merging my comments in the description. Completion according to !175 (merged)]

  • why3 shell prints by default on stdout
  • Add an option to print in a file
  • --quiet option to print nothing
  • restore printing of the proof tree with identifiers
  • allows to put commands on the command line. Not on stdin. --batch mode
  • allows to use command request Add_file to add a file to the session
  • Remove the debug messages: use standard Why3 debugging
  • Add any other relevant features in this list
Edited Jun 06, 2019 by DAILLER Sylvain
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#333