Skip to content
GitLab
    • GitLab: the DevOps platform
    • Explore GitLab
    • Install GitLab
    • How GitLab compares
    • Get started
    • GitLab docs
    • GitLab Learn
  • Pricing
  • Talk to an expert
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
    • Switch to GitLab Next
    Projects Groups Topics Snippets
  • Register
  • Sign in
  • LIGO LIGO
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 44
    • Merge requests 44
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Packages and registries
    • Packages and registries
    • Package Registry
    • Container Registry
    • Infrastructure Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • ligolang
  • LIGOLIGO
  • Merge requests
  • !1451

Work around dune/coq bug (delete generated .ml)

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Tom Jack requested to merge coq-bug-nodeps2 into dev Dec 09, 2021
  • Overview 0
  • Commits 3
  • Pipelines 5
  • Changes 39
  • has a changelog entry

This works around the dune/coq build bug by removing the dependency from the extracted Coq code to tezos-micheline, and inserting conversions back and forth between the two copies of the Micheline node type.

This is only a temporary workaround. Upcoming changes to the backend will avoid this Coq->Tezos dependency naturally. (We could also get the dune/coq bug fixed someday... It would be good to report it, but I feel obligated to create a small test project which reproduces the bug first.)

(I also snuck in some noop changes to suppress those annoying Coq warnings.)

Edited Dec 09, 2021 by Tom Jack
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: coq-bug-nodeps2