Skip to content

Unverified binary generation #70

@hrutvik

Description

@hrutvik

When testing compiler modifications we generally don't want to wait for a verified binary to be compiled in-logic. This issue is about creating an unverified binary pipeline. The idea is to translate the PureCake compiler to CakeML in-logic, and print the result to S-expressions. Then we should be able to use a pre-built CakeML binary to produce an executable PureCake compiler.

Overall:

  1. Create a folder compiler/binary/unverified which prints the result of pure_compilerProgTheory to S-expressions
  2. Add a Makefile in this directory for downloading the latest CakeML and compiling the S-expressions to produce a PureCake executable (borrowing from examples/Makefile)
  3. Update the GitHub Actions workflow for creating a binary (.github/binary.yml) to use the unverified pathway

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions