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
  • #413
Closed
Open
Issue created Apr 29, 2021 by Ralf Jung@jungOwner

Better errors when tactic fails to automatically resolve some side-condition

@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as iMod with mismatching masks:

  1. ElimModal already has support for a pure side-condition; we could introduce something like
Definition pm_error (s : string) := False

and add instances with error "foo" as their side-condition; together with some support in iSolveSideCondition this could be used to then show better, instance-specific error messages when iMod fails.

  1. We could add a new typeclass like ElimModalError that is used to compute an error message when ElimModal failed to find an instance.

Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.

Edited May 25, 2021 by Ralf Jung
Assignee
Assign to
Time tracking