Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 25
    • Merge requests 25
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #286
Closed
Open
Issue created Jan 30, 2020 by Jonas Kastberg@jihgfeeContributor

Address the STS encodings lack of usefulness

The current encoding of STS's has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".

Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out. Going forward we should do either of the following:

  • Include a disclaimer discouraging people from using them
  • Remove the encoding from the repository
  • Update the implementation to be more user-friendly

I suggest doing either of the first two short-term and then possibly look into the third long-term. It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.

Assignee
Assign to
Time tracking