Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Merge Requests
  • !18

Merged
Opened Oct 27, 2016 by Ralf Jung@jungOwner

Move global functor to base_logic

  • Overview 15
  • Commits 1
  • Changes 8

Sorry to bring this up again, I just think it's important to get this as right as we can, right now. ;)

This moves the global functor and dynamic composeable ownership to base_logic. The reasoning behind this is that if someone builds another program logic in our base logic, they will likely want to re-use this, so it makes more sense to have it in base_logic than in program_logic.

The rule for stuff to be in program_logic is: It depends on the Iris' notion of a language, or on world satisfaction (i.e., on our specific way to do invariants). Thus, saved_prop also moves to base_logic and becomes reusable by other program logics. (If we want, we can talk about changing this to just "anything that depends on our notion of a language". Is it conceivable that our world satisfaction is reusable?)

When we talked about this previously, Robbert raised concerns about the name iProp. However, considering that we also have iTactics and use I for the uPred_scope, I feel like the letter "i" has already leaked way beyond program_logic, so this PR doesn't actually change anything. If you want, interpret iProp as "internal propositions", that even makes sense. ;)

Cc @robbertkrebbers @jjourdan

Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!18
Source branch: move-global-func