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
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions