CakeML / CakeML/cakeml

Add regression test to track main function number

Open
#929 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

The compiler assumes that the main function is the first function after the various stubs introduced in `data_to_word`; at the time of writing, this is function `62`. This number isn't specified anywhere, but is rather calculated.

The Pancake compiler needs to somehow know what this number is going to be, which is currently done by hard-coding it in `crep_to_loop` as follows

```
Definition first_name_def:
first_name = 62:num
End
```

I think this hardcoding is not terrible: the alternative would be to have the pancake compiler depend on `data_to_word`. But it does create hard-to-trace errors whenever stubs are added or removed, causing the number to be out of synch. The end-to-end proofs for Pancake, once they exist, should break when this happens. But until they do, it would be nice to have some way of keeping them synched.

This issue is to create a regression test which fails if the number of stubs and `first_name` fails to line up.

Contributor guide

No contributing guide indexed for this repository

Research direction

Locate the data_to_word stubs and the crep_to_loop definition of first_name_def, then trace how the main function number is derived. Add a regression test that compares the calculated stub count with the hard-coded 62 value. Done means the test fails when stubs are added or removed without updating first_name.

Written by the indexing model from the issue text.

Assessment

Domain
compilers, testing-qa
Issue type
Feature
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.