Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Heapster: remove generated coq files #1427

Merged
merged 15 commits into from
Aug 24, 2021

Conversation

eddywestbrook
Copy link
Contributor

This change removes all the generated Coq files from the repo so that they get regenerated as part of CI. It also renames all the generated Coq files to XXX_gen.v, in order to make it easier to add them to the .gitignore file.

NOTE: this PR depends on #1426, so should not be merged until that one is.

Eddy Westbrook added 2 commits August 23, 2021 13:45
… to match a given recognizer; this ensures that globals with non-normalized types (e.g., with types that are computed) which evaluate to function, pair, or record types can still be eliminated via applications or the appropriate projections, respectively
… named XXX_gen.v; also removed all generated Coq files from the repo, so they can be re-generated by CI
@eddywestbrook eddywestbrook requested a review from m-yac August 23, 2021 21:32
@eddywestbrook eddywestbrook added the subsystem: heapster Issues specifically related to memory verification using Heapster label Aug 23, 2021
Copy link
Contributor

@m-yac m-yac left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did we ever add a flag to silence the Heapster typechecking debug output? It might be nice to turn that on for the CI so the output isn't so long.

Other than these two comments, looks good to me! Thanks for dealing with this, Eddy.

shell: bash
run: |
chmod +x dist/bin/*
echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this $GITHUB_PATH variable used? Seems like you use $GITHUB_WORKSPACE/dist/bin directly below.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, there is some duplication of concerns here, because I was trying to get it to work. I'll fix some of that now...

@@ -193,6 +193,15 @@ jobs:
name: "${{ runner.os }}-bins"
path: dist/bin

- name: Update PATH to include sAW
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
- name: Update PATH to include sAW
- name: Update PATH to include SAW

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Doh! Thanks for the catch!

…CI to set the PATH correctly, rather than using a github-specific path to SAW
@eddywestbrook eddywestbrook added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Aug 24, 2021
@eddywestbrook eddywestbrook merged commit 66b3e26 into master Aug 24, 2021
@mergify mergify bot deleted the heapster-remove-generated-coq-files branch August 24, 2021 23:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants