Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • RefinedC RefinedC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 21
    • Issues 21
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 3
    • Merge requests 3
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Metrics
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • RefinedCRefinedC
  • Merge requests
  • !137

update Iris for later credits

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Ralf Jung requested to merge ralf/iris into master Jul 07, 2022
  • Overview 5
  • Commits 1
  • Pipelines 0
  • Changes 2

Should help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box

Error: Cannot find a physical path bound to logical path type with prefix refinedc.typing.

Note sure what that is about. I see some _build things in _CoqProject. Maybe dune stuff? Anyway something that breaks the workflow I have been using for 10 years... so let's just see what CI says. ;)

(make builddep insists on installing cerberus which I don't want to do since I just want to change some Coq files.)

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/iris