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 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • 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
  • #128
Closed
Open
Issue created Dec 30, 2017 by Robbert Krebbers@robbertkrebbersMaintainer

WP tactics do not `simpl` enough

See for example line 133 of ticket_lock.v, after calling wp_cas_fail:

|={⊤ ∖ ↑N,⊤}=> WP if: LitV false then (wait_loop #n) (#lo, #ln) else acquire (#lo, #ln) {{ v, ϕ v }}

Here, there is an of_val (LitV false), which should be simplified into Lit false, which is then pretty printed properly.

I expect the problem to be related to the fact that the WP in this case is below an update modality, and as such, simpl is not used.

Edited Dec 30, 2017 by Robbert Krebbers
Assignee
Assign to
Time tracking