Skip to content
Snippets Groups Projects

Improve some iIntros error messages

Merged Improve some iIntros error messages
tchajed/iris:fix-intros-errors into master
1 unresolved thread
Merged Tej Chajed requested to merge tchajed/iris:fix-intros-errors into master
1 unresolved thread

A failing iIntros for implications should prettify the identifier before printing, and iIntros on something that isn't a wand or implication should say what couldn't be introduced (to clarify that iIntros "HP HQ" failed because of the HQ in particular, for example).

Merge request reports

Approval is optional

Merged by Robbert KrebbersRobbert Krebbers 4 years ago (Sep 28, 2020 5:19pm UTC)

Merge details

  • Changes merged into master with c2019dd3.
  • Deleted the source branch.

Pipeline #34802 passed

Stage: build

    Pipeline passed for c2019dd3 on master

    Activity

    Filter activity
    • Approvals
    • Assignees & reviewers
    • Comments (from bots)
    • Comments (from users)
    • Commits & branches
    • Edits
    • Labels
    • Lock status
    • Mentions
    • Merge request status
    • Tracking
  • Tej Chajed added 1 commit

    added 1 commit

    • 3732f05e - Improve some iIntros error messages

    Compare with previous version

  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers mentioned in commit c2019dd3

    mentioned in commit c2019dd3

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Owner

    Thanks!

  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • tests/proofmode.ref
    654 654 The command has indeed failed with message:
    655 655 Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
    656 "iIntros_fail_nonempty_spatial"
    657 : string
    658 The command has indeed failed with message:
    659 Tactic failure: iIntro: introducing non-persistent "HP" : P
    660 into non-empty spatial context.
    661 "iIntros_fail_not_fresh"
    662 : string
    663 The command has indeed failed with message:
    664 Tactic failure: iIntro: "HP" not fresh.
    665 "iIntros_fail_nothing_to_introduce"
    666 : string
    667 The command has indeed failed with message:
    668 Tactic failure: iIntro: could not introduce "HQ"
    669 , goal is not a wand or implication.
    Please register or sign in to reply